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
Times are displayed in time zone: Greenwich Mean Time : Belfast change

13:45 - 14:51: Model CheckingResearch Papers at Sala II
Chair(s): P. MadhusudanUniversity of Illinois at Urbana-Champaign
13:45 - 14:07
Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations
Research Papers
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 Media Attached File Attached
14:07 - 14:29
Bounded Model Checking of Signal Temporal Logic Properties Using Syntactic Separation
Research Papers
Kyungmin BaePohang University of Science and Technology (POSTECH), Jia LeePohang University of Science and Technology (POSTECH)
Link to publication DOI Media Attached File Attached
14:29 - 14:51
Adventures in Monitorability: From Branching to Linear Time and Back Again
Research Papers
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 Media Attached