Composing FOCoRe Hybrid Automata

This paper addresses questions regarding the decidability ofhybrid automata that may be built hierarchically as is the case in many exemplar systems, be it natural or engineered. Parallel composition canbe considered a fundamental tool in such costructions. Somewhat surprisingly, this operation does not always preseve the decidability of reachability problem i.e., even if we prove the decidability of reachability overcomponent automata, we cannot guarantee the decidability over theirparallel composition. Despite these limitations, this paper provides a re-duction 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 coefficients,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.