SAT-Based Counterexample-Guided Inductive Synthesis of Distributed Controllers

dc.contributorAalto-yliopistofi
dc.contributorAalto Universityen
dc.contributor.authorChukharev, Konstantin
dc.contributor.authorSuvorov, Dmitrii
dc.contributor.authorChivilikhin, Daniil
dc.contributor.authorVyatkin, Valeriy
dc.contributor.departmentSirius University of Science and Technology
dc.contributor.departmentSt. Petersburg National Research University of Information Technologies, Mechanics and Optics (ITMO)
dc.contributor.departmentInformation Technologies in Industrial Automation
dc.contributor.departmentDepartment of Electrical Engineering and Automationen
dc.date.accessioned2021-01-25T10:18:27Z
dc.date.available2021-01-25T10:18:27Z
dc.date.issued2020
dc.description.abstractThis 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.description.versionPeer revieweden
dc.format.extent14
dc.format.extent207485-207498
dc.format.mimetypeapplication/pdf
dc.identifier.citationChukharev , 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.3037780en
dc.identifier.doi10.1109/ACCESS.2020.3037780
dc.identifier.issn2169-3536
dc.identifier.otherPURE UUID: e10e3fd6-ac7c-4674-b874-26041c9da08c
dc.identifier.otherPURE ITEMURL: https://research.aalto.fi/en/publications/e10e3fd6-ac7c-4674-b874-26041c9da08c
dc.identifier.otherPURE LINK: http://www.scopus.com/inward/record.url?scp=85097345103&partnerID=8YFLogxK
dc.identifier.otherPURE FILEURL: https://research.aalto.fi/files/54788130/ELEC_Chukharev_etal_SAT_Based_Counterexample_Guided_IEEEAccess_2020_finalpublishedversion.pdf
dc.identifier.urihttps://aaltodoc.aalto.fi/handle/123456789/102270
dc.identifier.urnURN:NBN:fi:aalto-202101251580
dc.language.isoenen
dc.publisherIEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
dc.relation.ispartofseriesIEEE Accessen
dc.relation.ispartofseriesVolume 8en
dc.rightsopenAccessen
dc.subject.keywordBoolean satisfiability
dc.subject.keywordControl system synthesis
dc.subject.keywordCounterexample-guided inductive synthesis
dc.subject.keywordFormal verification
dc.subject.keywordInference algorithms
dc.subject.keywordModel checking
dc.titleSAT-Based Counterexample-Guided Inductive Synthesis of Distributed Controllersen
dc.typeA1 Alkuperäisartikkeli tieteellisessä aikakauslehdessäfi
dc.type.versionpublishedVersion
Files