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/Description | Theorem | Input-File | Output-File | Proof (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.in | lm432.out | lm432.xml |
| Lemma 4.3.3. | (a · b)ω≤ (a + b)ω | lm433.in | lm433.out | lm433.xml |
| Lemma 4.3.4. | (a+)ω = aω | lm434.in | lm434.out | lm434.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.in | ex51.out | ex51.xml |
| Case Study II | F· l1 ≤ (l1 + l2 + i)+ | cs2.in | cs2.out | cs2.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