4
Algebraic semantics for PITL
Algebraic semantics for PITL [Slide 12]
Can we give the semantic domain an algebraic structure?
Let ⟦f⟧ denote the set of intervals for which M⟦f⟧(σ) = tt, i.e.,
⟦f⟧ ≜ {σM⟦f⟧(σ) = tt}
The ∨ of two PITL formula is then
⟦f_{1} ∨ f_{2}⟧ = 
use deﬁnition of ⟦ ⟧ 
{σM⟦f_{1} ∨ f_{2}⟧(σ) = tt} 
use deﬁnition of M⟦f_{1} ∨ f_{2}⟧(σ) 
{σM⟦f_{1}⟧(σ) = tt or M⟦f_{2}⟧(σ) = tt} 
use set theory, let ∪ denote union 
{σM⟦f_{1}⟧(σ) = tt}∪{σM⟦f_{2}⟧(σ) = tt} 
use deﬁnition of ⟦ ⟧ 
⟦f_{1}⟧∪⟦f_{2}⟧ 

Algebraic semantics for PITL [Slide 13]
So we need algebraic operators that correspond to ¬, ∨,skip,; and
^{∗}
 ∨ corresponds to union (∪) of sets of intervals
 ¬ corresponds to complement of a set, i.e.,
⟦¬f⟧ = 
use deﬁnition of ⟦ ⟧ 
{σM⟦¬f⟧(σ) = tt} 
use deﬁnition of M⟦¬f⟧(σ) 
{σnot (M⟦f⟧(σ) = tt)} 
use set theory, let ∼A denote set complement 
∼{σM⟦f⟧(σ) = tt} 
use deﬁnition of ⟦ ⟧ 
∼⟦f⟧ 

Algebraic semantics for PITL [Slide 14]
What about chop (‘;’)?
Let ⋅ denote the fusion of two intervals σ_{1},σ_{2} ∈ Σ^{+} ∪ Σ^{ω}, i.e.,
Let a,b ∈ Σ (a and b are not the same), v,w ∈ Σ^{∗} and s,t ∈ Σ^{ω}
σ_{1} ⋅σ_{2} ≜ vaw  if  σ_{1} = va,  σ_{2} = aw 
∅ 
if 
σ_{1} = va, 
σ_{2} = bw 
vas 
if 
σ_{1} = va, 
σ_{2} = as 
∅ 
if 
σ_{1} = va, 
σ_{2} = bs 
s 
if 
σ_{1} = s, 
σ_{2} = aw 
s 
if 
σ_{1} = s, 
σ_{2} = t 

Let S,T ⊆ Σ^{+} ∪ Σ^{ω} then
S ⋅ T ≜ {σ_{1} ⋅ σ_{2}σ_{1} ∈S and σ_{2} ∈T}
Algebraic semantics for PITL [Slide 15]
 ‘;’ corresponds to fusion ‘⋅’, i.e.,
⟦f_{1} ; f_{2}⟧ = 
use deﬁnition of ⟦ ⟧ 
{σM⟦f_{1} ; f_{2}⟧(σ) = tt} 
use deﬁnition of M⟦f_{1} ; f_{2}⟧(σ) 
{σ( exists k, s.t. M⟦f_{1}⟧(σ_{0}…σ_{k}) = tt and M⟦f_{2}⟧(σ_{k}…σ_{σ}) = tt) 
or (σ is inﬁnite and M⟦f_{1}⟧(σ) = tt)} 
use deﬁnition of ⋅ 
{σM⟦f_{1}⟧(σ) = tt}⋅{σM⟦f_{2}⟧(σ) = tt} 
use deﬁnition of ⟦ ⟧ 
⟦f_{1}⟧⋅⟦f_{2}⟧ 

Algebraic semantics for PITL [Slide 16]
What about empty?
⟦empty⟧ = 
use deﬁnition of ⟦ ⟧ 
{σM⟦empty⟧(σ) = tt} 
use deﬁnition of M⟦empty⟧(σ) 
{σσ is a 1 state interval} 
use deﬁnition of Σ 
Σ 
Algebraic semantics for PITL [Slide 17]
What about skip?
skip can be deﬁned as ∼(Σ ∪∼Σ ⋅∼Σ)
∼(Σ ∪∼Σ ⋅∼Σ) = 
use De Morgan for set theory 
∼Σ ∩∼(∼Σ ⋅∼Σ) 

∼Σ
is the set of intervals containing ≥ 2 states
∼Σ ⋅ ∼Σ is the set of intervals containing ≥ 3 states
∼(∼Σ ⋅∼Σ) is the set of intervals containing ≤ 2 states
∼Σ ∩ ∼(∼Σ ⋅∼Σ) is the set of intervals containing exactly 2 states
Algebraic semantics for PITL [Slide 18]
What about a state formula, i.e., a formula without temporal operators?
A state formula only constrains the ﬁrst state of an interval. Let p be a
state formula. Then the following holds
⟦p⟧ = (⟦p⟧∩Σ) ⋅T where
T ≜⟦true⟧ = Σ^{+} ∪ Σ^{ω} 
∅≜⟦false⟧ = ∅ 
Algebraic semantics for PITL [Slide 19]
What about chopstar ‘^{∗}’?
In the semantics of ‘^{∗}’ both ﬁnite and inﬁnite iteration are considered
simultaneously. Let’s deﬁne separate algebraic operators for them.
Let S^{∗} and S^{ω} denote respectively ﬁnite and inﬁnite iteration of a set
S
⊆ Σ^{+} ∪ Σ^{ω} and can be deﬁned as follows
f(X) 
≜ 
Σ ∪S ⋅X 
g(X) 
≜ 
S ⋅X 
f^{0}(X) 
≜ 
X 
g^{0}(X) 
≜ 
X 
f^{i+1}(X)  ≜  f(f^{i}(X))  g^{i+1}(X)  ≜  g(g^{i}(X)) 
S^{∗} 
≜ 
⋃
_{i}f^{i}(∅) 
S^{ω} 
≜ 
⋂
_{i}g^{i}(T) 

Then we have
⟦f^{∗}⟧ = … = ⟦f⟧^{∗}∪⟦f⟧^{ω}
