(3.80.6.131) 您好!臺灣時間:2021/05/14 02:42
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果

詳目顯示:::

我願授權國圖
: 
twitterline
研究生:蔡明憲
研究生(外文):Ming-Hsien Tsai
論文名稱:基於自動機理論的模型檢測演算法與工具之改善
論文名稱(外文):Improved Algorithms and Tools for Automata-Theoretic Model Checking
指導教授:蔡益坤
指導教授(外文):Yih-Kuen Tsay
口試委員:顏嗣鈞王凡熊博安
口試委員(外文):Hsu-Chun YenFarn WangPao-Ann Hsiung
口試日期:2013-07-03
學位類別:博士
校院名稱:國立臺灣大學
系所名稱:資訊管理學研究所
學門:電算機學門
學類:電算機一般學類
論文種類:學術論文
論文出版年:2013
畢業學年度:101
語文別:英文
論文頁數:140
中文關鍵詞:自動機模型檢測時態邏輯
外文關鍵詞:AutomataModel CheckingTemporal Logic
相關次數:
  • 被引用被引用:0
  • 點閱點閱:144
  • 評分評分:系統版面圖檔系統版面圖檔系統版面圖檔系統版面圖檔系統版面圖檔
  • 下載下載:0
  • 收藏至我的研究室書目清單書目收藏:0
以自動機理論為基礎的模型檢測方法已經發展近三十年,此方法被認為具有效率且容易使用,在確保軟體或硬體設計的正確性上,已成為業界測試與模擬之外的另一項選擇。在這個方法中,一個待測的系統會用一個Buchi自動機來表示,而系統所需滿足的規格則用一個線性時態邏輯(PTL)式來表示。在線性時態邏輯中,比較常用到的是只能描述未來的版本(LTL)。此方法首先將規格的否定轉換成一個Buchi自動機,然後和表示系統的自動機作交集,最後測試交集部分是否不接受任何行為。在這些步驟中,時態邏輯式的轉換扮演一個重要的角色,因為一般來說,轉換出來的自動機越小,則與系統的交集也越小,而模型檢測可以比較快完成。雖然目前已經有很多LTL轉換演算法,然而在其他時態邏輯的部分,仍有改善的空間,例如比LTL更容易書寫較短規格的PTL。

系統規格也可以直接用Buchi自動機來表示,在某些情況下會比時態邏輯式更自然與直接。如此一來,在與系統自動機作交集之前,需要先計算規格自動機的補集。Buchi自動機的補集計算與有限字串長度的傳統自動機相比更加複雜許多,所以一些最佳化方法對補集計算的效能與效率有很大的幫助。因為Buchi自動機補集的高複雜度,最近許多研究都跳往不需完整建置補集的漸進式行為包含測試。在行為包含測試中,以Ramsey理論為基礎的方法已被證明相當有效率,不過在補集計算的部分卻相當不具競爭力,反而確定性方法是最好的。同樣地,為了加速模型檢測,我們除了改進時態邏輯轉換演算法之外,也可以改進補集計算與包含測試的演算法。

在時態邏輯轉換的部分,我們改善了五個漸進式演算法,利用一個回朔的程序讓這些演算法可以支援過去時態運算子,同時保持漸進式轉換的好處。對於狀態基礎演算法中的涵蓋計算程序,我們也利用質含項(Prime Implicant)加以改善。此外,我們也實作了過去與未來的分離程序,使得一個PTL式子可以被轉換成另一個相等的LTL式子,然後再利用目前最有效率的LTL轉換演算法(例如LTL2BA或是LTL3BA)來轉換。這使得我們可以比較我們所改善的演算法,以及目前最有效率的LTL轉換演算法。

在Buchi補集計算的部分,我們審視四個主要方法,並透過實驗加以比較。雖然傳統的看法是非確定性方法比確定性方法更好,因為非確定性方法有比較低的理論複雜度。然而我們的實驗顯示在Buchi補集計算中,確定性方法是最好的。此外,我們也對其中三個方法提出數個改善的點子,使得這三個方法的效率與效能大為改善。

在包含測試中,我們提出一個基於確定性方法的漸進式包含測試演算法。雖然確定性方法的執行一般被認為需要分離成幾個階段,不過我們展示這些階段其實可以合併成一個,而且可以被漸進式地執行。實驗顯示包含關係成立時,我們的方法比以Ramsey理論為基礎的方法來得好。不過包含關係不成立時,以Ramsey理論為基礎的方法卻比我們的方法來得好。

最後,我們要應付的問題是自動機與時態邏輯在教育與研究的工具支援。雖然目前已有許多以自動機理論為基礎的模型檢測工具,不過都沒有支援自動機或時態邏輯式視覺化呈現與操作。這激發了我們的第一個工具:GOAL,第一個可以用來學習無限自動機與時態邏輯的視覺化互動工具。除此之外,GOAL也提供功能幫助研究學者開發和測試新演算法、執行實驗、與收集統計資料。除了GOAL以外,我們還建制一個網頁形式的工具:Buchi Store。這個工具是許多常見時態邏輯式與其最小相等自動機的集合,可以被搜尋、瀏覽與擴展。這樣的集合不僅可以當成一個最佳時態邏輯式轉換演算法,同時也可以作為實驗的比較基礎。GOAL與Buchi Store已經幫助我們開發許多改進的演算法,讓模型檢測更加快速。我們相信這兩個工具可以提供研究學者一個好的平台,幫助未來開發相關演算法與進行實驗。

The automata-theoretic approach to model checking has been developed for near three decades. Because of its proven effectiveness and ease of use, the approach has become a viable alternative to testing and simulation in industry. In the approach, a system is typically represented by a Buchi automaton, while a specification is encoded by a formula in propositional linear temporal logic (PTL), of which the future fragment (usually referred to as LTL) is more often used. The approach proceeds by translating the negation of the formula to a Buchi automaton, which is later intersected with the system automaton for testing emptiness. Such translation plays an important role in the approach because in general, the smaller the negated-specification automaton is, the sooner the model checking process may be completed. Although there has been a long line of research on LTL translation algorithms aiming to produce smaller automata, there are still opportunities of improving translation algorithms for other temporal logics such as PTL, which is expressively more succinct than LTL.

Specifications may also be directly encoded by Buchi automata which in certain cases are more natural and easier than temporal formulae. In such cases, complementation of a specification automaton is performed before taking the intersection with the system automaton. The complementation of Buchi automata is significantly more complicated than that of classic finite automata on finite words. Optimization heuristics are critical to good performance. Due to the high complexity of Buchi complementation, much recent emphasis has been shifted to containment testing without constructing the complement. The Ramsey-based approach has been proven to be quite effective in such containment testing, although it is not competitive in complementation where the determinization-based approach is the best in general. Again, to expedite the model checking process, we can improve not only the translation algorithm but also the complementation algorithm and the containment testing algorithm.

For translation of temporal formulae, we extend five existing incremental algorithms with a backtrace procedure to support past operators of PTL, while maintaining the advantages of incremental automata construction. The cover computation common to the state-based incremental algorithms is improved based on prime implicants to obtain smaller automata. Besides, we also implement the separation of past and future separators. The separation procedure can convert a PTL formula to an equivalent LTL formula, which can later be translated by an efficient LTL translation algorithm such as LTL2BA or LTL3BA. This allows us to compare our extended algorithms with those existing efficient LTL translation algorithms.

For Buchi complementation, we review four approaches and perform a comparative experimentation on the best construction in each approach. Although the conventional wisdom is that the nondeterministic approaches are better than the deterministic approach because of better worse-case bounds, our experimental results show that the deterministic construction is the best for complementation in general. We also propose optimization heuristics for three of the four best constructions. Our experiment shows that the optimization heuristics substantially improve the three constructions.

For containment testing, we propose an incremental containment testing approach based on the determinization-based constructions, of which Safra-Piterman construction is the best in Buchi complementation. Although the determinization-based constructions are typically performed in stages, we show that the stages can be merged such that the containment testing can be performed incrementally. Our experimental results show that for cases where the containment relation holds, our incremental Safra-Piterman approach is much better then the Ramsey-based approach. For other cases where the containment relation does not hold, the Ramsey-based outperforms our incremental Safra-Piterman approach.

Finally, we address the issue of tool support for education and research on ω-automata and temporal logics. Although there are various tools for automata-theoretic model checking, none of the tools provide facilities for visually manipulating automata and temporal formulae. This motivated our GOAL tool, which is the first interactive graphical tool for learning ω-automata and temporal logics. Besides, GOAL also provides facilities for helping researchers develop and test new algorithms, perform experiments, and collect statistical data. We also build a Web-based tool called Buchi Store, which is an extensible collection of temporal formulae and their equivalent automata. Such a collection can be used not only as a new translation tool that always returns the smallest automata available but also as benchmark cases for experiments. Both GOAL and Buchi Store already helped us develop our improved algorithms, which expedite the model checking process. We believe the two tools provide researchers with a good environement for future development and experimentation of related algorithms.

1 Introduction 1
1.1 Translation of Temporal Formulae.................... 2
1.2 Complementation of Buchi Automata.................. 5
1.3 Incremental Containment Testing .................... 7
1.4 Tool Support ............................... 8
1.4.1 GOAL............................... 8
1.4.2 BuchiStore ............................ 11
1.5 Overview.................................. 14
2 Related Work 16
2.1 Translation of Propositional Temporal Formulae . . . . . . . . . . . . 16
2.2 Complementation of Buchi Automata.................. 20
2.3 Containment Testing of Buchi Automata . . . . . . . . . . . . . . . . 23
3 Preliminaries 25
3.1 Common Notations............................ 25
3.2 Propositional Temporal Logic ...................... 25
3.3 ω-Automata ............................... 28
3.4 Temporal Hierarchy............................ 30
4 Incremental Translation of PTL Formulae 32
4.1 The Classic Construction......................... 32
4.2 Construction wtih Past Operators.................... 35
4.2.1 The Translation Algorithm.................... 36
4.2.2 The Backtrace Procedure .................... 37
4.2.3 The AddTransition Procedure.................. 39
4.3 Correctness ................................ 39
4.4 Optimization Heuristics ......................... 44
4.5 Extension to Other Algorithms ..................... 46
4.5.1 Extended GPVW.......................... 46
4.5.2 Extended MoDeLLa........................ 47
4.5.3 Extended Couvreur ....................... 48
4.5.4 Extended LTL2BUCHI....................... 50
4.6 Experimental Results........................... 51
4.7 Summary of this Chapter......................... 54
5 Complementation Algorithms 56
5.1 Comparison of Complementation Approaches. . . . . . . . . . . . . . 56
5.2 Safra-Piterman Construction....................... 59
5.3 Rank-Based Construction ........................ 63
5.4 Slice-Based Construction......................... 64
5.4.1 Definitions............................. 65
5.4.2 The Basic Slice Construction.................. 67
5.4.3 The Improved Slice Construction ............... 71
5.5 Experimental Results........................... 76
5.6 Complete Experimental Results ..................... 79
5.6.1 Comparisons of Basic Constructions. . . . . . . . . . . . . . . 80
5.6.2 Comparisons of Improved Constructions . . . . . . . . . . . . 82
5.7 Summary of this Chapter......................... 83
6 Containment Testing Algorithms 86
6.1 Safra-Piterman Construction....................... 86
6.2 Incremental Universality Testing..................... 88
6.3 Incremental Containment Testing .................... 91
6.4 Experimental Results........................... 92
6.5 Summary of this Chapter......................... 94
7 Tool Support 95
7.1 GOAL................................... 96
7.1.1 Main Functions .......................... 96
7.1.2 Use Cases .............................105
7.1.3 Implementation Details......................112
7.2 BuchiStore ................................112
7.2.1 Features..............................113
7.2.2 Use Cases .............................117
7.2.3 Implementation Details......................122
7.3 Summary of this Chapter.........................125
8 Conclusion 127
8.1 Contributions ...............................127
8.2 Future Work................................128

[1] P. Abdulla, Y.-F. Chen, L. Clemente, L. Hol ́ık, C.-D. Hong, R. Mayr, and T. Vojnar. Simulation subsumption in Ramsey-based Buchi automata universality and inclusion testing. In CAV 2010, LNCS 6174, pages 132–147. Springer, 2010.
[2] P. Abdulla, Y.-F. Chen, L. Clemente, L. Hol ́ık, C.-D. Hong, R. Mayr, and T. Vojnar. Advanced Ramsey-based Buchi automata inclusion testing. In CONCUR 2011, LNCS 6901, pages 187–202. Springer, 2011.
[3] P. Abdulla, Y.-F. Chen, L. Hol ́ık, R. Mayr, and T. Vojnar. When simulation meets antichains. In TACAS 2010, LNCS 6015, pages 158–174. Springer, 2010.
[4] C. Altho↵, W. Thomas, and N. Wallmeier. Observations on determinization of Buchi automata. TCS, 363(2):224–233, 2006.
[5] A. Ben-Amram and C. Lee. Program termination analysis in polynomial time. TOPLAS, 29(1), 2007.
[6] U. Boker and O. Kupferman. Co-ing Buchi made tight and useful. In LICS 2009, pages 245–254. IEEE Computer Society, 2009.
[7] R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE TC, 35(8):677–691, 1986.
[8] J. Buchi. On a decision method in restricted second order arithmetic. In ICLMPS 1960, pages 1–12. Stanford University Press, 1962.
[9] O.CartonandR.Maceiras.ComputingtheRabinindexofaparityautomaton. ITA, 33(6):495–506, 1999.
[10] I. Cern ́a and R. Pela ́nek. Relating hierarchy of temporal properties to model checking. In MFCS, LNCS 2747, pages 318–327. Springer, 2003.
[11] K. Chatterjee, T. Henzinger, B. Jobstmann, and A. Radhakrishna. GIST: A solver for probabilistic games. In CAV 2010, LNCS 6174, pages 665–669. Springer, 2010.
[12] K. Chatterjee, T. Henzinger, B. Jobstmann, and R. Singh. QUASY: Quantitative synthesis tool. In TACAS 2011, LNCS 6605, pages 267–271. Springer, 2011.
[13] J. Cichon ́, A. Czubak, and A. Jasin ́ski. Minimal Buchi automata for certain classes of LTL formulas. In DepCoS-RELCOMEX, pages 17–24. IEEE, 2009.
[14] E. Clarke, O. Grumberg, and D. Peled. Model Checking. The MIT Press, 2000.
[15] CodeIgniter. http://codeigniter.com/.
[16] J.-M. Couvreur. On-the-fly verification of linear temporal logic. In FM, LNCS 1708, pages 253–271. Springer, 1999.
[17] M. Daniele, F. Giunchiglia, and M. Vardi. Improved automata generation for linear temporal logic. In CAV 1999, LNCS 1633, pages 249–260. Springer, 1999.
[18] M. De Wulf, L. Doyen, T. Henzinger, and J.-F. Raskin. Antichains: A new algorithm for checking universality of finite automata. In CAV, LNCS 4144, pages 17–30. Springer, 2006.
[19] V. Diekert and P. Gastin. First-order definable languages. In Logic and Automata: History and Perspective, TLG 2, pages 261–306. Amsterdam University Press, 2008.
[20] L. Doyen and J.-F. Raskin. Improved algorithms for the automata-based approach to model-checking. In TACAS 2007, LNCS 4424, pages 451–465. Springer, 2007.
[21] L. Doyen and J.-F. Raskin. Antichains for the automata-based approach to model-checking. LMCS, 5(1:5):1–20, 2009.
[22] M. Dwyer, G. Avrunin, and J. Corbett. Patterns in property specifications for finite-state verification. In ICSE 1999, pages 411–420. ACM, 1999.
[23] K. Etessami and G. Holzmann. Optimizing Buchi automata. In CONCUR 2000, LNCS 1877, pages 153–167. Springer, 2000.
[24] K. Etessami, T. Wilke, and R. A. Schuller. Fair simulation relations, parity games, and state space reduction for Buchi automata. In ICALP 2011, LNCS 2076, pages 694–707. Springer, 2001.
[25] S. Fogarty and M. Vardi. Buchi complementation and size-change termination. In TACAS 2009, LNCS 5505, pages 16–30. Springer, 2009.
[26] S. Fogarty and M. Vardi. Efficient Buchi universality checking. In TACAS 2010, LNCS 6015, pages 205–220. Springer, 2010.
[27] E. Friedgut, O. Kupferman, and M. Y. Vardi. Buchi complementation made tighter. IJFCS, 17(4):851–868, 2006.
[28] O. Friedmann and M. Lange. Solving parity games in practice. In ATVA 2009, LNCS 5799, pages 182–196. Springer, 2009.
[29] D. Gabbay. The declarative past and imperative future: Executable temporal logic for interactive systems. In TLS 1987, LNCS 398, pages 409–448. Springer, 1987.
[30] D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. In POPL 1980, pages 163–173. ACM Press, 1980.
[31] P. Gastin and D. Oddoux. LTL2BA: fast translation from LTL formulae to Buchi automata. http:// www.lsv.ens-cachan.fr/~gastin/
[32] P. Gastin and D. Oddoux. Fast LTL to Buchi automata translation. In CAV 2001, LNCS 2102, pages 53–65. Springer, 2001.
[33] P. Gastin and D. Oddoux. LTL with past and two-way very-weak alternating automata. In MFCS 2003, LNCS 2747, pages 439–448. Springer, 2003.
[34] R. Gerth, D. Peled, M. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In PSTV, pages 3–18. Chapman & Hall, 1995.
[35] D. Giannakopoulou and F. Lerda. From states to transitions: Improving translation of LTL formulae to Buchi automata. In FORTE 2002, LNCS 2529, pages 308–326. Springer, 2002.
[36] E. Gr ̈adel, W. Thomas, and T. Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001], LNCS 2500. Springer, 2002.
[37] O. Grumberg and D. Long. Model checking and modular verification. TOPLAS, 16(3):843–871, 1994.
[38] S. Gurumurthy, R. Bloem, and F. Somenzi. Fair simulation minimization. In CAV 2002, LNCS 2404, pages 610–624. Springer, 2002.
[39] S. Gurumurthy, O. Kupferman, F. Somenzi, and M. Vardi. On complementing nondeterministic Buchi automata. In CHARME 2003, LNCS 2860, pages 96– 110. Springer, 2003.
[40] M. Hammer, A. Knapp, and S. Merz. Truly on-the-fly LTL model checking. In TACAS 2005, LNCS 3440, pages 191–205, 2005.
[41] M. Henzinger, T. Henzinger, and P. Kopke. Computing simulations on finite and infinite graphs. In FOCS 1995, pages 453–462. IEEE Computer Society, 1995.
[42] G. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2003.
[43] Java Plugin Framework. http://jpf.sourceforge.net.
[44] D. Johnson. Finding all the elementary circuits of a directed graph. SICOMP, 4(1):77–84, 1975.
[45] M. Jurdzin ́ski. Small progress measures for solving parity games. In STACS 2000, LNCS 1770, pages 290–301. Springer, 2000.
[46] M. Jurdzin ́ski, M. Paterson, and U. Zwick. A deterministic subexponential algorithm for solving parity games. SICOMP, 38(4):1519–1532, 2008.
[47] D. K ̈ahler and T. Wilke. Complementation, disambiguation, and determinization of Buchi automata unified. In ICALP 2008, LNCS 5125, pages 724–735. Springer, 2008.
[48] H. Karmarkar and S. Chakraborty. On minimal odd rankings for Buchi complementation. In ATVA 2009, LNCS 5799, pages 228–243. Springer, 2009.
[49] Y. Kesten, Z. Manna, H. McGuire, and A. Pnueli. A decision algorithm for full propositional temporal logic. In CAV 1993, LNCS 697, pages 97–109. Springer, 1993.
[50] Y. Kesten and A. Pnueli. Verification by augmented finitary abstraction. Information and Computation, 163(1):203–243, 2000.
[51] Y. Kesten and A. Pnueli. Complete proof system for QPTL. IJLP, 12(5):701– 745, 2002.
[52] Y. Kesten, A. Pnueli, and L. Raviv. Algorithmic verification of linear temporal logic specifications. In ICALP 1998, LNCS 1443, pages 1–16. Springer, 1998.
[53] V. King, O. Kupferman, and M. Vardi. On the complexity of parity word automata. In FoSSaCS 2001, LNCS 2030, pages 276–286. Springer, 2001.
[54] N. Klarlund. Progress measures for complementation of ω-automata with applications to temporal logic. In FOCS 1991, pages 358–367. IEEE, 1991.
[55] J. Klein and C. Baier. Experiments with deterministic ω-automata for formulas of linear temporal logic. TCS, 363(2):182–195, 2006.
[56] T. Klotz, N. Sesler, B. Straube, and E. Fordran. Compositional verification of material handling systems. In ETFA 2012, pages 1–8. IEEE, 2012.
[57] O. Kupferman and M. Vardi. Weak alternating automata are not that weak. TOCL, 2(3):408–429, 2001.
[58] O. Kupferman and M. Vardi. Safraless decision procedures. In FOCS 2005, pages 531–540. IEEE Computer Society, 2005.
[59] R. Kurshan. Complementing deterministic Buchi automata in polynomial time. JCSS, 35(1):59–71, 1987.
[60] R. Ku ̈sters. Memoryless determinacy of parity games. In Automata, Logics, and Infinite Games, LNCS 2500, pages 95–106. Springer, 2001.
[61] L. H. Landweber. Decision problems for ω-automata. MST, 3(4):376–384, 1969.
[62] F. Laroussinie, N. Markey, and P. Schnoebelen. Temporal logic with forgettable past. In LICS 2002, pages 383–392. IEEE, 2002.
[63] T. Latvala, A. Biere, K. Heljanko, and T. A. Junttila. Simple is better: Efficient bounded model checking for past LTL. In VMCAI 2005, LNCS 3385, pages 380–395. Springer, 2005.
[64] O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In Logic of Programs, LNCS 193, pages 196–218. Springer, 1985.
[65] Z. Manna and A. Pnueli. A hierarchy of temporal properties. In PODC 1990, pages 377–410. ACM, 1990.
[66] Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer, 1995.
[67] R. Mazala. Infinite games. In Automata, Logics, and Infinite Games, LNCS 2500, pages 23–42. Springer, 2001.
[68] R. McNaughton. Infinite games played on finite graphs. APAL, 65(2):149–184, 1993.
[69] M. Michel. Complementation is more difficult with automata on infinite words. In CNET, 1988.
[70] D. Muller and P. Schupp. Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra. TCS, 141(1&2):69–107, 1995.
[71] K. Namjoshi and R. Trefler. On the completeness of compositional reasoning. In CAV 2000, LNCS 1855, pages 139–153. Springer, 2000.
[72] H. Peng, Y. Mokhtari, and S. Tahar. Environment synthesis for compositional model checking. In ICCD 2002, pages 70–75. IEEE, 2002.
[73] PHP/Java Bridge. http://php-java-bridge. sourceforge.net/.
[74] N. Piterman. From nondeterministic Buchi and Streett automata to deterministic parity automata. LMCS, 3(3), 2007.
[75] M. Rabin and D. Scott. Finite automata and their decision problems. IBM JRD, 3:115–125, 1959.
[76] S. Rodger and T. Finley. JFLAP. http://www.jflap.org/. 137
[77] S. Safra. On the complexity of ω-automata. In FOCS 1988, pages 319–327. IEEE, 1988.
[78] S. Schewe. Solving parity games in big steps. In FSTTCS 2007, LNCS 4855, pages 449–460. Springer, 2007.
[79] S. Schewe. Buchi complementation made tight. In STACS 2009, LIPIcs 3, pages 661–672. Schloss Dagstuhl Leibniz-Zentrum fuer Informatik, 2009.
[80] S. Schewe. Tighter bounds for the determinisation of Buchi automata. In FOSSACS 2009, LNCS 5504, pages 167–181. Springer, 2009.
[81] R. Sebastiani and S. Tonetta. “More deterministic” vs. “smaller” Buchi automata for efficient LTL model checking. In CHARME 2003, LNCS 2860, pages 126–140. Springer, 2003.
[82] A. Sistla. Theoretical Issues in the Design and Verification of Distributed Systems. PhD thesis, Harvard, 1983.
[83] A. Sistla, M. Vardi, and P. Wolper. The complementation problem for Buchi automata with applications to temporal logic. TCS, 49:217–237, 1987.
[84] S. Sohail and F. Somenzi. Safety first: A two-stage algorithm for LTL games. In FMCAD 2009, pages 77–84. IEEE, 2009.
[85] S. Sohail, F. Somenzi, and K. Ravi. A hybrid algorithm for LTL games. In VMCAI 2008, LNCS 4905, pages 309–323. Springer, 2008.
[86] F. Somenzi and R. Bloem. Efficient Buchi automata from LTL formulae. In CAV 2000, LNCS 1855, pages 248–263. Springer, 2000.
[87] The Spec Patterns repository. http://patterns.projects.cis.ksu.edu/.
[88] H. Tauriainen and K. Heljanko. Testing LTL formula translation into Buchi automata. STTT, 4(1):57–70, 2002.
[89] W. Thomas. Complementation of Buchi automata revisited. In Jewels are Forever, pages 109–120. Springer, 1999.
[90] Tomcat. http://tomcat.apache.org/.
[91] M.-H. Tsai, S. Fogarty, M. Vardi, and Y.-K. Tsay. State of Buchi complementation. In CIAA 2010, LNCS 6482, pages 261–271. Springer, 2010.
[92] M.-H. Tsai, Y.-K. Tsay, and Y.-S. Hwang. GOAL for games, omega-automata, and logics. In CAV 2013, LNCS 8044. Springer, 2013.
[93] Y.-K. Tsay. Compositional verification in linear-time temporal logic. In FoSSaCS 2000, LNCS 1784, pages 344–358. Springer, 2000.
[94] Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, W.-C. Chan, and C.-J. Luo. GOAL extended: Towards a research tool for omega automata and temporal logic. In TACAS 2008, LNCS 4963, pages 346–350, 2008.
[95] Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, K.-N. Wu, and W.-C. Chan. GOAL: A graphical tool for manipulating Buchi automata and temporal formulae. In TACAS 2007, LNCS 4424, pages 466–471, 2007.
[96] Y.-K. Tsay, M.-H. Tsai, J.-S. Chang, and Y.-W. Chang. Buchi Store: An open repository of Buchi automata. In TACAS 2011, LNCS 6605, pages 262–266. Springer, 2011.
[97] Y.-K. Tsay, M.-H. Tsai, J.-S. Chang, Y.-W. Chang, and C.-S. Liu. Buchi Store: An open repository of ω-automata. STTT, 15(2):109–123, 2013.
[98] M. Vardi. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency: Structure versus Automata, LNCS 1043, pages 238–266. Springer, 1996.
[99] M. Vardi. Automata-theoretic model checking revisited. In VMCAI 2007, LNCS 4349, pages 137–150. Springer, 2007.
[100] M. Vardi. The Buchi complementation saga. In STACS 2007, LNCS 4393, pages 12–22. Springer, 2007.
[101] M. Vardi and T. Wilke. Automata: from logics to algorithms. In Logic and Automata: History and Perspective, TLG 2, pages 629–736. Amsterdam University Press, 2007.
[102] M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In LICS 1986, pages 322–331, Cambridge, 1986.
[103] Q. Yan. Lower bounds for complementation of omega-automata via the full automata technique. LMCS, 4(1), 2008.
[104] W. Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. TCS, 200(1-2):135–183, 1998.

QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top
系統版面圖檔 系統版面圖檔