Skip to Main content Skip to Navigation
Conference papers

Deadlock-free Discrete Controller Synthesis for Infinite State Systems

Nicolas Berthier 1 Hervé Marchand 1
1 SUMO - SUpervision of large MOdular and distributed systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
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 overapproximations, 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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [26 references]  Display  Hide  Download
Contributor : Hervé Marchand <>
Submitted on : Tuesday, January 5, 2016 - 5:15:08 PM
Last modification on : Friday, July 10, 2020 - 4:08:50 PM
Long-term archiving on: : Thursday, April 7, 2016 - 3:32:38 PM


Files produced by the author(s)


  • HAL Id : hal-01200976, version 1


Nicolas Berthier, Hervé Marchand. Deadlock-free Discrete Controller Synthesis for Infinite State Systems. 54th IEEE Conference on Decision and Control, Dec 2015, Osaka, Japan. ⟨hal-01200976⟩



Record views


Files downloads