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

https://hal.inria.fr/hal-01200976
Contributor : Hervé Marchand <>
Submitted on : Tuesday, January 5, 2016 - 5:15:08 PM
Last modification on : Thursday, February 7, 2019 - 4:02:28 PM
Long-term archiving on : Thursday, April 7, 2016 - 3:32:38 PM

File

paper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01200976, version 1

Citation

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⟩

Share

Metrics

Record views

524

Files downloads

205