Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Fri 18 Jan 2019 14:07 - 14:29 at Sala II - Model Checking Chair(s): P. Madhusudan

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.

Fri 18 Jan

13:45 - 14:51: Research Papers - Model Checking at Sala II
Chair(s): P. MadhusudanUniversity of Illinois at Urbana-Champaign
POPL-2019-Research-Papers13:45 - 14:07
Taolue ChenBirkbeck, University of London, Matthew HagueRoyal Holloway, University of London, Anthony Widjaja LinOxford University, Philipp RuemmerUppsala University, Zhilin WuState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
Link to publication DOI File Attached
POPL-2019-Research-Papers14:07 - 14:29
Kyungmin BaePohang University of Science and Technology (POSTECH), Jia LeePohang University of Science and Technology (POSTECH)
Link to publication DOI File Attached
POPL-2019-Research-Papers14:29 - 14:51
Luca AcetoReykjavik University, Antonis AchilleosReykjavik University, Adrian FrancalanzaUniversity of Malta, Anna IngolfsdottirReykjavik University, Karoliina LehtinenUniversity of Kiel and University of Liverpool
Link to publication DOI