| Summary: | 碩士 === 臺灣大學 === 電機工程學研究所 === 98 === 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.
|
|---|
