SAT-Based Counterexample-Guided Inductive Synthesis of Distributed Controllers

Loading...
Thumbnail Image
Journal Title
Journal ISSN
Volume Title
A1 Alkuperäisartikkeli tieteellisessä aikakauslehdessä
Date
2020
Major/Subject
Mcode
Degree programme
Language
en
Pages
14
207485-207498
Series
IEEE Access, Volume 8
Abstract
This article proposes a new method for automatic synthesis of distributed discrete-state controllers from given temporal specification and behavior examples. The proposed method develops known synthesis methods to the distributed case, which is a fundamental extension. This method can be applied for automatic generation of correct-by-design distributed control software for industrial automation. The proposed approach is based on reduction to the Boolean satisfiability problem (SAT) and has Counterexample-Guided Inductive Synthesis (CEGIS) at its core. We evaluate the proposed approach using the classical distributed alternating bit protocol.
Description
Keywords
Boolean satisfiability, Control system synthesis, Counterexample-guided inductive synthesis, Formal verification, Inference algorithms, Model checking
Other note
Citation
Chukharev , K , Suvorov , D , Chivilikhin , D & Vyatkin , V 2020 , ' SAT-Based Counterexample-Guided Inductive Synthesis of Distributed Controllers ' , IEEE Access , vol. 8 , 9257351 , pp. 207485-207498 . https://doi.org/10.1109/ACCESS.2020.3037780