© 1996-2019

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

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

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

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

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

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

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

 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ω

 2019-01-03 Contact | Home | ITL home | Course | Proofs | Algebra | FL