微信服务号

微信订阅号

2025-5-13- 4
Home > Archive>Volume 34, Issue 8, 2023 >3659-3673. DOI:10.13328/j.cnki.jos.006614
PDF HTML XML Export Cite reminder
Tool for Determinization of Streett Automata
Author:
Affiliation:

Clc Number:

TP311

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

    Determinization of an automaton refers to the transformation of a nondeterministic automaton into a deterministic automaton recognizing the same language, which is one of the fundamental notions in automata theory. Determinization of ω automata serves as a basic step in the decision procedures of SnS, CTL*, and μ-calculus. Meanwhile, it is also the key to solving infinite games. Therefore, studies on the determinization of ω automata are of great significance. This study focuses on a kind of ω automata called Streett automata. Nondeterministic Streett automata can be transformed into equivalent deterministic Rabin or Parity automata. In the previous work, the study has obtained algorithms with optimal state complexity and optimal asymptotical performance, respectively. Furthermore, it is necessary to develop a tool supporting Streett determinization, so as to evaluate the actual effect of proposed algorithms and show the procedure of determinization visually. This study first introduces four different Streett determinization structures including μ-Safra trees, H-Safra trees, compact Streett Safra trees, and LIR-H-Safra trees. By H-Safra trees, which are optimal, and μ-Safra trees, deterministic Rabin transformation automata are obtained. In addition, deterministic parity transformation automata are constructed via another two structures, where LIR-H-Safra trees are asymptotically optimal. Furthermore, based on the open source software named graphical tool for omega-automata and logics (GOAL), the study develops a tool for Streett determinization and names it NS2DR&PT to support the four structures. Besides, corresponding test sets are constructed by randomly generating 100 Streett automata, and comparative experiments are carried out. Results show that the actual effect of state complexity in each structure is consistent with theoretical analysis. Moreover, the efficiency of different algorithms is compared and analyzed.

    Reference
    [1] Büchi JR. On a decision method in restricted second order arithmetic. In: Nagel E, Suppes P, Tarski A, eds. 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. [doi: 10.2307/1995086
    [3] McNaughton R. Testing and generating infinite sequences by a finite automaton. Information and Control, 1966, 9(5): 521–530. [doi: 10.1016/S0019-9958(66)80013-X
    [4] Boker U, Kupferman O. Translating to co-Büchi made tight, unified, and useful. ACM Trans. on Computational Logic, 2012, 13(4): 29. [doi: 10.1145/2362355.2362357
    [5] Pnueli A. The temporal logic of programs. In: Proc. of the 18th Annual Symp. on Foundations of Computer Science. Providence: IEEE, 1977. 46–57.
    [6] Esparza J, Křetínský J, Sickert S. A unified translation of linear temporal logic to ω-automata. Journal of the ACM, 2020, 67(6): 33. [doi: 10.1145/3417995
    [7] Tsai MH, Fogarty S, Vardi MY, Tsay YK. State of Büchi complementation. Logical Methods in Computer Science, 2014, 10(4: 13): 1–27.
    [8] 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.
    [9] 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.
    [10] Streett RS. Propositional dynamic logic of looping and converse. In: Proc. of the 13th Annual ACM Symp. on Theory of Computing. Rome: ACM, 1981. 375–383.
    [11] Mostowski AW. Regular expressions for infinite trees and a standard form of automata. In: Proc. of the 5th Computation Theory. Zaborow: Springer, 1985. 157–168.
    [12] 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
    [13] 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. British Columbia: ACM, 1992. 275–282.
    [14] Cai Y, Zhang T. Can nondeterminism help complementation? In: Proc. of the 3rd Int’l Symp. on Games, Automata, Logics and Formal Verification. Naples: GandALF, 2012. 57–70.
    [15] 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.
    [16] Althoff CS, Thomas W, Wallmeier N. Observations on determinization of Büchi automata. Theoretical Computer Science, 2006, 363(2): 224–233. [doi: 10.1016/j.tcs.2006.07.026
    [17] 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.
    [18] 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.
    [19] Muller DE, Schupp PE. Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra. Theoretical Computer Science, 1995, 141(1–2): 69–107. [doi: 10.1016/0304-3975(94)00214-4
    [20] Rabin MO, Scott D. Finite automata and their decision problems. IBM Journal of Research and Development, 1959, 3(2): 114–125. [doi: 10.1147/rd.32.0114
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

王文胜,田聪,段振华. Streett自动机确定化工具.软件学报,2023,34(8):3659-3673

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:August 24,2021
  • Revised:October 14,2021
  • Online: January 28,2022
  • Published: August 06,2023
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2044091Visitors
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