ITL
© 1996-2015







9 Informal Semantics Propositional ITL

In propositional logic semantics is given wrt a state:

If σ0(p) = tt  and σ0(q) = ff  then ⟦p ∨ q⟧σ0 = tt

|-------|
|  σ0   |
|   ∙   |
| p,q  |
---------

In propositional ITL semantics is given wrt a sequence of states:

Let σ0  and σ1  be states then ⟦skip⟧σ0σ1 = tt

|-------------------|
|  | < — skip— >  |  |
| σ0            σ1  |
---∙-------------∙---

Let σ0  , σ1  and σ2  be states then ⟦skip; skip⟧σ0σ1σ2 = tt

|---------------------------------|
|  | < —skip— >  | < — skip— >  |  |
| σ0            σ1            σ2  |
|  ∙             ∙             ∙  |
-----------------------------------

Let σ0  and σ1  be states and σ0(Q ) = tt  then ⟦Q ∧ skip⟧σ0σ1 = tt

|-----------------------|
|  | < —Q  ∧ skip—  > |  |
| σ0                σ1  |
| ∙                  ∙  |
| Q                     |
-------------------------

Let σ0  and σ1  be states and σ0(Q ) = tt  and σ1(Q ) = ff  then ⟦Q ∧ (skip ;Q )⟧σ0σ1 = tt

|----------------------|
| | < — skip—  >| <>  | |
|σ0              σ1    |
| ∙               ∙    |
--Q--------------Q-----

Let σ
  0  and σ
  1  be states and σ (P ) = tt
 0  , σ (R ) = ff
 0  and σ (Q ) = tt
 1  then ⟦P ∧ (((R ) ∧ skip);Q )⟧    = tt
                        σ0σ1

|---------------------------------|
|   |  <  — (R  ) ∧ skip — > | < > |
|  σ                         σ    |
|   ∙0                       ∙1   |
| P,R                       Q    |
-----------------------------------

Let σ0  , σ1  and σ2  be states and σ0(Q ) = tt  , σ1(Q) = tt  and σ2(Q ) = ff  then ⟦Q ∧ (C Q ) ∧ (C CQ )⟧σ0σ1σ2 = tt

|---------------------------------|
| | < — skip—  > | < — skip — >  |  |
| σ0            σ1            σ2  |
| ∙             ∙              ∙  |
| Q             Q             Q  |
------------------------------------

Let σ0  , σ1  and σ2  be states and σ0(P ) = tt  and σ2 (Q ) = tt  then ⟦(  P) ∧ (  Q)⟧σ0σ1σ2 = tt

|---------------------------------|
|  | < —skip— >  | < — skip— >  |  |
| σ0            σ1            σ2  |
|  ∙             ∙             ∙  |
| P                           Q   |
-----------------------------------

Let σ0  , σ1  and σ2  be states and σ0 (Q ) = tt  , σ1(Q ) = tt  and σ3(Q ) = tt  then

|-----------------------------------------------------|
|                 | | < > ||                          |
|                 |   σ0   |                          |
|                 |   ∙    |                          |
|                 |   Q    |                          |
| ⟦! Q ⟧σ0 = tt     |-------------------|               |
|                 |  | < — skip— > |  |               |
|                 | σ0            σ1  |               |
|                 | ∙              ∙  |               |
|                 | Q             Q   |               |
| ⟦! Q ⟧σ0σ1 = tt  |---------------------------------| |
|                 |  | < — skip— > | < —skip— >  |  | |
|                 | σ             σ             σ   | |
|                 | ∙0             1∙             2∙  | |
|                 | Q             Q             Q   | |
| ⟦! Q ⟧σ σσ  = tt ----------------------------------- |
--------0-12--------------------------------------------

Let σi be a state (i ≥ 0 ) then

|---------------------------------------------------------|
|                     | | < > ||                          |
|                     |  σ     |                          |
|                     |   ∙0   |                          |
| ⟦skip*⟧σ      =   tt -----------                         |
|        0            |------------------||               |
|                     | | < — skip—  >  | ||               |
|                     | σ0            σ1 ||               |
|     *               --∙-------------∙----               |
| ⟦skip ⟧σ0σ1   =   tt |---------------------------------| |
|                     | | < — skip—  >  | < — skip — > |  | |
|                     | σ0            σ1            σ2  | |
|     *               --∙-------------∙-------------∙---- |
| ⟦skip ⟧σ0σ1σ2 =   tt                                     |
| ...                 |-------------|                     |
|                     | σ0  ... σi  |                     |
|                     | ∙   ...  ∙  |                     |
| ⟦skip*⟧σ0...σi  =   tt ---------------                     |
-----------------------------------------------------------