labelled state transition system
A state transition system (TS) is a pair $(S,\to )$, where $\to $ is a binary relation^{} on $S$. Elements of $S$ are called states and elements of $\to $ are called transitions. When $(p,q)\in \to $, we write $p\to q$.
A labelled state transition system (LTS) is a triple $(S,\mathrm{\Sigma},\to )$ where $\to \subseteq S\times \mathrm{\Sigma}\times S$. Elements of $\mathrm{\Sigma}$ are called labels of the system. If $(p,\alpha ,q)\in \to $, we write $p\stackrel{\alpha}{\to}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,\to )$ 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,\to )$, if we take the reflexive transitive closure of $\to $, 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},\mathrm{\dots}{p}_{n+1}=q$, such that ${p}_{i}\to {p}_{i+1}$ for $i=1,\mathrm{\dots}n$. When $p\Rightarrow q$, we say that $q$ is reachable from $p$.
For an LTS $(S,\to )$ 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 breadthfirst 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\to q$.

3.
Then cross out each $p$ after all $q$ such $p\to 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 $\to $ is a partial function^{}. Otherwise, it is nondeterministic.
Title  labelled state transition system 
Canonical name  LabelledStateTransitionSystem 
Date of creation  20130322 19:23:20 
Last modified on  20130322 19:23:20 
Owner  CWoo (3771) 
Last modified by  CWoo (3771) 
Numerical id  17 
Author  CWoo (3771) 
Entry type  Definition 
Classification  msc 03B45 
Classification  msc 68Q85 
Classification  msc 68Q10 
Synonym  labeled state transition system 
Synonym  TS 
Synonym  LTS 
Synonym  STS 
Synonym  LSTS 
Related topic  SemiThueSystem 
Defines  state transition system 
Defines  reachability 
Defines  reachable 
Defines  inaccessible state 