2006 | OriginalPaper | Buchkapitel
Model Checking Quantified Computation Tree Logic
verfasst von : Arend Rensink
Erschienen in: CONCUR 2006 – Concurrency Theory
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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
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. The reallocations enable minimization of the automata modulo bisimilarity, essentially through symmetry reduction. Our main result is to show that each combination of a
QCTL
formula and a finite algebra automaton can be transformed to an equivalent
PCTL
formula over an ordinary Kripke structure, while maintaining the symmetry reduction. The transformation is structure-preserving on the formulae. This gives rise to a method to lift any model checking technique for
PCTL
to
QCTL
.