This paper addresses questions regarding the decidability of hybrid automata that may be constructed hierarchically and in a modular way, as is the case in many exemplar systems, be it natural or engineered. Since an important step in such constructions is a product operation, which constructs a new product hybrid automaton by combining two simpler component hybrid automata, an essential property that would be desired is that the reachability property of the product hybrid automaton be decidable, provided that the component hybrid automata belong to a suitably restricted family of automata. Somewhat surprisingly, the product operation does not assure a closure of decidability for the reachability problem. Nonetheless, this paper establishes the decidability of the reachability condition over automata which are obtained by composing two semi-algebraic o-minimal systems. The class of semi-algebraic o-minimal automata is not even closed under composition, i.e., the product of two automata of this class is not necessarily a semi-algebraic o-minimal automaton. However, we can prove our decidability result combining the decidability of both semi-algebraic formulæ over the reals and linear Diophantine equations.

Synchronized Product of Semi-Algebraic O-Minimal Hybrid Automata

CORVAJA, Pietro;PIAZZA, Carla;
2007

Abstract

This paper addresses questions regarding the decidability of hybrid automata that may be constructed hierarchically and in a modular way, as is the case in many exemplar systems, be it natural or engineered. Since an important step in such constructions is a product operation, which constructs a new product hybrid automaton by combining two simpler component hybrid automata, an essential property that would be desired is that the reachability property of the product hybrid automaton be decidable, provided that the component hybrid automata belong to a suitably restricted family of automata. Somewhat surprisingly, the product operation does not assure a closure of decidability for the reachability problem. Nonetheless, this paper establishes the decidability of the reachability condition over automata which are obtained by composing two semi-algebraic o-minimal systems. The class of semi-algebraic o-minimal automata is not even closed under composition, i.e., the product of two automata of this class is not necessarily a semi-algebraic o-minimal automaton. However, we can prove our decidability result combining the decidability of both semi-algebraic formulæ over the reals and linear Diophantine equations.
9783540714927
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11390/857030
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 5
social impact