ITL
© 1996-2015







22 Informal Semantics First Order ITL

In first order logic semantics is given wrt a state:

Let σ0  be a state and σ0(A) = 0 and σ0(B ) = 5 then ⟦A = 0 ∨ B =  1⟧σ0 = tt

|--------|
|  σ0    |
|   ∙    |
|A  = 0  |
|B  = 5  |
---------

In first order ITL semantics is given wrt a sequence of states:

Let σ0  and σ1  be states and σ1(B ) = 0 and σ1 (A) = 1 then ⟦(C B) = 0 ∧ (skip ;A = 1)⟧σ0σ1 = tt

|----------------------|
| | < — skip—  >| <>  | |
|σ0              σ1    |
| ∙               ∙    |
|              A  = 1  |
---------------B--=-0---

Let σ0  and σ1  be states and σ0 (A ) = 0 , σ0(B ) = 1 , σ1(A) = 1 and σ1 (B ) = 0 then ⟦A =  0 ∧ ((B = 1 ∧ skip);(A = 1 ∧ B = 0))⟧σ0σ1 = tt

|----------------------------------|
|   |  < —B   = 1 ∧ skip—  >| <>  | |
|  σ0                        σ1    |
|   ∙                         ∙    |
|A  = 0                    A  = 1  |
|B  = 1                    B  = 0  |
------------------------------------

Let σ0  , σ1  and σ2  be states and σ0(A ) = 0 , σ1(A ) = 1 and σ2(A ) = 2 then ⟦A =  0 ∧ C (A = 1) ∧ CC (A = 2)⟧σ0σ1σ2 = tt

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

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

|---------------------------------------|
|   |  <  —skip— >  | < — skip— >    |   |
|  σ               σ               σ    |
|   ∙0              1∙              ∙2   |
| A = 0                          B =  0 |
------------------------------------------

Let σ0  , σ1  and σ2  be states and σ0 (A ) = 5 , σ1(A ) = 5 and σ3(A ) = 5 then

|-------------------------------------------------------------|
|                    | | < > ||                               |
|                    |   σ    |                               |
|                    |   ∙0   |                               |
|                    | A =  5 |                               |
|⟦! A  = 5⟧σ =  tt     -----------                              |
|          0         |-----------------------|                |
|                    |   |   < -skip- >  |    |                |
|                    |   σ0             σ1   |                |
|                    |   ∙              ∙    |                |
|                    --A-=-5----------A-=-5---                |
|⟦! A  = 5⟧σ0σ1 = tt  |--------------------------------------| |
|                    |   |   < -skip- >  |  <  -skip- >  |    | |
|                    |   σ0             σ1            σ2    | |
|                    |   ∙              ∙              ∙    | |
|                    --A-=-5----------A-=-5----------A-=-5--- |
-⟦!-A--=-5⟧σ0σ1σ2-=-tt--------------------------------------------
                                                              |

Let σi be a state (i ≥ i ) and σi(A) = 0 then

|---------------*---------------------------|
| ⟦(A = 0 ∧ skip)* ∧ (finA ) = 0 ⟧σ0     =  tt |
| ⟦(A = 0 ∧ skip)* ∧ (finA ) = 0 ⟧σ0σ1   =  tt |
| ⟦(A = 0 ∧ skip)  ∧ (finA ) = 0 ⟧σ0σ1σ2 =  tt |
| ...           *                           |
--⟦(A-=-0-∧-skip)--∧-(finA-) =-0-⟧σ0...σi-=--tt--

Note: looks similar to ! A =  0 but is it really equal?