TY - GEN
T1 - Decidable compositions of O-minimal automata
AU - Casagrande, Alberto
AU - Corvaja, Pietro
AU - Piazza, Carla
AU - Mishra, Bud
N1 - Funding Information:
This work is partially supported by PRIN ”BISCA” 2006011235, FIRB ”LIBI” RBLA039M7M, two NSF ITR grants, and one NSF EMT grant.
PY - 2008
Y1 - 2008
N2 - We identify a new class of decidable hybrid automata: namely, parallel compositions of semi-algebraic o-minimal automata. The class we consider is fundamental to hierarchical modeling in many exemplar systems, both natural and engineered. Unfortunately, parallel composition, which is an atomic operator in such constructions, does not preserve the decidability of reachability. Luckily, this paper is able to show that when one focuses on the composition of semi-algebraic o-minimal automata, it is possible to translate the decidability problem into a satisfiability problem over formulæinvolving both real and integer variables. While in the general case such formulæ would be undecidable, the particular format of the formulæ obtained in our translation allows combining decidability results stemming from both algebraic number theory and first-order logic over (ℝ, 0, 1, +,*, <) to yield a novel decidability algorithm. From a more general perspective, this paper exposes many new open questions about decidable combinations of real/integer logics.
AB - We identify a new class of decidable hybrid automata: namely, parallel compositions of semi-algebraic o-minimal automata. The class we consider is fundamental to hierarchical modeling in many exemplar systems, both natural and engineered. Unfortunately, parallel composition, which is an atomic operator in such constructions, does not preserve the decidability of reachability. Luckily, this paper is able to show that when one focuses on the composition of semi-algebraic o-minimal automata, it is possible to translate the decidability problem into a satisfiability problem over formulæinvolving both real and integer variables. While in the general case such formulæ would be undecidable, the particular format of the formulæ obtained in our translation allows combining decidability results stemming from both algebraic number theory and first-order logic over (ℝ, 0, 1, +,*, <) to yield a novel decidability algorithm. From a more general perspective, this paper exposes many new open questions about decidable combinations of real/integer logics.
UR - http://www.scopus.com/inward/record.url?scp=56749155690&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=56749155690&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-88387-6_25
DO - 10.1007/978-3-540-88387-6_25
M3 - Conference contribution
AN - SCOPUS:56749155690
SN - 354088386X
SN - 9783540883869
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 274
EP - 288
BT - Automated Technology for Verification and Analysis - 6th International Symposium, ATVA 2008, Proceedings
PB - Springer Verlag
T2 - 6th International Symposium on Automated Technology for Verification and Analysis, ATVA 2008
Y2 - 20 October 2008 through 23 October 2008
ER -