{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T02:57:52Z","timestamp":1791341872090,"version":"4.3.1"},"reference-count":49,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"11","license":[{"start":{"date-parts":[[2018,11,1]],"date-time":"2018-11-01T00:00:00Z","timestamp":1541030400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2018,11,1]],"date-time":"2018-11-01T00:00:00Z","timestamp":1541030400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2018,11,1]],"date-time":"2018-11-01T00:00:00Z","timestamp":1541030400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"name":"IOSENSE through the Electronic Component Systems for European Leadership Joint Undertaking","award":["692480"],"award-info":[{"award-number":["692480"]}]},{"name":"AutoDrive through the Electronic Component Systems for European Leadership Joint Undertaking","award":["737469"],"award-info":[{"award-number":["737469"]}]},{"name":"CPS\/IoT Project (HRSM) through Austrian Government through the Federal Ministry of Science, Research and Economy (BMWFW) in the funding program Hochschulraum-Strukturmittel (HRSM) 2016"},{"name":"Austrian National Research Network SHiNE"},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S 11405-N23"],"award-info":[{"award-number":["S 11405-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S 11412-N23"],"award-info":[{"award-number":["S 11412-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."],"published-print":{"date-parts":[[2018,11]]},"DOI":"10.1109\/tcad.2018.2858460","type":"journal-article","created":{"date-parts":[[2018,10,16]],"date-time":"2018-10-16T18:46:00Z","timestamp":1539715560000},"page":"2233-2243","source":"Crossref","is-referenced-by-count":29,"title":["An Algebraic Framework for Runtime Verification"],"prefix":"10.1109","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3203-9415","authenticated-orcid":false,"given":"Stefan","family":"Jak\u0161i\u0107","sequence":"first","affiliation":[{"name":"Center for Digital Safety and Security, Austrian Institute of Technology, Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ezio","family":"Bartocci","sequence":"additional","affiliation":[{"name":"Faculty of Informatics, TU Wien, Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5715-2142","authenticated-orcid":false,"given":"Radu","family":"Grosu","sequence":"additional","affiliation":[{"name":"Faculty of Informatics, TU Wien, Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dejan","family":"Ni\u010dkovi\u0107","sequence":"additional","affiliation":[{"name":"Center for Digital Safety and Security, Austrian Institute of Technology, Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref39","first-page":"321","article-title":"Semiring frameworks and algorithms for shortest-distance problems","volume":"7","author":"mohri","year":"2002","journal-title":"J Automata Lang Combinatorics"},{"key":"ref38","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/s10009-012-0247-9","article-title":"Monitoring properties of analog and mixed-signal circuits","volume":"15","author":"maler","year":"2013","journal-title":"Int J Softw Tools Technol Transf"},{"key":"ref33","first-page":"25","article-title":"Benchmarks for temporal logic requirements for automotive systems","author":"hoxha","year":"2014","journal-title":"Proc 1st 2nd Int Workshop Appl Verification Continuous Hybrid Syst"},{"key":"ref32","first-page":"3","article-title":"Simple on-the-fly automatic verification of linear temporal logic","author":"gerth","year":"1995","journal-title":"Protocol Specification Testing and Verification X"},{"key":"ref31","first-page":"60","author":"finkbeiner","year":"2009","journal-title":"Monitor Circuits for LTL With Bounded and Unbounded Future"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2009.26"},{"key":"ref37","doi-asserted-by":"crossref","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","article-title":"Monitoring temporal properties of continuous signals","author":"maler","year":"2004","journal-title":"Proc Joint Conf Formal Modell Anal Timed Syst Formal Techniques Real-Time Fault Tolerant Syst"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"ref35","first-page":"201","article-title":"Quantitative monitoring of STL with edit distance","volume":"10012","author":"jak\u0161i?","year":"2016","journal-title":"Proc Int'l Conf Runtime Verification (RV)"},{"key":"ref34","doi-asserted-by":"crossref","first-page":"218","DOI":"10.1109\/MEMCOD.2015.7340489","article-title":"From signal temporal logic to FPGA monitors","author":"jak\u0161i?","year":"2015","journal-title":"Proc 8th ACM\/IEEE Int Conf Formal Methods Models Codesign (MEMOCODE)"},{"key":"ref28","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/978-3-540-75454-1_12","article-title":"Robust sampling for MITL specifications","author":"fainekos","year":"2007","journal-title":"Proc 3rd Int Conf Formal Model Anal Timed Syst (FORMATS)"},{"key":"ref27","article-title":"A clock-optimal hierarchical monitoring automaton construction for MITL","author":"d\u2019souza","year":"2013"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.06.021"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2014.6961854"},{"key":"ref1","article-title":"Conformance testing as falsification for cyber-physical systems","author":"abbas","year":"2014","journal-title":"CoRR"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0286-7"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/EMSOFT.2015.7318257"},{"key":"ref21","first-page":"231","article-title":"On-line monitoring for temporal logic robustness","volume":"8734","author":"dokhanchi","year":"2014","journal-title":"Proc Int'l Conf Runtime Verification (RV)"},{"key":"ref24","first-page":"264","article-title":"Efficient robust monitoring for STL","author":"donz\u00e9","year":"2013","journal-title":"Computer Aided Verification (CAV)"},{"key":"ref23","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-3-642-14295-6_17","article-title":"Breach, A toolbox for verification and parameter synthesis of hybrid systems","author":"donz\u00e9","year":"2010","journal-title":"Proc Comput -Aided Verification 22nd Int Conf (CAV)"},{"key":"ref26","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/978-3-319-17524-9_10","article-title":"Efficient guiding strategies for testing of temporal properties of hybrid systems","author":"dreossi","year":"2015","journal-title":"Proc 7th Int Symp NASA Formal Methods"},{"key":"ref25","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/978-3-642-15297-9_9","article-title":"Robust satisfaction of temporal logic over real-valued signals","author":"donz\u00e9","year":"2010","journal-title":"Formal Modeling and Analysis of Times Systems (FORMATS)"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2000799.2000800"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1090\/qam\/102435"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054103002114"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2005.66"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.125.2"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87531-4_28"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/ISQED.2005.32"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2005.26"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535849"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-015-0233-4"},{"key":"ref19","first-page":"337","article-title":"Z3: An efficient SMT solver","author":"de moura","year":"2008","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1025"},{"key":"ref3","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1007\/978-3-319-21668-3_21","article-title":"Time robustness in MTL and expressivity in hybrid system falsification","author":"akazaki","year":"2015","journal-title":"Proc Comput -Aided Verification 27th Int Conf CAV"},{"key":"ref6","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/978-3-319-65765-3_11","article-title":"On the quantitative semantics of regular expressions over real-valued signals","author":"bakhirkin","year":"2017","journal-title":"Proc 3rd Int Conf Formal Model Anal Timed Syst (FORMATS)"},{"key":"ref5","doi-asserted-by":"crossref","first-page":"254","DOI":"10.1007\/978-3-642-19835-9_21","article-title":"S-TaLiRo: A tool for temporal logic falsification for hybrid systems","volume":"6605","author":"annpureddy","year":"2011","journal-title":"Proc 17th Int Conf Tools Algorithms Construct Anal Syst (TACAS)"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/3127041.3127050"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2004.1303336"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103674"},{"key":"ref9","first-page":"128","article-title":"Specification-based monitoring of cyber-physical systems: A survey on theory, tools and applications","author":"bartocci","year":"2018","journal-title":"Lectures on Runtime Verification—Introductory and Advanced Topics"},{"key":"ref46","first-page":"44","article-title":"An autonomous vehicle control stack","author":"rodionova","year":"2017","journal-title":"Proc ARCH 4th Int Workshop Appl Verification Continuous Hybrid Syst Collocated Cyber Phys Syst Week (CPSWeek)"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1145\/2883817.2883839"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.02.007"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-02444-8_30"},{"key":"ref42","doi-asserted-by":"crossref","first-page":"304","DOI":"10.1007\/978-3-540-75454-1_22","article-title":"AMT: A property-based monitoring tool for analog systems","author":"nickovic","year":"2007","journal-title":"Proc 3rd Int Conf Formal Model Anal Timed Syst (FORMATS)"},{"key":"ref41","article-title":"Checking timed and hybrid properties: Theory and applications","author":"nickovic","year":"2008"},{"key":"ref44","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/978-3-540-88562-7_19","article-title":"On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology","author":"rizk","year":"2008","journal-title":"Proc 6th Int Conf Comput Methods Syst Biol (CMSB)"},{"key":"ref43","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/978-3-540-69850-0_11","article-title":"On the merits of temporal testers","author":"pnueli","year":"2008","journal-title":"25 Years of Model Checking—History Achievements Perspectives"}],"container-title":["IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/43\/8496924\/08493500.pdf?arnumber=8493500","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,16]],"date-time":"2023-08-16T17:31:21Z","timestamp":1692207081000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8493500\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,11]]},"references-count":49,"journal-issue":{"issue":"11"},"URL":"https:\/\/doi.org\/10.1109\/tcad.2018.2858460","relation":{},"ISSN":["0278-0070","1937-4151"],"issn-type":[{"value":"0278-0070","type":"print"},{"value":"1937-4151","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,11]]}}}