The verification of temporal logic properties of reactive systems has been classically introduced as a model checking problem where one has to check that a temporal logic property holds on all initial states of a considered state transition system. A major breakthrough has been achieved by symbolic model checking, first by fixpoint computations where the state sets were stored as canonical normal forms of propositional logic formulas like BDDs, and later as bounded and SAT-based model checking procedures using SAT solvers. Interpolation-based model checking finally paved the way for induction-based methods like property-directed reachability (PDR) that are currently the most efficient verification procedures. However, PDR is so-far only used for the verification of safety properties, i.e., to prove that a desired property holds on all reachable states. In this paper, we prove the correctness and completeness of induction rules for general fixpoint formulas that extend Park's fixpoint induction rules. We instantiate these rules for all CTL operators so that induction becomes available for all CTL properties. Moreover, we develop further induction rules for liveness properties by considering liveness properties as bounded safety properties. In general, we therefore point out that induction-based proof methods are not limited to safety properties.
展开▼
