Constraint-Based Abstract Semantics for Temporal Logic: A Direct Approach to Design and Implementation

摘要: Abstract interpretation provides a practical approach to verifying properties of infinite-state systems. We apply the framework abstract derive an semantic function for modal µ-calculus, which is basis model checking. The constructed directly from standard concrete semantics together with Galois connection between state-space and domain. There no need mixed or transition systems arbitrary temporal properties, as in previous work area Using µ-calculus implement CTL, gives over-approximation set states CTL formula holds. Then we show that this leads effective implementation checking algorithm using domains based on linear constraints. makes use SMT solver. describe implemented system proving hybrid automata give some experimental results.