Learning Centre

SAT-Based Counterexample-Guided Inductive Synthesis of Distributed Controllers

 |  Login

Show simple item record

dc.contributor Aalto-yliopisto fi
dc.contributor Aalto University en
dc.contributor.author Chukharev, Konstantin
dc.contributor.author Suvorov, Dmitrii
dc.contributor.author Chivilikhin, Daniil
dc.contributor.author Vyatkin, Valeriy
dc.date.accessioned 2021-01-25T10:18:27Z
dc.date.available 2021-01-25T10:18:27Z
dc.date.issued 2020
dc.identifier.citation Chukharev , K , Suvorov , D , Chivilikhin , D & Vyatkin , V 2020 , ' SAT-Based Counterexample-Guided Inductive Synthesis of Distributed Controllers ' , IEEE Access , vol. 8 , 9257351 , pp. 207485-207498 . https://doi.org/10.1109/ACCESS.2020.3037780 en
dc.identifier.issn 2169-3536
dc.identifier.other PURE UUID: e10e3fd6-ac7c-4674-b874-26041c9da08c
dc.identifier.other PURE ITEMURL: https://research.aalto.fi/en/publications/e10e3fd6-ac7c-4674-b874-26041c9da08c
dc.identifier.other PURE LINK: http://www.scopus.com/inward/record.url?scp=85097345103&partnerID=8YFLogxK
dc.identifier.other PURE FILEURL: https://research.aalto.fi/files/54788130/ELEC_Chukharev_etal_SAT_Based_Counterexample_Guided_IEEEAccess_2020_finalpublishedversion.pdf
dc.identifier.uri https://aaltodoc.aalto.fi/handle/123456789/102270
dc.description.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. en
dc.format.extent 14
dc.format.extent 207485-207498
dc.format.mimetype application/pdf
dc.language.iso en en
dc.relation.ispartofseries IEEE Access en
dc.relation.ispartofseries Volume 8 en
dc.rights openAccess en
dc.title SAT-Based Counterexample-Guided Inductive Synthesis of Distributed Controllers en
dc.type A1 Alkuperäisartikkeli tieteellisessä aikakauslehdessä fi
dc.description.version Peer reviewed en
dc.contributor.department Sirius University of Science and Technology
dc.contributor.department St. Petersburg National Research University of Information Technologies, Mechanics and Optics (ITMO)
dc.contributor.department Information Technologies in Industrial Automation
dc.contributor.department Department of Electrical Engineering and Automation en
dc.subject.keyword Boolean satisfiability
dc.subject.keyword Control system synthesis
dc.subject.keyword Counterexample-guided inductive synthesis
dc.subject.keyword Formal verification
dc.subject.keyword Inference algorithms
dc.subject.keyword Model checking
dc.identifier.urn URN:NBN:fi:aalto-202101251580
dc.identifier.doi 10.1109/ACCESS.2020.3037780
dc.type.version publishedVersion

Files in this item

Files Size Format View

There are no open access files associated with this item.

This item appears in the following Collection(s)

Show simple item record

Search archive

Advanced Search

article-iconSubmit a publication