DOI:
Abstract:
We propose the propositional modal mu-calculus -- which subsumes most known temporal and modal propositional logics -- as a broad logical framework for the formal analysis and verification of hybrid systems. Over transition system models additionally equipped with a topological or metric structure, the logic can express continuity properties of transition relations and metric tolerance properties such as being within distance epsilon of a set of states, thus enabling formal verification of robustness and stability properties of hybrid dynamical systems.