<div class="csl-bib-body">
<div class="csl-entry">El Manssour, R. A., Kenison, G., Shirmohammadi, M., Varonka, A., & Worrell, J. B. (2026). Determination Problems for Orbit Closures and Matrix Groups. In M. Hicks (Ed.), <i>Proceedings of the ACM on Programming Languages</i> (pp. 1615–1640). Association for Computing Machinery. https://doi.org/10.1145/3776698</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/225296
-
dc.description.abstract
Computational problems concerning the orbit of a point under the action of a matrix group occur throughout computer science, including in program analysis, complexity theory, quantum computation, and automata theory. In many cases the focus extends beyond orbits proper to orbit closures under a suitable topology. Typically one starts from a group and a set of points and asks questions about the orbit closure of the set under the action of the group, e.g., whether two given orbit closures intersect.
In this paper we consider a collection of what we call determination problems concerning matrix groups and orbit closures. These problems begin with a given variety and seek to understand whether and how it arises either as an algebraic matrix group or as an orbit closure. The how question asks whether the underlying group is s-generated, meaning it is topologically generated by s matrices for a given number s. Among other applications, problems of this type have recently been studied in the context of synthesising loops subject to certain specified invariants on program variables.
Our main result is a polynomial-space procedure that inputs a variety and a number s and determines whether the given variety arises as an orbit closure of a point under an s-generated commutative algebraic matrix group. The main tools in our approach are structural properties of commutative algebraic matrix groups and module theory. We leave open the question of determining whether a variety is an orbit closure of a point under an s-generated algebraic matrix group (without the requirement of commutativity).
en
dc.description.sponsorship
European Commission
-
dc.language.iso
en
-
dc.relation.ispartofseries
Proceedings of the ACM on Programming Languages
-
dc.subject
Algebraic Loop Invariant
en
dc.subject
Zariski Closure
en
dc.subject
Polynomial Space
en
dc.subject
Algebraic Reasoning
en
dc.subject
Program Synthesis
en
dc.title
Determination Problems for Orbit Closures and Matrix Groups
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.contributor.affiliation
University of Oxford, United Kingdom of Great Britain and Northern Ireland (the)
-
dc.contributor.affiliation
Liverpool John Moores University, United Kingdom of Great Britain and Northern Ireland (the)
-
dc.contributor.affiliation
Centre National de la Recherche Scientifique, France
-
dc.contributor.affiliation
University of Oxford, United Kingdom of Great Britain and Northern Ireland (the)
-
dc.description.startpage
1615
-
dc.description.endpage
1640
-
dc.relation.grantno
ERC Consolidator Grant 2020
-
dc.type.category
Full-Paper Contribution
-
dc.relation.eissn
2475-1421
-
tuw.booktitle
Proceedings of the ACM on Programming Languages
-
tuw.container.volume
10
-
tuw.peerreviewed
true
-
tuw.relation.publisher
Association for Computing Machinery
-
tuw.relation.publisherplace
New York, United States
-
tuw.project.title
Automated Reasoning with Theories and Induction for Software Technologies
-
tuw.project.title
LogiCs-Stipendien
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.id
A3
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.name
Fundamental Mathematics Research
-
tuw.researchTopic.value
80
-
tuw.researchTopic.value
20
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
tuw.publication.orgunit
E056-13 - Fachbereich LogiCS
-
tuw.publisher.doi
10.1145/3776698
-
dc.description.numberOfPages
26
-
tuw.author.orcid
0000-0001-6228-9071
-
tuw.author.orcid
0000-0002-7661-7061
-
tuw.author.orcid
0000-0002-7779-2339
-
tuw.author.orcid
0000-0001-5758-0657
-
tuw.author.orcid
0000-0001-8151-2443
-
tuw.event.name
53rd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2026)
en
tuw.event.startdate
11-01-2026
-
tuw.event.enddate
14-01-2026
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Rennes
-
tuw.event.country
FR
-
tuw.event.presenter
Kenison, George
-
tuw.event.track
Multi Track
-
wb.sciencebranch
Informatik
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.oefos
1010
-
wb.sciencebranch.value
80
-
wb.sciencebranch.value
20
-
item.openairetype
conference paper
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.cerifentitytype
Publications
-
item.languageiso639-1
en
-
item.grantfulltext
restricted
-
item.fulltext
no Fulltext
-
crisitem.author.dept
University of Oxford, United Kingdom of Great Britain and Northern Ireland (the)
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
Centre National de la Recherche Scientifique, France
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
University of Oxford, United Kingdom of Great Britain and Northern Ireland (the)