Formats for Labelled Transition Systems

These pages explain the storage formats for labelled transition systems (LTSs). For a general explanation of labelled transition systems see Labelled transition systems.

mCRL2 LTS format

An mCRL2 LTS file consists of a labelled transition system together with a declaration of the data types and action declarations. Each transition is labelled with a multi-action, which is a sequence of action labels each optionally having data arguments. States can also have labels. Such a label generally is a vector of data values corresponding to the values of process parameters in the linear process specification from which the lts was generated. But such a label can also be a set of such vectors. This typically occurs when a labelled transition system is reduced using (branching/weak) bisimulation in which case all labels of equivalent states are accumulated in a set and this set is used as the new label.

A labelled transition system contain probabilities. In this case a transition goes to a discrete probability distribution. These can be viewed as non-labelled states with outgoing transitions that are labelled with probabilities. The sum of the probabilities of all outgoing transistion equals 1. Only a few tools support probabilistic transition systems, such as ltsgraph and ltspbisim.

An LTS in LTS format requires relatively little diskspace as it is stored as a compressed, shared ATerm. This ATerm storage format supports streaming, and therefore labelled transition systems in LTS format can be streamed.

Files in the LTS format typically have the extension .lts. As all data and action declarations are stored in the file format, this format is very suitable to transform an LTS into a linear process using the tool lts2lps.

A disadvantage of the .lts format is that it is not human readable. For this, the LTS should be translated into .aut or .fsm format, which can be done using the tool ltsconvert.

The aut format

The aut file format is a simple format for storing labelled transition systems. It is widely used by other tools, for instance the Caesar-Aldebaran or CADP toolset.

The syntax

The syntax of an Aldebaran file consists of a number of lines, where the first line is a aut_header and the remaining lines are of type aut_edge.

An aut_header is defined as follows:

aut_header        ::=  'des (' first_state ',' nr_of_transitions ',' nr_of_states ')'
first_state       ::=  number
nr_of_transitions ::=  number
nr_of_states      ::=  number

Here:

first_state is a number representing the first state;
nr_of_transitions is a number representing the number of transitions;
nr_of_states is a number representing the number of states.

An aut_edge is defined as follows:

aut_edge    ::=  '(' start_state ',' label ',' end_state ')'
start_state ::=  number
label       ::=  '"' string '"'
end_state   ::=  number

Here:

start_state is a number representing the start state of the edge;
label is a string enclosed in double quotes representing the label of the edge;
end_state is a number representing the end state of the edge.

An example

The following example shows a simple labelled transition system of the dining philosophers problem for two philosophers, visualised using ltsgraph:

This transition system is represented by the following Aldebaran file:

des (0,12,10)
(0,"lock(p2, f2)",1)
(0,"lock(p1, f1)",2)
(1,"lock(p1, f1)",3)
(1,"lock(p2, f1)",4)
(2,"lock(p2, f2)",3)
(2,"lock(p1, f2)",5)
(4,"eat(p2)",6)
(5,"eat(p1)",7)
(6,"free(p2, f2)",8)
(7,"free(p1, f1)",9)
(8,"free(p2, f1)",0)
(9,"free(p1, f2)",0)

The probabilistic aut format

There is a straightforward probabilistic extension of the aut format. The first state and each end state of an edge can be written as a discrete probability distribution in the form \(s_0~p_0~s_1\cdots p_{n-1}~s_n\). This means that state \(s_i\) is reached with probability \(p_i\) for \(i<n\) and state \(p_n\) is reached with probability \(1-\sum_{i=0}^{n-1}p_i\). Each probability is denoted as a fraction n/m where n and m are positive numbers. Note that this notation is a conservative extions of the probability free format. If a state is reached with probability one, it suffices to only denote the number of the state.

A probabilistic example

A small but typical example of a probabilistic aut file is given below. The initial probability distribution chooses state 0 or state 1 with respective probabilities 1/3 and 2/3. In state 0 an action is possible after which either state 0 or 1 are chosen with equal probability. In state 1 only an action b can be done, and after that state 1 is always reached:

des(0 1/3 1, 2, 2)
(0,"a",0 1/2 1)
(1,"b",1)

Acknowledgements

The Aldebaran format originally stems from the CADP toolset. To be fully compatible with the original syntax definition, the labels of the edges should consist of at most 5000 characters.

The FSM file format

An FSM file is a human-readable, plain-text file that specifies an LTS and it supports not only labelling of transitions but also of states. Besides that it can also express probabilities. The states are numbered from 1 to n where n is the highest state number occurring in the transition system, or n is the number of state labels. In general these are the same, but there are situations where they can differ, for instance when there are no state labels. An FSM file typically has the extension .fsm.

The content of a FSM file has the following form:

FSM ::=  PARAMETERS '\n' '---' '\n' STATES '\n' '---' '\n' TRANSITIONS '---' '\n' 'INITIAL_STATE'

containing four sections of which the last one is optional:

The first section specifies the state parameters and their domains;
The second section specifies the labels of the states of the LTS;
The third section specifies the transitions of the LTS;
The fourth section is optional and contains the initial state or initial probability distribution.

These sections are separated by lines that contain three dashes: ---.

The format of each of these sections is described separately below.

The parameters section

The parameters section defines the state parameters (or state variables) and their domains of possible values. In every state of the LTS, each of the parameters has one specific value from its domain.

Zero or more parameter should be specified. Every parameter is specified on a separate line of the following form:

PARAMETER ::=  PARAMETER_NAME '(' DOMAIN_CARDINALITY ')' DOMAIN_NAME ('"' DOMAIN_VALUE '"')*

containing the following items:

The parameter name: a string of alphanumerical characters;
The domain cardinality: a natural number;
The domain name: a string of alphanumerical characters;
A list of domain values: a space-separated list of quoted values, where every value is a string of characters that does not contain quotes (").

The number of domain values should be equal to the domain cardinality. Note that when there are no parameters, this section is empty.

The states section

The states section defines labels for states. If the states have no label, this section can be left empty. The parameter list for every state is specified on a separate line of the following form:

STATE ::=  (PARAMETER_VALUE)*

being a list of parameter values: a space-separated list of natural numbers.

The number of parameter values should be equal to the number of parameters defined in the parameters section, including parameters with a domain cardinality of 0.

The i-th value in the list specifies the value of the i-th parameter of the parameters section in the following way: a value of n specifies that in this state, that parameter has the nth value from its domain. These values are 0-based, meaning that a value of 0 corresponds to the first domain value of that parameter.

Every value should be at least 0 and smaller than the domain cardinality of the corresponding parameter. If that domain cardinality is 0, then the latter restriction does not apply and the value will be ignored.

The transitions section

The transitions section defines the transitions between the states of the LTS.

Every transition is specified on a separate line of the following form:

TRANSITION ::=  SOURCE_STATE TARGET_STATE '"'LABEL'"'

containing the following items:

The source state: a positive natural number;
The target state: a positive natural number or a probability distribution;
The label: a quoted string of characters that does not contain quotes (").

A value of n for either of the states indicates the n-th state of the states section. Each of these values should be at least 1 and at most the number of states specified in the states section.

A probability distribution is a sequence of pairs of state number followed by a fraction indicating the probability for this state to happen. This sequence is surrounded by square brackets. All probabilities in a distribution must add up to 1. A typical example is [ 1 1/2 3 1/4 7 1/4].

The initial state section

The initial state section is generally omitted and the initial state is by default assumed to be state 1. This section can be used to indicate an alternative initial state number, or it can be used to indicate that this transition system has a probability distribution over states as the initial state.

An example without probabilities

The following FSM file specifies the LTS depicted in the figure above. The state parameter values are indicated next to every state. The state identifiers used in the transitions section of the FSM file are shown inside every state:

b(2) Bool "F" "T"
n(2) Nat "1" "2"
---
0
1
0
1
---
2 "increase"
3 "on"
4 "on"
1 "decrease"
1 "off"
4 "increase"
2 "off"
3 "decrease"

An example with probabilities

A probabilistic example, based on a probabilistic fan controller, is given below:

s1_P(6) Pos  "2" "3" "4" "6" "1" "5"
b2_P(2) Bool  "true" "false"
b1_P(2) Bool  "true" "false"
k_P(3) Nat  "0" "1" "2"
---
0 0 0
0 0 0
0 1 0
0 0 1
0 0 0
1 0 0
0 0 1
0 0 2
0 0 0
0 0 2
0 0 0
---
[2 99/100 3 1/100] "on"
4 "fan_on(1, true)"
[5 99/100 6 1/100] "fan_on(1, false)"
7 "off"
8 "fan_on(2, true)"
9 "fan_on(2, false)"
1 "fan_off(1)"
10 "off"
11 "fail"
1 "fan_off(2)"
---
[1 1/2 2 1/4 3 1/4]