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, we show 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 we relate these to the concepts of input/output and state/algebraic variables most control designers are familiar with. Additionaly, we enlargen the applicability of our HIOA 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, we show how we can algorithmically bring control systems given by semi-explicit differential algebraic equations to the form understood by the SpaceEx reachability algorithm.

@inproceedings{DonzeF13,
  author = {Alexandre Donz\'{e}, Goran Frehse},
  title = {Modular, Hierarchical Models of Control Systems in SpaceEx},
  booktitle = {Proc.\ European Control Conf.\ (ECC'13)},
  address = {Zurich, Switzerland},
  year = {2013}
}