Decidable compositions of O-minimal automata

Alberto Casagrande, Pietro Corvaja, Carla Piazza, Bud Mishra

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationAutomated Technology for Verification and Analysis - 6th International Symposium, ATVA 2008, Proceedings
PublisherSpringer Verlag
Number of pages15
ISBN (Print)354088386X, 9783540883869
StatePublished - 2008
Event6th International Symposium on Automated Technology for Verification and Analysis, ATVA 2008 - Seoul, Korea, Republic of
Duration: Oct 20 2008Oct 23 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5311 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other6th International Symposium on Automated Technology for Verification and Analysis, ATVA 2008
Country/TerritoryKorea, Republic of

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Decidable compositions of O-minimal automata'. Together they form a unique fingerprint.

Cite this