Transition system

A transition system (English transition system in) describes automata theory , the possible states of a state based system and the possible transitions (transitions) between these states.

A distinction is made between discrete and continuous systems. As a rule, only discrete systems are considered, as these can be checked much more easily.

Furthermore, a distinction is made between deterministic and nondeterministic transition systems. In the first case, a state and a transition are assigned at most one subsequent state, while in the nondeterministic case, the same state can have several subsequent states for a transition. In this sense, deterministic transition systems are special cases of nondeterministic transition systems.

A transition system can be used to show certain properties of a state-based system, in particular its termination . For this reason it is used to verify the correctness of algorithms . Also to prove the deadlocks of distributed systems , this construct can be applied.

Formal definition

Formally, a discrete transition system is described by a quadruple , where ${\displaystyle TS=(S,S_{0},A,T)}$

• ${\displaystyle S}$ is a lot of states.
• ${\displaystyle S_{0}\subseteq S}$ is a non-empty set of starting states.
• ${\displaystyle A}$is a finite alphabet where . The elements of A are called TS labels . ${\displaystyle S\cap A=\emptyset }$
• ${\displaystyle T\subseteq S\times A\times S}$is the transition relation of which determines for each state and each input character which successor states exist. ${\displaystyle TS}$

The transition system corresponds to a finite automaton , except that the state set does not have to be finite and the transition relation can therefore be arbitrarily complex. Even these seemingly small extensions mean that transition systems are generally powerful in Turing .

A transition system is called deterministic if the following two conditions are met:

• ${\displaystyle S_{0}}$ contains exactly one element.
• If so , then follows for everyone with and also . ${\displaystyle (z_{0},a,z_{1})\in T}$ ${\displaystyle (w_{0},b,w_{1})\in T}$ ${\displaystyle w_{0}=z_{0}}$ ${\displaystyle b=a}$ ${\displaystyle w_{1}=z_{1}}$

In each state it is therefore clearly defined for each input character what the next state must be.

properties

A transition system is called finite if the set of states is finite. A finite transition system is a finite automaton. Such transition systems can be represented as a transition diagram: It generally forms a directed cyclic graph with named edges. ${\displaystyle S}$

With (mostly) finite graph is concerned, a whole branch of theoretical computer science , the so-called model checking ( model checking ). The aim is to automatically check the transition system defined in a language ( e.g. Guarded Commands , Petri-Netze ) whether it fulfills a specification that is also written in a suitable language (usually a temporal logic such as LTL , CTL or CTL * ) given is.

Examples

traffic light

A traffic light can be understood as a transition system. A traffic light has the five states . In normal operation the light changes their states in the following order: . In addition, a traffic light has a night mode: . The description of these two cycles as a change of state is called a transition system. ${\displaystyle \{rot,rot-gelb,gruen,gelb,aus\}}$ ${\displaystyle rot\ {\overrightarrow {a}}\ rot-gelb\ {\overrightarrow {a}}\ gruen\ {\overrightarrow {a}}\ gelb\ {\overrightarrow {a}}\ rot}$ ${\displaystyle gelb\ {\overrightarrow {b}}\ aus\ {\overrightarrow {b}}\ gelb}$

Deterministic finite automaton

The graph above is a DEA with the three states , and . The state is an end state. The alphabet consists of the two letters and . The machine does not accept any other letters. The regular expression corresponds to the language that this DEA accepts. ${\displaystyle S_{0}}$ ${\displaystyle S_{1}}$ ${\displaystyle S_{2}}$ ${\displaystyle S_{1}}$ ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle a^{*}b(a^{+}b|b^{+}a)^{*}}$

literature

• John E. Hopcroft , Jeffrey Ullman : Introduction to Automata Theory, Formal Languages, and Complexity Theory . 2nd Edition. Addison-Wesley , Bonn, Munich 1990, ISBN 3-89319-181-X (Original title: Introduction to automata theory, languages ​​and computation .).
• Peter Sander, Wolffried Stucky, Rudolf Herschel: Automata, Languages, Computability , ISBN 3-519-02937-5