Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
SAT-based Counterexample-Guided Inductive Synthesis of Distributed Controllers
Sirius University of Science and Technology, 1 Olympic Ave, 354340, Sochi, Russia; Computer Technologies Laboratory, ITMO University, St. Petersburg, Russia.
Sirius University of Science and Technology, 1 Olympic Ave, 354340, Sochi, Russia; Computer Technologies Laboratory, ITMO University, St. Petersburg, Russia.
Sirius University of Science and Technology, 1 Olympic Ave, 354340, Sochi, Russia; Computer Technologies Laboratory, ITMO University, St. Petersburg, Russia.
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Computer Science. Computer Technologies Laboratory, ITMO University, St. Petersburg, Russia; Department of Electrical Engineering and Automation, Aalto University, Espoo, Finland.ORCID iD: 0000-0002-9315-9920
2020 (English)In: IEEE Access, E-ISSN 2169-3536, Vol. 8, p. 207485-207498Article 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)

Available from: 2020-11-20 Created: 2020-11-20 Last updated: 2025-04-17Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Vyatkin, Valeriy

Search in DiVA

By author/editor
Vyatkin, Valeriy
By organisation
Computer Science
In the same journal
IEEE Access
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 86 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf