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

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 (M⟦f⟧(σ) = tt)}

  use set theory, let ∼A denote set complement

  ∼{σ | M⟦f⟧(σ) = tt}

  use definition of ⟦ ⟧

  ∼⟦f⟧

Algebraic semantics for PITL [Slide 14]

What about chop (‘;’)?

Let ⋅ denote the fusion of two intervals σ₁,σ₂ ∈ Σ⁺ ∪ Σ^ω, i.e.,

Let a,b ∈ Σ (a and b are not the same), v,w ∈ Σ^∗ and s,t ∈ Σ^ω

σ₁ ⋅σ₂ ≜

Let S,T ⊆ Σ⁺ ∪ Σ^ω then

S ⋅T ≜{σ₁ ⋅ σ₂ | σ₁ ∈S and σ₂ ∈T}

Algebraic semantics for PITL [Slide 15]

• ‘;’ corresponds to fusion ‘⋅’, i.e.,

  ⟦f1 ; f2⟧ =

  use definition of ⟦ ⟧

  {σ | M⟦f1 ; f2⟧(σ) = tt}

  use definition of M⟦f1 ; f2⟧(σ)

  {σ | ( exists k, s.t. M⟦f1⟧(σ0…σk) = tt and M⟦f2⟧(σk…σ|σ|) = tt)

  or (σ is infinite and M⟦f1⟧(σ) = tt)}

  use definition of ⋅

  {σ | M⟦f1⟧(σ) = tt}⋅{σ | M⟦f2⟧(σ) = tt}

  use definition of ⟦ ⟧

  ⟦f1⟧⋅⟦f2⟧

Algebraic semantics for PITL [Slide 16]

What about empty?

Algebraic semantics for PITL [Slide 17]

What about skip?

skip can be defined as ∼(Σ ∪∼Σ ⋅∼Σ)

∼Σ 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

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

where μX.f(X) denotes the least fixpoint of f and νX.g(X) the greatest fixpoint of g.

Then we have

⟦f^∗⟧ = … = ⟦f⟧^∗∪⟦f⟧^ω