Decidable compositions of O-minimal automata

Alberto Casagrande, Pietro Corvaja, Carla Piazza, Bhubaneswar Mishra

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

Abstract

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
Pages274-288
Number of pages15
Volume5311 LNCS
DOIs
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)03029743
ISSN (Electronic)16113349

Other

Other6th International Symposium on Automated Technology for Verification and Analysis, ATVA 2008
CountryKorea, Republic of
CitySeoul
Period10/20/0810/23/08

Fingerprint

O-minimal
Computability and decidability
Decidability
Automata
Parallel Composition
Chemical analysis
Number theory
Hybrid Automata
Hierarchical Modeling
Integer
Algebraic number
Satisfiability Problem
First-order Logic
Reachability
Logic
Operator
Class

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Casagrande, A., Corvaja, P., Piazza, C., & Mishra, B. (2008). Decidable compositions of O-minimal automata. In Automated Technology for Verification and Analysis - 6th International Symposium, ATVA 2008, Proceedings (Vol. 5311 LNCS, pp. 274-288). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5311 LNCS). https://doi.org/10.1007/978-3-540-88387-6-25

Decidable compositions of O-minimal automata. / Casagrande, Alberto; Corvaja, Pietro; Piazza, Carla; Mishra, Bhubaneswar.

Automated Technology for Verification and Analysis - 6th International Symposium, ATVA 2008, Proceedings. Vol. 5311 LNCS 2008. p. 274-288 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5311 LNCS).

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

Casagrande, A, Corvaja, P, Piazza, C & Mishra, B 2008, Decidable compositions of O-minimal automata. in Automated Technology for Verification and Analysis - 6th International Symposium, ATVA 2008, Proceedings. vol. 5311 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5311 LNCS, pp. 274-288, 6th International Symposium on Automated Technology for Verification and Analysis, ATVA 2008, Seoul, Korea, Republic of, 10/20/08. https://doi.org/10.1007/978-3-540-88387-6-25
Casagrande A, Corvaja P, Piazza C, Mishra B. Decidable compositions of O-minimal automata. In Automated Technology for Verification and Analysis - 6th International Symposium, ATVA 2008, Proceedings. Vol. 5311 LNCS. 2008. p. 274-288. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-540-88387-6-25
Casagrande, Alberto ; Corvaja, Pietro ; Piazza, Carla ; Mishra, Bhubaneswar. / Decidable compositions of O-minimal automata. Automated Technology for Verification and Analysis - 6th International Symposium, ATVA 2008, Proceedings. Vol. 5311 LNCS 2008. pp. 274-288 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{1fa1887f3e7b4b20959a5aff3370f189,
title = "Decidable compositions of O-minimal automata",
abstract = "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{\ae}involving both real and integer variables. While in the general case such formul{\ae} would be undecidable, the particular format of the formul{\ae} 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.",
author = "Alberto Casagrande and Pietro Corvaja and Carla Piazza and Bhubaneswar Mishra",
year = "2008",
doi = "10.1007/978-3-540-88387-6-25",
language = "English (US)",
isbn = "354088386X",
volume = "5311 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "274--288",
booktitle = "Automated Technology for Verification and Analysis - 6th International Symposium, ATVA 2008, Proceedings",

}

TY - GEN

T1 - Decidable compositions of O-minimal automata

AU - Casagrande, Alberto

AU - Corvaja, Pietro

AU - Piazza, Carla

AU - Mishra, Bhubaneswar

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

SN - 354088386X

SN - 9783540883869

VL - 5311 LNCS

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

ER -