Informatik-Kolloquium/MOVES Seminar, 16. Februar 2006
Model Checking Quantified Computation Tree Logic
Dr. ir. Arend Rensink
University of Twente
Abstract:
Propositional temporal logic is not suitable for expressing properties on the evolution of dynamically allocated entities over time. In particular, it is not possible to trace such entities through computation steps, since this requires the ability to freely mix quantification and temporal operators. In this paper we study a logic, called Quantified Computation Tree Logic (QCTL), which extends the well-known propositional computation tree logic, PCTL, with first and (monadic) second order quantification. The semantics of QCTL is expressed on algebra automata, which are automata enriched with abstract algebras at each state, and with reallocations at each transition that express an injective renaming of the algebra elements from one state to the next. Our main result is to show that each combination of a QCTL formula and an algebra automaton can be transformed to an equivalent PCTL formula over an ordinary Kripke structure. The transformation is structure-preserving on the formulae. This gives rise to a method to lift any model checking technique for PCTL to QCTL.
Propositional temporal logic is not suitable for expressing properties on the evolution of dynamically allocated entities over time. In particular, it is not possible to trace such entities through computation steps, since this requires the ability to freely mix quantification and temporal operators. In this paper we study a logic, called Quantified Computation Tree Logic (QCTL), which extends the well-known propositional computation tree logic, PCTL, with first and (monadic) second order quantification. The semantics of QCTL is expressed on algebra automata, which are automata enriched with abstract algebras at each state, and with reallocations at each transition that express an injective renaming of the algebra elements from one state to the next. Our main result is to show that each combination of a QCTL formula and an algebra automaton can be transformed to an equivalent PCTL formula over an ordinary Kripke structure. The transformation is structure-preserving on the formulae. This gives rise to a method to lift any model checking technique for PCTL to QCTL.
