Unbeast – Symbolic Bounded Synthesis
Copyright © 2010 Rüdiger Ehlers, Saarland University
Introduction
Synthesis of finite state systems has been proven to be a valuable concept for the development of open systems that are correct by construction Unbeast is a tool for this task capable of handling full linear-time temporal logic (LTL). It is designed for specifications comprising a set of assumptions (which the system under construction can assume to be correct) and a set of guarantees (which the system needs to fulfill). From a technical point of view, Unbeast builds upon the bounded synthesis approach.
Requirements & Instructions
For correct operation of the Unbeast tool, a moderately modern Linux distribution is required. The tool has to be compiled before usage. Under Ubuntu Linux, it should suffice to install the package build-essential.
Additionally, at least one of the following LTL-to-Büchi converters needs to be installed. The converter is called by the Unbeast tool at runtime.
ltl2baby Dennis Oddoux and Paul Gastinspotby Alexandre Duret-Lutz et al., version 0.5a or greater
Installation instructions can be found on the respective homepages.
The Unbeast tool uses the CUDD library (v.2.4.1 or greater) for manipulating binary decision diagrams. The file README, which is included in the Unbeast distribution, contains detailed instructions on building Unbeast with CUDD. The usage of the Unbeast tool is also explained in the README file.
Publications
| [Ehl10c] | Rüdiger Ehlers. Symbolic Bounded Synthesis. 22nd International Conference on Computer Aided Verification (CAV 2010). |
License
The prototype is free for use in academic context. For all other purposes, including integration into other tools, please contact the author. Furthermore, the licensing details stated in this document apply.
Download
Note that this tool set is in a prototype stage. Thus, there may be bugs in the implementation. If you find one, please contact the author.
- Unbeast v.0.6b – Bugfix in the simulator (for the case of unrealisable specifications), now compatible with later Boost versions, November 2012
- Unbeast v.0.6 – New version including a simulator for the synthesised system (realisable specifications) or the environment (unrealisable specifications), October 2010
- Unbeast v.0.5 – Initial release, July 2010
- The Lily examples – This package contains the 23 examples that come with the Lily tool for LTL synthesis in a form readable by Unbeast.
The examples have been described in the paper Optimizations for LTL Synthesis by Barbara Jobstmann and Roderick Bloem, who also gave the kind permission to put them here.
- The Load balancer examples – This package contains the specifications used for benchmarking in the CAV 2010 paper. Translated versions for use with Acacia are also provided.