François Laroussinie ; Antoine Meyer ; Eudes Petonnet - Counting CTL

lmcs:1058 - Logical Methods in Computer Science, February 15, 2013, Volume 9, Issue 1 - https://doi.org/10.2168/LMCS-9(1:3)2013
Counting CTLArticle

Authors: François Laroussinie ; Antoine Meyer ORCID; Eudes Petonnet

    This paper presents a range of quantitative extensions for the temporal logic CTL. We enhance temporal modalities with the ability to constrain the number of states satisfying certain sub-formulas along paths. By selecting the combinations of Boolean and arithmetic operations allowed in constraints, one obtains several distinct logics generalizing CTL. We provide a thorough analysis of their expressiveness and succinctness, and of the complexity of their model-checking and satisfiability problems (ranging from P-complete to undecidable). Finally, we present two alternative logics with similar features and provide a comparative study of the properties of both variants.

    https://doi.org/10.2168/LMCS-9(1:3)2013
    Source: arXiv.org:1211.4651
    Volume: Volume 9, Issue 1
    Published on: February 15, 2013
    Imported on: February 10, 2012
    Keywords: Computer Science - Logic in Computer Science,F.4.1,D.2.4
    Licence: arXiv.org - Non-exclusive license to distribute

    1 Document citing this article

    Share and export

    Consultation statistics

    This page has been seen 1512 times.
    This article's PDF has been downloaded 372 times.