A model consisting of a set of states, a transition relation , initial states , a set of atomic propositions, and a label function identifying which atomic propositions hold at each state. A path in a transition system follows permitted transitions. Some definitions omit labels or initial conditions; specify the convention used in each application.
A transition system whose edges carry action labels. A CSP operational semantics uses visible CSP events and the internal label .
A state with no successor in the transition relation. Assuming no terminal states makes every finite path in a transition system extendible and avoids choosing a separate convention for interpreting infinite-path temporal logic at a dead end.
A finite or infinite sequence of states in which for each consecutive pair. In infinite-path linear temporal logic semantics, paths are infinite; an initial path must also start in the specified initial set. Repeated states are allowed, unlike conventions for a simple path in a graph.
An infinite path in a transition system represented by a finite prefix followed by infinite repetition of a nonempty finite loop. If stored positions are and , the represented sequence is . The linear temporal logic condition holds exactly when occurs on the repeated part, and holds exactly when holds everywhere on that part.
A binary relation on the states of a system, with meaning that one permitted step changes to . A Boolean formula can encode a transition relation after choosing bits for the current and next states.
Articles by others on the same topic
A **transition system** is a mathematical model used to describe the behavior of a system in terms of states and transitions. It is particularly useful in fields such as computer science, particularly in the study of formal verification, automata theory, and modeling dynamic systems. A transition system is formally defined as a tuple \( T = (S, S_0, \Sigma, \rightarrow) \), where: - \( S \): A set of states.