Discrete Controller Synthesis for Infinite State Systems
In relation with my work on control techniques for clouds management, discrete controller synthesis techniques needed to be augmented so as to handle quantitative aspects of managed systems (e.g., power consumption, workloads), as well as to be able to enforce properties about such quantities. In effect, existing techniques and tools performing discrete controller synthesis on synchronous programs (Sigali) need to be extended in order to handle infinite state systems (e.g., programs comprising real or integer variables). I worked (and am still working) on such extensions with Hervé Marchand.
These investigations have led to the development of the tool ReaX. It is distributed as part of the Reactive Systems Verification and Synthesis ToolKit (ReaTK), available in my OPAM repository.
Papers
-
Discrete Controller Synthesis for Infinite State Systems with ReaX
Nicolas Berthier, Hervé Marchand. In 12th Int. Workshop on Discrete Event Systems, WODES ’14. pages 46–53, IFAC, May 2014.Abstract
We investigate the control of infinite reactive synchronous systems modeled by arithmetic symbolic transition systems for safety properties. We provide effective algorithms allowing to solve the safety control problem, and report on experiments based on ReaX, our tool implementing these algorithms.
-
Deadlock-Free Discrete Controller Synthesis for Infinite State Systems
Nicolas Berthier, Hervé Marchand. In 54th IEEE Conference on Decision and Control, CDC ’15, pages 1000–1007, December 2015.Abstract
We elaborate on our former work for the safety control of infinite reactive synchronous systems modeled by arithmetic symbolic transition systems. By using abstract interpretation techniques involving disjunctive polyhedral over-approximations, we provide effective symbolic algorithms allowing to solve the deadlock-free safety control problem while overcoming previous limitations regarding the non-convexity of the set of states violating the invariant to enforce.
-
Symbolic Limited Lookahead Control for Best-effort Dynamic Computing Resource Management
Nicolas Berthier, Hervé Marchand, and Éric Rutten. In 14th Int. Workshop on Discrete Event Systems, WODES ’18, pages 112–119. IFAC, June 2018.Abstract
We put forward a new modeling technique for Dynamic Resource Management (DRM) based on discrete events control for symbolic logico-numerical systems, especially Discrete Controller Synthesis (DCS). The resulting models involve state and input variables defined on an infinite domain (Integers), thereby no exact DCS algorithm exists for safety control. We thus formally define the notion of limited lookahead, and associated best-effort control objectives targeting safety and optimization on a sliding window for a number of steps ahead. We give symbolic algorithms, illustrate our approach on an example model for DRM, and report on performance results based on an implementation in our tool ReaX.
-
Article:
;
-
Slides:
;
- HAL.
-
Article:
General Search Techniques for Discrete Controller Synthesis
Paper
-
A Hot Method for Synthesising Cool Controllers
Idress Husien, Nicolas Berthier, and Sven Schewe. In International SPIN Symposium on Model Checking of Software, SPIN ’17. pages 122–131, ACM, July 2017.Abstract
Several general search techniques such as genetic programming and simulated annealing have recently been investigated for synthesising programs from specifications of desired objective behaviours. In this context, these techniques explore the space of all candidate programs by performing local changes to candidates selected by means of a measure of their fitness w.r.t the desired objectives. Previous performance results advocated the use of simulated annealing over genetic programming for such problems.
In this paper, we investigate the application of these techniques for the computation of deterministic strategies solving symbolic Discrete Controller Synthesis (DCS) problems, where a model of the system to control is given along with desired objective behaviours. We experimentally confirm that relative performance results are similar to program synthesis, and give a complexity analysis of our simulated annealing algorithm for symbolic DCS.
![[XHTML 1.0]](/_img/logo-xhtml-1.0.png){kind=logo}
![[CSS 3]](/_img/logo-css.png){kind=logo}