請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/79440完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 蔡益坤(Yih-Kuen Tsay) | |
| dc.contributor.author | Shou-Yu Tseng | en |
| dc.contributor.author | 曾守瑜 | zh_TW |
| dc.date.accessioned | 2022-11-23T09:00:31Z | - |
| dc.date.available | 2022-03-07 | |
| dc.date.available | 2022-11-23T09:00:31Z | - |
| dc.date.copyright | 2022-03-07 | |
| dc.date.issued | 2022 | |
| dc.date.submitted | 2022-02-15 | |
| dc.identifier.citation | IEEE Standard for Property Specification Language (PSL). IEEE Std 1850™-2010, 2010. A. Aziz, V. Singhal, G.M. Swamy, and Robert K. Brayton. Minimizing interacting finite state machines. Technical Report UCB/ERL M93/68, EECS Department, University of California, Berkeley, Sep 1993. Tomáš Babiak, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Křetínský, David Müller, David Parker, and Jan Strejček. The Hanoi omegaautomata format. In Daniel Kroening and Corina S. Păsăreanu, editors, Computer Aided Verification, volume 9206 of Lecture Notes in Computer Science, pages 479–486, Cham, 2015. Springer International Publishing. Tomáš Babiak, Mojmír Křetínský, Vojtěch Řehák, and Jan Strejček. LTL to Büchi automata translation: Fast and more deterministic. In Cormac Flanagan and Barbara König, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 7214 of Lecture Notes in Computer Science, pages 95–109, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. Supplementary materials for simulation subsumption in Ramsey-based Büchi automata universality and inclusion testing. http://www.languageinclusion.org/CAV2010/. R. Bloem, A. Cimatti, I. Pill, M. Roveri, and S. Semprini. Symbolic implementation of alternating automata. In Oscar H. Ibarra and Hsu-Chun Yen, editors, Implementation and Application of Automata, volume 4094 of Lecture Notes in Computer Science, pages 208–218, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. U. Boker and O. Kupferman. Co-ing Büchi made tight and useful. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science (LICS ’09), pages 245–254. IEEE Computer Society, 2009. Janusz A. Brzozowski and Ernst Leiss. On equations for regular languages, finite automata, and sequential networks. Theoretical Computer Science, 10(1):19–35, 1980. J.R. Büchi. On a decision method in restricted second-order arithmetic. In Proceedings of the 1960 International Congress on Logic, Methodology and Philosophy of Science, pages 1–11, 1962. J. R. Burch, E. M. Clarke, and K.L. McMillan. Symbolic model checking: 1020 states and beyond. In Proceedings of the 5th IEEE Symposium on Logic in Computer Science, pages 428–439, June 1990. Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer. Alternation. J. ACM, 28(1):114–133, Jan 1981. T.-C. Chang. Translation of PSL formulae for automata-based verification. Master’s thesis, Department of Information Management, National Taiwan University, January 2020. A. Cimatti, E.M. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: A new symbolic model checker. International Journal on Software Tools for Technology Transfer, 2(4):410–425, 2000. Alessandro Cimatti, Edmund Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. NuSMV 2: An opensource tool for symbolic model checking. In International Conference on Computer Aided Verification, volume 2404 of Lecture Notes in Computer Science, pages 359–364. Springer, 2002. E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, 1999. Christian Dax, Felix Klaedtke, and Martin Lange. On regular temporal logics with past. Acta informatica, 47(4):251–277, 2010. Giuseppe De Giacomo and Moshe Y. Vardi. Linear temporal logic and linear dynamic logic on finite traces. In Twenty-Third International Joint Conference on Artificial Intelligence, 2013. M. De Wulf, L. Doyen, N. Maquet, and J. F. Raskin. Antichains: Alternative algorithms for LTL satisfiability and model-checking. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 4963 of Lecture Notes in Computer Science, pages 63–77, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. Martin De Wulf, Laurent Doyen, Thomas A Henzinger, and J-F Raskin. Antichains: A new algorithm for checking universality of finite automata. In International Conference on Computer Aided Verification, volume 4144 of Lecture Notes in Computer Science, pages 17–30. Springer, 2006. Laurent Doyen and Jean-François Raskin. Antichains for the automata-based approach to model-checking. Log. Methods Comput. Sci., 5(1), 2009. A. Duret-Lutz and D. Poitrenaud. SPOT: An extensible model checking library using transition-based generalized Büchi automata. In Proceedings of the 12th Annual International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems (MASCOTS ’04), pages 76–83. IEEE Computer Society, 2004. Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, and Laurent Xu. SPOT 2.0 — a framework for LTL and ωautomata manipulation. In Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA’16), volume 9938 of Lecture Notes in Computer Science, pages 122–129. Springer, October 2016. K. Etessami and G.J. Holzmann. Optimizing Büchi automata. In Proceedings of the 11th International Conference on Concurrency Theory (CONCUR ’00), LNCS 1877, pages 153–167. pringer-Verlag, 2000. Peter Faymonville and Martin Zimmermann. Parametric linear dynamic logic. Information and Computation, 253:237–256, 2017. GandALF 2014. Carsten Fritz and Thomas Wilke. Simulation relations for alternating Büchi automata. Theoretical Computer Science, 338(1):275 – 314, 2005. P. Gastin and D. Oddoux. LTL2BA: fast translation from LTL formulae to Büchi automata. http:// www.lsv.ens-cachan.fr/~gastin/ltl2ba/index.php. P. Gastin and D. Oddoux. Fast LTL to Büchi automata translation. In Proceedings of the 13th International Conference on Computer Aided Verification (CAV ’01), LNCS 2102, volume 2102 of Lecture Notes in Computer Science, pages 53–65. Springer, 2001. Paul Gastin and Denis Oddoux. LTL with past and two-way very-weak alternating automata. In International Symposium on Mathematical Foundations of Computer Science, volume 2747 of Lecture Notes in Computer Science, pages 439–448. Springer, 2003. Sankar Gurumurthy, Orna Kupferman, Fabio Somenzi, and Moshe Y. Vardi. On complementing nondeterministic Büchi automata. In Daniel Geist and Enrico Tronci, editors, Correct Hardware Design and Verification Methods, volume 2860 of Lecture Notes in Computer Science, pages 96–110, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg. The Hanoi omega-automata format. https://github.com/adl/hoaf. G. J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5), 1997. G.J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. AddisonWesley, 2003. O. Kupferman and M.Y. Vardi. An automata-theoretic approach to modular model checking. ACM Transactions on Programming Languages and Systems, 22(1):87–128, January 2000. O. Kupferman and M.Y. Vardi. Weak alternating automata are not that weak. ACM Transactions on Computational Logic, 2(3):408–429, 2001. Orna Kupferman. Automata Theory and Model Checking, pages 107–151. Springer International Publishing, Cham, 2018. L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, 3(2), 1977. Z. Manna and A. Pnueli. A hierarchy of temporal properties. In Proceedings of the 9th ACM Symposium on Principles of Distributed Computing (PODC ’90), pages 377–408. ACM, 1990. Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995. Kenneth L. McMillan. The SMV system. In Symbolic Model Checking, pages 61–85. Springer, 1993. Satoru Miyano and Takeshi Hayashi. Alternating finite automata on ω-words. Theoretical Computer Science, 32(3):321–330, 1984. David E. Muller, Ahmed Saoudi, and Paul E. Schupp. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In Proceedings Third Annual Symposium on Logic in Computer Science, pages 422–423. IEEE Computer Society, 1988. David E. Muller and Paul E. Schupp. Alternating automata on infinite trees. Theoretical Computer Science, 54(2):267–276, 1987. David E. Muller and Paul E. Schupp. Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra. Theoretical Computer Science, 141(1-2):69–107, 1995. D.E. Muller. Infinite sequences and finite machines. In Proceedings of the 4th Annual IEEE Symposium on Foundations of Computer Science (FOCS 1963), pages 3–16, 1963. N. Piterman. From nondeterministic Büchi and Streett automata to deterministic parity automata. In Proceedings of the 21th Annual IEEE Symposium on Logic in Computer Science (LICS ’06), pages 255–264. IEEE, 2006. A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13:45–60, 1981. S. Safra. On the complexity of ω-automta. In Proceedings of the 29th Annual IEEE Symposium on Foundations of Computer Science (FOCS ’88), pages 319–327. IEEE, 1988. Sven Schewe. Tighter bounds for the determinisation of Büchi automata. In International Conference on Foundations of Software Science and Computational Structures, volume 5504 of Lecture Notes in Computer Science, pages 167–181. Springer, 2009. Salomon Sickert. A Unified Translation of Linear Temporal Logic to ω-Automata. Dissertation, Technische Universität München, München, 2019. A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science, 49:217–237, 1987. W. Thomas. Complementation of Büchi automata revisited. In Jewels are Forever, Contributions on Theoretical Computer Science in Honor of Arto Salomaa, pages 109–120. Springer, 1999. M.-H. Tsai, S. Fogarty, M.Y. Vardi, and Y.-K. Tsay. State of Büchi complementation. In Proceedings of the 15th International Conference on Implementation and Application of Automata (CIAA ’10), LNCS 6482, pages 261–271. Springer, 2011. M.-H. Tsai, Y.-K. Tsay, and Y.-S. Hwang. GOAL for games, omega-automata, and logics. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV ’13), LNCS 8044. Springer, 2013. To appear. 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 Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS ’08), LNCS 4963, pages 346–350. Springer, 2008. Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, K.-N. Wu, and W.-C. Chan. GOAL: A graphical tool for manipulating Büchi automata and temporal formulae. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS ’07), LNCS 4424, pages 466–471. Springer, March 2007. Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, K.-N. Wu, W.-C. Chan, C.-J. Luo, and J.-S. Chang. Tool support for learning Büchi automata and linear temporal logic. Formal Aspects of Computing, 21(3):259–275, 2009. Arash Vahidi. JDD-a pure Java BDD and Z-BDD library, 2004. Moshe Y. Vardi. Nontraditional applications of automata theory. In International Symposium on Theoretical Aspects of Computer Software, volume 789 of Lecture Notes in Computer Science, pages 575–597. Springer, 1994. | |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/79440 | - |
| dc.description.abstract | 「交替」是非確定性的一種延伸，賦予了自動機更便利的狀態接合表達能力。儘管交替式自動機與非確定性自動機一樣，表述力侷限在ω正規語言，但善用交替的性質，我們能以更少的狀態建構出表達語言交集與聯集的自動機。將狀態接合的能力應用在邏輯接合，以時序邏輯表述的命題可更容易地轉譯成交替式自動機。然而，若是要將交替式自動機轉換成非確定性自動機，去除交替性將使狀態數量產生指數性成長。研究已經顯示我們可以直接檢查交替式自動機辨識的語言是否為空，而不需要事先去除自動機的交替性。因此，我們可以同時利用交替式自動機在大小與建置難易度方面的優點，並且在不犧牲空間與時間的前提下進行模型檢查。 這篇論文闡述我們對可操作ω自動機與時序邏輯公式的圖像化工具GOAL進行的擴充。GOAL已經實作了交替式自動機，不過支援交替式自動機的函式仍舊有限。我們針對交替式自動機的擴充將包含空集問題與宇集問題的檢查、建構Büchi與co-Büchi自動機的補集、以及從LTL與LDL公式轉譯至交替式自動機的演算法。我們亦實作了以反鏈為基礎的非確定性自動機的宇集問題檢查。我們還將GOAL表述自動機初始狀態的能力擴充到可以支援多個起始狀態，這將讓我們更方便呈現語言的聯集，而此擴充也已經植入GOAL既有的演算法。最後，我們引入符號型交替式自動機，以便使用者更方便地建構出定點運算以檢查時序邏輯公式的滿足性。 | zh_TW |
| dc.description.provenance | Made available in DSpace on 2022-11-23T09:00:31Z (GMT). No. of bitstreams: 1 U0001-1002202201323300.pdf: 2463522 bytes, checksum: 0003663e7b1b4147aa9cc5c7c91131a6 (MD5) Previous issue date: 2022 | en |
| dc.description.tableofcontents | 摘要 ii THESIS ABSTRACT iii 1 Introduction 1 1.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Motivation and Objectives . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.3 Thesis Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2 Preliminaries 3 2.1 Pre-automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.1.1 Nondeterministic Pre-automaton . . . . . . . . . . . . . . . . . . 3 2.1.2 Alternating Pre-automaton . . . . . . . . . . . . . . . . . . . . . 4 2.1.3 Symbolic Pre-automaton . . . . . . . . . . . . . . . . . . . . . . . 5 2.2 Accepting Conditions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.2.1 Conditions on Finite Words . . . . . . . . . . . . . . . . . . . . . 6 2.2.2 Conditions on Infinite Words . . . . . . . . . . . . . . . . . . . . . 7 2.3 ω-Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.3.1 Nondeterministic Büchi Automata (NBW) . . . . . . . . . . . . . 9 2.3.2 Alternating Büchi Automata (ABW) . . . . . . . . . . . . . . . . 10 2.3.3 Complement of Büchi Automata . . . . . . . . . . . . . . . . . . . 11 2.3.4 Removal of Alternation . . . . . . . . . . . . . . . . . . . . . . . . 11 2.3.5 Symbolic Automata . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.4 Propositional Linear Temporal Logic (PTL) . . . . . . . . . . . . . . . . 13 2.4.1 State Formulae . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.4.2 Booolean Operators . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.4.3 Future Operators . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.5 Linear Dynamic Logic (LDL) . . . . . . . . . . . . . . . . . . . . . . . . 15 2.5.1 Regular Expressions for Sequences . . . . . . . . . . . . . . . . . 15 2.5.2 Temporal Operators Added in LDL . . . . . . . . . . . . . . . . . 16 2.6 Property Specification Language (PSL) . . . . . . . . . . . . . . . . . . . 16 2.6.1 Sequential Extended Regular Expressions (SEREs) . . . . . . . . 16 2.6.2 Sequential Expressions . . . . . . . . . . . . . . . . . . . . . . . . 18 3 Related Works 19 3.1 Classification of Properties . . . . . . . . . . . . . . . . . . . . . . . . . . 19 3.2 Simulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3.3 Tools and Algorithms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3.3.1 LTL2BA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3.3.2 LTL3BA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3.3.3 PSL2BA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 3.3.4 PLDL Translation . . . . . . . . . . . . . . . . . . . . . . . . . . 21 3.3.5 Translation from PSL into NGBW . . . . . . . . . . . . . . . . . 21 3.3.6 HOA Format . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 3.3.7 Spot . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 3.3.8 SPIN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 3.3.9 NuSMV . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 3.3.10 GOAL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 4 Implemented Methods 25 4.1 Extensions for Alternating Automata . . . . . . . . . . . . . . . . . . . . 25 4.1.1 ABW Emptiness Check . . . . . . . . . . . . . . . . . . . . . . . . 25 4.1.2 Universality Problem for NFA and NBW . . . . . . . . . . . . . . 25 4.1.3 ABW Universality Check . . . . . . . . . . . . . . . . . . . . . . . 25 4.1.4 Complementation of ABW and ACW . . . . . . . . . . . . . . . . 26 4.1.5 Direct Input Test for AFA and Weak ABW . . . . . . . . . . . . 26 4.1.6 Random Generator for One-Way Alternating Automata . . . . . . 27 4.1.7 Alternating Transitions to the Empty Set . . . . . . . . . . . . . . 28 4.2 Support of Multiple Initial States . . . . . . . . . . . . . . . . . . . . . . 29 4.3 Translation from PSL/LDL to ABW . . . . . . . . . . . . . . . . . . . . 30 4.3.1 With Queries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 4.3.2 Without Queries . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 4.4 Symbolic Representation . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 4.4.1 Symbolic Automata . . . . . . . . . . . . . . . . . . . . . . . . . . 33 4.4.2 Symbolic Boolean Expression . . . . . . . . . . . . . . . . . . . . 35 4.4.3 BDD for Symbolic Transitions of Automata . . . . . . . . . . . . 35 5 Experimental Results 36 5.1 GUI Changes and New Functions . . . . . . . . . . . . . . . . . . . . . . 36 5.1.1 Multiple Initial States . . . . . . . . . . . . . . . . . . . . . . . . 36 5.1.2 Empty Nodes of Alternating Automata . . . . . . . . . . . . . . . 38 5.1.3 Complement Alternating Automata . . . . . . . . . . . . . . . . . 40 5.2 Symbolic Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 5.3 Emptiness and Universality . . . . . . . . . . . . . . . . . . . . . . . . . 42 5.3.1 Emptiness for ABW . . . . . . . . . . . . . . . . . . . . . . . . . 42 5.3.2 Universality for NBW . . . . . . . . . . . . . . . . . . . . . . . . 44 5.4 Translation from LTL via Very Weak SABW . . . . . . . . . . . . . . . . 47 5.5 Translation from PSL/LDL via Weak ABW . . . . . . . . . . . . . . . . 47 6 Conclusion 52 6.1 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 6.2 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 References 54 | |
| dc.language.iso | en | |
| dc.title | GOAL針對交替式自動機與時序邏輯翻譯的支援 | zh_TW |
| dc.title | Support for Alternating Automata and Temporal Formula Translation in GOAL | en |
| dc.date.schoolyear | 110-1 | |
| dc.description.degree | 碩士 | |
| dc.contributor.advisor-orcid | 蔡益坤(0000-0002-5960-1615) | |
| dc.contributor.oralexamcommittee | 陳郁方(Chi-Sheng Shih),郁方(Cheng-Wei Chen),(Feng-Li Lian),(Yung-jen Hsu) | |
| dc.subject.keyword | 交替式自動機,Büchi自動機,GOAL,LDL,LTL,模型檢查,時序邏輯,公式轉譯, | zh_TW |
| dc.subject.keyword | Alternating Automata,Büchi Automata,GOAL,LDL,LTL,Model Checking,Temporal Logic,Translation, | en |
| dc.relation.page | 59 | |
| dc.identifier.doi | 10.6342/NTU202200497 | |
| dc.rights.note | 同意授權(全球公開) | |
| dc.date.accepted | 2022-02-15 | |
| dc.contributor.author-college | 管理學院 | zh_TW |
| dc.contributor.author-dept | 資訊管理學研究所 | zh_TW |
| 顯示於系所單位： | 資訊管理學系 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| U0001-1002202201323300.pdf | 2.41 MB | Adobe PDF | 檢視/開啟 |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。