labelled state transition system


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

A labelled state transition system (LTS) is a triple (S,Σ,) where S×Σ×S. Elements of Σ are called labels of the system. If (p,α,q), we write pα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 machinesMathworldPlanetmath. An automaton, for example, is just an LTS (S,) 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,), if we take the reflexive transitive closure of , then we get a binary relation on S called the reachability relation. In other words, for any pS, pp, and for any qS, if pq, then there is a finite sequencePlanetmathPlanetmath p=p1,pn+1=q, such that pipi+1 for i=1,n. When pq, we say that q is reachable from p.

For an LTS (S,) 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 algorithmMathworldPlanetmath:

  1. 1.

    Initially, circle all start states as accessible. If there are no start states, skip to step 5.

  2. 2.

    Then for each circled p, circle all q such that pq.

  3. 3.

    Then cross out each p after all q such pq have been circled.

  4. 4.

    Repeat the last two steps for each circled q. Do this until there are no more circled states.

  5. 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 deterministicMathworldPlanetmath if is a partial functionMathworldPlanetmath. Otherwise, it is non-deterministic.

Title labelled state transition system
Canonical name LabelledStateTransitionSystem
Date of creation 2013-03-22 19:23:20
Last modified on 2013-03-22 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