Next Prev Up

### 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 deﬁnition of ⟦ ⟧ {σ | M⟦f1 ∨ f2⟧(σ) = tt} use deﬁnition of M⟦f1 ∨ f2⟧(σ) {σ | M⟦f1⟧(σ) = tt or M⟦f2⟧(σ) = tt} use set theory, let ∪ denote union {σ | M⟦f1⟧(σ) = tt}∪{σ | M⟦f2⟧(σ) = tt} use deﬁnition of ⟦ ⟧ ⟦f1⟧∪⟦f2⟧

#### 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]

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 deﬁnition of ⟦ ⟧ {σ | M⟦f1 ; f2⟧(σ) = tt} use deﬁnition of M⟦f1 ; f2⟧(σ) {σ | ( exists k, s.t. M⟦f1⟧(σ0…σk) = tt and M⟦f2⟧(σk…σ|σ|) = tt) or (σ is inﬁnite and M⟦f1⟧(σ) = tt)} use deﬁnition of ⋅ {σ | M⟦f1⟧(σ) = tt}⋅{σ | M⟦f2⟧(σ) = tt} use deﬁnition of ⟦ ⟧ ⟦f1⟧⋅⟦f2⟧

#### Algebraic semantics for PITL [Slide 16]

 ⟦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]

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]

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 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ω

 Next Prev Up

 2023-09-12 Contact | Home | ITL home | Course | Proofs | Algebra | FL © 1996-2023