## The T(O)RMC Toolset |

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.

- Download the latest version of the LASH toolset (latest version is 0.92), which is available here.
- Go to the directory
`/lash-v0.92/src/`and create a new version of the`lash-core`subdirectory by extracting the following file. This operation is needed to create a first interaction between LASH and T(O)RMC. The`/lash-v0.92/src/lash-core/`directory contains all the files for creating and manipulating finite-word and weak BUCHI automata. LASH also provides compilers to directly create automata from formulas (see the documentation). Documentation about modifications and/or uses of functions can be found in each file of the directory. - Go to the directory
`/lash-v0.92/`and type: "make clean" followed by "make depend" followed by "make".

- Go to the directory
`/lash-v0.92/src/`and create the T(0)RMC subdirectory by extracting the following the file. This subdirectory contains the T(O)RMC C functions as well as several examples. - Go to the directory
`/lash-v0.92/`and replace the content of the`Makefile`file by the following piece of code one. - Go to the directory
`/lash-v.0.92/`and type: "make clean" followed by "make depend" followed by "make".

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

`README`contains general informations about the tool.`lash-transducers.h`contains the data structures needed to manipulate transducers.`composition.h`contains the prototypes of several C functions that can be used to manipulate transducers. The The code of those functions as well as some documentation can be found in file`composition.c`.`extrapolate.h`contains the structures and the prototypes of the C functions that are used to compute the extrapolation of a sequence of automata. The code of those functions as well as some documentation can be found in file`extrapolate.c`.`dominance.h`contains the prototypes of several heuristic-based functions that can be used to improve the efficiency of the tool. The code of those functions as well as some documentation can be found in file`dominance.c`. See Section 7.2 of [Leg07] to know how and when those heuristics can be used.`auto-help.h`and`auto-info.h`contain the prototypes of several functions that can help in the process of testing whether the extrapolation made by T(O)RMC is correct or not. The code of those functions as well as some documentation can be found in files`auto-help.c`and`auto-info.c`- Some (non commented) testing examples that illustrate the use of
T(O)RMC (and in fact also the one of LASH...) can be found in
`/lash-v0.92/src/TORMC/examples/`

- The following C file illustrates how to encode the well-know token ring parametric system. Use the following command to compile.
- The following C file illustrates how to compute the powers of several arithmetique relations (encoded by finite-word automata), sometimes with the help of heuristics. Use the following command to compile.
- The following C file illustrates how to compute the powers of several arithmetique relations (encoded by weak BUCHI automata), sometimes with the help of heuristics. Use the following command to compile.
- The following C file illustrates how to compute the transitive closure of an arithmetic relation. Use the following command to compile.

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

- the set of reachable states of several parametric systems. Those sets of states are represented by finite-word automata.
- the set of reachable states of several systems manipulating integer variables. Those sets of states are represented by finite-word automata, often called NDDs (states for Number Decision Diagrams). Those automata allow to represent any set that can be defined in Presburger arithmetic (see [BW02] and Chapter 4 of [Leg07] for surveys).
- the set of reachable states of several linear hybrid systems. Those sets of states are represented by deterministic weak BUCHI automata, often called RVAs (states for Real Vector Automata). Those automata allow to represent any set that can be defined in Presburger arithmetic over the reals (see [BJW05] and Chapter 4 of [Leg07] for surveys).
- the set of reachable states of several communication protocols. Those sets of states are represented by finite-word automata, that are often called QDDs (states for Queue Decision Diagrams, see [BG99] and Chapter 4 of [Leg07] for surveys). The tool has also been used to compute:
- The transitive closure of several arithmetic relations (both over the integers and the reals) represented by transducers.
- The convex hull over the reals (hence a RVA) of a finite set of integer vectors represented by a NDD.
- A symbolic simulation over the state-space of an infinite-state system, with the aim of verifying temporal properties.

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

Past contributors and testers include François Cantin.

[BG99] B. Boigelot and P. Godefroid. Symbolic Verification of Communication Protocols with Infinite State Spaces using QDDs, Formal Methods in System Design, volume 14, pages 237-255, 1999, Kluwer Academic Publishers.

[BJW05] B. Boigelot, S. Jodogne, and P. Wolper. An Effective Decision Procedure for Linear Arithmetic with Integer and Real Variables. ACM Transactions in Computational Logic, 6(3): 614-633, 2005.

[BLW03] B. Boigelot, A. Legay, P. Wolper. Iterating Transducers in the Large.

*Proc. 15th International Conference on Computer-Aided Verification*, volume 2725,*Lecture Notes in Computer Science*, pages 223-235, Boulder, July 2003, Springer-Verlag. Paper.[BLW04a] B. Boigelot, A. Legay, P. Wolper. Omega-regular Model Checking.

*Proc. 10th International Conference on Tools ans Algorithms for the Construction and Analysis of Systems*, volume 2988, Lecture Notes in Computer Science, pages 561-575, Barcelona, April 2004, Springer-Verlag. Abstract. Paper.-
[BLW04b] A. Bouajjani, A. Legay, P. Wolper. Handling Liveness properties in (Omega-)Regular Model Checking.

*Proc of Infinity04 Workshop*, pages 37-48, London, September 2004. Also: Volume 138(3) of ENTCS, pages 101-115. (2005). Abstract. Paper. [BW02]B. Boigelot and P. Wolper. Representing Arithmetic Constraints with Automata: An Overview.

*Proc. Proc. 18th International Conference on Logic Programming*, volume 2401, Lecture Notes in Computer Science, pages 1-19, Copenhagen, July 2002, Springer-Verlag.[CLW07] F. Cantin, A. Legay, P. Wolper. Computing Convex hulls by automata iterations. To appear in AUTOMATHA 07. Abstract. Paper.

[Leg07] A. Legay. Generic Techniques for the Verification of Infinite-State Systems. PhD thesis. Ulg December 2007. Abstract. Thesis.