SAT-Based Counterexample-Guided Inductive Synthesis of Distributed Controllers

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...

Full description

Saved in:
Bibliographic Details
Published in:IEEE access 2020, Vol.8, p.207485-207498
Main Authors: Chukharev, Konstantin, Suvorov, Dmitrii, Chivilikhin, Daniil, Vyatkin, Valeriy
Format: Article
Language:English
Subjects:
Automata
Automatic control
Automation
Boolean algebra
Boolean satisfiability
Control system synthesis
Controllers
Counterexample-guided inductive synthesis
Dependable Communication and Computation Systems
Encoding
Formal verification
IEC Standards
Inference algorithms
Kommunikations- och beräkningssystem
Model checking
Protocols
Synthesis
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2169-3536
2169-3536
DOI:10.1109/ACCESS.2020.3037780