交互時態邏輯公式之即時模型驗證與策略建立

On-the-Fly Strategy Construction in ATL Model-Checking

何熙明(Hsi-Ming Ho)

指導教授 ： 王凡

國立臺灣大學/電機資訊學院/電機工程學研究所/碩士(2010年)

https://doi.org/10.6342/NTU.2010.10760

摘要

嵌入式系統常需要與不可預知的環境互動。對此類系統進行驗證時，交互時態邏輯模型檢驗可用來檢查是否無論環境行為如何，都能確保某些性質的成立。在此論文中，我們提出一個可以運用在開放式系統驗證上的即時正向策略建立演算法。在我們的實驗架構中，開放式系統會被對應到多人賽局。我們再利用ATL的一個子集（稱為EFATL）中之邏輯公式來描述想要驗證的性質。如果模型中存在簡短的策略可使性質成立，我們的演算法可有效率地建立出一個策略。我們亦描述一個簡單的heuristics來展現我們演算法之發展性。最後我們利用REDLIB來實作一套完整的模型檢驗器，並與一套類似的工具比較效能。

關鍵字

同步賽局 ； 開放式系統 ； 交互時態邏輯 ； 驗證 ； 模型檢驗 ； 策略

並列摘要

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.

並列關鍵字

simultaneous-move game ； open systems ； ATL ； verification ； model-checking ； strategy

參考文獻

[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.

[7] P.-J. Courtois, F. Heymans, and D. L. Parnas. Concurrent control with "read- ers" and "writers". Commun. ACM, 14(10):667-668, 1971.