Labelled transition systems
An LTS consists of a set of states and a set of transitions between those states. These transitions are labelled by actions and one state is designated as the initial state.
Formally, an LTS is a tuple where:
is a (finite) set of states;
is a set of actions;
is a transition relation;
is the initial state.
For any set of actions we denote by
the set of all finite
sequences of elements of
. An element of
is called an
action sequence or trace and the empty trace is denoted by
.
For any LTS , states
and action
sequence
, with
for some
, we denote by
the fact that there exist
such that
,
, and
for all
. Note that
for all states
it holds that
.
An LTS usually describes the (discrete) behaviour of some system or protocol: in any state of the system, a number of actions can be performed, each of which leads to a new state. The initial state corresponds to the state in which the system resides before any action has been performed.
This LTS model can be extended in various ways. We briefly describe the addition of internal actions and of state values below.
Internal actions
When studying the behaviour of a system, one often wants to view the system as a
black box. Only the interactions of the system with its environment are of
interest and all internal behaviour should be hidden. For this, a special action
called the internal action is introduced. It is often designated by
. The internal behaviour of a system can now be hidden by renaming
all actions that it performs internally, to
. In the LTS model, the
is a special label that can be carried by a transition.
We can then consider traces between states on which any number of actions
may occur in between; we do not care how many. For convenience we introduce
additional notation to express this. Let
denote any finite sequence of
actions.
For any LTS , states
and action
sequence
, with
for
, we denote by
the fact that there exist
such that
, and
for
all
.
State values
The state of a system can be defined as the combination of the values of all relevant parameters or variables. Hence, the LTS model can be extended by associating a state vector with every state. This is the list of parameters along with their values in that specific state.
Formally, we write a state vector declaration as a tuple where
is the name and
is the domain
(the set of possible values) of parameter
. The set of states of an LTS
now becomes a subset of
. Hence, every state
is an n-tuple that contains one specific value for every declared parameter.
Equivalences
Given two LTSs, a natural question is whether they describe the same behaviour. To answer this question we must first specify what we mean by “the same”. For example, are we satisfied if both LTSs can perform the same sequences of actions (starting from their initial states) or do we want to impose stricter criteria? In other words, we have to specify when we consider two LTSs to be equivalent.
Various notions of equivalence have been defined in the literature. Some are finer than others, meaning that the criteria that two LTSs should meet for them to be called equivalent, are stronger. The equivalences that we consider here are explained in the following sections.
Trace equivalence
According to trace equivalence, two LTSs are equivalent if and only if they can perform the same sequences of actions, starting from their initial states.
Formally, for any LTS and state
we
define
to be the set of traces possible from
:
Given two LTSs and
,
we say that
and
are trace equivalent iff
.
Weak trace equivalence
Weak trace equivalence* is very similar to trace equivalence. The only
difference is that it “skips” any actions that appear on the traces.
Hence, weak trace equivalence is particularly useful when some parts of the
behaviour have been hidden.
For example, if one LTS describes the desired, external behaviour of a system
and another LTS describes its implementation with internal actions renamed to
, then a natural question would be whether the two LTSs are weakly trace
equivalent. In this case, “normal” trace equivalence would be too strong.
Formally, for any LTS and state
we
define
to be the set of weak traces possible from
:
Given two LTSs and
,
we say that
and
are weakly trace equivalent iff
.
Obviously, if then there exists a sequence
(possibly containing
steps) such that
.
Using this fact, it is not hard to see that if two LTSs are trace equivalent
then they are also weakly trace equivalent.
Strong bisimilarity
Strong bisimilarity (or strong bisimulation equivalence) relates two LTSs in
the following way: if one LTS can perform an action then the other LTS
must also be able to perform an
action and in such a way that the
resulting states are again related. This relation works both ways simultaneously
(which is suggested by the “bi-” prefix in the name of the equivalence).
The formal definition is as follows.
A relation
on the states of an LTS is called a simulation if for any states
and action
, if
and
then there exists a state
such that
and
.
A symmetric simulation is called a bisimulation.
Two states
and
are called strongly bisimilar (or strongly bisimulation equivalent) iff there exists a bisimulation
such that
.
Given two LTSs
and
, we say that
and
are strongly bisimilar iff
and
are strongly bisimilar.

These LTSs are trace equivalent, but not strongly bisimilar.
Strong bisimilarity is a finer equivalence than trace equivalence, meaning it is stricter and relates less LTSs.
An example showing the difference between strong bisimilarity and trace equivalence is given in the figure above. These LTSs model a game show in which the contestant can open one of two doors to determine the prize he/she will win. Behind one is a very luxurious car, behind the other a nice bouquet of flowers. In the red model, the contestant can somehow still choose the prize after opening a door. In the blue model, the choice is made as soon as he/she opens a door.
According to trace equivalence, these models are equivalent. However, strong bisimilarity distinguishes the two: the blue model can simulate the open_door action by the red model, but in each of the resulting states it cannot simulate one of the win actions that the red model can perform.
Branching bisimilarity
Branching bisimilarity (or branching bisimulation equivalence) is a variant
of strong bisimilarity that treats actions in a special way. In
cases where one of the LTSs under comparison contains internal actions, strong
bisimilarity is often too strict and branching bisimilarity makes more sense.
The idea behind branching bisimilarity is that an LTS may skip
actions when simulating an action of the other LTS, but the intermediate states
need to be related. (If the latter requirement is lifted, we obtain an
equivalence known as weak bisimilarity.)
Branching bisimilarity is formally defined as follows.
A relation
on the states of an LTS is called a branching simulation if for any states
and action
, if
and
then:
either
and
or there exist states
such that
and
and
.
A symmetric branching simulation is called a branching bisimulation.
Two states
and
are called branching bisimilar (or branching bisimulation equivalent) iff there exists a branching bisimulation
such that
.
Given two LTSs
and
, we say that
and
are branching bisimilar iff
and
are branching bisimilar.
Isomorphism
One of the strongest equivalences is isomorphism. Two labelled transition systems are isomorphic if their structure is exactly the same. To compare, trace equivalence preserves a minimal amount of structure; only the order in which actions can occur is preserved. Bisimilarity, on the other hand, also preserves the branching structure.
Formally, two LTSs and
are isomorphic if, and only if,
and there is a bijective
function
mapping states from
to
such that
and
, for some
,
if and only if
.
Effectively this means that the isomorphic LTSs are only allowed to differ in their labelling of states.
Determinism
An LTS is called deterministic if for every state and action
,
there is at most one state
such that
. (Note
that in the classical definition of determinism, in the context of finite state
acceptors, there should be precisely one such
for every
and
.)
For example, in the figure above, the red LTS is deterministic, while the blue one is not.
For deterministic LTSs, trace equivalence and strong bisimilarity coincide. This means that two LTSs are trace equivalent if and only if they are strongly bisimilar. As mentioned before, for nondeterministic LTSs we do not have the only if part, just the if part.
We can also refer to determinism modulo an equivalence. We say an LTS
is deterministic modulo an equivalence
if, and only if, there is a
deterministic LTS that is
-equivalent to
. Note that modulo trace
equivalence every LTS is deterministic and that the normal notion of determinism
(i.e. without modulo) corresponds to determinism modulo isomorphism.