A Uniform Approach to Three-Valued Semantics for µ-Calculus on Abstractions of Hybrid Automata

Abstraction/refinement methods play a central role in the analysis of hybrid automata, that are rarely decidable. Soundness (of evaluated properties) is a major challenge for these methods, since abstractions can introduce unrealistic behaviors. In this paper, we consider the definition of a three-valued semantics for μ-calculus on abstractions of hybrid automata. Our approach relies on two steps: First, we develop a framework that is general in the sense that it provides a preservation result that holds for several possible semantics of the modal operators. In a second step, we instantiate our framework to two particular abstractions. To this end, a key issue is the consideration of both over- and under-approximated reachability analysis, while classic simulation-based abstractions rely only on overapproximations, and limit the preservation to the universal (μ-calculus’) fragment. To specialize our general result, we consider (1) so-called discrete bounded bisimulation abstractions, and (2) modal abstractions based on may/must transitions.