The LAAS TINA.tedd tool laureate

 For its Third participation to the MCC (Model-Checking Contest), the TINA.tedd tool, developed by the LAAS-CNRS VerTICS  team ranked first among the “StateSpace” category.

The trials consist in the efficient exploration of the Petri net state space. In other words the whole of different configurations that may occur during execution. These state spaces range in size from 10^6 to 10^130 elements: each space has to be integrally explored in less than an hour, and its precise size must be calculated, to reach the exact element.

The contest issue is contribute to improve these tools performance known as “model-checking”  so they can scale on more and more study cases.


Petri nets are a theoretical model largely used to model, mathematically, production lines, simultaneous software tasks, protocols, distributed systems, etc. The LAAS-CNRS Vertics  team is interested in, among other things, a Petri Net extension, taking in account the “time” dimension.


People involved in TINA.Tedd:

  • Bernard Berthomieu
  • Silvano Dal Zilio
  • Didier Le Botlan