SAT-Based Counterexample-Guided Inductive Synthesis of Distributed Controllers

Chukharev, Konstantin; Suvorov, Dmitrii; Chivilikhin, Daniil; Vyatkin, Valeriy

Aaltodoc
→
6b Artikkelit / Articles from Research information portal
→
[article-cris] Sähkötekniikan korkeakoulu / ELEC
→
View Item

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.publisher	IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
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