TY - GEN
T1 - Limit deterministic and probabilistic automata for LTL\GU
AU - Kini, Dileep
AU - Viswanathan, Mahesh
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2015.
PY - 2015
Y1 - 2015
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84926613640&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84926613640&partnerID=8YFLogxK
U2 - 10.1007/978-3-662-46681-0_57
DO - 10.1007/978-3-662-46681-0_57
M3 - Conference contribution
AN - SCOPUS:84926613640
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 628
EP - 642
BT - 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
A2 - Tinelli, Cesare
A2 - Baier, Christel
PB - Springer
T2 - 21st 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
Y2 - 11 April 2015 through 18 April 2015
ER -