Framed Temporal Logic Programming Interpreter And Model Checker

This thesis mainly discusses the implementation of an interpreter for Framed Temporal Logic Programming Language (FTLL) and a model checker with Proposition Projection Temporal Logic (PPTL) specifying the properties of the system. The basic approach using normal form theory is presented firstly. Then, the structure of the interpreter is discussed and each of its modules is explained. In particular, the implementation approaches of several important constructs including frame, await, projection and pointer are given. As an application, the interpreter is used as the simulator of service models of OWL-S Web service composition.Subsequently, this thesis shows a model checking method. It models the system with FTLL and specifies the properties with PPTL. After transforming the system and the negation of the properties to their normal forms, it unites them to see whether there are counter-examples. The algorithm and an example are given in succession. Finally, this thesis reviews the existing model checkers.