Efficient decision procedure for propositional projection temporal logic

The decision problem for Propositional Projection Temporal Logic (PPTL) has been solved successfully, however time complexity of the procedure is increased exponentially to the length of the formula. To solve the problem, a labeled unified complete normal form is introduced as the intermediate form to rewrite a PPTL formula into its equivalent labeled normal form, based on which the labeled normal form graph is constructed, and an efficient decision procedure for PPTL is formalized with the time complexity linear to the length of the formula and the size of the power set of the atomic propositions in the formula. Besides, an example is given to show how the improved decision procedure works.

Authors

• Xinfeng Shu
• Nan Zhang
• Xiaobing Wang
• Liang Zhao

Keywords

• Projection temporal logic
• Decision procedure
• Labeled normal form
• Labeled normal form graph