This is a learning note of a course in CISPA, UdS. Taught by Swen Jacobs
Labeled Transition Systems (LTS)
LTS is a concept in theoretical computer science used in the study of computation. It is used to describe the potential behavior of discrete systems, e.g. Model Checking.
It consists 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. Mathematically, it can be described as directed graph.
Labels
Labels can be used to describe the behaviour or distinguish between states.
If the set of label is a singleton (only contains one label), then it can be omitted in the system.
LTS v.s. Finite-state Automata
In Transition systems:
- The set of states is not necessarily finite, or even countable.
- The set of transitions is not necessarily finite, or even countable.
- No “start” state or “final” states are given.
Formal definition
Let $AP$ be a set of atomic propositions (statement or assertion that must be true or false),
i.e., observable properties of the system.
A labeled transition system (LTS) over $AP$ is a tuple $Q, Q_0, \Sigma, \delta, \lambda$, where
- $Q$ is a set of states
- $Q_0 \subseteq Q$ is the set of initial states
- $\Sigma$ is the set of transition labels (or actions)
- $\delta \subseteq Q \times \Sigma \times Q$ is the transition relation (also write as $ q\buildrel a \over\rightarrow q’ \in \delta$)
- $\lambda : Q \rightarrow 2^{AP}$ is the state labeling.
In this course, we assume finite LTS, which means $AP$ and $Q$ are finite, unless explicitly stated.
Run of an LTS
Consider an LTS $M = (Q, Q_0, \Sigma, \delta, \lambda)$.
Path
A path of $M$ an is a finite sequence $q_0a_0q_1a_1…q_n \in (Q\Sigma)\ast Q$, such that $ q_i \buildrel a_i \over\rightarrow q_{i+1}$ for all $i < n$
or an infinite sequence $q_0a_0q_1a_1…q_n \in (Q\Sigma)^\omega$, such that $ q_i \buildrel a_i \over\rightarrow q_{i+1}$ for all $i \in \mathbb{N}$.
Run
A run of $M$ is a path of $M$ with $q_0 \in Q_0$, and that is maximal, i.e., it cannot be extended.
A run is deadlocked if it is finite.
State-labeled paths
$q_0q_1…$, the projection of a path onto states $Q$,
Action-labeled paths
$a_0a_1…$, the projection of a path onto actions $\Sigma$,
Traces
$\lambda (q_0)\lambda q_1…$, the sequence of labels of a state-labeled path.
Next post: Synchronization Primitives of Processes
Further Reading: Transition System, Model Checking.
Please cite the source for reprints, feel free to verify the sources cited in the article, and point out any errors or lack of clarity of expression. You can comment in the comments section below or email to GreenMeeple@yahoo.com