LTL to self-loop alternating automata with generic acceptance and back. (English) Zbl 1460.68049
Summary: Self-loop alternating automata (SLAA) with Büchi or co-Büchi acceptance are popular formalisms also known as very weak alternating automata (VWAA). They are often used as an intermediate results in translations of LTL to deterministic or nondeterministic automata. This paper considers SLAA with generic transition-based Emerson-Lei acceptance and presents translations of LTL to these automata and back. Importantly, the translation of LTL to SLAA with generic acceptance produces considerably smaller automata than previous translations of LTL to Büchi or co-Büchi SLAA. Our translation is already implemented in the tool ltl3tela, where it helps to produce small deterministic or nondeterministic transition-based Emerson-Lei automata for given LTL formulae.
MSC:
| 68Q45 | Formal languages and automata |
| 03B44 | Temporal logic |
| 03D05 | Automata and formal grammars in connection with logical questions |
References:
| [1] | Babiak, T.; Blahoudek, F.; Křetínský, M.; Strejček, J., Effective translation of LTL to deterministic Rabin automata: beyond the (F, G)- fragment, (Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA’13). Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA’13), Lecture Notes in Computer Science, vol. 8172 (2013), Springer), 24-39 · Zbl 1414.03003 |
| [2] | Babiak, T.; Křetínský, M.; Řehák, V.; Strejček, J., LTL to Büchi automata translation: fast and more deterministic, (Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’12). Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’12), Lecture Notes in Computer Science, vol. 7214 (2012), Springer), 95-109 · Zbl 1352.68142 |
| [3] | Babiak, T.; Blahoudek, F.; Duret-Lutz, A.; Klein, J.; Křetínský, J.; Müller, D.; Parker, D.; Strejček, J., The Hanoi omega-automata format, (Proceedings of the 27th International Conference on Computer Aided Verification (CAV’15). Proceedings of the 27th International Conference on Computer Aided Verification (CAV’15), Lecture Notes in Computer Science, vol. 9206 (2015), Springer), 479-486 |
| [4] | Baier, C.; Blahoudek, F.; Duret-Lutz, A.; Klein, J.; Müller, D.; Strejček, J., Generic emptiness check for fun and profit, (Proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA’19). Proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA’19), Lecture Notes in Computer Science, vol. 11781 (2019), Springer), 445-461 · Zbl 1437.68092 |
| [5] | Blahoudek, F.; Major, J.; Strejček, J., LTL to smaller self-loop alternating automata and back, (Proceedings of the 16th International Colloquium on Theoretical Aspects of Computing (ICTAC’19). Proceedings of the 16th International Colloquium on Theoretical Aspects of Computing (ICTAC’19), Lecture Notes in Computer Science, vol. 11884 (2019), Springer), 152-171 · Zbl 1539.68132 |
| [6] | Chatterjee, K.; Gaiser, A.; Křetínský, J., Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis, (Proceedings of the 25th International Conference on Computer Aided Verification (CAV’13). Proceedings of the 25th International Conference on Computer Aided Verification (CAV’13), Lecture Notes in Computer Science, vol. 8044 (2013), Springer), 559-575 |
| [7] | Couvreur, J.-M.; Duret-Lutz, A.; Poitrenaud, D., On-the-fly emptiness checks for generalized Büchi automata, (Proceedings of the 12th International Spin Workshop on Model Checking of Software (SPIN’05). Proceedings of the 12th International Spin Workshop on Model Checking of Software (SPIN’05), Lecture Notes in Computer Science, vol. 3639 (2005), Springer), 169-184 · Zbl 1151.68475 |
| [8] | Duret-Lutz, A., Manipulating LTL formulas using spot 1.0, (Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA’13). Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA’13), Lecture Notes in Computer Science, vol. 8172 (2013), Springer), 442-445 · Zbl 1410.68223 |
| [9] | Duret-Lutz, A.; Lewkowicz, A.; Fauchille, A.; Michaud, T.; Renault, E.; Xu, L., Spot 2.0 - a framework for LTL and w-automata manipulation, (Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA’16). Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA’16), Lecture Notes in Computer Science, vol. 9938 (2016)), 122-129 |
| [10] | Dwyer, M. B.; Avrunin, G. S.; Corbett, J. C., Property specification patterns for finite-state verification, (Proceedings of the 2nd Workshop on Formal Methods in Software Practice (FMSP’98) (1998), ACM), 7-15 |
| [11] | Emerson, E. A.; Lei, C.-L., Modalities for model checking: branching time logic strikes back, (Science of Computer Programming 8.3 (1987)), 275-306 · Zbl 0615.68019 |
| [12] | Etessami, K.; Holzmann, G. J., Optimizing Büchi automata, (Proceedings of the 11th International Conference on Concurrency Theory (CONCUR’OO). Proceedings of the 11th International Conference on Concurrency Theory (CONCUR’OO), Lecture Notes in Computer Science, vol. 1877 (2000), Springer), 153-167 · Zbl 0999.68113 |
| [13] | Gastin, P.; Oddoux, D., Fast LTL to Büchi automata translation, (Proceedings of the 13th International Conference on Computer Aided, Verification (CAV’01). Proceedings of the 13th International Conference on Computer Aided, Verification (CAV’01), Lecture Notes in Computer Science, vol. 2102 (2001), Springer), 53-65 · Zbl 0991.68044 |
| [14] | Geldenhuys, J.; Hansen, H., Larger automata and less work for LTL model checking, (Proceedings of the 13th International SPIN Symposium on Model Checking of Software (SPIN’06). Proceedings of the 13th International SPIN Symposium on Model Checking of Software (SPIN’06), Lecture Notes in Computer Science, vol. 3925 (2006), Springer), 53-70 · Zbl 1178.68343 |
| [15] | Hammer, M.; Knapp, A.; Merz, S., Truly on-the-fly LTL model checking, (Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’05). Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’05), Lecture Notes in Computer Science, vol. 3440 (2005), Springer), 191-205 · Zbl 1087.68591 |
| [16] | Holeček, J.; Kratochvíla, T.; Řehák, V.; Šafránek, D.; Šimeček, P., Verification Results in Liberouter Project (Sept. 2004), ESNET, 32 pp |
| [17] | Křetínský, J.; Meggendorfer, T.; Sickert, S., Owl: a library for ω-words, automata, and LTL, (Proceedings of the 16th International Symposium, on Automated Technology for Verification and Analysis (ATVA’18). Proceedings of the 16th International Symposium, on Automated Technology for Verification and Analysis (ATVA’18), Lecture Notes in Computer Science, vol. 11138 (2018), Springer), 543-550 · Zbl 1517.68203 |
| [18] | Křetínský, J.; Meggendorfer, T.; Sickert, S.; Ziegler, C., Rabinizer 4: from LTL to your favourite deterministic automaton, (Proceedings of the 30th International Conference on Computer Aided Verification (CAV’18). Proceedings of the 30th International Conference on Computer Aided Verification (CAV’18), Lecture Notes in Computer Science, vol. 10981 (2018), Springer), 567-577 |
| [19] | Löding, C.; Thomas, W., Alternating automata and logics over infinite words, (Proceedings of International Conference Theoretical Computer Science, Exploring New Frontiers of Theoretical Informatics (IFIP TCS’00). Proceedings of International Conference Theoretical Computer Science, Exploring New Frontiers of Theoretical Informatics (IFIP TCS’00), Lecture Notes in Computer Science, vol. 1872 (2000), Springer), 521-535 · Zbl 0998.68526 |
| [20] | Major, J., Translation of LTL into nondeterministic automata with generic acceptance condition (2017), Masaryk University: Masaryk University Brno, MA thesis |
| [21] | Major, J.; Blahoudek, F.; Strejček, J.; Sasaráková, M.; Zbončáková, T., ltl3tela: LTL to small deterministic or nondeterministic Emerson-Lei automata, (Proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA’19). Proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA’19), Lecture Notes in Computer Science, vol. 11781 (2019), Springer), 357-365 |
| [22] | Muller, D. E.; Saoudi, A.; Schupp, P. E., Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time, (Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS’88) (1988), IEEE Computer Society), 422-427 |
| [23] | Müller, D.; Sickert, S., LTL to deterministic Emerson-Lei automata, (Proceedings of the 8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF’17). Proceedings of the 8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF’17), EPTCS, vol. 256 (2017)), 180-194 · Zbl 1483.68177 |
| [24] | Pelánek, R., BEEM: benchmarks for explicit model checkers, (Proceedings of the 14th International SPIN Conference on Model Checking Software (SPIN’07). Proceedings of the 14th International SPIN Conference on Model Checking Software (SPIN’07), Lecture Notes in Computer Science, vol. 4595 (2007), Springer), 263-267 |
| [25] | Pelánek, R.; Strejček, J., Deeper connections between LTL and alternating automata, (Proceedings of the 10th International Conference on Implementation and Application of Automata (CIAA’05). Proceedings of the 10th International Conference on Implementation and Application of Automata (CIAA’05), Lecture Notes in Computer Science, vol. 3845 (2005), Springer), 238-249 · Zbl 1172.68523 |
| [26] | Pnueli, A., The temporal logic of programs, (Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS’77) (1977), IEEE Computer Society), 46-57 |
| [27] | Renault, E.; Duret-Lutz, A.; Kordon, F.; Poitrenaud, D., Parallel explicit model checking for generalized Büchi automata, (Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’15). Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’15), Lecture Notes in Computer Science, vol. 9035 (2015), Springer), 613-627 · Zbl 1420.68137 |
| [28] | Rohde, G. S., Alternating Automata and the Temporal Logic of Ordinals (1997), University of Illinois at Urbana-Champaign, PhD thesis |
| [29] | Somenzi, F.; Bloem, R., Efficient Büchi automata from LTL formulae, (Proceedings of the 12th International Conference on Computer Aided, Verification (CAV’00). Proceedings of the 12th International Conference on Computer Aided, Verification (CAV’00), Lecture Notes in Computer Science, vol. 1855 (2000), Springer), 248-263 · Zbl 0974.68086 |
| [30] | Tauriainen, H., Automata and Linear Temporal Logic: Translations with Transition-Based Acceptance (2006), Helsinki University of Technology, Laboratory for Theoretical Computer Science, PhD thesis |
| [31] | Vardi, M. Y., Nontraditional applications of automata theory, (Proceedings of the International Conference on Theoretical Aspects of Computer Software (TACS’94). Proceedings of the International Conference on Theoretical Aspects of Computer Software (TACS’94), Lecture Notes in Computer Science, vol. 789 (1994), Springer), 575-597 · Zbl 0942.68600 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
