請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/22630完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 王凡(Farn Wang) | |
| dc.contributor.author | Hsi-Ming Ho | en |
| dc.contributor.author | 何熙明 | zh_TW |
| dc.date.accessioned | 2021-06-08T04:22:51Z | - |
| dc.date.copyright | 2010-07-02 | |
| dc.date.issued | 2010 | |
| dc.date.submitted | 2010-06-30 | |
| dc.identifier.citation | [1] M. Abadi, L. Lamport, and P. Wolper. Realizable and unrealizable speci-ca- tions of reactive systems. In Ausiello et al. [6], pages 1-17.
[2] R. Alur, C. Courcoubetis, and D. L. Dill. Model checking for real-time systems. In IEEE LICS, 1990. [3] R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183-235, 1994. [4] R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672-713, 2002. [5] R. Alur, T. A. Henzinger, F. Y. C. Mang, S. Qadeer, S. K. Rajamani, and S. Tasiran. Mocha: Modularity in model checking. In A. J. Hu and M. Y. Vardi, editors, CAV, volume 1427 of Lecture Notes in Computer Science, pages 521-525. Springer, 1998. [6] G. Ausiello, M. Dezani-Ciancaglini, and S. R. D. Rocca, editors. Automata, Languages and Programming, 16th International Colloquium, ICALP89, Stresa, Italy, July 11-15, 1989, Proceedings, volume 372 of Lecture Notes in Computer Science. Springer, 1989. [7] P.-J. Courtois, F. Heymans, and D. L. Parnas. Concurrent control with 'read- ers' and 'writers'. Commun. ACM, 14(10):667-668, 1971. [8] L. de Alfaro, T. A. Henzinger, and O. Kupferman. Concurrent reachability games. Theor. Comput. Sci., 386(3):188-217, 2007. [9] J. Dick and A. Faivre. Automating the generation and sequencing of test cases from model-based speci-cations. In J. Woodcock and P. G. Larsen, edi- tors, FME, volume 670 of Lecture Notes in Computer Science, pages 268-284. Springer, 1993. [10] E. W. Dijkstra. Hierarchical ordering of sequential processes. Acta Inf., 1:115- 138, 1971. [11] E. W. Dijkstra. Cooperating sequential processes. In P. B. Hansen, editor, The origin of concurrent programming: from semaphores to remote procedure calls, pages 65-138. Springer-Verlag New York, Inc., New York, NY, USA, 2002. [12] E. A. Emerson and C. S. Jutla. The complexity of tree automata and logics of programs (extended abstract). In FOCS, pages 328-337. IEEE, 1988. [13] M. Helmert, R. Mattmuller, and S. Schewe. Selective approaches for solving weak games. In S. Graf and W. Zhang, editors, ATVA, volume 4218 of Lecture Notes in Computer Science, pages 200-214. Springer, 2006. [14] G. ITU-T. Recommendation z. 120: Message sequence chart (msc). See also: http://www. win. tue. nl/win/cs/fm/sjouke/msc. html, 1993. [15] W. Jamroga. Strategic planning through model checking of atl formulae. In L. Rutkowski, J. H. Siekmann, R. Tadeusiewicz, and L. A. Zadeh, editors, ICAISC, volume 3070 of Lecture Notes in Computer Science, pages 879-884. Springer, 2004. [16] W. Jamroga. Easy yet hard: Model checking strategies of agents. In M. Fisher, F. Sadri, and M. Thielscher, editors, CLIMA IX, volume 5405 of Lecture Notes in Computer Science, pages 1-12. Springer, 2008. [17] W. Jamroga and J. Dix. Do agents make model checking explode (computa- tionally)- In M. Pechoucek, P. Petta, and L. Z. Varga, editors, CEEMAS, volume 3690 of Lecture Notes in Computer Science, pages 398-407. Springer, 2005. [18] W. Jamroga and J. Dix. Model checking abilities of agents: A closer look. Theory Comput. Syst., 42(3):366-410, 2008. [19] O. Kupferman and M. Y. Vardi. Module checking. In R. Alur and T. A. Henzinger, editors, CAV, volume 1102 of Lecture Notes in Computer Science, pages 75-86. Springer, 1996. [20] A. Lomuscio, H. Qu, and F. Raimondi. Mcmas: A model checker for the veri-cation of multi-agent systems. In A. Bouajjani and O. Maler, editors, CAV, volume 5643 of Lecture Notes in Computer Science, pages 682-688. Springer, 2009. [21] R. Mazala. In-nite games. In E. Gradel, W. Thomas, and T. Wilke, edi- tors, Automata, Logics, and In-nite Games, volume 2500 of Lecture Notes in Computer Science, pages 23-42. Springer, 2001. [22] H. Pennington. GTK+/Gnome Application Development. New Riders Publish- ing Thousand Oaks, CA, USA, 1999. [23] A. Pnueli. The temporal logic of programs. In FOCS, pages 46-57. IEEE, 1977. [24] A. Pnueli and R. Rosner. On the synthesis of a reactive module. In POPL, pages 179-190, 1989. [25] A. Pnueli and R. Rosner. On the synthesis of an asynchronous reactive module. In Ausiello et al. [6], pages 652-671. [26] P. Ramadge and W. Wonham. The control of discrete event systems. Proceed- ings of the IEEE, 77(1):81-98, 1989. [27] P. Schobbens. Alternating-time logic with imperfect recall. Electronic Notes in Theoretical Computer Science, 85(2):82-93, 2004. 38 [28] E. Standard. 201 873 V3. 2.1: The Testing and Test Control Notation version 3; Parts 1-8. European Telecommunications Standards Institute (ETSI), Sophia- Antipolis, France, also published as ITU-T Recommendation series, 140, 2007. [29] W. van der Hoek, A. Lomuscio, and M. Wooldridge. On the complexity of practical atl model checking. In H. Nakashima, M. P. Wellman, G. Weiss, and P. Stone, editors, AAMAS, pages 201-208. ACM, 2006. [30] F.Wang. Efficient veri-cation of timed automata with bdd-like data-structures. STTT (Software Tools for Technology Transfer), 6(1), 2004. special issue for the 4th VMCAI, Jan. 2003, LNCS 2575, Springer-Verlag. [31] F. Wang. Model-checking distributed real-time systems with states, events, and multiple fairness assumptions. In AMAST, volume LNCS 3116. Springer- Verlag, 2004. [32] F. Wang. Symbolic parametric safety analysis of linear hybrid systems with bdd-like data-structures. IEEE Transactions on Software Engineering, 31(1):38-51, 2005. A preliminary version is in proceedings of 16th CAV, 2004, LNCS 3114, Springer-Verlag. [33] F. Wang. Symbolic veri-cation of distributed real-time systems with complex synchronizations. In 7th ICFEM, volume LNCS 3785. Springer-Verlag, Novem- ber 2005. [34] J. Wu, C.-J. Wang, L. Zhang, and J. Xie. Coalitional planning in game-like domains via atl model checking. In ICTAI, pages 645-652. IEEE Computer Society, 2009. | |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/22630 | - |
| dc.description.abstract | 嵌入式系統常需要與不可預知的環境互動。對此類系統進行驗證時，交互時態邏輯模型檢驗可用來檢查是否無論環境行為如何，都能確保某些性質的成立。在此論文中，我們提出一個可以運用在開放式系統驗證上的即時正向策略建立演算法。在我們的實驗架構中，開放式系統會被對應到多人賽局。我們再利用ATL的一個子集（稱為EFATL）中之邏輯公式來描述想要驗證的性質。如果模型中存在簡短的策略可使性質成立，我們的演算法可有效率地建立出一個策略。我們亦描述一個簡單的heuristics來展現我們演算法之發展性。最後我們利用REDLIB來實作一套完整的模型檢驗器，並與一套類似的工具比較效能。 | zh_TW |
| dc.description.abstract | Embedded systems often have to interact with an environment with unpredictable behaviors. To verify such embedded systems, ATL (Alternating-Time Temporal Logic) model-checking can be used to check whether certain properties hold regardless how the environment may behave. In this thesis, we present a new on-the-fly forward reasoning strategy construction algorithm that can be used for the verification of open systems. In our framework, an open system is modeled as a multi-agent game. We then use formulas in a subclass of ATL, called EFATL, to describe the speci-fication properties we want to check. Our algorithms have the advantage to efficiently construct of a strategy when there exists compact strategies. We also investigate a simple heuristics of forward exploration to show the potential of our approach. Finally, we implement our techniques on top of REDLIB and compare the performance of our tool with another model checker. | en |
| dc.description.provenance | Made available in DSpace on 2021-06-08T04:22:51Z (GMT). No. of bitstreams: 1 ntu-99-R96921029-1.pdf: 2438690 bytes, checksum: 77bf63c127a98531d4fdad8eb9da0a3e (MD5) Previous issue date: 2010 | en |
| dc.description.tableofcontents | Contents i
List of Figures iii List of Tables iv Acknowledgements v 1 Introduction 1 2 Related Work 5 3 Preliminaries 7 3.1 Simultaneous-Move Game . . . . . . . . . . . . . . . . . . . . . . . . 7 3.2 ATL (Alternating-Time Temporal Logic) . . . . . . . . . . . . . . . . 10 4 On-the-Fly ATL Strategy Construction 13 4.1 Strategy Graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 4.2 Strategy Construction for <A>□φ1 . . . . . . . . . . . . . . . . . . . . 17 4.3 Strategy Construction for <A>φ1∪φ2 . . . . . . . . . . . . . . . . . . 21 5 On-the-Fly Algorithm for EFATL Strategy Construction 23 6 Implementation 26 6.1 Libraries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 6.2 A Simple Heuristics . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 6.3 Representation of SGGs . . . . . . . . . . . . . . . . . . . . . . . . . 27 6.4 Representation of EFATL Formulas . . . . . . . . . . . . . . . . . . . 29 7 Experiment 30 7.1 Airline Cargo Service . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 7.2 Readers-Writers System . . . . . . . . . . . . . . . . . . . . . . . . . 31 7.3 Bounded-Bu¤er System . . . . . . . . . . . . . . . . . . . . . . . . . . 32 8 Conclusion and Future Directions 35 Bibliography 36 A A Sample Model File of Our Tool 40 B A Sample Speci…cation File of Our Tool 45 C A Sample Output S-graph of Our Tool 46 D Another Sample Model File of Our Tool 47 E Another Sample Output S-graph of Our Tool 51 | |
| dc.language.iso | en | |
| dc.subject | 模型檢驗 | zh_TW |
| dc.subject | 策略 | zh_TW |
| dc.subject | 驗證 | zh_TW |
| dc.subject | 開放式系統 | zh_TW |
| dc.subject | 交互時態邏輯 | zh_TW |
| dc.subject | 同步賽局 | zh_TW |
| dc.subject | strategy | en |
| dc.subject | simultaneous-move game | en |
| dc.subject | open systems | en |
| dc.subject | ATL | en |
| dc.subject | verification | en |
| dc.subject | model-checking | en |
| dc.title | 交互時態邏輯公式之即時模型驗證與策略建立 | zh_TW |
| dc.title | On-the-Fly Strategy Construction in ATL Model-Checking | en |
| dc.type | Thesis | |
| dc.date.schoolyear | 98-2 | |
| dc.description.degree | 碩士 | |
| dc.contributor.oralexamcommittee | 顏嗣鈞(Hsu-Chun Yen),雷欽隆(Chin-Laung Lei),張時中(Shi-Chung Chang),呂學一(Hsueh-I Lu) | |
| dc.subject.keyword | 同步賽局,開放式系統,交互時態邏輯,驗證,模型檢驗,策略, | zh_TW |
| dc.subject.keyword | simultaneous-move game,open systems,ATL,verification,model-checking,strategy, | en |
| dc.relation.page | 51 | |
| dc.rights.note | 未授權 | |
| dc.date.accepted | 2010-06-30 | |
| dc.contributor.author-college | 電機資訊學院 | zh_TW |
| dc.contributor.author-dept | 電機工程學研究所 | zh_TW |
| 顯示於系所單位： | 電機工程學系 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-99-1.pdf 未授權公開取用 | 2.38 MB | Adobe PDF |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。