In Propositional Projection Temporal Logic (PPTL), a well-formed formula is generally formed by applying rules of its syntax finitely many times. However, under some circumstances, although formulas such as ones expressed by index set expressions, are constructed via applying rules of the syntax infinitely many times, they are possibly still well-formed. With this motivation, this paper investigates the relationship between formulas specified by index set expressions and concise syntax expressions by means of fixed-point induction approach. Firstly, we present two kinds of formulas, namely and V i∈N0 OiP and V i∈N0 Pi, and prove they are indeed well-formed by demonstrating their equivalence to formulas ◇P and P + respectively. Further, we generalize V i∈N0 OiQ to Vi∈N0 P(i) ∧ OiQ and explore solutions of an abstract equation X ≡ Q V P ∧ OX. Moreover, we equivalently represent 'U' (strong until) and 'W' (weak until) constructs in Propositional Linear Temporal Logic within PPTL using the index set expression techniques. © 2013 Springer-Verlag.
CITATION STYLE
Duan, Z., Ma, Q., Tian, C., & Zhang, N. (2013). Some fixed-point issues in PPTL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8051 LNCS, pp. 151–165). https://doi.org/10.1007/978-3-642-39698-4_10
Mendeley helps you to discover research relevant for your work.