Modular, hierarchical models of control systems in SpaceEx

The Hybrid I/O-automaton (HIOA) is a rigorous formal model designed for the analysis of complex hybrid (discrete-continuous) dynamical systems. The use of the HIOA formalism renders compositional reasoning possible, in the sense that once a property has been established for an automaton, it still holds if the automaton is composed with other automata. In this paper, it is shown how control systems can be modeled and verified in SpaceEx as HIOA in a modular fashion. Formally, HIOA models distinguish between controlled and uncontrolled variables.With examples and usage guidelines, they are related to the concepts of input/output and state/algebraic variables most control designers are familiar with. Additionally, the applicability of HIOA is enlarged by allowing variables to be controlled in more than one automaton. While this invalidates compositionality, it gives users who do not intend to use compositional reasoning more freedom in their modeling choices. Finally, it is shown how control systems given by semi-explicit differential algebraic equations can be algorithmically brought to the form understood by the SpaceEx reachability algorithm.