labelled state transition system

A state transition system (TS) is a pair $(S,\\rightarrow)$ , where $\\rightarrow$ is a binary relation on $S$ . Elements of $S$ are called states and elements of $\\rightarrow$ are called transitions. When $(p,q)\\in\\rightarrow$ , we write $p\\rightarrow q$ .

A labelled state transition system (LTS) is a triple $(S,\\Sigma,\\rightarrow)$ where $\\rightarrow\\subseteq S\\times\\Sigma\\times S$ . Elements of $\\Sigma$ are called labels of the system. If $(p,\\alpha,q)\\in\\rightarrow$ , we write $p\\lx@stackrel{{\\scriptstyle\\alpha}}{{\\rightarrow}}q$ . In this way, an LTS can be thought of as an STS where each transition is labelled (possibly by more than one label). On the other hand, any TS is just a LTS with one label and every transition has the same label.

Examples of LTS are mostly found in theoretical computer science, such as automata and Turing machines. An automaton, for example, is just an LTS $(S,\\rightarrow)$ with two distinguished mutually disjoint sets (subsets of $S$ ) of states: a set of start states, and a set of final or accept states.

Given an LTS $(S,\\rightarrow)$ , if we take the reflexive transitive closure of $\\rightarrow$ , then we get a binary relation $\\Rightarrow$ on $S$ called the reachability relation. In other words, for any $p\\in S$ , $p\\Rightarrow p$ , and for any $q\\in S$ , if $p\\Rightarrow q$ , then there is a finite sequence $p=p_{1},\\ldots p_{n+1}=q$ , such that $p_{i}\\rightarrow p_{i+1}$ for $i=1,\\ldots n$ . When $p\\Rightarrow q$ , we say that $q$ is reachable from $p$ .

For an LTS $(S,\\rightarrow)$ with a set $I$ of start states, a state is said to be inaccessible if it is not reachable from any start state. If $S$ is finite, one can use the one of the search techniques to find all inaccessible states of $S$ . Here’s a basic breadth-first search algorithm:

1.
Initially, circle all start states as accessible. If there are no start states, skip to step 5.
2.
Then for each circled $p$ , circle all $q$ such that $p\\rightarrow q$ .
3.
Then cross out each $p$ after all $q$ such $p\\rightarrow q$ have been circled.
4.
Repeat the last two steps for each circled $q$ . Do this until there are no more circled states.
5.
Finally, the states in $S$ are either crossed out or unmarked, and inaccessible states are precisely the unmarked states.

An LTS is said to be deterministic if $\\rightarrow$ is a partial function. Otherwise, it is non-deterministic.

单词	LabelledStateTransitionSystem
释义	labelled state transition system A state transition system (TS) is a pair $(S,\\rightarrow)$ , where $\\rightarrow$ is a binary relation on $S$ . Elements of $S$ are called states and elements of $\\rightarrow$ are called transitions. When $(p,q)\\in\\rightarrow$ , we write $p\\rightarrow q$ . A labelled state transition system (LTS) is a triple $(S,\\Sigma,\\rightarrow)$ where $\\rightarrow\\subseteq S\\times\\Sigma\\times S$ . Elements of $\\Sigma$ are called labels of the system. If $(p,\\alpha,q)\\in\\rightarrow$ , we write $p\\lx@stackrel{{\\scriptstyle\\alpha}}{{\\rightarrow}}q$ . In this way, an LTS can be thought of as an STS where each transition is labelled (possibly by more than one label). On the other hand, any TS is just a LTS with one label and every transition has the same label. Examples of LTS are mostly found in theoretical computer science, such as automata and Turing machines. An automaton, for example, is just an LTS $(S,\\rightarrow)$ with two distinguished mutually disjoint sets (subsets of $S$ ) of states: a set of start states, and a set of final or accept states. Given an LTS $(S,\\rightarrow)$ , if we take the reflexive transitive closure of $\\rightarrow$ , then we get a binary relation $\\Rightarrow$ on $S$ called the reachability relation. In other words, for any $p\\in S$ , $p\\Rightarrow p$ , and for any $q\\in S$ , if $p\\Rightarrow q$ , then there is a finite sequence $p=p_{1},\\ldots p_{n+1}=q$ , such that $p_{i}\\rightarrow p_{i+1}$ for $i=1,\\ldots n$ . When $p\\Rightarrow q$ , we say that $q$ is reachable from $p$ . For an LTS $(S,\\rightarrow)$ with a set $I$ of start states, a state is said to be inaccessible if it is not reachable from any start state. If $S$ is finite, one can use the one of the search techniques to find all inaccessible states of $S$ . Here’s a basic breadth-first search algorithm: 1. Initially, circle all start states as accessible. If there are no start states, skip to step 5. 2. Then for each circled $p$ , circle all $q$ such that $p\\rightarrow q$ . 3. Then cross out each $p$ after all $q$ such $p\\rightarrow q$ have been circled. 4. Repeat the last two steps for each circled $q$ . Do this until there are no more circled states. 5. Finally, the states in $S$ are either crossed out or unmarked, and inaccessible states are precisely the unmarked states. An LTS is said to be deterministic if $\\rightarrow$ is a partial function. Otherwise, it is non-deterministic.
随便看	Albert Einstein ALebesgueMeasurableButNonBorelSet a Lebesgue measurable but non-Borel set ALectureOnIntegrationByParts a lecture on integration by parts ALectureOnIntegrationBySubstitution a lecture on integration by substitution ALectureOnThePartialFractionDecompositionMethod a lecture on the partial fraction decomposition method ALectureOnTrigonometricIntegralsAndTrigonometricSubstitution A lecture on trigonometric integrals and trigonometric substitution AlephNumbers aleph numbers AlexanderGrothendieck Alexander Grothendieck AlexanderGrothendiecksBiographyWithHisMajorMathematicalContributions AlexanderGrothendiecksMathematicalgenealogy AlexanderGrothendiecksSeminarsAndBooks Alexander Grothendieck’s biography with his major mathematical contributions Alexander Grothendieck’s mathematical ‘genealogy’ Alexander Grothendieck’s seminars and books AlexanderTrick Alexander trick AlexandroffSpace Alexandroff space