SucheAlgebraic Calculi for Hybrid Systems
P. Höfner
erschienen 2009
ISBN: 978-3-8391-2510-6
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 thesis, 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 thesis we pay special attention to the relationship between the logics involved and hybrid systems.
The thesis 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.
Verlag: Books on Demand
ISBN: 978-3-8391-2510-6
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 thesis, 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 thesis we pay special attention to the relationship between the logics involved and hybrid systems.
The thesis 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.