ITL
© 1996-2015







4 Algebraic semantics for PITL

Can we give the semantic domain an algebraic structure?

Let ⟦f⟧ denote the set of intervals for which ⟦f⟧σ = tt  , i.e.,

⟦f ⟧ ^= {σ |⟦f ⟧σ = tt}

The ∨ of two PITL formula is then

⟦f1 ∨ f2⟧ =
—  definition of⟦⟧
{ σ|⟦f1 ∨ f2⟧σ = tt}
—  definition of⟦f1 ∨ f2⟧σ
{ σ|⟦f1⟧σ = ttor⟦f2⟧σ = tt}
—  settheory,let ∪ denoteunion
{ σ|⟦f1⟧σ = tt} ∪ {σ|⟦f2⟧σ =  tt}
—  definition of⟦⟧
⟦f1⟧ ∪⟦f2⟧

So we need algebraic operators that correspond to ,∨, skip,; and *

  • ∨ corresponds to union (∪ ) of sets of intervals
  •  corresponds to complement, i.e.,
    ⟦f ⟧ =
—  definitionof⟦ ⟧
{σ |⟦f ⟧σ = tt}
—  definitionof⟦f ⟧σ
{σ |not(⟦f⟧σ = tt)}
—--settheory,let--denotesetcomplement
{σ |⟦f⟧σ = tt}
—--definitionof⟦ ⟧
⟦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 ∈ Σ

         (|  vaw   if   σ1 = va,  σ2 = aw
         ||||  ∅     if   σ1 = va,  σ2 = bw
         |{  vas   if   σ1 = va,  σ2 = as
σ1 ⋅σ2 ^= |  ∅     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.,
    ⟦f1 ;f2⟧ =
— definition of⟦⟧
{σ|⟦f1 ;f2⟧σ = tt}
— definition of⟦f1 ;f2⟧σ
{σ|(existsk, s.t. ⟦f1 ⟧σ0...σk = ttand⟦f2⟧σk...σ|σ| = tt)
or(σ is infiniteand ⟦f1⟧σ = tt)}
— definition of⋅
{σ|⟦f1⟧σ = tt} ⋅{σ |⟦f2⟧σ = tt}
— definition of⟦⟧
⟦f1⟧ ⋅⟦f2 ⟧

What about empty  ?

⟦em pty⟧ =
—  definition of ⟦⟧
{σ |⟦em pty⟧σ = tt}
—  definition of ⟦em pty⟧σ
{σ |σ isa1 stateinterval}
—  definition of Σ
Σ

What about skip  ?

skip  can be defined as ----------
Σ  ∪Σ  ⋅Σ

---------
Σ ∪ Σ ⋅Σ =
—-De-M-organforsettheory
Σ ∩ Σ ⋅Σ

--
Σ 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 first 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 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⋃(f i(X )) |gi+1(X )  ^=  g⋂(gi(X ))
S*       =^    if i(∅)   |Sω        ^=    igi(T)

Then we have

⟦f*⟧ = ...=  ⟦f ⟧* ∪ ⟦f⟧ω