Automatic Inference of Finite-State Plant Models From Traces and Temporal Properties

 |  Login

Show simple item record

dc.contributor Aalto-yliopisto fi
dc.contributor Aalto University en
dc.contributor.author Buzhinsky, Igor
dc.contributor.author Vyatkin, Valeriy
dc.date.accessioned 2019-06-03T14:20:34Z
dc.date.available 2019-06-03T14:20:34Z
dc.date.issued 2017-08-01
dc.identifier.citation Buzhinsky , I & Vyatkin , V 2017 , ' Automatic Inference of Finite-State Plant Models From Traces and Temporal Properties ' IEEE Transactions on Industrial Informatics , vol. 13 , no. 4 , 7857798 , pp. 1521-1530 . https://doi.org/10.1109/TII.2017.2670146 en
dc.identifier.issn 1551-3203
dc.identifier.other PURE UUID: ff2050f5-c66d-4342-9a05-4c4a1b58c502
dc.identifier.other PURE ITEMURL: https://research.aalto.fi/en/publications/automatic-inference-of-finitestate-plant-models-from-traces-and-temporal-properties(ff2050f5-c66d-4342-9a05-4c4a1b58c502).html
dc.identifier.other PURE LINK: http://www.scopus.com/inward/record.url?scp=85029439382&partnerID=8YFLogxK
dc.identifier.other PURE FILEURL: https://research.aalto.fi/files/33889150/ELEC_Buzhinsky_etal_Automatic_Inference_of_Finite_IEEETraIndInf_13_1521_accepted.pdf
dc.identifier.uri https://aaltodoc.aalto.fi/handle/123456789/38413
dc.description.abstract Closed-loop model checking, a formal verification technique for industrial automation systems, increases the richness of specifications to be checked and reduces the state space to be verified compared to the open-loop case. To be applied, it needs the controller and the plant formal models to be coupled. There are approaches for controller synthesis, but little has been done regarding plant model construction. While manual plant modeling is time consuming and error-prone, discretizing a simulation model of the plant leads to state excess. This paper aims to solve the problem of automatic plant model construction from existing specification, which is represented in the form of plant behavior examples, or traces, and temporal properties. The proposed method, which is based on the translation of the problem to the Boolean satisfiability problem, is evaluated and shown to be applicable on several case study plant model synthesis tasks and on randomly generated problem instances. en
dc.format.extent 10
dc.format.extent 1521-1530
dc.format.mimetype application/pdf
dc.language.iso en en
dc.publisher IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
dc.relation.ispartofseries IEEE Transactions on Industrial Informatics en
dc.relation.ispartofseries Volume 13, issue 4 en
dc.rights openAccess en
dc.subject.other Control and Systems Engineering en
dc.subject.other Information Systems en
dc.subject.other Computer Science Applications en
dc.subject.other Electrical and Electronic Engineering en
dc.subject.other 113 Computer and information sciences en
dc.subject.other 213 Electronic, automation and communications engineering, electronics en
dc.title Automatic Inference of Finite-State Plant Models From Traces and Temporal Properties en
dc.type A1 Alkuperäisartikkeli tieteellisessä aikakauslehdessä fi
dc.description.version Peer reviewed en
dc.contributor.department Department of Electrical Engineering and Automation
dc.contributor.department Department of Electrical Engineering and Automation en
dc.subject.keyword Automatic model synthesis
dc.subject.keyword closed-loop modeling
dc.subject.keyword industrial automation software
dc.subject.keyword model checking
dc.subject.keyword SAT
dc.subject.keyword Control and Systems Engineering
dc.subject.keyword Information Systems
dc.subject.keyword Computer Science Applications
dc.subject.keyword Electrical and Electronic Engineering
dc.subject.keyword 113 Computer and information sciences
dc.subject.keyword 213 Electronic, automation and communications engineering, electronics
dc.identifier.urn URN:NBN:fi:aalto-201906033498
dc.identifier.doi 10.1109/TII.2017.2670146
dc.type.version acceptedVersion


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

Browse