Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic. (English) Zbl 1153.03016
Summary: This paper addresses the problem of generating deterministic \(\omega\)-automata for formulas of linear temporal logic, which can be solved by applying well-known algorithms to construct a nondeterministic Büchi automaton for the given formula on which we then apply a determinization algorithm. We study here in detail Safra’s determinization algorithm, present several heuristics that attempt to decrease the size of the resulting automata and report on experimental results.
MSC:
| 03D05 | Automata and formal grammars in connection with logical questions |
| 03B44 | Temporal logic |
| 68Q45 | Formal languages and automata |
Keywords:
determinization; Safra’s algorithm; \(\omega\)-automata; LTL; deterministic Rabin/Streett automataReferences:
| [1] | C.S. Althoff, W. Thomas, N. Wallmeier, Observations on determinization of Büchi automata, in: CIAA’05, Proc. Lecture Notes in Computer Science, Vol. 3845, Springer, Berlin, 2006, pp. 262-272.; C.S. Althoff, W. Thomas, N. Wallmeier, Observations on determinization of Büchi automata, in: CIAA’05, Proc. Lecture Notes in Computer Science, Vol. 3845, Springer, Berlin, 2006, pp. 262-272. · Zbl 1172.68490 |
| [2] | Baier, C.; Kwiatkowska, M., Model checking for a probabilistic branching time logic with fairness, Distributed Comput., 11, 125-155 (1998) · Zbl 1448.68285 |
| [3] | L. de Alfaro, Formal verification of probabilistic systems, Ph.D. Thesis, Department of Computer Science, Stanford University, Stanford, 1997.; L. de Alfaro, Formal verification of probabilistic systems, Ph.D. Thesis, Department of Computer Science, Stanford University, Stanford, 1997. |
| [4] | M.B. Dwyer, G.S. Avrunin, J.C. Corbett, Patterns in property specifications for finite-state verification, in: ICSE, 1999, pp. 411-420.; M.B. Dwyer, G.S. Avrunin, J.C. Corbett, Patterns in property specifications for finite-state verification, in: ICSE, 1999, pp. 411-420. |
| [5] | Emerson, E. A.; Sistla, A. P., Deciding branching time logic, (STOC’84 (1984), ACM: ACM New York), 14-24 · Zbl 0593.03007 |
| [6] | K. Etessami, G.J. Holzmann, Optimizing Büchi automata, in: CONCUR, Lecture Notes in Computer Science, Vol. 1877, Springer, Berlin, 2000, pp. 153-167.; K. Etessami, G.J. Holzmann, Optimizing Büchi automata, in: CONCUR, Lecture Notes in Computer Science, Vol. 1877, Springer, Berlin, 2000, pp. 153-167. · Zbl 0999.68113 |
| [7] | K. Etessami, T. Wilke, R.A. Schuller, Fair simulation relations, parity games, and state space reduction for Büchi automata, in: ICALP’2001, Lecture Notes in Computer Science, Vol. 2076, Springer, Berlin, 2001, pp. 694-707.; K. Etessami, T. Wilke, R.A. Schuller, Fair simulation relations, parity games, and state space reduction for Büchi automata, in: ICALP’2001, Lecture Notes in Computer Science, Vol. 2076, Springer, Berlin, 2001, pp. 694-707. · Zbl 0986.68049 |
| [8] | C. Fritz, Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata, in: CIAA 2003, Lecture Notes in Computer Science, Vol. 2759, Springer, Berlin, 2003, pp. 35-48.; C. Fritz, Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata, in: CIAA 2003, Lecture Notes in Computer Science, Vol. 2759, Springer, Berlin, 2003, pp. 35-48. · Zbl 1279.68152 |
| [9] | P. Gastin, D. Oddoux, Fast LTL to Büchi automata translation, in: Computer Aided Verification (CAV’2001), Proc. Lecture Notes in Computer Science, Vol. 2102, Springer, Berlin. 2001, pp. 53-65.; P. Gastin, D. Oddoux, Fast LTL to Büchi automata translation, in: Computer Aided Verification (CAV’2001), Proc. Lecture Notes in Computer Science, Vol. 2102, Springer, Berlin. 2001, pp. 53-65. · Zbl 0991.68044 |
| [10] | R. Gerth, D. Peled, M.Y. Vardi, P. Wolper, Simple on-the-fly automatic verification of linear temporal logic, in: PSTV’95, Proc. IFIP Conference Proceedings, Vol. 38, Chapman & Hall, London, 1995, pp. 3-18.; R. Gerth, D. Peled, M.Y. Vardi, P. Wolper, Simple on-the-fly automatic verification of linear temporal logic, in: PSTV’95, Proc. IFIP Conference Proceedings, Vol. 38, Chapman & Hall, London, 1995, pp. 3-18. |
| [11] | E. Grädel, W. Thomas, T. Wilke (Eds.), Automata logics, and infinite games: a guide to current research, Lecture Notes in Computer Science, Vol. 2500, Springer, Berlin, 2002.; E. Grädel, W. Thomas, T. Wilke (Eds.), Automata logics, and infinite games: a guide to current research, Lecture Notes in Computer Science, Vol. 2500, Springer, Berlin, 2002. · Zbl 1011.00037 |
| [12] | Holzmann, G. J., The model checker spin, IEEE Trans. Software Eng., 23, 5, 279-295 (1997), (special issue on Formal Methods in Software Practice) |
| [13] | J. Klein, Linear time logic and deterministic omega-automata, Diploma Thesis, Universität Bonn, Institut für Informatik, 2005.; J. Klein, Linear time logic and deterministic omega-automata, Diploma Thesis, Universität Bonn, Institut für Informatik, 2005. |
| [14] | S.C. Krishnan, A. Puri, R.K. Brayton, Deterministic \(\operatorname{\Omega;}\) automata vis-a-vis deterministic Buchi automata, in: Algorithms and Computation, Fifth International Symposium (ISAAC’94), Lecture Notes in Computer Science, Vol. 834, Springer, Berlin, 1994, pp. 378-386.; S.C. Krishnan, A. Puri, R.K. Brayton, Deterministic \(\operatorname{\Omega;}\) automata vis-a-vis deterministic Buchi automata, in: Algorithms and Computation, Fifth International Symposium (ISAAC’94), Lecture Notes in Computer Science, Vol. 834, Springer, Berlin, 1994, pp. 378-386. · Zbl 0953.68563 |
| [15] | O. Kupferman, M. Y. Vardi, Freedom, weakness, and determinism: from lineartime to branching-time, in: Proc. 13th IEEE Symposium on Logic in Computer Science, 1998, pp. 81-92.; O. Kupferman, M. Y. Vardi, Freedom, weakness, and determinism: from lineartime to branching-time, in: Proc. 13th IEEE Symposium on Logic in Computer Science, 1998, pp. 81-92. · Zbl 0945.68522 |
| [16] | O. Kupferman, M.Y. Vardi, Model checking of safety properties, in: Computer Aided Verification (CAV’99), Proc. Lecture Notes in Computer Science, Vol. 1633, Springer, Berlin, 1999, pp. 172-183.; O. Kupferman, M.Y. Vardi, Model checking of safety properties, in: Computer Aided Verification (CAV’99), Proc. Lecture Notes in Computer Science, Vol. 1633, Springer, Berlin, 1999, pp. 172-183. · Zbl 1046.68597 |
| [17] | T. Latvala, On model checking safety properties, Research Report A76, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, 2002.; T. Latvala, On model checking safety properties, Research Report A76, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, 2002. · Zbl 1023.68625 |
| [18] | C. Löding, Methods for the transformation of omega-automata: complexity and connection to second order logic, Diploma Thesis, Universität Kiel, Germany, 1998.; C. Löding, Methods for the transformation of omega-automata: complexity and connection to second order logic, Diploma Thesis, Universität Kiel, Germany, 1998. |
| [19] | C. Löding, Optimal bounds for the transformation of omega-automata, in: FSTTCS’99, Lecture Notes in Computer Science, Vol. 1738, Springer, Berlin, 1999, pp. 97-109.; C. Löding, Optimal bounds for the transformation of omega-automata, in: FSTTCS’99, Lecture Notes in Computer Science, Vol. 1738, Springer, Berlin, 1999, pp. 97-109. · Zbl 0961.68074 |
| [20] | Löding, C., Efficient minimization of deterministic weak omega-automata, Inform. Process. Lett., 79, 3, 105-109 (2001) · Zbl 1032.68103 |
| [21] | M. Michel, Complementation is more difficult with automata on infinite words, Technical Report CNET, Paris, 1988.; M. Michel, Complementation is more difficult with automata on infinite words, Technical Report CNET, Paris, 1988. |
| [22] | Muller, D. E.; Schupp, P. E., Simulating alternating tree automata by nondeterministic automata: new results and new proofs of the theorems of Rabin, McNaughton and Safra, Theoret. Comput. Sci., 141, 1-2, 69-107 (1995) · Zbl 0873.68135 |
| [23] | Paige, R.; Tarjan, R. E., Three partition refinement algorithms, SIAM J. Comput., 16, 6, 973-989 (1987) · Zbl 0654.68072 |
| [24] | S. Safra, On the complexity of \(\operatorname{\Omega;} \)-automata, in: Proc. 29th Annual Symposium on Foundations of Computer Science (FOCS), IEEE Computer Soc. Press, Silver Spring, Berlin, 1988, pp. 319-327.; S. Safra, On the complexity of \(\operatorname{\Omega;} \)-automata, in: Proc. 29th Annual Symposium on Foundations of Computer Science (FOCS), IEEE Computer Soc. Press, Silver Spring, Berlin, 1988, pp. 319-327. |
| [25] | S. Safra, Complexity of automata on infinite objects, Ph.D. Thesis, The Weizmann Institute of Science, Rehovot, Israel, 1989.; S. Safra, Complexity of automata on infinite objects, Ph.D. Thesis, The Weizmann Institute of Science, Rehovot, Israel, 1989. |
| [26] | R. Sebastiani, S. Tonetta, “More deterministic” vs. “Smaller” Büchi automata for efficient LTL model checking, in: CHARME 2003, Proc. Lecture Notes in Computer Science, Vol. 2860, Springer, Berlin, 2003, pp. 126-140.; R. Sebastiani, S. Tonetta, “More deterministic” vs. “Smaller” Büchi automata for efficient LTL model checking, in: CHARME 2003, Proc. Lecture Notes in Computer Science, Vol. 2860, Springer, Berlin, 2003, pp. 126-140. · Zbl 1179.68095 |
| [27] | F. Somenzi, R. Bloem, Efficient Büchi automata from LTL formulae, in: Computer Aided Verification (CAV’2000), Proc. Lecture Notes in Computer Science, Vol. 1855, Springer, Berlin, 2000, pp. 248-263.; F. Somenzi, R. Bloem, Efficient Büchi automata from LTL formulae, in: Computer Aided Verification (CAV’2000), Proc. Lecture Notes in Computer Science, Vol. 1855, Springer, Berlin, 2000, pp. 248-263. · Zbl 0974.68086 |
| [28] | S. Tasiran, R. Hojati, R.K. Brayton, Language containment of nondeterministic \(\operatorname{\Omega;} \)-automata, in: CHARME’95, Lecture Notes in Computer Science, Vol. 987, Springer, Berlin, 1995, pp. 261-277.; S. Tasiran, R. Hojati, R.K. Brayton, Language containment of nondeterministic \(\operatorname{\Omega;} \)-automata, in: CHARME’95, Lecture Notes in Computer Science, Vol. 987, Springer, Berlin, 1995, pp. 261-277. |
| [29] | H. Tauriainen, Automated testing of Büchi automata translators for linear temporal logic, Research Report, Laboratory for Theoretical Computer Science, Helsinki University of Technology, December 2000.; H. Tauriainen, Automated testing of Büchi automata translators for linear temporal logic, Research Report, Laboratory for Theoretical Computer Science, Helsinki University of Technology, December 2000. |
| [30] | Thomas, W., Languages, automata, and logic, Handbook of Formal Languages, 3, 389-455 (1997) |
| [31] | M. Vardi, Probabilistic linear-time model checking: an overview of the automata-theoretic approach, in: Proc. Formal Methods for Real-Time and Probabilistic Systems (ARTS), Vol. 1601, 1999, pp. 265-276.; M. Vardi, Probabilistic linear-time model checking: an overview of the automata-theoretic approach, in: Proc. Formal Methods for Real-Time and Probabilistic Systems (ARTS), Vol. 1601, 1999, pp. 265-276. |
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.
