Model Checking Quantified Computation Tree Logic

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    14 Citations (Scopus)

    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 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.
    Original languageEnglish
    Title of host publicationCONCUR 2006 – Concurrency Theory
    Subtitle of host publication17th International Conference, CONCUR 2006, Bonn, Germany, August 27-30, 2006. Proceedings
    EditorsChristel Baier, Holger Hermanns
    Place of PublicationBerlin, Heidelberg
    PublisherSpringer
    Pages110-125
    Number of pages16
    ISBN (Electronic)978-3-540-37377-3
    ISBN (Print)978-3-540-37376-6
    DOIs
    Publication statusPublished - 2006
    Event17th International Conference on Concurrency Theory, CONCUR 2006 - Bonn, Germany
    Duration: 27 Aug 200630 Aug 2006
    Conference number: 17

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume4137
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference17th International Conference on Concurrency Theory, CONCUR 2006
    Abbreviated titleCONCUR
    Country/TerritoryGermany
    CityBonn
    Period27/08/0630/08/06

    Fingerprint

    Dive into the research topics of 'Model Checking Quantified Computation Tree Logic'. Together they form a unique fingerprint.

    Cite this