ReaX: Technical References
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 for such programs.
This document details some of the internals of the ReaX tool.
Table of Contents
1 Introduction
ReaX implements Discrete Controller Synthesis (DCS) algorithms operating on logico-numerical reactive programs specified as Arithmetic Symbolic Transitions Systems (ASTSs). We give in this document a detailed description of the kind of models manipulated by ReaX, and sketch its purpose based on this formalism. The paper by [Berthier and Marchand, 2014] gives further details about the model, the discrete controller synthesis problem, and the implemented algorithms.
We first present a basic model of reactive nodes and the associated DCS problem in this framework.
2 Contents TODO
Actually, that’s all for now (this document is still under construction). See the paper by [Berthier and Marchand, 2014].
References
References
| [Berthier and Marchand, 2014] | Berthier, N. and Marchand, H. (2014). Discrete Controller Synthesis for Infinite State Systems with ReaX. In 12th Int. Workshop on Discrete Event Systems, WODES '14. [ DOI ] |
| [Berthier and Marchand, 2015] | Berthier, N. and Marchand, H. (2015). Deadlock-Free Discrete Controller Synthesis for Infinite State Systems. In 54th IEEE Conference on Decision and Control, CDC '15, pages 1000--10007. [ DOI ] |
| [Delaval et al., 2010] | Delaval, G., Marchand, H., and Rutten, E. (2010). Contracts for modular discrete controller synthesis. In Proceedings of the Conference on Languages, Compilers, and Tools for Embedded Systems, pages 57--66. |