State transition system
Encyclopedia
In theoretical computer science
, a state transition system is an abstract machine
used in the study of computation
. The machine consists of a set of states
and transitions between states, which may be labeled with labels chosen from a set; the same label may appear on more than one transition. If the label set is a singleton, the system is essentially unlabeled, and a simpler definition that omits the labels is possible.
State transition systems coincide mathematically with abstract rewriting system
s (as explained further in this article). State transition systems differ however from finite state automata in several ways:
State transition systems can be represented as directed graph
s.
(S, →) where S is a set (of states) and → ⊆ S × S is a binary relation
over S (of transitions). If p, q ∈ S, (p, q) ∈ → is usually written as p → q. This represents the fact that there is a transition from state p to state q.
A labelled transition system is a tuple (S, Λ, →) where S is a set (of states), Λ is a set (of labels) and → ⊆ S × Λ × S is a ternary relation (of labelled transitions). If p, q ∈ S and α ∈ Λ, then (p,α,q) ∈ → is written as
Theoretical computer science
Theoretical computer science is a division or subset of general computer science and mathematics which focuses on more abstract or mathematical aspects of computing....
, a state transition system is an abstract machine
Abstract machine
An abstract machine, also called an abstract computer, is a theoretical model of a computer hardware or software system used in automata theory...
used in the study of computation
Computation
Computation is defined as any type of calculation. Also defined as use of computer technology in Information processing.Computation is a process following a well-defined model understood and expressed in an algorithm, protocol, network topology, etc...
. The machine consists of a set of states
State (computer science)
In computer science and automata theory, a state is a unique configuration of information in a program or machine. It is a concept that occasionally extends into some forms of systems programming such as lexers and parsers....
and transitions between states, which may be labeled with labels chosen from a set; the same label may appear on more than one transition. If the label set is a singleton, the system is essentially unlabeled, and a simpler definition that omits the labels is possible.
State transition systems coincide mathematically with abstract rewriting system
Abstract rewriting system
In mathematical logic and theoretical computer science, an abstract rewriting system is a formalism that captures the quintessential notion and properties of rewriting systems...
s (as explained further in this article). State transition systems differ however from finite state automata in several ways:
- In a state transition system the set of states is not necessarily finite, or even countable.
- In a state transition system the set of transitions is not necessarily finite, or even countable.
- A finite-state automaton distinguishes a special "start" state and a set of special "final" states.
State transition systems can be represented as directed graph
Directed graph
A directed graph or digraph is a pair G= of:* a set V, whose elements are called vertices or nodes,...
s.
Formal definition
Formally, an unlabelled state transition system is a tupleTuple
In mathematics and computer science, a tuple is an ordered list of elements. In set theory, an n-tuple is a sequence of n elements, where n is a positive integer. There is also one 0-tuple, an empty sequence. An n-tuple is defined inductively using the construction of an ordered pair...
(S, →) where S is a set (of states) and → ⊆ S × S is a binary relation
Binary relation
In mathematics, a binary relation on a set A is a collection of ordered pairs of elements of A. In other words, it is a subset of the Cartesian product A2 = . More generally, a binary relation between two sets A and B is a subset of...
over S (of transitions). If p, q ∈ S, (p, q) ∈ → is usually written as p → q. This represents the fact that there is a transition from state p to state q.
A labelled transition system is a tuple (S, Λ, →) where S is a set (of states), Λ is a set (of labels) and → ⊆ S × Λ × S is a ternary relation (of labelled transitions). If p, q ∈ S and α ∈ Λ, then (p,α,q) ∈ → is written as
-
This represents the fact that there is a transition from state p to state q with label α. Labels can represent different things depending on the language of interest. Typical uses of labels include representing input expected, conditions that must be true to trigger the transition, or actions performed during the transition.
If, for any given p and α, there exists only a single tuple (p,α,q) in →, then one says that α is deterministic (for p). If, for any given p and α, there exists at least one tuple (p,α,q) in →, then one says that α is executable (for p).
Relation between labelled and unlabelled transition systems.
There are many relations between these concepts. Some are simple, such as observing that a labelled transition system where the set of labels consists of only one element is equivalent to an unlabelled transition system. However not all these relations are equally trivial.
Comparison with abstract rewriting systems
As a mathematical object, an unlabeled state transition system is identical with an (unindexed) abstract rewriting systemAbstract rewriting systemIn mathematical logic and theoretical computer science, an abstract rewriting system is a formalism that captures the quintessential notion and properties of rewriting systems...
. If we consider the rewriting relation as an indexed set of relations, as some authors do, then a labeled state transition system is equivalent with an abstract rewriting system with the indices being the labels. The focus of the study and the terminology are different however. In a state transition system one is interested in interpreting the labels as actions, whereas in an ARS the focus is on how objects may be transformed (rewritten) into others.
Extensions
In model checkingModel checkingIn computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
, a state transition system is sometimes defined to include an additional labeling function for the states as well, resulting in a notion that encompasses that of Kripke structureKripke structureA Kripke structure is a type of nondeterministic finite state machine proposed by Saul Kripke , used in model checking to represent the behavior of a system.It is a simple abstract machine to capture an idea of a computing machine,...
.
Action languageAction languageIn computer science, an action language is a language for specifying state transition systems, and is commonly used to create formal models of the effects of actions on the world...
s are a special case of transition systems, adding a set of fluents F, a set of values V, and a function that maps F × S to V.
See also
- Simulation preorderSimulation preorderIn theoretical computer science a simulation preorder is a relation between state transition systems associating systems which behave in the same way in the sense that one system simulates the other....
- BisimulationBisimulationIn theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems which behave in the same way in the sense that one system simulates the other and vice-versa....
- Operational semanticsOperational semanticsIn computer science, operational semantics is a way to give meaning to computer programs in a mathematically rigorous way. Operational semantics are classified into two categories: structural operational semantics formally describe how the individual steps of a computation take place in a...
- Kripke structureKripke structureA Kripke structure is a type of nondeterministic finite state machine proposed by Saul Kripke , used in model checking to represent the behavior of a system.It is a simple abstract machine to capture an idea of a computing machine,...
- Simulation preorder