{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T22:30:17Z","timestamp":1783549817338,"version":"3.55.0"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2023,2,28]],"date-time":"2023-02-28T00:00:00Z","timestamp":1677542400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"crossref","award":["778233"],"award-info":[{"award-number":["778233"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Runtime enforcement is a dynamic analysis technique that instruments a\nmonitor with a system in order to ensure its correctness as specified by some\nproperty. This paper explores bidirectional enforcement strategies for\nproperties describing the input and output behaviour of a system. We develop an\noperational framework for bidirectional enforcement and use it to study the\nenforceability of the safety fragment of Hennessy-Milner logic with recursion\n(sHML). We provide an automated synthesis function that generates correct\nmonitors from sHML formulas, and show that this logic is enforceable via a\nspecific type of bidirectional enforcement monitors called action disabling\nmonitors.<\/jats:p>","DOI":"10.46298\/lmcs-19(1:14)2023","type":"journal-article","created":{"date-parts":[[2023,3,1]],"date-time":"2023-03-01T08:27:52Z","timestamp":1677659272000},"source":"Crossref","is-referenced-by-count":6,"title":["Bidirectional Runtime Enforcement of First-Order Branching-Time Properties"],"prefix":"10.46298","volume":"Volume 19, Issue 1","author":[{"given":"Luca","family":"Aceto","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ian","family":"Cassar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Adrian","family":"Francalanza","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anna","family":"Ingolfsdottir","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"25203","published-online":{"date-parts":[[2023,2,28]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/11002\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/11002\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T20:20:40Z","timestamp":1687292440000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/8944"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,2,28]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-19(1:14)2023","relation":{"has-preprint":[{"id-type":"arxiv","id":"2201.03108v2","asserted-by":"subject"},{"id-type":"arxiv","id":"2201.03108v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2201.03108","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2201.03108","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,2,28]]},"article-number":"8944"}}