LTS WorkBench

Labelled Transition Systems (LTSs) are a fundamental semantic model in many areas of informatics, especially concurrency theory. Yet, reasoning on LTSs and relations between their states can be difficult and elusive: very simple process algebra terms can give rise to a large (possibly infinite) number of intricate transitions and interactions. To ease this kind of study, we present LTSwb, a flexible and extensible LTS toolbox.

Main features

  • Genericity:
    • no restrictions on the type of states and labels in LTSs and processes
    • no hardwired process calculus (CCS is included, but you can add your own calculi)
    • generic operators for buffered semantics and parallel composition
  • Laziness: supports infinite-state LTSs and processes, avoids state space explosion
  • On-the-fly synthesis and verification of behavioural relations (without pre-constructing the state graph):
    • Simulation, Bisimulation
    • ClientProgress, Progress
    • ClientIOCompliance, Compliance

Online resources

The following tutorial paper presents LTSwb through several examples:

You can try LTSwb in two ways: by downloading the precompiled binaries, or its source code.

Precompiled binaries

You will need to install Scala, and then:

  • download ltswb-assembly-0.0.3.jar (last update: Jun 5, 2015; sha1sum: 00b169872bef54364184000c07c76fb74b63e2f5)
  • launch the interactive Scala console: scala -cp ltswb-assembly-0.0.3.jar
  • on the Scala console, execute: import it.unica.tcs.ltswb._
  • you can now try the examples in the tutorial above.

Source code

The LTSwb source code can be downloaded here (see included README for instructions):

  • ltswb-0.0.3.tar.gz (last update: Jun 5, 2015; sha1sum: cbd9583d86ae634b544912a263abd5f9b61d33d5)

Presentations

  • Interaction and Concurrency Experience (ICE) workshop - Grenoble, June 5, 2015 (slides) (last update: June 9, 2015)

Acknowledgements

This research has been partially supported by the following projects:

  • Autonomous Region of Sardinia grant L.R.7/2007 CRP-17285 TRICS
  • Autonomous Region of Sardinia P.I.A. 2010 Social Glue
  • MIUR PRIN 2010-11 project Security Horizons
  • EU COST Action IC1201 "Behavioural Types for Reliable Large-Scale Software Systems" (BETTY).