Algebraic Reasoning for Hybrid Systems -Two Case Studies -
in R. Berghammer, B. Möller, G. Struth (eds.): Relations and Kleene algebra in computer science.
Lecture Notes in Computer Science 4988. Springer 2008, pp. 191-205
At an abstract level hybrid systems are related to variants
of Kleene algebra. Since it has recently been showed that Kleene algebras
and their variants, like omega algebras, provide a reasonable base
for automated reasoning, the aim of the present paper is to show that
automated algebraic reasoning for hybrid system is feasible. We mainly
focus on applications. In particular, we present case studies and proof experiments
to show how concrete properties of hybrid systems, like safety
and liveness, can be algebraically characterised and how off-the-shelf automated
theorem provers can be used to verify them.