{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,7]],"date-time":"2026-02-07T12:54:54Z","timestamp":1770468894729,"version":"3.49.0"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","funder":[{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"crossref","award":["ICT22-023 (TAIGER)"],"award-info":[{"award-number":["ICT22-023 (TAIGER)"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"crossref"}]},{"name":"European Commission in the Horizon Europe research and innovation programme","award":["101107303 (MSCA Postdoctoral Fellowship CORPORA), 101160022 (VASSAL), 101212818 (RobustifAI)"],"award-info":[{"award-number":["101107303 (MSCA Postdoctoral Fellowship CORPORA), 101160022 (VASSAL), 101212818 (RobustifAI)"]}]},{"name":"Italian Ministry of University and Research under the National Recovery and Resilience Plan (NRRP) and European Commission under the NextGenerationEU project","award":["DM352\/22"],"award-info":[{"award-number":["DM352\/22"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2025,9,30]]},"abstract":"<jats:p>Signal Temporal Logic (STL) is a widely recognized formal specification language to express rigorous temporal requirements on mixed analog signals produced by cyber-physical systems (CPS). A relevant problem in CPS design is how to efficiently and automatically check whether a set of STL requirements is logically consistent. This problem reduces to solving the STL satisfiability problem, which is decidable when we assume that our system operates in discrete time steps dictated by an embedded system\u2019s clock.<\/jats:p>\n          <jats:p>This article introduces a novel tree-shaped, one-pass tableau method for satisfiability checking of discrete-time STL with bounded temporal operators. Originally designed to prove the consistency of a given set of STL requirements, this method has a wide range of applications beyond consistency checking. These include synthesizing example signals that satisfy the given requirements, as well as verifying or refuting the equivalence and implications of STL formulas.<\/jats:p>\n          <jats:p>Our tableau exploits redundancy arising from large time intervals in STL formulas to speed up satisfiability checking, and can also be employed to check Mission-Time Linear Temporal Logic (MLTL) satisfiability. We compare our tableau with Satisfiability Modulo Theories (SMT) and First-Order Logic encodings from the literature on a benchmark suite, partly collected from the literature, and partly provided by an industrial partner. Our experiments show that, in many cases, our tableau outperforms state-of-the-art encodings.<\/jats:p>","DOI":"10.1145\/3759917","type":"journal-article","created":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T07:52:43Z","timestamp":1754639563000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A Tree-Shaped Tableau for Checking the Satisfiability of Signal Temporal Logic with Bounded Temporal Operators"],"prefix":"10.1145","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9051-1597","authenticated-orcid":false,"given":"Beatrice","family":"Melani","sequence":"first","affiliation":[{"name":"Dipartimento di Elettronica, Informazione e Bioingegneria, Politecnico di Milano","place":["Milan, Italy"]}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8004-6601","authenticated-orcid":false,"given":"Ezio","family":"Bartocci","sequence":"additional","affiliation":[{"name":"Institute of Computer Engineering (E191-01), TU Wien","place":["Vienna, Austria"]}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7742-9233","authenticated-orcid":false,"given":"Michele","family":"Chiari","sequence":"additional","affiliation":[{"name":"Institute of Computer Engineering (E191-01), TU Wien","place":["Vienna, Austria"]}]}],"member":"320","published-online":{"date-parts":[[2025,9,26]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/227595.227602"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1006\/INCO.1993.1025"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/174644.174651"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290364"},{"key":"e_1_3_2_6_2","volume-title":"Principles of Model Checking","author":"Baier Christel","year":"2008","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-75632-5_5"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-020-00599-4"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3714467"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2022.104957"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2013.20"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2015.06.007"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/S00236-015-0229-Y"},{"key":"e_1_3_2_14_2","first-page":"950","volume-title":"Proceedings of the IJCAI\u201916","author":"Bertello Matteo","year":"2016","unstructured":"Matteo Bertello, Nicola Gigante, Angelo Montanari, and Mark Reynolds. 2016. Leviathan: A new LTL satisfiability checking tool based on a one-pass tree-shaped tableau. In Proceedings of the IJCAI\u201916. IJCAI\/AAAI Press, 950\u2013956. Retrieved from http:\/\/www.ijcai.org\/Abstract\/16\/139"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.JSS.2020.110881"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2023.3242588"},{"key":"e_1_3_2_17_2","volume-title":"SC \\(^2\\) @ISSAC\u201917 (CEUR Workshop Proceedings)","author":"Brain Martin","year":"2017","unstructured":"Martin Brain, James H. Davenport, and Alberto Griggio. 2017. Benchmarking solvers, SAT-style. In SC \\(^2\\) @ISSAC\u201917 (CEUR Workshop Proceedings). CEUR-WS.org. Retrieved from https:\/\/ceur-ws.org\/Vol-1974\/RP3.pdf"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_29"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3147451"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_17"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2020.104599"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-023-09691-1"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.29007\/3HB9"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510171"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/234426.234431"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_26"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2004.12.002"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.29007\/xwrs"},{"key":"e_1_3_2_31_2","volume-title":"Systems and Software Engineering \u2013 Life Cycle Processes \u2013 Requirements Engineering","year":"2018","unstructured":"ISO\/IEC\/IEEE. 2018. Systems and Software Engineering \u2013 Life Cycle Processes \u2013 Requirements Engineering. Technical Report ISO\/IEC\/IEEE 29148:2018. International Organization for Standardization, Geneva, Switzerland."},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2015.7340489"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/2562059.2562140"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.4271\/2016-01-0621"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/0041-5553(80)90061-0"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE51524.2021.9678719"},{"key":"e_1_3_2_38_2","article-title":"mltlsat","author":"Li Jianwen","year":"2019","unstructured":"Jianwen Li. 2019. mltlsat. GitHub.com. Retrieved August 20th, 2025 from https:\/\/github.com\/lijwen2748\/mltlsat","journal-title":"GitHub.com"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2022.104923"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/8.1.55"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.256.12"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"e_1_3_2_44_2","unstructured":"Beatrice Melani Ezio Bartocci and Michele Chiari. 2025. STLTree. Retrieved August 20th 2025 from https:\/\/github.com\/beamelani\/Consistency_Check"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-75434-0_18"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_35"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2018.00038"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2014.7039363"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_24"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.226.20"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_11"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-010-0140-3"},{"key":"e_1_3_2_54_2","first-page":"119","article-title":"The tableau method for temporal logic: An Overview","volume":"28","author":"Wolper Pierre","year":"1985","unstructured":"Pierre Wolper. 1985. The tableau method for temporal logic: An Overview. Logique et Analyse 28, 110\/111 (1985), 119\u2013136.","journal-title":"Logique et Analyse"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3759917","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T14:28:45Z","timestamp":1759933725000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3759917"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,26]]},"references-count":53,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2025,9,30]]}},"alternative-id":["10.1145\/3759917"],"URL":"https:\/\/doi.org\/10.1145\/3759917","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,26]]},"assertion":[{"value":"2025-07-30","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-03","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-09-26","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}