DC Field | Value | Language |
---|---|---|
dc.contributor.author | LEE, JIA | - |
dc.contributor.author | Yu, Geunyeol | - |
dc.contributor.author | BAE, KYUNGMIN | - |
dc.date.accessioned | 2021-12-05T11:45:16Z | - |
dc.date.available | 2021-12-05T11:45:16Z | - |
dc.date.created | 2021-11-30 | - |
dc.date.issued | 2021-11-17 | - |
dc.identifier.uri | https://oasis.postech.ac.kr/handle/2014.oak/108189 | - |
dc.description.abstract | Signal temporal logic (STL) is widely used to specify and analyze properties of cyber-physical systems with continuous behaviors. However, STL model checking is still quite limited, as existing STL model checking methods are either incomplete or very inefficient. This paper presents a new SMT-based model checking algorithm for verifying STL properties of cyber-physical systems. We propose a novel translation technique to reduce the STL bounded model checking problem to the satisfiability of a first-order logic formula over reals, which can be solved using state-of-the-art SMT solvers. Our algorithm is based on a new theoretical result, presented in this paper, to build a small but complete discretization of continuous signals, which preserves the bounded satisfiability of STL. Our translation method allows an efficient STL model checking algorithm that is refutationally complete for bounded signals, and that is much more scalable than the previous refutationally complete algorithm. | - |
dc.language | English | - |
dc.publisher | IEEE/ACM | - |
dc.relation.isPartOf | 36th IEEE/ACM International Conference on Automated Software Engineering | - |
dc.relation.isPartOf | Proc. International Conference on Automated Software Engineering | - |
dc.title | Efficient SMT-Based Model Checking for Signal Temporal Logic | - |
dc.type | Conference | - |
dc.type.rims | CONF | - |
dc.identifier.bibliographicCitation | 36th IEEE/ACM International Conference on Automated Software Engineering | - |
dc.citation.conferenceDate | 2021-11-14 | - |
dc.citation.conferencePlace | AT | - |
dc.citation.conferencePlace | 온라인 | - |
dc.citation.title | 36th IEEE/ACM International Conference on Automated Software Engineering | - |
dc.contributor.affiliatedAuthor | LEE, JIA | - |
dc.contributor.affiliatedAuthor | Yu, Geunyeol | - |
dc.contributor.affiliatedAuthor | BAE, KYUNGMIN | - |
dc.identifier.scopusid | 2-s2.0-85125488224 | - |
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.