{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T02:57:38Z","timestamp":1791341858533,"version":"4.3.1"},"reference-count":66,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100003725","name":"National Research Foundation of Korea","doi-asserted-by":"crossref","award":["2017M3C4A7068175,2016R1D1A1B03935275"],"award-info":[{"award-number":["2017M3C4A7068175,2016R1D1A1B03935275"]}],"id":[{"id":"10.13039\/501100003725","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100002541","name":"Pohang University of Science and Technology","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002541","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/3290364","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":39,"title":["Bounded model checking of signal temporal logic properties using syntactic separation"],"prefix":"10.1145","volume":"3","author":[{"given":"Kyungmin","family":"Bae","sequence":"first","affiliation":[{"name":"POSTECH, South Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jia","family":"Lee","sequence":"additional","affiliation":[{"name":"POSTECH, South Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2465787.2465797"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461358"},{"key":"e_1_2_2_3_1","volume-title":"Principles of cyber-physical systems","author":"Alur Rajeev"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/227595.227602"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/174644.174651"},{"key":"e_1_2_2_6_1","series-title":"Lecture Notes in Computer Science","volume-title":"S-taliro: a tool for temporal logic falsification for hybrid systems","author":"Annpureddy Yashwanth"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/3168451.3168490"},{"key":"e_1_2_2_8_1","volume-title":"Computer Aided Verification (Lecture Notes in Computer Science)","author":"Bak Stanley"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.06.007"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-015-0229-y"},{"key":"e_1_2_2_11_1","volume-title":"Bounded model checking. Advances in computers 58","author":"Biere Armin","year":"2003"},{"key":"e_1_2_2_12_1","volume-title":"Handbook of satisfiability","author":"Biere Armin"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11590156_35"},{"key":"e_1_2_2_14_1","volume-title":"Flow*: an analyzer for non-linear hybrid systems","author":"Chen Xin"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_4"},{"key":"e_1_2_2_16_1","volume-title":"Formal Methods in Computer-Aided Design (FMCAD)","author":"Cimatti Alessandro"},{"key":"e_1_2_2_17_1","volume-title":"AAAI Conference on Artificial Intelligence. AAAI. https:\/\/www.aaai.org\/ocs\/index.php\/AAAI\/AAAI12\/paper\/view\/5072","author":"Cimatti Alessandro","year":"2012"},{"key":"e_1_2_2_18_1","volume-title":"Model checking","author":"Clarke Edmund M"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2011.59"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1519231.1519267"},{"key":"e_1_2_2_21_1","first-page":"128","article-title":"Reachability analysis for polynomial dynamical systems using the Bernstein expansion","volume":"17","author":"Dang Thao","year":"2012","journal-title":"Reliable Computing"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0286-7"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2015.7340472"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_17"},{"key":"e_1_2_2_26_1","volume-title":"Efficient robust monitoring for STL","author":"Donz\u00e9 Alexandre"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/2555754.2555780"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-012-0295-3"},{"key":"e_1_2_2_29_1","volume-title":"Automatic reachability analysis for nonlinear hybrid models with C2E2","author":"Fan Chuchu"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/2387933.2387940"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/1239153.1239179"},{"key":"e_1_2_2_32_1","volume-title":"Alexandre Donz\u00e9, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler.","author":"Frehse Goran","year":"2011"},{"key":"e_1_2_2_33_1","volume-title":"Expressive functional completeness in tense logic","author":"Gabbay Dov M."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_23"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"e_1_2_2_36_1","volume-title":"Clarke","author":"Gao Sicun","year":"2013"},{"key":"e_1_2_2_37_1","volume-title":"Computer Aided Verification","author":"Geilen Marc"},{"key":"e_1_2_2_38_1","volume-title":"Protocol Specification","author":"Gerth Rob"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/11730637_22"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40648-0_29"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_18"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/2944225.2944368"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59615-5_13"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1581"},{"key":"e_1_2_2_45_1","volume-title":"Online monitoring of metric temporal logic","author":"Ho Hsi-Ming"},{"key":"e_1_2_2_46_1","volume-title":"Hodkinson and Mark Reynolds","author":"Ian","year":"2005"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.41"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0193-y"},{"key":"e_1_2_2_49_1","volume-title":"Quantitative monitoring of STL with edit distance","author":"Jak\u0161i\u0107 Stefan"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2562059.2562140"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_27"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_15"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"e_1_2_2_55_1","volume-title":"Planning algorithms","author":"LaValle Steven M"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"e_1_2_2_57_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Ni\u010dkovi\u0107 Dejan"},{"key":"e_1_2_2_58_1","volume-title":"Formal Modeling and Analysis of Timed Systems, Jean-Fran\u00e7ois Raskin and P","author":"Nickovic Dejan"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85778-5_1"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9103-8"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0079-8"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2007.902736"},{"key":"e_1_2_2_63_1","volume-title":"Hybrid systems","author":"Raisch J\u00f6rg"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/2728606.2728628"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_26"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3178126.3178140"},{"key":"e_1_2_2_67_1","volume-title":"Computer Aided Verification (Lecture Notes in Computer Science)","author":"Tiwari Ashish"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290364","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290364","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290364"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":66,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290364"],"URL":"https:\/\/doi.org\/10.1145\/3290364","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}