SAT-based Counterexample-Guided Inductive Synthesis of Distributed Controllers
2020 (English)In: IEEE Access, E-ISSN 2169-3536, Vol. 8, p. 207485-207498
Article in journal (Refereed) Published
Abstract [en]
This paper 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.
Place, publisher, year, edition, pages
IEEE, 2020. Vol. 8, p. 207485-207498
Keywords [en]
Control system synthesis, Inference algorithms, Boolean satisfiability, Counterexample-guided inductive synthesis, Formal verification, Model checking
National Category
Computer Sciences
Research subject
Dependable Communication and Computation Systems
Identifiers
URN: urn:nbn:se:ltu:diva-81478DOI: 10.1109/ACCESS.2020.3037780ISI: 000595012700001Scopus ID: 2-s2.0-85097345103OAI: oai:DiVA.org:ltu-81478DiVA, id: diva2:1502468
Note
Validerad;2020;Nivå 2;2020-12-03 (alebob)
2020-11-202020-11-202025-04-17Bibliographically approved