A Transformation from PPTL to SIS*

摘要

A transformation from Prepositional Projection Temporal Logic (PPTL) as well as Prepositional Interval Temporal Logic (PITL) with infinite models to monadic second order logic with one successor (SIS) is presented in this paper. To this end, intervals where PPTL and PITL formulas are interpreted over are represented as £-structures. Further, the semantics of PPTL and PITL formulas are redefined over £-structures. Moreover, according to £-structure semantics, a PPTL or PITL formula is translated to a formula in SIS. As a result, many mature theoretical and technical results, such as decidability etc. for SIS can be easily inherited by PPTL and PITL.