Expressive Power of Hybrid Systems with Real Variables, Integer Variables and Arrays

Hybrid systems is a suitable model to describe systems composed of both continuous and discrete components. The continuous components typically represent physic events. The discrete components are logic devices, such as switches and digital circuitry. A typical example is a system where physical processes are controlled by embedded controllers. Different classes of hybrid systems have been proposed. In this paper we consider hybrid systems equipped with real variable (as usual), integer variables and unbounded arrays. We study the expressive power of five classes: Linear real hybrid systems, Polynomial real hybrid systems, Mixed hybrid systems, D-hybrid systems and S-hybrid systems. For these classes there exists a quantifier elimination technique for computing the successor operator, hence the reachability problem is semidecidable.
Journal of Automata, Languages and Combinatorics, Volume 12, Number 3, 2007, 373-405