Tool for Determinization of Büchi Automata
Author:
Affiliation:

  • Article
  • | |
  • Metrics
  • |
  • Reference [21]
  • |
  • Related [20]
  • | | |
  • Comments
    Abstract:

    The ω automata determinization is an important part of theoretical computer research and has important applications in formal verification, sequential logic, and model checking. Since the Büchi automata was proposed for half a century, its deterministic algorithm has always been the basis. Different from the exploration of the upper and lower bounds of its size in theory at the beginning, the use of ever-changing high-performance computer technology is an effective auxiliary means. To deeply study the implementation process of the deterministic algorithm of non-deterministic Büchi automata, this study focuses on the question of whether the index can continue to be optimized and realizes the deterministic research tool NB2DR. The non-deterministic Büchi automata can be determined efficiently, and the determinization algorithm can be improved by analyzing the determinization process provided by the tool. A theoretical upper bound on correlation indexing is explored through an in-depth analysis of the indexing of generated deterministic ω automata. The tool also realizes that the deterministic Rabin automaton family can be generated according to the size of the required Büchi automaton and the alphabet parameters. It can also be reversed to generate all the Büchi automata families according to the size of the specified index required and test the equivalence of ω functions.

    Reference
    [1] Büchi JR. On a decision method in restricted second order arithmetic. In: Proc. of the 1962 Int’l Congress on Logic, Methodology and Philosophy of Science. Stanford: Stanford University Press, 1962. 1–12.
    [2] Rabin MO. Decidability of second-order theories and automata on infinite trees. Trans. of the American Mathematical Society, 1969, 141: 1–35.
    [3] Boker U, Kupferman O. Translating to co-Büchi made tight, unified, and useful. ACM Trans. on Computational Logic, 2012, 13(4): 29.
    [4] Muller DE. Infinite sequences and finite machines. In: Proc. of the 4th Annual Symp. on Switching Circuit Theory and Logical Design. Chicago: IEEE, 1963. 3–16. [doi: 10.1109/SWCT.1963.8]
    [5] Vardi MY. The Büchi complementation saga. In: Thomas W, Weil P, eds. Proc. of the 24th Annual Symp. on Theoretical Aspects of Computer Science. Aachen: Springer, 2007. 12–22. [doi: 10.1007/978-3-540-70918-3_2]
    [6] Tsai MH, Fogarty S, Vardi MY, Tsay YK. State of Büchi complementation. Logical Methods in Computer Science, 2014, 10(4): 1–27. [doi: 10.2168/LMCS-10(4:13)2014]
    [7] Safra S. Exponential determinization for Ω-automata with strong-fairness acceptance condition (extended abstract). In: Proc. of the 24th Annual ACM Symp. on Theory of Computing. Victoria: ACM, 1992. 275–282. [doi: 10.1145/129712.129739]
    [8] Meyer PJ, Sickert S, Luttenberger M. Strix: Explicit reactive synthesis strikes back! In: Proc. of the 30th Int’l Conf. on Computer Aided Verification. Oxford: Springer, 2018. 578–586. [doi: 10.1007/978-3-319-96145-3_31]
    [9] Streett RS. Propositional dynamic logic of looping and converse. In: Proc. of the 13th Annual ACM Symp. on Theory of Computing. Milwaukee: ACM, 1981. 375–383. [doi: 10.1145/800076.802492]
    [10] Mostowski AW. Regular expressions for infinite trees and a standard form of automata. In: Proc. of the 5th Symp. on Computation Theory. Zaborow: Springer, 1984. 157–168. [doi: 10.1007/3-540-16066-3_15]
    [11] Piterman N. From nondeterministic Büchi and Streett automata to deterministic parity automata. Logical Methods in Computer Science, 2007, 3(3): 1–21. [doi: 10.2168/LMCS-3(3:5)2007]
    [12] Safra S. On the complexity of ω-automata. In: Proc. of the 29th Annual Symp. on Foundations of Computer Science. White Plains: IEEE, 1988. 319–327. [doi: 10.1109/SFCS.1988.21948]
    [13] Schewe S. Tighter bounds for the determinisation of Büchi automata. In: Proc. of the 12th Int’l Conf. on Foundations of Software Science and Computational Structures. York: Springer, 2009. 167–181. [doi: 10.1007/978-3-642-00596-1_13]
    [14] Tian C, Wang WS, Duan ZH. Making streett determinization tight. In: Proc. of the 35th Annual ACM/IEEE Symp. on Logic in Computer Science. Saarbrücken: ACM, 2020. 859–872. [doi: 10.1145/3373718.3394757]
    [15] Althoff CS, Thomas W, Wallmeier N. Observations on determinization of Büchi automata. Theoretical Computer Science, 2006, 363(2): 224–233.
    [16] Duret-Lutz A, Poitrenaud D. SPOT: An extensible model checking library using transition-based generalized Büchi automata. In: Proc. of the 12th IEEE Computer Society’s Annual Int’l Symp. on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems. Volendam: IEEE, 2004. 76–83. [doi: 10.1109/MASCOT.2004.1348184]
    [17] Tsay YK, Chen YF, Tsai MH, Wu KN, Chan WC. GOAL: A graphical tool for manipulating Büchi automata and temporal formulae. In: Proc. of the 13th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Braga: Springer, 2007. 466–471.
    [18] Tian C, Duan ZH. Büchi determinization made tighter. arXiv:1404.1436, 2014.
    [19] Yan QQ. Lower bounds for complementation of ω-automata via the full automata technique. In: Bugliesi M, Preneel B, Sassone V, Wegener I, eds. Proc. of the 33rd Int’l Colloquium Automata, Languages and Programming. Venice: Springer, 2006. 589–600.
    [20] Jirásková G. State complexity of some operations on binary regular languages. Theoretical Computer Science, 2005, 330(2): 287–298.
    [21] Ellson J, Gansner E, Koutsofios L, North SC, Woodhull G. Graphviz—Open source graph drawing tools. In: Mutzel P, Jünger M, Leipert S, eds. Proc. of the 9th Int’l Symp. on Graph Drawing. Vienna: Springer, 2002. 483–484. [doi: 10.1007/3-540-45848-4_57]
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

马润哲,田聪,王文胜,段振华. Büchi自动机确定化分析工具.软件学报,2024,35(9):4310-4323

Copy
Share
Article Metrics
  • Abstract:516
  • PDF: 2537
  • HTML: 805
  • Cited by: 0
History
  • Received:September 18,2023
  • Revised:October 30,2023
  • Online: January 05,2024
  • Published: September 06,2024
You are the first2036686Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063