deck_15621990 Flashcards

1
Q

What is a labelled transition system?

A

A formal representation of the states, the stepwise behaviour, and the initial states of a system.

A tuple (S, s0, Act, ->) where:
- S is the set of states
- s0 is the intial state
- Act is a set of actions
- -> subset of (S * (Act U {pi}) * S) is a transition relation

where pi is an internal action

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
2
Q

What is an internal action

A

An internal action is an ordinary action which we cannot directly observe

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
3
Q

What are the predecessors of a state s

A

The predecessors of a state s’ are all of the states such that there exists an action for which the LTS transitions from s’ to s.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
4
Q

What are the successors of a state s

A

All states s’ for which there exists an action for which the LTS transitions from s to s’.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
5
Q

The traces of a given state s are

A

all of those combinations of actions (including internal actions) that can start in state s and take the LTS to some other state

represented by a line with two arrows

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
6
Q

The traces of a given LTS

A

are the traces of the initial state of that LTS

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
7
Q

Weak traces

A

consider internal transitions silent or unobservable

still consider them, but the internal transitions are just not mentioned in the traces

represented by an implication sign

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
8
Q

s after y meaning

A

the set of states that can be reached by s after following the weak trace y

since this is a weak trace, internal transitions are allowed at any point

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
9
Q

S’ after y (where S’ is a set of states)

A

the set of states reached after following trace y from any of the sets in S’

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
10
Q

Reach(s) meaning

A

the set of states for which there exists a trace such that they can be reached from s by following that trace

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
11
Q

The reachable states of an LTS are

A

all of the states reachable from the LTS’ initial state

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
12
Q

When is an LTS without internal transitions deterministic?

A

When for all combinations of three states and one action, if one state can follow that same action to two of the states, then those states are the same state.

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
13
Q

When is an LTS with internal transitions determinstic?

A

Never, LTS’s with internal transitions are alwasys considered non-deterministic

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
14
Q

Parallel Composition of LTS’s

A

First, one needs a set of handshaking actions H, which are a subset of the intersection of the sets of actions of the two LTS’s

Then, the parallel composition LTS is as follows:

S: S1 * S2
s0 = (s10, s20)
Act = Act1 U Act2

and -> is as follows

For all actions in H:

(s1,t1)->a(s2,t2) only if s1 goes to s2 with a in LTS 1 and t1 goes t2 in LTS2.

For all actions not in H:
(s1,t1)->a(s2,t1) if s1->as2 in LTS1
(s1,t1)->a(s1,t2) if t1->t2 in LTS2

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
15
Q

Three Types of States in State Machine Diagrams

A
  1. Basic states:
    - simple state, no nested states inside
  2. Composite state / Or:
    - at most one nested state inside is current
  3. Orthogonal / And:
    - each region is current, and is itself considered an or-state
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
16
Q

What are the children of a basic state?

A

it has no children

17
Q

What are the children of an or state?

A

The states contained directly inside

18
Q

What are the children of an and state?

A

All of the different regions inside at depth 1

19
Q

What are the descendants of a state s

A

The state s, its children and all of the descendants of its children

20
Q

What are the ancestors of s?

A

All of the states for which s is a descendant

21
Q

What are strict descendants/ascendants?

A

The descendants/ascendants excluding the state itself

22
Q

The state configuration with respect to a state s is:

A

a subset of the descendants of s such that:

s is in the configuration
for every or-state in the configuration, exactly one child of it is in the configuration
for every and state in the configuration, all children of it are in the configuration

23
Q

What is a transition, formally, in a state machine diagram?

A

A transition is a tuple (ss, Et, C, Eg, st) where:

ss is the source state
Et are the trigger event(s)
C are the guards
Eg are the generated events
st is the target state

24
Q

Least common strict or-ancestor (LCSOA)

A

the or-state having all the states in the set as descendants, while being closest in hierarchy distance to these states

if there is no such or-state, it is said that the lcsoa is “root”

25
Q

What is the scope of a given transition?

A

The lcsoa of the source and target state

26
Q

The unique exit state of a transition

A

The state that is both:
1. the child of the scope of transition
2. the ancestor of the source of the transition

captures the part of the configuration left when executing the transition

27
Q

The exit set of a transition

A

The unique exit state plus all its descendants in the current configuration

28
Q

The unique enter state of a transition

A

The state satisfying both the conditions:
1. the child of the scope of transition
2. ancestor of the target of the transition

captures the (sub)configuration entered when executing the transition

29
Q

The enter set of a transition

A

the target state and all descendant of the unique enter set that are not ancestors of the target state

30
Q

Situation

A

a pair st = (conf, Ev) where:
- conf is a configuration
- Ev are the available events

31
Q

When is a transition tr with dispatched event f and situation (conf,Ev) enabled?

A

It is enabled if and only if:
1. its source state is in the configuration
2. the dispatched event is a trigger of the transition
3. the guard is satisfied

32
Q

When is a transition tr with dispatched event e at situation st=(conf,Ev) fireable>

A

When:
1. The transition is enabled for that event and situation.
2. For all other enabled transitions for that event and situation, their source state is not a strict descendant of the source state of this transition’s source state.

33
Q

When are two transitions conflicting in a configuration?

A

Two transitions are conflicting in a configuration if and only if their exit sets overlap.