Open-Kronos: a model-checker for timed (Buchi) automata

Open-Kronos was built around 1997 as a successor to Kronos. The main objectives have been, on one hand, to endow Kronos with a more convenient modeling language (e.g., with discrete variables) and, on the other hand, to have an "open" software architecture where users could contribute their model-checking algorithms.

For this, Open-Kronos was based on the SMI tool built by Marius Bozga, for symbolic model-checking discrete systems. SMI, in turn, uses some libraries from CADP.

In the meantime, a large part of the technology used in both SMI and Open-Kronos has been transfered to the successor tool IF. However, there are still a few algorithms in Open-Kronos which have not been transfered to IF, in particular those implemented in the module Profounder. Profounder is able of checking reachability of timed automata and emptiness of timed Buchi automata. It can produce concrete timed traces in the first case. Profounder is a powerful tool. For instance, full DFS can explore 10 million states and 15 million transitions in less than 30 seconds (measured on a Xeon 2,8Ghz machine with 512MB RAM running Linux i686).

Profounder implements a number of algorithms, including standard depth-first search (DFS), "full" DFS (keep only a stack but no set of visited nodes), the "double" DFS algorithm of paper [1] below for (timed) Buchi automata emptiness, etc. These algorithms are run on the so-called "simulation" graph of the timed-automaton model, the same graph used for reachability. The theory behind all this can be found in the paper [2].

Profounder is available free of charge for academic use. Note that in order to be able to use Profounder, you must first obtain CADP. To receive Profounder, email me at Stavros.Tripakis@imag.fr , and also: print the distribution license, then fill it in and post it to

Christine Saunier
Verimag
Centre Equation
2, avenue de Vignate
39610 Gieres
France

For more information, contact Stavros Tripakis at Stavros.Tripakis@imag.fr

References (read the copyright note)

  1. C. Courcoubetis, M. Vardi, P. Wolper and M. Yannakakis. Memory Efficient Algorithms for the Verification of Temporal Properties. Formal Methods in System Design, volume 1, pages 275-288, Kluwer, 1992.

  2. S. Tripakis, S. Yovine and A. Bouajjani. Checking Timed Buchi Automata Emptiness Efficiently. In Formal Methods in System Design, 26(3):267-292, May 2005. Postscript.

  3. S. Tripakis. Checking Timed Buchi Automata Emptiness on Simulation Graphs. Available as VERIMAG Technical Report TR-2006-1.



Back to home page of Stavros Tripakis