• DocumentCode
    2569901
  • Title

    Counting LTL

  • Author

    Laroussinie, François ; Meyer, Antoine ; Petonnet, Eudes

  • Author_Institution
    LIAFA, Univ. Paris Diderot - Paris 7, Paris, France
  • fYear
    2010
  • fDate
    6-8 Sept. 2010
  • Firstpage
    51
  • Lastpage
    58
  • Abstract
    This paper presents a quantitative extension for the linear-time temporal logic LTL allowing to specify the number of states satisfying certain sub-formulas along paths. We give decision procedures for the satisfiability and model checking of this new temporal logic and study the complexity of the corresponding problems. Furthermore we show that the problems become undecidable when more expressive constraints are considered.
  • Keywords
    computational complexity; decision making; formal verification; temporal logic; linear time temporal logic; model checking; Automata; Complexity theory; Computational modeling; Encoding; Lead; Polynomials; Semantics; counting; model-checking; satisfiability; temporal logic;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Temporal Representation and Reasoning (TIME), 2010 17th International Symposium on
  • Conference_Location
    Paris
  • ISSN
    1530-1311
  • Print_ISBN
    978-1-4244-8014-2
  • Type

    conf

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