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}⟧ |
So we need algebraic operators that correspond to ¬, ∨,skip,; and ^{∗}
¬ 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⟧ |
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}
‘;’ 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}⟧ |
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 Σ |
Σ |
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
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⟧ = ∅ |
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
ﬁnite |
≜ |
∼(T ⋅∅) |
fmore |
≜ |
∼Σ ∩ﬁnite |
f(X) | ≜ | Σ ∪ (S ∩fmore) ⋅X | g(X) | ≜ | (S ∩fmore) ⋅X |
S^{∗} |
≜ |
μX.f(X) |
S^{ω} |
≜ |
νX.g(X) |
where μX.f(X) denotes the least ﬁxpoint of f and νX.g(X) the greatest ﬁxpoint of g.
Then we have
⟦f^{∗}⟧ = … = ⟦f⟧^{∗}∪⟦f⟧^{ω}