ReaTK
ReaTK is the Reactive System Verification and Synthesis ToolKit. It provides the ReaVer tool dedicated to the static verification of logico-numerical programs by abstract interpretation, and the ReaX tool performing discrete controller synthesis on such programs.
The controller synthesis tool ReaX was initially developed by Nicolas Berthier and Hervé Marchand from the SUMO Team at INRIA Rennes — Bretagne Atlantique in France. Further developments and investigations are now performed at the Department of Computer Science of the University of Liverpool in the UK, still by Nicolas Berthier. The ReaVer tool was originally implemented by Peter Schrammel
This page is about the ReaX tool and its usage. Documentation about ReaVer is available here.
Installation
The recommended way for installing ReaTK is to use the OCaml Package Manager (OPAM). See http://nberth.space/opam for further instructions.
Download
The project is distributed under the terms of the GNU General Public License. Its source code is hosted here.
Further Documentation
User Manual
The user manual gives some example executions of ReaX. It also describes the Controllable-Nbac language in which input systems (ASTSs) can be specified and outputs are generated.
Related Publications
References
Nicolas Berthier and Hervé Marchand. Discrete Controller Synthesis for Infinite State Systems with ReaX. In 12th Int. Workshop on Discrete Event Systems, WODES '14, May 2014. [ DOI ]
Nicolas Berthier and Hervé Marchand. Deadlock-Free Discrete Controller Synthesis for Infinite State Systems. In 54th IEEE Conference on Decision and Control, CDC '15, pages 1000--10007, December 2015. [ DOI ]
Acknowledgments
- This project was supported by the French ANR project Ctrl-Green, funded by ANR INFRA and MINALOGIC.
- The visual presentation of this page is highly based on Solarized CSS.