Hybrid System Extraction of Control Automata with Small Topologies

摘要

We propose a game framework for analyzing, extracting and verifying digitalcontrol programs for continuous plants by regarding such programs as finite state winning strategies in associated games. We call such interacting systems of digital control programs and continuous plants hybrid systems and model them as networks of interacting concurrent digital programs or automata. This extends to hybrid systems the paradigm introduced by Nerode, Yakhnis and Yakhnis for analysing concurrent digital programs meeting program specifications as winning finite state strategies in associated two person games.