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.

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

¹ To produce these files we used hypothesis learning.
² 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.