| |
| This paper investigates the decision procedure for checking
the satisfiability of Propositional Projection Temporal Logic (PPTL).
The syntax, semantics and logic laws of PPTL are presented. Within this logic, besides the usual logic connectives, two basic temporal operators, O and prj are introduced. A normal form of PPTL is formalized and a proof for transforming a formula of PPTL into the normal form is given by induction on the structure of formulas in details. An algorithm
transforming a formula into the normal form is presented. To find out a model for a given formula, the notation of Normal Form Graph (NFG) and an algorithm constructing NFG for the formula are introduced. A decision procedure for checking the satisfiability of PPTL formulas with finite models is demonstrated and some examples are given to illustrate how the algorithms work.
|
|
| Keywords:temporal logic, decision procedure, satisfiablity |
|
