|
From the Content
|
||||||||||
|
|
From the Content
|
||||||||||
Over the past decades incorrect software has claimed numerous lives and has caused environmental damages. Furthermore incorrect software regularly yields economic losses. Systems that interact with their environment are especially fault-prone. On the one hand, they have to be flexible enough to react to environment changes, on the other hand they have to be predictable. Unlike software systems for office work, interacting systems must satisfy restrictive safety criteria — an airbag that inflates too late is unacceptable.
Hybrid systems are often used to model such safety critical systems. They are heterogeneous systems characterised by the interaction of continuous dynamics and discrete events that cause state changes. They have found widespread applications ranging from control and medical engineering to avionics. But even biological and chemical processes can concisely be described by such systems.
In many cases, hybrid systems are too complex for computer-aided verification — even with today's computers that offer enormous memory and calculating capacities. In this book, we aim at a compact treatment of verification tasks. Algebraic techniques are of particular interest and arise in a natural way. Systems are algebraically described by systems of equations that are similar to those known from high school. Advantages that accrue by an algebraic approach are conciseness, clarity and simplicity; in particular with respect to (computer-aided) calculation rules. The developed algebraic characterisation of hybrid systems allows, for example, the verification of safety aspects by simple algebraic transformations. The approach further enables the use of off-the-shelf automated theorem provers. These provers can be employed to verify fundamental properties of hybrid systems.
Over the last decade dozens of logic-based approaches have been applied to hybrid systems. These approaches range from classical propositional logics and modal or temporal logics that have been transferred over to hybrid systems to special logics that have been developed for them. Most of them are well-understood, but due to their different notions, syntax and semantics a uniform treatment is not available. Therefore we explore a compact and uniform treatment for all these logics. The unification is based on the same algebraic techniques as for the characterisation of hybrid systems. This allows cross-reasoning through all unified logics. In this book we pay special attention to the relationship between the logics involved and hybrid systems.
This book presents fundamental methods for the analysis of hybrid systems and results in a coherent family of algebraic calculi for hybrid systems. The suitability and the relevance of the theory is proved by first case studies.
Preview at Google Books.
Get this book
BoD-Books on Demand / Libri,
Amazon.de
Most of the proofs have been verified by the automated theorem prover Prover9, version LADR-April-2007. (thanks to William McCune).
The corresponding input files can be downloaded here; the saved output files can be downloaded as well.1,2
We have done more proof experiments including various algebraic theory and different first-order theorem provers. The files concerning these experiments can be found in a proof database.
(forthcoming)
Every chapter of the book starts with a quotation. Most of the quotations are in different languages. To make them understandable for a broader community, we provide translations to English and German.
| Original Quote | English | German | Year of Publication |
|---|---|---|---|
|
“Begin at the beginning,” the King said gravely, “and go on till you come to the end: then stop.”
L. Carroll (Alice's Adventures in Wonderland) |
“Begin at the beginning,” the King said gravely, “and go on till you come to the end: then stop.”
L. Carroll (Alice's Adventures in Wonderland) |
„Fange beim Anfang an,” sagte der König ernsthaft, „und fahre fort bis du an's Ende kommst, dann halte an”
L. Carroll (Alice im Wunderland) |
1865 AD |
|
Εν χρὁνω γἀρ πᾶσα κινησις καἰ τἑλονς τινὁς.
Ἀριστοτέλης (ὴθικἀ Νικ;ομἁχεια Κ) |
Every motion is a process in time and comes to an intended end.
Aristotle (Nicomachean Ethics X) |
Jede Bewegung verläuft in der Zeit und hat ein Ziel.
Aristoteles (Nikomachische Ethik X) |
around 350 BC |
| Из нета не Выкроишь естя. |
You cannot make something from nothing.
(Russian Proverb) |
Aus einem Nichts kann man kein Etwas schneiden.
(Russisches Sprichwort) |
|
|
[...] De Manera, que quien sabe por Algebra, sabe scientificamente.
P. Nuñes (Libro de Algebra en Arithmetica y Geometria) |
Therefore, he who knows algebra thinks scientifically.
P. Nuñes (Algebra Book on Arithmetic and Geometry) |
Derjenige der also Algebra beherrscht denkt wissenschaftlich.
P. Nuñes (Algebra-Buch über Arithmetik und Geometrie) |
1567 AD |
| 空 穴 来 风 未 必 无 因 |
If the wind comes from an empty cave, it's not without a reason. (meaning: everything has a (logical) reason) (Chinese Proverb) |
Wenn Wind aus einer leere Höhle bläst, geschieht das nicht ohne Grund (Bedeutung: alles hat eine (logische) Erklärung) (Chinesisches Sprichwort) |
|
| Obodo n'ezu ezu azu nwa. |
It takes a whole village to raise a child.
(Igbo and Yoruba Proverb (Nigeria)) |
Es braucht ein ganzes Dorf um ein Kind aufzuziehen.
(Igboisches und Yorubaisches Sprichwort (Nigeria)) |
|
Ptahhotep |
Don't be too proud of your knowledge.
Ptahhotep |
Sei nicht arrogant/hochmütig auf Dein Wissen.
Ptahhotep |
around 2500 BC |
|
Fata viam invenient.
Virgil (Aeneis X) |
The fate will find a way.
Virgil (Aeneis X) |
Das Schicksal findet seinen Weg.
Virgil (Aeneis X) |
between 29 and 19 BC |
|
Quand on veut un mouton, c'est la preuve qu'on existe.
A. de Saint-Exupéry (Le Petit Prince) |
If anybody wants a sheep, that is a proof that he exists.
A. de Saint-Exupéry (The little prince) |
Denn wenn man sich ein Schaf wünscht, ist es doch ein Beweis dafür, daß man lebt.
A. de Saint-Exupéry (Der kleine Prinz) |
1943 AD |
|
Die Liebe zum Detail verbaut so manchem die Aussicht auf ein sorgenfreies Leben.
Anonym |
The attention to detail often deprives from any chances for a life without care.
Anonymus |
Die Liebe zum Detail verbaut so manchem die Aussicht auf ein sorgenfreies Leben.
Anonym |
| 1 | The proofs we provide have been generated on May 14, 2014. Running times are w.r.t. a 2.8 GHz Intel Core i7, 8GB RAM MacBook Pro; as a consequence these times are much shorter than the ones indicated in the thesis. |
| 2 | It has been pointed out that some of the input files do not run with newer versions of Prover 9 (e.g LADR-Dec-2007 which runs beneath the GUI). A conjecture is that the axiom selection mechanism has been changed in newer versions, but this has not yet been verified. I will look at this problem as soon as I have some spare time. |
Contact: Peter Höfner: peter <at> hoefner-online.de
Last update: 2013