{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,14]],"date-time":"2026-07-14T15:52:24Z","timestamp":1784044344158,"version":"3.55.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"JST ACT-X","award":["JPMJAX200U"],"award-info":[{"award-number":["JPMJAX200U"]}]},{"name":"JST ERATO HASUO Metamathematics for Systems Design Project","award":["JPMJER1603"],"award-info":[{"award-number":["JPMJER1603"]}]},{"name":"JSPS Grant-in-Aid","award":["18J22498"],"award-info":[{"award-number":["18J22498"]}]},{"name":"ANR-NRF ProMiS","award":["ANR-19-CE25-0015"],"award-info":[{"award-number":["ANR-19-CE25-0015"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Cyber-Phys. Syst."],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>\n            Monitoring of hybrid systems attracts both scientific and practical attention. However, monitoring algorithms suffer from the methodological difficulty of only observing sampled discrete-time signals, while real behaviors are continuous-time signals. To mitigate this problem of sampling uncertainties, we introduce a\n            <jats:italic>model-bounded monitoring<\/jats:italic>\n            scheme, where we use prior knowledge about the target system to prune interpolation candidates. Technically, we express such prior knowledge by linear hybrid automata (LHAs)\u2014the LHAs are called\n            <jats:italic>bounding models<\/jats:italic>\n            . We introduce a novel notion of\n            <jats:italic>monitored language<\/jats:italic>\n            of LHAs, and we reduce the monitoring problem to the membership problem of the monitored language. We present two partial algorithms\u2014one is via reduction to reachability in LHAs and the other is a direct one using polyhedra\u2014and show that these methods, and thus the proposed model-bounded monitoring scheme, are efficient and practically relevant.\n          <\/jats:p>","DOI":"10.1145\/3529095","type":"journal-article","created":{"date-parts":[[2022,4,25]],"date-time":"2022-04-25T16:29:32Z","timestamp":1650904172000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Model-bounded Monitoring of Hybrid Systems"],"prefix":"10.1145","volume":"6","author":[{"given":"Masaki","family":"Waga","sequence":"first","affiliation":[{"name":"Kyoto University, Sakyo-ku, Kyoto-shi, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"\u00c9tienne","family":"Andr\u00e9","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Lorraine, CNRS, Inria, LORIA, Vandoeuvre-l\u00e8s-Nancy, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ichiro","family":"Hasuo","sequence":"additional","affiliation":[{"name":"National Institute of Informatics, Chiyoda-ku, Tokyo, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,11,5]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.1998.739751"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS2018.2018.00010"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-92970-5_13"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-00151-3_13"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32304-2_10"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22012-8_33"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-02444-8_6"},{"key":"e_1_3_2_10_2","first-page":"120","volume-title":"Proceedings of the ARCH@CPSIoTWeek (EPiC Series in Computing)","volume":"61","author":"Bu Lei","year":"2019","unstructured":"Lei Bu, Rajarshi Ray, and Stefan Schupp. 2019. ARCH-COMP19 category report: Bounded model checking of hybrid systems with piecewise constant dynamics. In Proceedings of the ARCH@CPSIoTWeek (EPiC Series in Computing), Vol. 61. EasyChair, 120\u2013128."},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-55089-9_2"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44618-4_12"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24288-5_13"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0066-0"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/11603009_13"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2012.69"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.29007\/xwl1"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.06.021"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24743-2_22"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0062-x"},{"key":"e_1_3_2_21_2","first-page":"1","volume-title":"Proceedings of the ARCH@CPSIoTWeek (EPiC Series in Computing)","volume":"61","author":"Frehse Goran","year":"2019","unstructured":"Goran Frehse, Alessandro Abate, Dieky Adzkiya, Anna Becchi, Lei Bu, Alessandro Cimatti, Mirco Giacobbe, Alberto Griggio, Sergio Mover, Muhammad Syifa\u2019ul Mufid, Idriss Riouak, Stefano Tonetta, and Enea Zaffanella. 2019. ARCH-COMP19 category report: Hybrid systems with piecewise constant dynamics. In Proceedings of the ARCH@CPSIoTWeek (EPiC Series in Computing), Vol. 61. EasyChair, 1\u201313."},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.future.2013.01.010"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58485-4_43"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0031995"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.4271\/2016-01-0621"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0241-z"},{"key":"e_1_3_2_28_2","volume-title":"Verified Runtime Validation for Partially Observable Hybrid Systems","author":"Mitsch Stefan","year":"2018","unstructured":"Stefan Mitsch and Andr\u00e9 Platzer. 2018. Verified Runtime Validation for Partially Observable Hybrid Systems. Technical Report. Retrieved from http:\/\/arxiv.org\/abs\/1811.06502."},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2017.06.060"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.64"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71493-4_37"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-57628-8_11"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/0-8176-4404-0_21"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10512-3_16"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3178126.3178129"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29662-9_1"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-20652-9_26"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_30"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/3450267.3450531"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-65765-3_13"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_37"}],"container-title":["ACM Transactions on Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3529095","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3529095","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:51:25Z","timestamp":1750182685000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3529095"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":40,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3529095"],"URL":"https:\/\/doi.org\/10.1145\/3529095","relation":{},"ISSN":["2378-962X","2378-9638"],"issn-type":[{"value":"2378-962X","type":"print"},{"value":"2378-9638","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2021-06-29","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-03-24","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-11-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}