• DocumentCode
    3722907
  • Title

    The Model Checking Fingerprints of CTL Operators

  • Author

    Andreas Krebs;Arne Meier;Martin Mundhenk

  • Author_Institution
    Univ. Tubingen, Tubingen, Germany
  • fYear
    2015
  • Firstpage
    101
  • Lastpage
    110
  • Abstract
    The aim of this study is to understand the inherent expressive power of CTL operators. We investigate the complexity of model checking for all CTL fragments with one CTL operator and arbitrary Boolean operators. This gives us a fingerprint of each CTL operator. The comparison between the fingerprints yields a hierarchy of the operators that mirrors their strength with respect to model checking.
  • Keywords
    "Model checking","Complexity theory","Erbium","Gold","Cloning","Semantics","Boolean functions"
  • Publisher
    ieee
  • Conference_Titel
    Temporal Representation and Reasoning (TIME), 2015 22nd International Symposium on
  • ISSN
    1530-1311
  • Type

    conf

  • DOI
    10.1109/TIME.2015.13
  • Filename
    7371929
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3722907