DC Field | Value | Language |
---|---|---|
dc.contributor.author | Bae, Kyungmin | - |
dc.date.accessioned | 2024-03-06T05:45:10Z | - |
dc.date.available | 2024-03-06T05:45:10Z | - |
dc.date.created | 2024-02-21 | - |
dc.date.issued | 2023-10-18 | - |
dc.identifier.uri | https://oasis.postech.ac.kr/handle/2014.oak/121478 | - |
dc.description.abstract | Signal temporal logic (STL) is a temporal logic formalism for specifying properties of continuous signals. STL has been widely used for specifying, monitoring, and testing properties of hybrid systems that exhibit both discrete and continuous behavior. However, model checking techniques for hybrid systems have been primarily limited to invariant and reachability properties. This is mainly due to the intrinsic nature of hybrid systems, which involve uncountably many signals that continuously change over time. For hybrid systems, checking whether all possible behaviors satisfy an STL formula requires a certain form of abstraction and discretization, which has not been developed for general STL properties. In this talk, I introduce bounded model checking algorithms and tools for general STL properties of hybrid systems. Central to our technique is a novel logical foundation for STL: (i) a syntactic separation of STL, which decomposes an STL formula into components, with each component relying exclusively on separate segments of a signal, and (ii) a signal discretization, which ensures a complete abstraction of a signal, given by a set of discrete elements. With this new foundation, the STL model checking problem can be reduced to the satisfiability of a first-order logic formula. This allows us to develop the first model checking algorithm for STL that can guarantee the correctness of STL up to given bound parameters, and a pioneering bounded model checker for hybrid systems, called STLmc. | - |
dc.language | English | - |
dc.publisher | ACM SIGPLAN | - |
dc.relation.isPartOf | 9th ACM International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2023) | - |
dc.relation.isPartOf | Proceedings of the 9th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems | - |
dc.title | Bounded STL Model Checking for Hybrid Systems (Invited Talk) | - |
dc.type | Conference | - |
dc.type.rims | CONF | - |
dc.identifier.bibliographicCitation | 9th ACM International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2023), pp.1 | - |
dc.citation.conferenceDate | 2023-10-22 | - |
dc.citation.conferencePlace | PO | - |
dc.citation.conferencePlace | Cascais Portugal | - |
dc.citation.endPage | 1 | - |
dc.citation.startPage | 1 | - |
dc.citation.title | 9th ACM International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2023) | - |
dc.contributor.affiliatedAuthor | Bae, Kyungmin | - |
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.