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.
Original language | English |
---|---|
Article number | 9257351 |
Pages (from-to) | 207485-207498 |
Number of pages | 14 |
Journal | IEEE Access |
Volume | 8 |
DOIs | |
Publication status | Published - 2020 |
MoE publication type | A1 Journal article-refereed |
Keywords
- Boolean satisfiability
- Control system synthesis
- Counterexample-guided inductive synthesis
- Formal verification
- Inference algorithms
- Model checking