## Automated Reasoning for Hybrid Systems --- Two Case Studies ---

P. Höfner
In R. Berghammer, B. Möller, G. Struth (Eds.): RelMiCS/AKA 2008,
Lecture Notes in Computer Science 4988, Springer, pp.191-205, 2008.
 Abstract
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.
 Data
For the experiments we used Prover9, a resolution- and paramodulation-based automated theorem prover developed by William McCune.

Nr/Describtion Theorem Input-File Output-File Proof (XML)
Lemma 4.3.1. $a\cdot(b\cdot a)^\omega \leq (a\cdot b)^\omega$ lm431.in
lm431ht.in 1
lm431.out
lm431ht.out
lm431.xml
lm431ht.xml
Lemma 4.3.2. $a^\omega\cdot b\leq a^\omega$ lm432.in
lm432.out
lm432.xml
Lemma 4.3.3. $(a\cdot b)^\omega\leq (a+b)^\omega$ lm433.in
lm433.out
lm433.xml
Lemma 4.3.4. $(a^+)^\omega = a^\omega$ lm434.in
lm434.out
lm434.xml
Equation (3) $p\cdot(p\cdot a)^\omega \leq (p\cdot a)^\omega$
$p\cdot(p\cdot a)^\omega \geq (p\cdot a)^\omega$
$(p\cdot a)^\omega \leq (p\cdot a\cdot p)^\omega$
$(p\cdot a)^\omega \geq (p\cdot a\cdot p)^\omega$
eq3i.in
eq3ii.in
eq3iii.in
eq3iv.in
eq3i.out
eq3ii.out
eq3iii.out
eq3iv.out
eq3i.xml
eq3ii.xml
eq3iii.xml
eq3iv.xml
Example 4.4./Lemma A.1. $(paqbrc)^\omega \leq p(paq+qbr+rcp)^\omega$ without the last step of isotony1,2
$(paqbrc)^\omega \leq p(paq+qap+qbr+rbq+rcp+pcr)^\omega$ 1,2
lmA1short.in
lmA1.in
lmA1short.out
lmA1.out
lmA1short.xml
lmA1.xml
Example 5.1. $(at_u\cdot a_5\cdot at_d\cdot a_{10}\cdot at_b\cdot a_{15})^\omega \leq (a_{30}\cdot at_u)^\omega$
$(at_u\cdot a_5\cdot at_d\cdot a_{10}\cdot at_b\cdot a_{15})^\omega \leq (a_{30}\cdot at_d)^\omega$
$(at_u\cdot a_5\cdot at_d\cdot a_{10}\cdot at_b\cdot a_{15})^\omega \leq (a_{30}\cdot at_b)^\omega$
ex51.in
ex51.out
ex51.xml
Case Study II $F\cdot l_1\leq (l_1+l_2+i)^+$
cs2.in
cs2.out
cs2.xml

1 To produce these files we used hypothesis learning.
2 Multiplication ($\cdot$) is left implicit.
We have done more proof experiments, including idempotent semirings, Kleene algebras, omega algebras, demonic refinement algebras, Boolean algebras with operators and relation algebras. The files concerning these experiments can be found in a proof database. The results of this web-site will be included into the database soon.