ITL
© 1996-2018







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 Mf(σ) = tt, i.e.,

f {σ|Mf(σ) = tt}

The of two PITL formula is then

f1 f2 =
use definition of  
{σ|Mf1 f2(σ) = tt}
use definition of Mf1 f2(σ)
{σ|Mf1(σ) = tt or Mf2(σ) = tt}
use set theory, let denote union
{σ|Mf1(σ) = tt}{σ|Mf2(σ) = tt}
use definition of  
f1f2

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 definition of  
    {σ|M¬f(σ) = tt}
    use definition of M¬f(σ)
    {σ|not (Mf(σ) = tt)}
    use set theory, let A denote set complement
    {σ|Mf(σ) = tt}
    use definition of  
    f

Algebraic semantics for PITL [Slide 14]

What about chop (‘;’)?

Let denote the fusion of two intervals σ12 Σ+ Σω, 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.,

    f1 ; f2 =
    use definition of  
    {σ|Mf1 ; f2(σ) = tt}
    use definition of Mf1 ; f2(σ)
    {σ|( exists k, s.t. Mf1(σ0σk) = tt and Mf2(σkσ|σ|) = tt)
    or (σ is infinite and Mf1(σ) = tt)}
    use definition of
    {σ|Mf1(σ) = tt}{σ|Mf2(σ) = tt}
    use definition of  
    f1f2

Algebraic semantics for PITL [Slide 16]

What about empty?

empty =
use definition of  
{σ|Mempty(σ) = tt}
use definition of Mempty(σ)
{σ|σ is a 1 state interval}
use definition of Σ
Σ

Algebraic semantics for PITL [Slide 17]

What about skip?

skip can be defined 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 first 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 finite and infinite iteration are considered simultaneously. Let’s define separate algebraic operators for them.

Let S and Sω denote respectively finite and infinite iteration of a set S Σ+ Σω and can be defined as follows

f(X)
Σ S X
g(X)
S X
f0(X)
X
g0(X)
X
fi+1(X)
f(fi(X))
gi+1(X)
g(gi(X))
S
ifi()
Sω
igi(T)

Then we have

f = = ffω







2018-02-26
Contact | Home | ITL home | Course | Proofs | Algebra | FL