SAT-Based Counterexample-Guided Inductive Synthesis of Distributed Controllers

dc.contributorAalto-yliopistofi
dc.contributorAalto Universityen
dc.contributor.authorChukharev, Konstantinen_US
dc.contributor.authorSuvorov, Dmitriien_US
dc.contributor.authorChivilikhin, Daniilen_US
dc.contributor.authorVyatkin, Valeriyen_US
dc.contributor.departmentDepartment of Electrical Engineering and Automationen
dc.contributor.groupauthorInformation Technologies in Industrial Automationen
dc.contributor.organizationSirius University of Science and Technologyen_US
dc.contributor.organizationSt. Petersburg National Research University of Information Technologies, Mechanics and Optics (ITMO)en_US
dc.date.accessioned2021-01-25T10:18:27Z
dc.date.available2021-01-25T10:18:27Z
dc.date.issued2020en_US
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/pdfen_US
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.3037780en_US
dc.identifier.issn2169-3536
dc.identifier.otherPURE UUID: e10e3fd6-ac7c-4674-b874-26041c9da08cen_US
dc.identifier.otherPURE ITEMURL: https://research.aalto.fi/en/publications/e10e3fd6-ac7c-4674-b874-26041c9da08cen_US
dc.identifier.otherPURE LINK: http://www.scopus.com/inward/record.url?scp=85097345103&partnerID=8YFLogxKen_US
dc.identifier.otherPURE FILEURL: https://research.aalto.fi/files/54788130/ELEC_Chukharev_etal_SAT_Based_Counterexample_Guided_IEEEAccess_2020_finalpublishedversion.pdfen_US
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 satisfiabilityen_US
dc.subject.keywordControl system synthesisen_US
dc.subject.keywordCounterexample-guided inductive synthesisen_US
dc.subject.keywordFormal verificationen_US
dc.subject.keywordInference algorithmsen_US
dc.subject.keywordModel checkingen_US
dc.titleSAT-Based Counterexample-Guided Inductive Synthesis of Distributed Controllersen
dc.typeA1 Alkuperäisartikkeli tieteellisessä aikakauslehdessäfi
dc.type.versionpublishedVersion
Files