On Hybrid Systems and the Modal m-Calculus (extended abstract)

J. M. Davoren

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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.