Limit deterministic and probabilistic automata for LTL\GU

Dileep Kini, Mahesh Viswanathan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

LTL\GU is a fragment of linear temporal logic (LTL), where negations appear only on propositions, and formulas are built using the temporal operators X (next), F (eventually), G (always), and U (until, with the restriction that no until operator occurs in the scope of an always operator. Our main result is the construction of Limit Deterministic B¨uchi automata for this logic that are exponential in the size of the formula. One consequence of our construction is a new, improved EXPTIME model checking algorithm (as opposed to the previously known doubly exponential time) for Markov Decision Processes and LTL\GU formulae. Another consequence is that it gives us a way to construct exponential sized Probabilistic B¨uchi Automata for LTL\GU.

Original languageEnglish (US)
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings
EditorsCesare Tinelli, Christel Baier
PublisherSpringer-Verlag
Pages628-642
Number of pages15
ISBN (Electronic)9783662466803
DOIs
StatePublished - Jan 1 2015
Event21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015 - London, United Kingdom
Duration: Apr 11 2015Apr 18 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9035
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015
CountryUnited Kingdom
CityLondon
Period4/11/154/18/15

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Limit deterministic and probabilistic automata for LTL\GU'. Together they form a unique fingerprint.

  • Cite this

    Kini, D., & Viswanathan, M. (2015). Limit deterministic and probabilistic automata for LTL\GU. In C. Tinelli, & C. Baier (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings (pp. 628-642). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9035). Springer-Verlag. https://doi.org/10.1007/978-3-662-46681-0_57