Views

Toolbox

LTS library

From MCRL2

Jump to: navigation, search

1 Introduction
2 Concepts
3 Structure
4 Tutorial
- 4.1 Creating an LTS
- 4.2 Read, reduce and print
5 Reference
6 Author

Introduction

The LTS library provides data structures and methods to handle labelled transition systems (LTS). Using the library, an LTS can be read from/written to file (various file formats are supported), minimised using various equivalences, determinised, and analysed.

This manual gives an overview of the library's structure and explains how to program with the library. First, the relevant concepts are introduced and defined.

Note that the current implementation of this library is mainly focussed on creating LTSs. That is, it is easy to add states, transitions and labels, but there is virtually no functionality to change or remove parts of an LTS.

Concepts

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 (S,A,→,s₀) where:

S is a (finite) set of states;
A is a set of actions;
→ ⊆ S × A × S is a transition relation;
s₀ ∈ S is the initial state.

For any set of actions A we denote by A^* the set of all finite sequences of elements of A. An element of A^* is called an action sequence or trace and the empty trace is denoted by ε. For any LTS (S,A,→,s₀), states s,t ∈ S and action sequence σ ∈ A^*, with σ = a₁ … a_n for n ≥ 0, we denote by s →^σ t the fact that there exist s₀,…,s_n ∈ S such that s = s₀, t = s_n, and (s_i,a_i+1,s_i+1) ∈ → for all i, 0 ≤ i < n. Note that for all states s it holds that s →^ε s.

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 (S,A,→,s₀), states s,t ∈ S and action sequence σ ∈ (A \ {τ})^*, with σ = a₁ … a_n for n ≥ 0, we denote by s ⇒^σ t the fact that there exist s₀,…,s_n ∈ S such that s = s₀, t = s_n, and s_i →^{(τ* a_i+1)} s_i+1 for all i, 0 ≤ i < n.

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 (d₁ : D₁ , … , d_n : D_n) where d_i is the name and D_i is the domain (the set of possible values) of parameter i. The set of states of an LTS now becomes a subset of D₁ × … × D_n. 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 (S,A,→,s₀) and state s ∈ S we define Tr(s) to be the set of traces possible from s:

Tr(s) = { σ ∈ A^* | ∃ t ∈ S . s →^σ t }

Given two LTSs T = (S,A,→,s₀) and T’ = (S’,A’,→’,s₀’), we say that T and T’ are trace equivalent iff Tr(s₀) = Tr(s₀’).

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 (S,A,→,s₀) and state s ∈ S we define Tr_w(s) to be the set of weak traces possible from s:

Tr_w(s) = { σ ∈ (A \ {τ})^* | ∃ t ∈ S . s ⇒^σ t }

Given two LTSs T = (S,A,→,s₀) and T’ = (S’,A’,→’,s₀’), we say that T and T’ are weakly trace equivalent iff Tr_w(s₀) = Tr_w(s₀’).

Obviously, if s ⇒^σ t then there exists a sequence π (possibly containing τs) such that s →^π t. 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 a then the other LTS must also be able to perform an a 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 R on the states of an LTS is called a simulation if for any states s, s’, t and action a, if s →^a s’ and s R t then there exists a state t’ such that t →^a t’ and s’ R t’.
A symmetric simulation is called a bisimulation.
Two states s and t are called strongly bisimilar (or strongly bisimulation equivalent) iff there exists a bisimulation R such that s R t.
Given two LTSs T = (S,A,→,s₀) and T’ = (S’,A’,→’,s₀’), we say that T and T’ are strongly bisimilar iff s₀ and s₀’ 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 R on the states of an LTS is called a branching simulation if for any states s, s’, t and action a, if s →^a s’ and s R t then:
- either a = τ and s’ R t;
- or there exist states t₁, t₂, t’ such that t →^τ* t₁ →^a t₂ →^τ* t’ and s R t₁, s’ R t₂ and s’ R t’.
A symmetric branching simulation is called a branching bisimulation.
Two states s and t are called branching bisimilar (or branching bisimulation equivalent) iff there exists a branching bisimulation R such that s R t.
Given two LTSs T = (S,A,→,s₀) and T’ = (S’,A’,→’,s₀’), we say that T and T’ are branching bisimilar iff s₀ and s₀’ 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 T = (S,A,→,s₀) and T’ = (S’,A’,→’,s₀’) are isomorphic if, and only if, A = A’ and there is a bijective function f mapping states from S to S’ such that f(s₀) = s’₀ and s → s’, for some s,s’ ∈ S, if, and only, if, f(s) →’ f'(s’).

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 s and action a, there is at most one state t such that s →^a t. (Note that in the classical definition of determinism, in the context of finite state acceptors, there should be precisely one such t for every s and a.)

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 l is deterministic modulo an equivalence e if, and only if, there is a deterministic LTS that is e-equivalent to l. 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.

Structure

The LTS library resides in the namespace mcrl2::lts. The main class of this library is the lts class. This class represents an LTS and contains almost all available functionality to work with LTSs. States and labels are identified by unsigned ints and transitions are triples (from, label, to) of unsigned ints, where from and to are the source and target states, respectively, and label is the label of the transition.

There is a possibility to assign ATerm values to states and labels. This has to be specified when creating an lts object or when one resets such an object (with the reset() method). In principle these values can be any ATerm, but not all LTS formats support this. In practice the following structures typically occur:

No state information (all formats)
μCRL states: ATermLists of μCRL data expressions (μCRL, FSM)
mCRL2 states: ATermAppl of mCRL2 data expressions (mCRL2, FSM)

String labels: ATermAppl without arguments; the function symbol name is the label (all formats except mCRL2)
mCRL2 multiaction labels: ATermAppl; mCRL2 multiaction in internal format (mCRL2)

Besides the main lts class, there are several auxiliary classes. Three of them (state_iterator, transition_iterator and label_iterator) are iterators to iterate over states, transitions and labels. The lts class has methods to obtain such iterators (e.g. lts::get_transitions()). Their use is illustrated in the tutorial below.

The other classes, lts_dot_options, lts_eq_options and lts_extra, are used to store options for certain operations.

Tutorial

We perform two typical programming tasks to illustrate the use of the LTS library. Before we do so, however, we describe the common parts.

First of all we must include the appropriate header to use the LTS library.

#include <mcrl2/lts/liblts.h>

Most of the time it is also useful to specify that we are using the namespace of the LTS library.

using namespace mcrl2::lts;

In the rest of the tutorial we assume that this is specified. If one does not wish to use this, one will have to prepend mcrl2::lts:: to all references to entities in the LTS library.

Creating an LTS

Now let us make a function make_blue_lts() that constructs the blue LTS as shown above and saves it to a file. We start with some declarations.

void make_blue_lts()
{
  unsigned int s[5];
  unsigned int lab_open,lab_car,lab_flowers;
 
  lts l(false,true);

All states and labels are identified by unsigned integers. We therefore have an array s of five unsigned integers to store the identifiers of the (five) states as well as an unsigned integer variable for each label. The LTS is created with two arguments: the first argument indicates that we do not store state information and the second argument indicates that we will use label information in this example.

Before we can add any transitions to the LTS, we must first add the states and labels. This is done as follows.

  for (unsigned int i=0; i<5; ++i)
  {
    s[i] = l.add_state();
  }
 
  lab_open = l.add_label((ATerm) ATmakeAppl0(ATmakeAFun("open_door",ATfalse,0)));
  lab_car = l.add_label((ATerm) ATmakeAppl0(ATmakeAFun("win_car",ATfalse,0)));
  lab_flowers = l.add_label((ATerm) ATmakeAppl0(ATmakeAFun("win_flowers",ATfalse,0)));

Note that these functions return the identifier of the state or label. With this information we can construct the LTS. We specify the initial state:

  l.set_initial_state(s[0]);

And add the transitions:

  l.add_transition(s[0],lab_open,s[1]);
  l.add_transition(s[0],lab_open,s[2]);
  l.add_transition(s[1],lab_car,s[3]);
  l.add_transition(s[2],lab_flowers,s[4]);

The LTS is now complete. To save it, we call the write_to() method with a filename and the type of the output (lts_aut in this case).

  l.write_to("blue.aut",lts_aut);
}

Read, reduce and print

Now we have created an LTS file, we describe how to read it in again, apply some reduction and print its contents. There are two ways to read an LTS from a file. The most straightforward method is to use the appropriate constructor:

lts l("blue.aut");

Note, however, that this method only works when the supplied file contains a valid LTS (according to the LTS library). If this is not the case, there is no way to detect failure. It is therefore advisable to use the following method.

lts l;
if ( l.read_from("blue.aut") )
{
  // reading went ok
} else {
  // reading failed
}

Now that the LTS has been read from file, our goal is to print the transitions of the minimal deterministic trace-equivalent LTS to the screen.

For the reduction we simply call the reduce() method with the option lts_eq_trace.

  l.reduce(lts_eq_trace);

The LTS l has now been reduced, so we can print the result. We iterate over all transitions in a loop as follows.

  for (transition_iterator i = l.get_transitions(); i.more(); ++i)
  {

We show the states by printing their identifiers (i.e. the unsigned integers), but for the labels we wish to use the actual value as a string, which we can obtain as follows.

    string label = l.label_value_str(i.label());

To print each transition we do the following.

    cout << i.from() << "  -- " << label << " -->  " i.to() << endl;
  }

The output is as follows:

1  -- open_door -->  0
0  -- win_flowers -->  2
0  -- win_car -->  2

Note that the initial state is 1. To verify this one could also print l.initial_state().

Reference

LTS Reference Manual

Author

Written by Muck van Weerdenburg. Please report bugs at [1].

Retrieved from "http://mcrl2.org/mcrl2/wiki/index.php/LTS_library"

Personal tools