On strongest algebraic program invariants
A polynomial program is one in which all assignments are given by polynomial expressions and in which all branching is nondeterministic (as opposed to conditional). Given such a program, an algebraic invariant is one that is defined by polynomial equations over the program variables at each program...
| Hlavní autoři: | , , , |
|---|---|
| Médium: | Journal article |
| Jazyk: | English |
| Vydáno: |
Association for Computing Machinery
2023
|
| _version_ | 1826313017472581632 |
|---|---|
| author | Hrushovski, E Ouaknine, J Pouly, A Worrell, J |
| author_facet | Hrushovski, E Ouaknine, J Pouly, A Worrell, J |
| author_sort | Hrushovski, E |
| collection | OXFORD |
| description | A polynomial program is one in which all assignments are given by polynomial expressions and in which all branching is nondeterministic (as opposed to conditional). Given such a program, an algebraic invariant is one that is defined by polynomial equations over the program variables at each program location. Müller-Olm and Seidl have posed the question of whether one can compute the strongest algebraic invariant of a given polynomial program. In this article, we show that, while strongest algebraic invariants are not computable in general, they can be computed in the special case of affine programs, that is, programs with exclusively linear assignments. For the latter result, our main tool is an algebraic result of independent interest: Given a finite set of rational square matrices of the same dimension, we show how to compute the Zariski closure of the semigroup that they generate. |
| first_indexed | 2024-09-25T04:05:58Z |
| format | Journal article |
| id | oxford-uuid:e25bde78-053b-4710-8ee3-3c81495bc695 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-09-25T04:05:58Z |
| publishDate | 2023 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | oxford-uuid:e25bde78-053b-4710-8ee3-3c81495bc6952024-05-21T11:41:52ZOn strongest algebraic program invariantsJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:e25bde78-053b-4710-8ee3-3c81495bc695EnglishSymplectic ElementsAssociation for Computing Machinery2023Hrushovski, EOuaknine, JPouly, AWorrell, JA polynomial program is one in which all assignments are given by polynomial expressions and in which all branching is nondeterministic (as opposed to conditional). Given such a program, an algebraic invariant is one that is defined by polynomial equations over the program variables at each program location. Müller-Olm and Seidl have posed the question of whether one can compute the strongest algebraic invariant of a given polynomial program. In this article, we show that, while strongest algebraic invariants are not computable in general, they can be computed in the special case of affine programs, that is, programs with exclusively linear assignments. For the latter result, our main tool is an algebraic result of independent interest: Given a finite set of rational square matrices of the same dimension, we show how to compute the Zariski closure of the semigroup that they generate. |
| spellingShingle | Hrushovski, E Ouaknine, J Pouly, A Worrell, J On strongest algebraic program invariants |
| title | On strongest algebraic program invariants |
| title_full | On strongest algebraic program invariants |
| title_fullStr | On strongest algebraic program invariants |
| title_full_unstemmed | On strongest algebraic program invariants |
| title_short | On strongest algebraic program invariants |
| title_sort | on strongest algebraic program invariants |
| work_keys_str_mv | AT hrushovskie onstrongestalgebraicprograminvariants AT ouakninej onstrongestalgebraicprograminvariants AT poulya onstrongestalgebraicprograminvariants AT worrellj onstrongestalgebraicprograminvariants |