This paper addresses questions regarding the decidability of hybrid automata that may be built hierarchically as is the case in many exemplar systems, be it natural or engineered. Parallel composition can be considered a fundamental tool in such constructions. Somewhat surprisingly, this operation does not always preserve the decidability of reachability problem i.e., even if we prove the decidability of reachability over component automata, we cannot guarantee the decidability over their parallel composition. Despite these limitations, this paper provides a reduction for the reachability problem over parallel composition of first-order constant reset automata (FOCoRe) to the satisfiability of a particular linear Diophantine system. Moreover, since such satisfiability problem have been proved decidable for systems with semi-algebraic coe cients, this paper presents an interesting class of hybrid automata for which the reachability problem of parallel composition is decidable. The resulting hybrid automata appear in systems biological modeling, and hence could be applied when one is interested in understanding a complex biological system composed of many smaller self-organizing systems.

Composing FOCoRe Hybrid Automata

CASAGRANDE, ALBERTO;
2011

Abstract

This paper addresses questions regarding the decidability of hybrid automata that may be built hierarchically as is the case in many exemplar systems, be it natural or engineered. Parallel composition can be considered a fundamental tool in such constructions. Somewhat surprisingly, this operation does not always preserve the decidability of reachability problem i.e., even if we prove the decidability of reachability over component automata, we cannot guarantee the decidability over their parallel composition. Despite these limitations, this paper provides a reduction for the reachability problem over parallel composition of first-order constant reset automata (FOCoRe) to the satisfiability of a particular linear Diophantine system. Moreover, since such satisfiability problem have been proved decidable for systems with semi-algebraic coe cients, this paper presents an interesting class of hybrid automata for which the reachability problem of parallel composition is decidable. The resulting hybrid automata appear in systems biological modeling, and hence could be applied when one is interested in understanding a complex biological system composed of many smaller self-organizing systems.
hybrid automata, parallel composition, decidability
File in questo prodotto:
File Dimensione Formato  
parallel_composition.pdf

non disponibili

Tipologia: Altro materiale allegato
Licenza: Digital Rights Management non definito
Dimensione 352.16 kB
Formato Adobe PDF
352.16 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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: http://hdl.handle.net/11368/2830613
 Attenzione

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

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