@inproceedings{10.1145/3597066.3597101,
    Abstract = {We consider the following problem: given d \texttimes{} d rational matrices A1, {{\l}dots}, Ak and a polyhedral cone , decide whether there exists a non-zero vector whose orbit under multiplication by A1, {{\l}dots}, Ak is contained in . This problem can be interpreted as verifying the termination of multi-path while loops with linear updates and linear guard conditions. We show that this problem is decidable for commuting invertible matrices A1, {{\l}dots}, Ak. The key to our decision procedure is to reinterpret this problem in a purely algebraic manner. Namely, we discover its connection with modules over the polynomial ring as well as the polynomial semiring . The loop termination problem is then reduced to deciding whether a submodule of contains a ``positive'' element.},
    Address = {New York, NY, USA},
    Author = {Dong, Ruiwen},
    BookTitle = {Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation},
    File = {Termination of linear loops under commutative updates - 3597066.3597101.pdf},
    ISBN = {9798400700392},
    Keywords = {positive polynomials, loop termination, module over polynomial ring, commuting matrices},
    Location = {Troms\o{}, Norway},
    Pages = {236--241},
    Publisher = {Association for Computing Machinery},
    Series = {ISSAC '23},
    Title = {Termination of Linear Loops under Commutative Updates},
    URL = {https://doi.org/10.1145/3597066.3597101},
    Year = {2023},
    bdsk-url-1 = {https://doi.org/10.1145/3597066.3597101},
    date-added = {2023-09-26 14:03:35 +0200},
    date-modified = {2023-09-26 14:03:35 +0200},
    numpages = {6},
    doi = {10.1145/3597066.3597101}
}

@inproceedings{10.1145/3597066.3597101, Abstract = {We consider the following problem: given d \texttimes{} d rational matrices A1, {{\l}dots}, Ak and a polyhedral cone , decide whether there exists a non-zero vector whose orbit under multiplication by A1, {{\l}dots}, Ak is contained in . This problem can be interpreted as verifying the termination of multi-path while loops with linear updates and linear guard conditions. We show that this problem is decidable for commuting invertible matrices A1, {{\l}dots}, Ak. The key to our decision procedure is to reinterpret this problem in a purely algebraic manner. Namely, we discover its connection with modules over the polynomial ring as well as the polynomial semiring . The loop termination problem is then reduced to deciding whether a submodule of contains a ``positive'' element.}, Address = {New York, NY, USA}, Author = {Dong, Ruiwen}, BookTitle = {Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation}, File = {Termination of linear loops under commutative updates - 3597066.3597101.pdf}, ISBN = {9798400700392}, Keywords = {positive polynomials, loop termination, module over polynomial ring, commuting matrices}, Location = {Troms\o{}, Norway}, Pages = {236--241}, Publisher = {Association for Computing Machinery}, Series = {ISSAC '23}, Title = {Termination of Linear Loops under Commutative Updates}, URL = {https://doi.org/10.1145/3597066.3597101}, Year = {2023}, bdsk-url-1 = {https://doi.org/10.1145/3597066.3597101}, date-added = {2023-09-26 14:03:35 +0200}, date-modified = {2023-09-26 14:03:35 +0200}, numpages = {6}, doi = {10.1145/3597066.3597101} }