Reducing CTL-live model checking to first-order logic validity checking
Citations Over TimeTop 25% of 2014 papers
Abstract
Temporal logic model checking of infinite state systems without the use of iteration or abstraction is usually considered beyond the realm of first-order logic (FOL) reasoners because of the need for a fixpoint computation. In this paper, we show that it is possible to reduce model checking of a finite or infinite Kripke structure that is expressed in FOL to a validity problem in FOL for a fragment of computational tree logic (CTL), which we call CTL-live. CTL-live includes the CTL connectives that are traditionally used to express liveness properties. Our reduction can form the basis for methods that use FOL reasoning techniques directly to accomplish model checking of CTL-live properties without the need for fixpoint operators, transitive closure, abstraction, or induction.
Related Papers
- → Symbolic Model Checking(1993)259 cited
- → Checking Interval Properties of Computations(2014)15 cited
- A formal verification method: model checking(2006)
- Model Checking Using Partial Kripke Structure with 3-Valued Temporal Logic(2006)
- → Vectorized model checking for computation tree logic(2005)2 cited