Composing FOCoRe Hybrid Automata

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.