DC Field | Value | Language |
---|---|---|
dc.contributor.author | BAE, KYUNGMIN | - |
dc.contributor.author | LEE, JIA | - |
dc.date.accessioned | 2019-02-25T04:41:51Z | - |
dc.date.available | 2019-02-25T04:41:51Z | - |
dc.date.created | 2018-11-28 | - |
dc.date.issued | 2019-01-18 | - |
dc.identifier.uri | https://oasis.postech.ac.kr/handle/2014.oak/94704 | - |
dc.description.abstract | Signal temporal logic (STL) is a temporal logic formalism for specifying properties of continuous signals. STL is widely used for analyzing programs in cyber-physical systems (CPS) that interact with physical entities. However, existing methods for analyzing STL properties are incomplete even for bounded signals, and thus cannot guarantee the correctness of CPS programs. This paper presents a new symbolic model checking algorithm for CPS programs that is refutationally complete for general STL properties of bounded signals. To address the difficulties of dealing with an infinite state space over a continuous time domain, we first propose a syntactic separation of STL, which decomposes an STL formula into an equivalent formula so that each subformula depends only on one of the disjoint segments of a signal. Using the syntactic separation, an STL model checking problem can be reduced to the satisfiability of a first-order logic formula, which is decidable for CPS programs with polynomial dynamics using satisfiability modulo theories (SMT). Unlike the previous methods, our method can verify the correctness of CPS programs for STL properties up to given bounds. | - |
dc.language | English | - |
dc.publisher | ACM | - |
dc.relation.isPartOf | The 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019) | - |
dc.relation.isPartOf | Proc. ACM Program. Lang. 3 | - |
dc.title | Bounded Model Checking of Signal Temporal Logic Properties Using Syntactic Separation | - |
dc.type | Conference | - |
dc.type.rims | CONF | - |
dc.identifier.bibliographicCitation | The 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019) | - |
dc.citation.conferenceDate | 2019-01-13 | - |
dc.citation.conferencePlace | PO | - |
dc.citation.conferencePlace | Hotel Cascais Miragem, Cascais/Lisbon | - |
dc.citation.title | The 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019) | - |
dc.contributor.affiliatedAuthor | BAE, KYUNGMIN | - |
dc.contributor.affiliatedAuthor | LEE, JIA | - |
dc.identifier.scopusid | 2-s2.0-85108511161 | - |
dc.description.journalClass | 1 | - |
dc.description.journalClass | 1 | - |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.
library@postech.ac.kr Tel: 054-279-2548
Copyrights © by 2017 Pohang University of Science ad Technology All right reserved.