SAT-Based Counterexample-Guided Inductive Synthesis of Distributed Controllers

Konstantin Chukharev*, Dmitrii Suvorov, Daniil Chivilikhin, Valeriy Vyatkin

*Corresponding author for this work

Research output: Contribution to journalArticleScientificpeer-review

48 Downloads (Pure)

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 languageEnglish
Article number9257351
Pages (from-to)207485-207498
Number of pages14
JournalIEEE Access
Volume8
DOIs
Publication statusPublished - 2020
MoE publication typeA1 Journal article-refereed

Keywords

  • Boolean satisfiability
  • Control system synthesis
  • Counterexample-guided inductive synthesis
  • Formal verification
  • Inference algorithms
  • Model checking

Fingerprint Dive into the research topics of 'SAT-Based Counterexample-Guided Inductive Synthesis of Distributed Controllers'. Together they form a unique fingerprint.

Cite this