In: Lecture Notes in Control and Information Science (LNCIS) Vol. 279, pages 1-295pp. Springer Verlag, July 2002.
Abstract: The design of discrete control systems for technical processes leads to hybrid systems. These can be modelled by a combination of several Petri Nets and extended state space models with appropriate interfaces between them. For the analysis of the whole system, the introduced evolution graph is used to describe hybrid reachability, including generally infinite converging cycles by a covered graph. The analysis results are utilised to synthesise minimal extensions to the control system to assure desired system behaviour like liveness or reversibility. The procedure is illustrated by a small example.