LTS and Simulations

Question 1

What is a Labelled Transition System? (Mathematically)

Answer 1

(X, Σ, L)
where 
    X = states
    Σ = alphabet of actions
    L = X x Σ x X

Question 2

Why are Labelled Transition Systems used?

Answer 2

To capture what can be observed about a program.

Question 3

What is internal no-determinism?

Answer 3

ND that is resolved by the scheduler.

“The machine chooses”.

Question 4

What is external non-determinism?

Answer 4

ND that is influenced by the external environment.

E.g. a vending machine and a user.

Question 5

What is trace equivalence?

Answer 5

2 states that have the same traces.

Question 6

What is a trace?

Answer 6

A sequence of observations from some state.

Question 7

Are traces always finite?

Answer 7

No

Question 8

What is a simulation, formally?

Answer 8

A relation on a set R s.t:
whenever xRy and x -a-> x’, there exists y’ s.t. y -a-> y’ and (x’,y’) ∈ R.
If (x,y) ∈ R, we say that y simulates x.

Question 9

What does x<=y mean?

Answer 9

y simulates x.

Question 10

What does y<=x mean?

Answer 10

x simulates y.

Question 11

What are the properties of simulation? (2)

Answer 11

The union of simulations are simulations.

The largest simulation is the similarity (union of all simulations).

Question 12

What is the simulation game? (4)

Answer 12

Game starts at (x,y).

1. Demon picks x-a->x’.
2. We respond with y-a-> y’.
3. Game repeats from new start point (x’,y’).

Question 13

What are the terminating conditions of the simulation game? [Start=(x,y)] (3)

Answer 13

If we can’t move, we lose.
If the demon has a winning strategy, y does NOT simulate x.
If we win, y simulates x (x<=y).

Question 14

What is simulation equivalence?

Answer 14

If x<=y and y<=x, then x and y are simulation equivalent.

Question 15

What are the implications of simulation equivalence?

Answer 15

If x and y are simulation equivalent, x and y are also trace equivalent.
The converse is NOT true.

Question 16

What is coarse and fine equivalence?

Answer 16

The amount something distinguishes about a system.

Fine equivalence distinguishes more than coarse equivalence.

Question 17

What is a bisimulation? (x~y)

Answer 17

A simulation that goes both ways.

R and its reverese are simulations.

Question 18

What is a bisimulation, formally?

Answer 18

A relation on states s.t:
if x -a-> x’, then there exists y’ s.t. y -a-> y’ and (x’,y’) ∈ R.
if y -a-> y’, then there exists x’ s.t. x-a-> x’ and (x’,y’) ∈ R.

Question 19

What are the properties of bisimulation?

Answer 19

The union of bisimulations is a bisimulation.

The largest bisimulation is the bisimilarity.

Question 20

What is the bisimulation game? (5)

Answer 20

Start at (x,y).

1. Demon choses whether to start at x or y.
2. If D choses x-a>x’, then we chose a y’ s.t y-a->y’.
3. If D choses y-a-> y’, then we chose a x’ s.t. x-a->x’.
4. Game restarts from new start position: (x’,y’).