Javier Esparza
ABSTRACT
We present a unified translation of LTL formulas into deterministic Rabin automata, limit-deterministic Büchi automata, and nondeterministic Büchi automata. The translations yield automata of asymptotically optimal size (double or single exponential, respectively). All three translations are derived from one single Master Theorem of purely logical nature. The Master Theorem decomposes the language of a formula into a positive boolean combination of languages that can be translated into ω-automata by elementary means. In particular, Safra's, ranking, and breakpoint constructions used in other translations are not needed.
- Valentin M. Antimirov. 1996. Partial Derivatives of Regular Expressions and Finite Automaton Constructions. Theor. Comput. Sci. 155, 2 (1996), 291--319. Google Scholar
Digital Library
- Tomáš Babiak, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Křetínský, David Müller, David Parker, and Jan Strejček. 2015. The Hanoi Omega-Automata Format. In CAV. 479--486.Google Scholar
- Tomás Babiak, Frantisek Blahoudek, Mojmír Křetínský, and Jan Strejcek. 2013. Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F, G)-Fragment. In ATVA. 24--39.Google Scholar
- Tomás Babiak, Mojmír Křetínský, Vojtech Rehák, and Jan Strejcek. 2012. LTL to Büchi Automata Translation: Fast and More Deterministic. In TACAS. 95--109. Google ScholarDigital Library
- Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press. Google ScholarDigital Library
- Christel Baier, Stefan Kiefer, Joachim Klein, Sascha Klüppelholz, David Müller, and James Worrell. 2016. Markov Chains and Unambiguous Büchi Automata. In CAV. 23--42.Google Scholar
- Janusz A. Brzozowski. 1964. Derivatives of Regular Expressions. J. ACM 11, 4 (1964), 481--494. Google ScholarDigital Library
- Krishnendu Chatterjee, Andreas Gaiser, and Jan Křetínský. 2013. Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis. In CAV. 559--575.Google Scholar
- Costas Courcoubetis and Mihalis Yannakakis. 1995. The Complexity of Probabilistic Verification. J. ACM 42, 4 (1995), 857--907. Google ScholarDigital Library
- Jean-Michel Couvreur. 1999. On-the-Fly Verification of Linear Temporal Logic. In FM. 253--271. Google ScholarDigital Library
- Marco Daniele, Fausto Giunchiglia, and Moshe Y. Vardi. 1999. Improved Automata Generation for Linear Temporal Logic. In CAV. 249--260. Google ScholarDigital Library
- Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, and Laurent Xu. 2016. Spot 2.0 - A Framework for LTL and ω-Automata Manipulation. In ATVA. 122--129.Google Scholar
- Javier Esparza and Jan Křetínský. 2014. From LTL to Deterministic Automata: A Safraless Compositional Approach. In CAV. 192--208. Google ScholarDigital Library
- Javier Esparza, Jan Křetínský, Jean-François Raskin, and Salomon Sickert. 2017. From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata. In TACAS. 426--442.Google Scholar
- Javier Esparza, Jan Křetínský, and Salomon Sickert. 2016. From LTL to deterministic automata - A safraless compositional approach. Formal Methods in System Design 49,3 (2016), 219--271. Google ScholarDigital Library
- Javier Esparza, Jan Křetínský, and Salomon Sickert. 2018. One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata. CoRR abs/1805.00748 (2018). arXiv:1805.00748 http://arxiv.org/abs/1805.00748 Google ScholarDigital Library
- Kousha Etessami and Gerard J. Holzmann. 2000. Optimizing Büchi Automata. In CONCUR. 153--167. Google ScholarDigital Library
- Carsten Fritz. 2003. Constructing Büchi Automata from Linear Temporal Logic Using Simulation Relations for Alternating Büchi Automata. In CIAA. 35--48. Google ScholarDigital Library
- Andreas Gaiser, Jan Křetínský, and Javier Esparza. 2012. Rabinizer: Small Deterministic Automata for LTL(F,G). In ATVA. 72--76. Google ScholarDigital Library
- Paul Gastin and Denis Oddoux. 2001. Fast LTL to Büchi Automata Translation. In CAV. 53--65. Google ScholarDigital Library
- Dimitra Giannakopoulou and Flavio Lerda. 2002. From States to Transitions: Improving Translation of LTL Formulae to Büchi Automata. In FORTE. 308--326. Google ScholarDigital Library
- Ernst Moritz Hahn, Guangyuan Li, Sven Schewe, Andrea Turrini, and Lijun Zhang. 2015. Lazy Probabilistic Model Checking without Determinisation. In CONCUR. 354--367.Google Scholar
- Dileep Kini and Mahesh Viswanathan. 2015. Limit Deterministic and Probabilistic Automata for LTL \ GU. In TACAS. 628--642. Google ScholarDigital Library
- Dileep Kini and Mahesh Viswanathan. 2017. Optimal Translation of LTL to Limit Deterministic Automata. In TACAS. 113--129. Google ScholarDigital Library
- Zuzana Komárková and Jan Křetínský. 2014. Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata. In ATVA (LNCS), Vol. 8837. 235--241.Google Scholar
- Jan Křetínský and Javier Esparza. 2012. Deterministic Automata for the (F,G)-Fragment of LTL. In CAV. 7--22. Google ScholarDigital Library
- Jan Křetínský and Ruslán Ledesma-Garza. 2013. Rabinizer 2: Small Deterministic Automata for LTL \ GU. In ATVA. 446--450.Google Scholar
- Jan Křetínský, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger. 2017. Index Appearance Record for Transforming Rabin Automata into Parity Automata. In TACAS. 443--460.Google Scholar
- Jianwen Li, Geguang Pu, Lijun Zhang, Zheng Wang, Jifeng He, and Kim Guldstrand Larsen. 2013. On the Relationship between LTL Normal Forms and Büchi Automata. In Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday. 256--270. Google ScholarDigital Library
- Jianwen Li, Lijun Zhang, Shufang Zhu, Geguang Pu, Moshe Y. Vardi, and Jifeng He. 2018. An explicit transition system construction approach to LTL satisfiability checking. Formal Asp. Comput. 30, 2 (2018), 193--217. Google ScholarDigital Library
- Nir Piterman. 2006. From Nondeterministic Buchi and Streett Automata to Deterministic Parity Automata. In LICS. 255--264. Google ScholarDigital Library
- Amir Pnueli. 1977. The Temporal Logic of Programs. In FOCS. 46--57. Google ScholarDigital Library
- Shmuel Safra. 1988. On the Complexity of omega-Automata. In FOCS. 319--327. Google ScholarDigital Library
- Sven Schewe. 2009. Tighter Bounds for the Determinisation of Büchi Automata. In FoSSaCS. 167--181.Google Scholar
- Salomon Sickert, Javier Esparza, Stefan Jaax, and Jan Křetínský. 2016. Limit-Deterministic Büchi Automata for Linear Temporal Logic. In CAV. 312--332.Google Scholar
- Fabio Somenzi and Roderick Bloem. 2000. Efficient Büchi Automata from LTL Formulae. In CAV. 248--263. Google ScholarDigital Library
- Moshe Y. Vardi. 1985. Automatic Verification of Probabilistic Concurrent Finite-State Programs. In FOCS. 327--338. Google ScholarDigital Library
- Moshe Y. Vardi and Pierre Wolper. 1986. An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report). In LICS. 332--344.Google Scholar
Index Terms
- One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
Recommendations
An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata
LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer ScienceIn the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formula of the form Λni =1 GFφi ∨FGψi, where φi and ψi contain only past ...
A Unified Translation of Linear Temporal Logic to ω-Automata
We present a unified translation of linear temporal logic (LTL) formulas into deterministic Rabin automata (DRA), limit-deterministic Büchi automata (LDBA), and nondeterministic Büchi automata (NBA). The translations yield automata of asymptotically ...
Efficient Normalization of Linear Temporal Logic
In the mid 1980s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of Linear Temporal Logic (LTL) with past operators) is equivalent to a formula of the form \(\bigwedge _{i=1}^n {\mathbf {G}}...
Comments