Sciweavers

Share
LFCS
2007
Springer

A Temporal Dynamic Logic for Verifying Hybrid System Invariants

11 years 5 months ago
A Temporal Dynamic Logic for Verifying Hybrid System Invariants
We combine first-order dynamic logic for reasoning about possible behaviour of hybrid systems with temporal logic for reasoning about the temporal behaviour during their operation. Our logic supports verification of hybrid programs with first-order definable flows and provides a uniform treatment of discrete and continuous evolution. For our combined logic, we generalise the semantics of dynamic modalities to refer to hybrid traces instead of final states. Further, we prove that this gives a conservative extension of dynamic logic. On this basis, we provide a modular verification calculus that reduces correctness of temporal behaviour of hybrid systems to non-temporal reasoning. Using this calculus, we analyse safety invariants in a train control system and symbolically synthesise parametric safety constraints.
André Platzer
Added 08 Jun 2010
Updated 08 Jun 2010
Type Conference
Year 2007
Where LFCS
Authors André Platzer
Comments (0)
books