TY - GEN
T1 - From ltl and limit-deterministic büchi automata to deterministic parity automata
AU - Esparza, Javier
AU - Křetínský, Jan
AU - Raskin, Jean François
AU - Sickert, Salomon
N1 - Publisher Copyright:
© Springer-Verlag GmbH Germany 2017.
PY - 2017
Y1 - 2017
N2 - Controller synthesis for general linear temporal logic (LTL) objectives is a challenging task. The standard approach involves translating the LTL objective into a deterministic parity automaton (DPA) by means of the Safra-Piterman construction. One of the challenges is the size of the DPA, which often grows very fast in practice, and can reach double exponential size in the length of the LTL formula. In this paper we describe a single exponential translation from limit-deterministic Büchi automata (LDBA) to DPA, and show that it can be concatenated with a recent efficient translation from LTL to LDBA to yield a double exponential, “Safraless” LTL-to-DPA construction. We also report on an implementation, a comparison with the SPOT library, and performance on several sets of formulas, including instances from the 2016 SyntComp competition.
AB - Controller synthesis for general linear temporal logic (LTL) objectives is a challenging task. The standard approach involves translating the LTL objective into a deterministic parity automaton (DPA) by means of the Safra-Piterman construction. One of the challenges is the size of the DPA, which often grows very fast in practice, and can reach double exponential size in the length of the LTL formula. In this paper we describe a single exponential translation from limit-deterministic Büchi automata (LDBA) to DPA, and show that it can be concatenated with a recent efficient translation from LTL to LDBA to yield a double exponential, “Safraless” LTL-to-DPA construction. We also report on an implementation, a comparison with the SPOT library, and performance on several sets of formulas, including instances from the 2016 SyntComp competition.
UR - http://www.scopus.com/inward/record.url?scp=85017506928&partnerID=8YFLogxK
U2 - 10.1007/978-3-662-54577-5_25
DO - 10.1007/978-3-662-54577-5_25
M3 - Conference contribution
AN - SCOPUS:85017506928
SN - 9783662545768
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 426
EP - 442
BT - Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings
A2 - Margaria , Tiziana
A2 - Legay, Axel
PB - Springer Verlag
T2 - 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017
Y2 - 22 April 2017 through 29 April 2017
ER -