The T(O)RMC Toolset


Content

Introduction

T(O)RMC (states for Tool for (Omega-)Regular Model Checking) is a tool that implements a generic technique for computing the limite of a possibly infinite sequence of automata by extrapolating a finite prefixe of this sequence. The automata T(O)RMC can handle are either finite-word or deterministic weak BUCHI automata. Those two types of automata admit a unique minimal form and can easily be complemented (see [Leg07] for a general overview).

T(O)RMC was first used in the context of (Omega)-regular checking (see [BLW03] and [BLW04a] and [BLW04b] to know more about the first prototypes that predate T(O)RMC). Suppose that states of state-transition systems are encoded by words over a fixed alphabet. If the states are encoded by finite words, then sets of states can be represented by finite-word automata and relations between states by finite-word transducers (i.e. automata on binary alphabets). This settings is referred to as regular model checking. If the states are encoded by infinite words, then sets of states can be represented by BUCHI automata and relations between states by BUCHI transducers. However, working with BUCHI automata is known to be hard, especially from an implementation point of view. For this reason, we restrict ourselves to sets of states that can be represented by deterministic weak BUCHI automata, and relations between states that can be represented by deterministic weak BUCHI transducers. This setting is referred to as OMEGA-regular model checking. The two (OMEGA)-regular model checking problems are (1) to compute the transitive closure a transducer and (2) to compute the set of reachable states of a system represented in the (OMEGA)-regular model checking framework. Those two problems are known to be undecidable, but can be reduced to the computation of the limite of infinite sequences (as an example, computing a transitive closure amounts to compute the limit of its successive powers), and can thus be handled by T(O)RMC.

T(O)RMC has also recently been used to compute the convex hull over the reals of a finite set of integer vectors that is represented by a finite-word automaton[CLW07].

To use T(O)RMC, you must be familiar with classical automata-based manipulations and transducers composition. If this is not the case, please read Chapter 2 of [Leg07] for a survey.

Underlying technique

 T(O)RMC computes the limit of a (possibly infinite) sequence of automata by extrapolating one of its finite sampling sequence, i.e., selected automata from a finite prefix of the sequence. The extrapolation step proceeds by comparing successive automata in the sampling sequence, trying to identify the difference between these in the form of an increment, and extrapolating the repetition of this increment by adding loops to the last automaton of the sequence. After having computed such an extrapolation, T(O)RMC offers techniques to test whether it corresponds or not to the limit. The technique to compute the extrapolation is general and can be applied to any sequence of automata. The choice of the sampling sequence depends on the application, but heuristics are known. Testing whether the extrapolation is correct rely on the case study that is considered. The Underlying theory of T(O)RMC is described in [Leg07]. Chapter 5 presents the extrapolation-based technique and illustrates the choice of a sampling sequence, while chapters 6 and 13 propose criteria to test whether the extrapolation is correct or not. The complete algorithm behinds T(0)RMC is given in Section 7.3 of Chapter 7.

Download and content

 T(O)RMC comes up at a set of C functions that rely on those of the LASH toolset. The LASH toolset provides a series of C functions for manipulating finite-word and weak BUCHI automata. To install T(O)RMC you first need to install and modify the LASH toolset. For this, proceed as follows: You are now ready to install T(O)RMC! For this, proceed as follows:

The /lash-v0.92/src/TORMC/ directory contains the following files:

See here for concrete examples that illustrate the use of the tool.

Examples

 The following examples illustrate the use of T(O)RMC (and in fact also the one of LASH for which there are no available examples).

Experiments

 The TORMC toolset has been evaluated over more than 100 case studies. This section only briefly recap the classes of problems for which T(O)RMC has been used so far. Details about the experiments (including performances) can be found in Chapters 7 and 13 of [Leg07] and in [BLW04b].

T(O)RMC has been used to compute an automata-based representation of

Details about those experiments (encoding, performances, ...) can be found in Chapters 4, 7, and 13 of [Leg07].

Credits

T(O)RMC is written, debugged, maintained and improved by Axel Legay.

Past contributors and testers include François Cantin.

References