ITL
© 1996-2018







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

Mtrue(σ)
tt
Mq(σ)
σ0(q) and
for all 0 < i |σ|i(q) = σ0(q)
MQ(σ)
σ0(Q)
M¬f(σ)
not (Mf(σ))
Mf1 f2(σ)
Mf1(σ) and Mf2(σ)
Mskip(σ) = tt
iff
|σ| = 1

Semantics of PITL [Slide 97]

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

(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 (satisfies f1) and σkσ|σ| (satisfies f2). State σk is shared by both.

Semantics of PITL [Slide 98]

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

(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
σln1
σ|σ|

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







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