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.
- 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
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.
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.
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)
- Interaction and Concurrency Experience (ICE) workshop - Grenoble, June 5, 2015 (slides) (last update: June 9, 2015)
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).