LLbox is a tool developped in the Real-Time Systems team of the french laboratory IRCCyN.
Its goal is to realize proofs of linear logic sequents that correspond to scenarii in Time Petri Nets.

This tool works in complementary with another tool developped by the team: Romeo.
Romeo is a software studio for analyzing Time Petri Nets. Its consists of a graphical user interface
to design and edit TPNs and computation modules to perform state space computation and model-checking.

LLbox can load Petri nets edited with Romeo to perform analysis on a given scenario.
A scenario is defined as a multiset of transitions. The goal of this analysis is to prove
the scenario, to determine the firing dates of the transitions in the scenario and to compute
a system of inequations that constraints these symbolic firing dates.

The last release version of the tool is LLbox 2.0

It is available in the download page.

Installation instructions are to be found here.

Documentation on the tool can be found in the documentation page.

For the previous version 1.3 the links are the following: install and documentation.

LLbox is developped under the supervision of David Delfieu.
The other contributors are: Florent de Lamotte, Sebastien Revol, Medesu Sogbohossou and Louis-Marie Traonouez.