III.4 Semantics of Propositional ITL

Semantics of PITL [Slide 96]

Let M() be the “meaning” function from PITL × Σ+ to {tt,} and let σ be an interval (σ Σ+) then

 M⟦true⟧(σ) ≜ tt M⟦q⟧(σ) ≜ σ0(q) and for all 0 < i ≤|σ|,σi(q) = σ0(q) M⟦Q⟧(σ) ≜ σ0(Q) M⟦¬f⟧(σ) ≜ not (M⟦f⟧(σ)) M⟦f1 ∧ f2⟧(σ) ≜ M⟦f1⟧(σ) and M⟦f2⟧(σ) M⟦skip⟧(σ) = tt iﬀ |σ| = 1

Semantics of PITL [Slide 97]

The semantics of ‘chop’ is as follows Mf1 ; f2(σ) = tt iﬀ

(exists k, s.t. Mf1(σ0σk) = tt and Mf2(σkσ|σ|) = tt)

 | ← f1 → | ← f2 → | σ0 σk σ|σ| ● … ● … ●

Interval σ is a fusion of two intervals σ0σk (satisﬁes f1) and σkσ|σ| (satisﬁes f2). State σk is shared by both.

Semantics of PITL [Slide 98]

The semantics of ‘chopstar’ is as follows Mf(σ) = tt iﬀ

(exist l0,,ln s.t. l0 = 0 and ln = |σ| and
for all 0 i < n,li li+1 and Mf(σliσli+1) = tt)

 | ← f → | … | ← f → | … | ← f → | σ0 σl1 σli σli+1 σln−1 σ|σ| ● … ● … ● … ● … ● … ●

Finite interval σ is the fusion of a ﬁnite number of ﬁnite sub-intervals each satisfying f.

 2018-03-10 Contact | Home | ITL home | Course | Proofs | Algebra | FL