# Formal Models UE
###### tags: `Exercise`

## Exercise Sheet 1

### Exercise 1

### Exercise 2

### Exercise 3

### Exercise 4

## Exercise Sheet 2

### Exercise 5

### Exercise 6

### Exercise 7

### Exercise 8

## Exercise Sheet 3

### Exercise 9

### Exercise 10

### Exercise 11

### Exercise 12

## Exercise Sheet 4

### Exercise 13

### Exercise 14

### Exercise 15

### Exercise 16

## Exercise Sheet 5

### Exercise 17


A)

S = {(0,a),(0,b),(1,a),(1,b),(2,a),(2,b),(3,a),(3,b)}

I = {(2,a),(2,b)}

T = {((0,a),(1,a)), ((0,a),(1,b)), ((0,a),(2,a)), ((0,a),(2,b)), ((0,b),(1,a)), ((0,b),(1,b)), ((1,a),(1,a)), ((1,a),(1,b)), ((1,b),(3,a)), ((1,b),(3,b)), ((2,a),(3,a)), ((2,a),(3,b)), ((2,b),(0,a)), ((2,b),(0,b)), ((3,a),(0,a)), ((3,a),(0,b)), ((3,a),(3,a)), ((3,a),(3,b)), ((3,b),(3,a)), ((3,b),(3,b))}

a Є L(s) iff s Є {(0,a),(1,a),(2,a),(3,a)}

b Є L(s) iff s Є {(0,b),(1,b),(2,b),(3,b)}

B)
𝜋1= ((2,b),(0,b),(1,a)ω)

𝜋2= ((2,b),(0, a)ω)

𝜋3= ((2,a),(3, b)ω)

𝜋4= ((2,a), (3,a),(3, b)ω)

C)

Equivalencies : 𝜋3^1 = 𝜋4^2

### Exercise 18

### Exercise 19

### Exercise 20

## Exercise Sheet 6

### Exercise 21


### Exercise 22

### Exercise 23

### Exercise 24



## Exercise Sheet 7

### Exercise 25

### Exercise 26

### Exercise 27

### Exercise 28

## Exercise Sheet 8

### Exercise 29

### Exercise 30

### Exercise 31
It is the same like 32.

### Exercise 32
%%%%%%%ex32%%%%%%%%

%% initial state %%
(Linz_0 & !Vienna_0 & !Salzburg_0 & !Innsbruck_0 & Good1_0 & !Good2_0 & !Goal1_0 & !Goal2_0) &

%% goal state %%
Goal1_5 & Goal2_5 &

%% actions %%
% for one step
(LV_0 -> (Linz_0 & !Linz_1 & Vienna_1 & Good2_1)) &
(LS_0 -> (Linz_0 & !Linz_1 & Salzburg_1)) &
(VL_0 -> (Vienna_0 & !Vienna_1 & Linz_1 & Good1_1)) &
(VS_0 -> (Vienna_0 & !Vienna_1 & Salzburg_1)) &
(SI_0 -> (Salzburg_0 & !Salzburg_1 & Innsbruck_1)) &
(drop1_0 -> (Good1_0 & Innsbruck_0 & !Goal1_0 & !Good1_1 & Innsbruck_1 & Goal1_1)) &
(drop2_0 -> (Good2_0 & Salzburg_0 & !Goal2_0 & !Good2_1 & Salzburg_1 & Goal2_1)) &

% for two steps
(LV_1 -> (Linz_1 & !Linz_2 & Vienna_2 & Good2_2)) &
(LS_1 -> (Linz_1 & !Linz_2 & Salzburg_2)) &
(VL_1 -> (Vienna_1 & !Vienna_2 & Linz_2 & Good1_2)) &
(VS_1 -> (Vienna_1 & !Vienna_2 & Salzburg_2)) &
(SI_1 -> (Salzburg_1 & !Salzburg_2 & Innsbruck_2)) &
(drop1_1 -> ((Good1_1 | Good1_0) & Innsbruck_1 & (!Goal1_1 & !Goal1_0) & !Good1_2 & Innsbruck_2 & Goal1_2)) &
(drop2_1 -> ((Good2_1 | Good2_0) & Salzburg_1 & (!Goal2_1 & !Goal2_0) & !Good2_2 & Salzburg_2 & Goal2_2)) &

% for three steps
(LV_2 -> (Linz_2 & !Linz_3 & Vienna_3 & Good2_3)) &
(LS_2 -> (Linz_2 & !Linz_3 & Salzburg_3)) &
(VL_2 -> (Vienna_2 & !Vienna_3 & Linz_3 & Good1_3)) &
(VS_2 -> (Vienna_2 & !Vienna_3 & Salzburg_3)) &
(SI_2 -> (Salzburg_2 & !Salzburg_3 & Innsbruck_3)) &
(drop1_2 -> ((Good1_2 | Good1_1 | Good1_0) & Innsbruck_2 & (!Goal1_2 & !Goal1_1 & !Goal1_0) & !Good1_3 & Innsbruck_3 & Goal1_3)) &
(drop2_2 -> ((Good2_2 | Good2_1 | Good2_0) & Salzburg_2 & (!Goal2_2 & !Goal2_1 & !Goal2_0) & !Good2_3 & Salzburg_3 & Goal2_3)) &

% for four steps
(LV_3 -> (Linz_3 & !Linz_4 & Vienna_4 & Good2_4)) &
(LS_3 -> (Linz_3 & !Linz_4 & Salzburg_4)) &
(VL_3 -> (Vienna_3 & !Vienna_4 & Linz_4 & Good1_4)) &
(VS_3 -> (Vienna_3 & !Vienna_4 & Salzburg_4)) &
(SI_3 -> (Salzburg_3 & !Salzburg_4 & Innsbruck_4)) &
(drop1_3 -> ((Good1_3 | Good1_2 | Good1_1 | Good1_0) & Innsbruck_3 & (!Goal1_3 & !Goal1_2 & !Goal1_1 & !Goal1_0) & !Good1_4 & Innsbruck_4 & Goal1_4)) &
(drop2_3 -> ((Good2_3 | Good2_2 | Good2_1 | Good2_0) & Salzburg_3 & (!Goal2_3 & !Goal2_2 & !Goal2_1 & !Goal2_0) & !Good2_4 & Salzburg_4 & Goal2_4)) &

% for five steps
(LV_4 -> (Linz_4 & !Linz_5 & Vienna_5 & Good2_5)) &
(LS_4 -> (Linz_4 & !Linz_5 & Salzburg_5)) &
(VL_4 -> (Vienna_4 & !Vienna_5 & Linz_5 & Good1_5)) &
(VS_4 -> (Vienna_4 & !Vienna_5 & Salzburg_5)) &
(SI_4 -> (Salzburg_4 & !Salzburg_5 & Innsbruck_5)) &
(drop1_4 -> ((Good1_4 | Good1_3 | Good1_2 | Good1_1 | Good1_0) & Innsbruck_4 & (!Goal1_4 & !Goal1_3 & !Goal1_2 & !Goal1_1 & !Goal1_0) & !Good1_5 & Innsbruck_5 & Goal1_5)) &
(drop2_4 -> ((Good2_4 | Good2_3 | Good2_2 | Good2_1 | Good2_0) & Salzburg_4 & (!Goal2_4 & !Goal2_3 & !Goal2_2 & !Goal2_1 & !Goal2_0) & !Good2_5 & Salzburg_5 & Goal2_5)) &

%% at most one action %%
% for one step
(!LV_0 | !LS_0) & (!LV_0 | !VL_0) & (!LV_0 | !VS_0) & (!LV_0 | !SI_0) & (!LV_0 | !drop1_0) & (!LV_0 | !drop2_0) &
(!LS_0 | !VL_0) & (!LS_0 | !VS_0) & (!LS_0 | !SI_0) & (!LS_0 | !drop1_0) & (!LS_0 | !drop2_0) &
(!VL_0 | !VS_0) & (!VL_0 | !SI_0) & (!VL_0 | !drop1_0) & (!VL_0 | !drop2_0) &
(!VS_0 | !SI_0) & (!VS_0 | !drop1_0) & (!VS_0 | !drop2_0) &
(!SI_0 | !drop1_0) & (!SI_0 | !drop2_0) &
(!drop1_0 | !drop2_0) &

% for two steps
(!LV_1 | !LS_1) & (!LV_1 | !VL_1) & (!LV_1 | !VS_1) & (!LV_1 | !SI_1) & (!LV_1 | !drop1_1) & (!LV_1 | !drop2_1) &
(!LS_1 | !VL_1) & (!LS_1 | !VS_1) & (!LS_1 | !SI_1) & (!LS_1 | !drop1_1) & (!LS_1 | !drop2_1) &
(!VL_1 | !VS_1) & (!VL_1 | !SI_1) & (!VL_1 | !drop1_1) & (!VL_1 | !drop2_1) &
(!VS_1 | !SI_1) & (!VS_1 | !drop1_1) & (!VS_1 | !drop2_1) &
(!SI_1 | !drop1_1) & (!SI_1 | !drop2_1) &
(!drop1_1 | !drop2_1) &

% for three steps
(!LV_2 | !LS_2) & (!LV_2 | !VL_2) & (!LV_2 | !VS_2) & (!LV_2 | !SI_2) & (!LV_2 | !drop1_2) & (!LV_2 | !drop2_2) &
(!LS_2 | !VL_2) & (!LS_2 | !VS_2) & (!LS_2 | !SI_2) & (!LS_2 | !drop1_2) & (!LS_2 | !drop2_2) &
(!VL_2 | !VS_2) & (!VL_2 | !SI_2) & (!VL_2 | !drop1_2) & (!VL_2 | !drop2_2) &
(!VS_2 | !SI_2) & (!VS_2 | !drop1_2) & (!VS_2 | !drop2_2) &
(!SI_2 | !drop1_2) & (!SI_2 | !drop2_2) &
(!drop1_2 | !drop2_2) &

% for four steps
(!LV_3 | !LS_3) & (!LV_3 | !VL_3) & (!LV_3 | !VS_3) & (!LV_3 | !SI_3) & (!LV_3 | !drop1_3) & (!LV_3 | !drop2_3) &
(!LS_3 | !VL_3) & (!LS_3 | !VS_3) & (!LS_3 | !SI_3) & (!LS_3 | !drop1_3) & (!LS_3 | !drop2_3) &
(!VL_3 | !VS_3) & (!VL_3 | !SI_3) & (!VL_3 | !drop1_3) & (!VL_3 | !drop2_3) &
(!VS_3 | !SI_3) & (!VS_3 | !drop1_3) & (!VS_3 | !drop2_3) &
(!SI_3 | !drop1_3) & (!SI_3 | !drop2_3) &
(!drop1_3 | !drop2_3) &

% for four steps
(!LV_4 | !LS_4) & (!LV_4 | !VL_4) & (!LV_4 | !VS_4) & (!LV_4 | !SI_4) & (!LV_4 | !drop1_4) & (!LV_4 | !drop2_4) &
(!LS_4 | !VL_4) & (!LS_4 | !VS_4) & (!LS_4 | !SI_4) & (!LS_4 | !drop1_4) & (!LS_4 | !drop2_4) &
(!VL_4 | !VS_4) & (!VL_4 | !SI_4) & (!VL_4 | !drop1_4) & (!VL_4 | !drop2_4) &
(!VS_4 | !SI_4) & (!VS_4 | !drop1_4) & (!VS_4 | !drop2_4) &
(!SI_4 | !drop1_4) & (!SI_4 | !drop2_4) &
(!drop1_4 | !drop2_4) &

%% at least one action %%
(LV_0 | LS_0 | VL_0 | VS_0 | SI_0 | drop1_0 | drop2_0) &
(LV_1 | LS_1 | VL_1 | VS_1 | SI_1 | drop1_1 | drop2_1) &
(LV_2 | LS_2 | VL_2 | VS_2 | SI_2 | drop1_2 | drop2_2) &
(LV_3 | LS_3 | VL_3 | VS_3 | SI_3 | drop1_3 | drop2_3) &
(LV_4 | LS_4 | VL_4 | VS_4 | SI_4 | drop1_4 | drop2_4) &

%% frame axioms %%
% set all of the goal states to true after it has been set to true for the first time
(Goal1_1 -> (Goal1_2 & Goal1_3 & Goal1_4 & Goal1_5)) &
(Goal1_2 -> (Goal1_3 & Goal1_4 & Goal1_5)) &
(Goal1_3 -> (Goal1_4 & Goal1_5)) &
(Goal1_4 -> Goal1_5) &

(Goal2_1 -> (Goal2_2 & Goal2_3 & Goal2_4 & Goal2_5)) &
(Goal2_2 -> (Goal2_3 & Goal2_4 & Goal2_5)) &
(Goal2_3 -> (Goal2_4 & Goal2_5)) &
(Goal2_4 -> Goal2_5) &

% if the goal changed from false to true the correct package had to be dropped off
((!Goal1_0 & Goal1_1) -> drop1_0) &
((!Goal1_1 & Goal1_2) -> drop1_1) &
((!Goal1_2 & Goal1_3) -> drop1_2) &
((!Goal1_3 & Goal1_4) -> drop1_3) &
((!Goal1_4 & Goal1_5) -> drop1_4) &

((!Goal2_0 & Goal2_1) -> drop2_0) &
((!Goal2_1 & Goal2_2) -> drop2_1) &
((!Goal2_2 & Goal2_3) -> drop2_2) &
((!Goal2_3 & Goal2_4) -> drop2_3) &
((!Goal2_4 & Goal2_5) -> drop2_4) &

% when a state changes from true to false after a timestep it means that we had to depart
((Linz_0 & !Linz_1) -> ( LV_0 | LS_0)) &
((Linz_1 & !Linz_2) -> ( LV_1 | LS_1)) &
((Linz_2 & !Linz_3) -> ( LV_2 | LS_2)) &
((Linz_3 & !Linz_4) -> ( LV_3 | LS_3)) &
((Linz_4 & !Linz_5) -> ( LV_4 | LS_4)) &

((Vienna_0 & !Vienna_1) -> ( VL_0 | VS_0)) &
((Vienna_1 & !Vienna_2) -> ( VL_1 | VS_1)) &
((Vienna_2 & !Vienna_3) -> ( VL_2 | VS_2)) &
((Vienna_3 & !Vienna_4) -> ( VL_3 | VS_3)) &
((Vienna_4 & !Vienna_5) -> ( VL_4 | VS_4)) &

((Salzburg_0 & !Salzburg_1) -> SI_0) &
((Salzburg_1 & !Salzburg_2) -> SI_1) &
((Salzburg_2 & !Salzburg_3) -> SI_2) &
((Salzburg_3 & !Salzburg_4) -> SI_3) &
((Salzburg_4 & !Salzburg_5) -> SI_4) &

% when a state changes from false to true after a timestep that means we had to arrive there
((!Linz_0 & Linz_1) -> VL_0) &
((!Linz_1 & Linz_2) -> VL_1) &
((!Linz_2 & Linz_3) -> VL_2) &
((!Linz_3 & Linz_4) -> VL_3) &
((!Linz_4 & Linz_5) -> VL_4) &

((!Vienna_0 & Vienna_1) -> LV_0) &
((!Vienna_1 & Vienna_2) -> LV_1) &
((!Vienna_2 & Vienna_3) -> LV_2) &
((!Vienna_3 & Vienna_4) -> LV_3) &
((!Vienna_4 & Vienna_5) -> LV_4) &

((!Salzburg_0 & Salzburg_1) -> (LS_0 | VS_0)) &
((!Salzburg_1 & Salzburg_2) -> (LS_1 | VS_1)) &
((!Salzburg_2 & Salzburg_3) -> (LS_2 | VS_2)) &
((!Salzburg_3 & Salzburg_4) -> (LS_3 | VS_3)) &
((!Salzburg_4 & Salzburg_5) -> (LS_4 | VS_4)) &

((!Innsbruck_0 & Innsbruck_1) -> SI_0) &
((!Innsbruck_1 & Innsbruck_2) -> SI_1) &
((!Innsbruck_2 & Innsbruck_3) -> SI_2) &
((!Innsbruck_3 & Innsbruck_4) -> SI_3) &
((!Innsbruck_4 & Innsbruck_5) -> SI_4) &

% when a Good is not there that was there before we had to drop it off
((Good1_0 & !Good1_1) -> drop1_0) &
((Good1_1 & !Good1_2) -> drop1_1) &
((Good1_2 & !Good1_3) -> drop1_2) &
((Good1_3 & !Good1_4) -> drop1_3) &
((Good1_4 & !Good1_5) -> drop1_4) &

((Good2_0 & !Good2_1) -> drop2_0) &
((Good2_1 & !Good2_2) -> drop2_1) &
((Good2_2 & !Good2_3) -> drop2_2) &
((Good2_3 & !Good2_4) -> drop2_3) &
((Good2_4 & !Good2_5) -> drop2_4) &

% when a Good is there that was not there before we had to have picked it up
((!Good1_0 & Good1_1) -> VL_0) &
((!Good1_1 & Good1_2) -> VL_1) &
((!Good1_2 & Good1_3) -> VL_2) &
((!Good1_3 & Good1_4) -> VL_3) &
((!Good1_4 & Good1_5) -> VL_4) &

((!Good2_0 & Good2_1) -> LV_0) &
((!Good2_1 & Good2_2) -> LV_1) &
((!Good2_2 & Good2_3) -> LV_2) &
((!Good2_3 & Good2_4) -> LV_3) &
((!Good2_4 & Good2_5) -> LV_4)

## Exercise Sheet 9

### Exercise 33

### Exercise 34

### Exercise 35

### Exercise 36


---

#### a)

?x0 ?y0 ?x1 ?y1 ?x2 ?y2 ?x3 ?y3 ?x4 ?y4 ?x5 ?y5 ?x6 ?y6 ?x7 ?y7
#x #y #x-next #y-next
( (((x <-> x0) & (y <-> y0) & (x-next <-> x1) & (y-next <-> y1)) |
((x <-> x1) & (y <-> y1) & (x-next <-> x2) & (y-next <-> y2)) |
((x <-> x2) & (y <-> y2) & (x-next <-> x3) & (y-next <-> y3)) |
((x <-> x3) & (y <-> y3) & (x-next <-> x4) & (y-next <-> y4)) |
((x <-> x4) & (y <-> y4) & (x-next <-> x5) & (y-next <-> y5)) |
((x <-> x5) & (y <-> y5) & (x-next <-> x6) & (y-next <-> y6)) |
((x <-> x6) & (y <-> y6) & (x-next <-> x7) & (y-next <-> y7)))
->
(((!x-next <-> (x & !y)) & (y-next <-> ((x & !y) | (!x & y)))) |
((x-next <-> (!x & !y)) & (y-next <-> x)))
) &
x0 & y0 & !x7 & !y7

---

#### b)

?x0 ?y0 ?x1 ?y1 ?x2 ?y2 ?x3 ?y3 ?x4 ?y4 ?x5 ?y5 ?x6 ?y6 ?x7 ?y7
#x #y #x-next #y-next
( (((x <-> x0) & (y <-> y0) & (x-next <-> x1) & (y-next <-> y1)) |
((x <-> x1) & (y <-> y1) & (x-next <-> x2) & (y-next <-> y2)) |
((x <-> x2) & (y <-> y2) & (x-next <-> x3) & (y-next <-> y3)) |
((x <-> x3) & (y <-> y3) & (x-next <-> x4) & (y-next <-> y4)) |
((x <-> x4) & (y <-> y4) & (x-next <-> x5) & (y-next <-> y5)) |
((x <-> x5) & (y <-> y5) & (x-next <-> x6) & (y-next <-> y6)) |
((x <-> x6) & (y <-> y6) & (x-next <-> x7) & (y-next <-> y7)))
->
(((!x-next <-> (x & !y)) & (y-next <-> ((x & !y) | (!x & y)))) |
((x-next <-> (!x & !y)) & (y-next <-> x)))
) &
x0 & y0 & y1 & y2 & y3 & y4 & y5 & !x7 & !y7

---

#### c)

?x0 ?y0 ?x1 ?y1 ?x2 ?y2 ?x3 ?y3 ?x4 ?y4 ?x5 ?y5 ?x6 ?y6
#x #y #x-next #y-next
( (((x <-> x0) & (y <-> y0) & (x-next <-> x1) & (y-next <-> y1)) |
((x <-> x1) & (y <-> y1) & (x-next <-> x2) & (y-next <-> y2)) |
((x <-> x2) & (y <-> y2) & (x-next <-> x3) & (y-next <-> y3)) |
((x <-> x3) & (y <-> y3) & (x-next <-> x4) & (y-next <-> y4)) |
((x <-> x4) & (y <-> y4) & (x-next <-> x5) & (y-next <-> y5)) |
((x <-> x5) & (y <-> y5) & (x-next <-> x6) & (y-next <-> y6)))
->
(((!x-next <-> (x & !y)) & (y-next <-> ((x & !y) | (!x & y)))) |
((x-next <-> (!x & !y)) & (y-next <-> x)))
) &
x0 & y0 & y1 & y2 & y3 & y4 & y5 & !x6 & !y6

## Exercise Sheet 10

### Exercise 37

### Exercise 38


### Exercise 39

### Exercise 40