Automated Reasoning for Hybrid Systems — Two Case Studies —

P. Höfner

Abstract: At an abstract level hybrid systems are related to variants of Kleene algebra. Since it has recently been shown 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.

Paper: pdf


In the paper we present case studies and proof experiments to show 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.

No/DescriptionTheoremInput-FileOutput-FileProof (XML)
Lemma 4.3.1.a · (b · a)ω ≤ (a · b)ωlm431.in
lm431ht.in 1
lm431.out
lm431ht.out
lm431.xml
lm431ht.xml
Lemma 4.3.2.aω · b ≤ aωlm432.inlm432.outlm432.xml
Lemma 4.3.3.(a · b)ω≤ (a + b)ωlm433.inlm433.outlm433.xml
Lemma 4.3.4.(a+)ω = aωlm434.inlm434.outlm434.xml
Equation (3)p · (p · a)ω ≤ (p · a)ω
p · (p · a)ω ≥ (p · a)ω
(p · a)ω ≤ (p · a · p)ω
(p · a)ω ≥ (p · a · p)ω
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.(p a q b r c)ω ≤ p (p a q + q b r + r c p)ω without the last step of isotony1,2
(p a q b r c)ω ≤ p (p a q + q a p + q b r + r b q + r c p + p c r)ω 1,2
lmA1short.in
lmA1.in
lmA1short.out
lmA1.out
lmA1short.xml
lmA1.xml
Example 5.1.(atu · a5 · atd · a10 · atb · a15)ω ≤ (a30 · atu)ω
(atu · a5 · atd · a10 · atb · a15)ω ≤ (a30 · atd)ω
(atu · a5 · atd · a10 · atb · a15)ω ≤ (a30 · atb)ω
ex51.inex51.outex51.xml
Case Study IIF· l1 ≤ (l1 + l2 + i)+cs2.incs2.outcs2.xml

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.

1 To produce these files we used hypothesis learning.
2 Multiplication (·) is left implicit.


Contact: Peter Höfner: peter.hoefner <at> informatik.uni-augsburg.de

Last update: 2008