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