State transition system
A transition system ( engl. transition system) describes in automata theory, the possible states of a state-based system and the possible transitions (transitions) between these states.
A distinction is made discrete and continuous systems. Usually one considers only discrete systems, because they can be much more easily checked.
A further distinction is deterministic and non-deterministic transition systems. In the first case, a state and a transition is associated with more than one successor state, while in the non-deterministic event, the same state may have a plurality of transition successor states. Deterministic transition systems in this sense are special cases of nondeterministic transition systems.
A transition system can be used to illustrate certain features of a state-based system, in particular the Terminiertheit. For this reason it is used to verify the correctness of algorithms. Also to prove the absence of deadlocks and distributed systems, this construct can be applied.
Formal definition
Formally, a discrete transition system is described by a quadruple, where
- Is a set of states.
- Is a non -empty set of initial states.
- Is a finite alphabet with. The elements of A are called markers (german label) of TS.
- Is the transition relation of which determines for each state and each input character, exist which successor states.
The transition system thus corresponds to a finite automaton, except that the set of states must be finite and the transition relation can not therefore be arbitrarily complex. Even this seemingly small extensions cause Transition systems are generally Turing powerful.
A transition system is called deterministic if the following two conditions are met:
- Contains exactly one element.
- If, then it follows for all with and also.
In each state is so clearly defined for each input character, which must be the next state.
Properties
A transition system is called finite if the set of states is finite. A finite transition system is a finite state machine. Such transition systems can be represented as a transition diagram: It generally forms a directed cyclic graphs with named edges.
With (mostly ) finite graph is concerned, a whole branch of theoretical computer science, the so-called model verification ( model checking ). The aim is to check the in one language ( for example, Guarded Commands, Petri nets ) defined transition system automatically to determine whether it satisfies a specification that also in an appropriate language (usually a Temporal logic as LTL, CTL or CTL * ) is given.
Examples
Traffic lights
A traffic light can be understood as a transition system. A traffic light has the five states. In normal operation, the light changes its 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.
Deterministic finite automaton
The graph shown above is a DEA with the three states, and. The state is a final state. The alphabet consists of both letters and numbers. Other letters are not accepted by the automaton. The regular expression matches the language that accepts this DEA.