{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T02:42:48Z","timestamp":1772505768209,"version":"3.50.1"},"reference-count":23,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","license":[{"start":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T00:00:00Z","timestamp":1570752000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2019,10,31]]},"abstract":"<jats:p>\n            This paper presents a novel framework for decentralized monitoring of Linear Temporal Logic (LTL) formulas, under the situation where processes are synchronous and the formula is represented as a tableau. The tableau technique allows one to construct a semantic tree for the input LTL formula, which can be used to optimize the decentralized monitoring of LTL in various ways. Given a system\n            <jats:italic>P<\/jats:italic>\n            and an LTL formula \u03c6, we construct a tableau T\n            <jats:sub>\u03c6<\/jats:sub>\n            . The tableau T\n            <jats:sub>\u03c6<\/jats:sub>\n            is used for two purposes: (a) to synthesize an efficient round-robin communication policy for processes, and (b) to find the minimal ways to decompose the formula and communicate observations of processes in an efficient way. In our framework, processes can propagate truth values of both atomic and compound formulas (non-atomic formulas) depending on the syntactic structure of the input LTL formula and the observation power of processes. We demonstrate that this approach of decentralized monitoring based on tableau construction is more straightforward, more flexible, and more likely to yield efficient solutions than alternative approaches.\n          <\/jats:p>","DOI":"10.1145\/3358219","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-21","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Efficient Decentralized LTL Monitoring Framework Using Tableau Technique"],"prefix":"10.1145","volume":"18","author":[{"given":"Omar","family":"Bataineh","sequence":"first","affiliation":[{"name":"National University of Singapore, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David S.","family":"Rosenblum","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Reynolds","sequence":"additional","affiliation":[{"name":"University of Western Australia, Crawley WA, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,10,11]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Hamid Alavi George Avrunin James Corbett Laura Dillon Matt Dwyer and Corina Pasareanu. 2011. Specification patterns website. http:\/\/patterns.projects.cis.ksu.edu\/.  Hamid Alavi George Avrunin James Corbett Laura Dillon Matt Dwyer and Corina Pasareanu. 2011. Specification patterns website. http:\/\/patterns.projects.cis.ksu.edu\/."},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the Thirteenth National Conference on Artificial Intelligence. 1215--1222","author":"Bacchus Fahiem","year":"1996","unstructured":"Fahiem Bacchus and Froduald Kabanza . 1996 . Planning for temporally extended goals . In Proceedings of the Thirteenth National Conference on Artificial Intelligence. 1215--1222 . Fahiem Bacchus and Froduald Kabanza. 1996. Planning for temporally extended goals. In Proceedings of the Thirteenth National Conference on Artificial Intelligence. 1215--1222."},{"key":"e_1_2_1_3_1","volume-title":"35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS","volume":"45","author":"Basin David","year":"2015","unstructured":"David Basin , Felix Klaedtke , and Eugen Zalinescu . 2015 . Failure-aware runtime verification of distributed systems . In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015), Vol. 45 , 590--603. David Basin, Felix Klaedtke, and Eugen Zalinescu. 2015. Failure-aware runtime verification of distributed systems. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015), Vol. 45, 590--603."},{"key":"e_1_2_1_4_1","volume-title":"Runtime verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology (TOSEM)","author":"Bauer Andreas","year":"2011","unstructured":"Andreas Bauer , Martin Leucker , and Christian Schallhart . 2011. Runtime verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology (TOSEM) ( 2011 ), 14:1--14:64. Andreas Bauer, Martin Leucker, and Christian Schallhart. 2011. Runtime verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology (TOSEM) (2011), 14:1--14:64."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32759-9_10"},{"key":"e_1_2_1_6_1","unstructured":"E. Beth. 1955. Semantic Entailment and Formal Derivability. Mededelingen der Koninklijke Nederlandse Akad. van Wetensch.  E. Beth. 1955. Semantic Entailment and Formal Derivability. Mededelingen der Koninklijke Nederlandse Akad. van Wetensch."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0251-x"},{"key":"e_1_2_1_8_1","volume-title":"13th International Workshop, FMICS 2008, L\u2019Aquila, Italy. 135--149","author":"Colombo Christian","year":"2008","unstructured":"Christian Colombo , Gordon J. Pace , and Gerardo Schneider . 2008 . Dynamic event-based runtime monitoring of real-time and contextual properties. In Formal Methods for Industrial Critical Systems , 13th International Workshop, FMICS 2008, L\u2019Aquila, Italy. 135--149 . Christian Colombo, Gordon J. Pace, and Gerardo Schneider. 2008. Dynamic event-based runtime monitoring of real-time and contextual properties. In Formal Methods for Industrial Critical Systems, 13th International Workshop, FMICS 2008, L\u2019Aquila, Italy. 135--149."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2005.26"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the 21st International Conference on Software Engineering. 411--420","author":"Dwyer Matthew B.","unstructured":"Matthew B. Dwyer , George S. Avrunin , and James C. Corbett . 1999. Patterns in property specifications for finite-state verification . In Proceedings of the 21st International Conference on Software Engineering. 411--420 . Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. 1999. Patterns in property specifications for finite-state verification. In Proceedings of the 21st International Conference on Software Engineering. 411--420."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3092723"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing (STOC\u201982)","author":"Allen Emerson E.","unstructured":"E. Allen Emerson and Joseph Y. Halpern . 1982. Decision procedures and expressiveness in the temporal logic of branching time . In Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing (STOC\u201982) . 169--180. E. Allen Emerson and Joseph Y. Halpern. 1982. Decision procedures and expressiveness in the temporal logic of branching time. In Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing (STOC\u201982). 169--180."},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Yli\u00e8s Falcone Tom Cornebize and Jean-Claude Fernandez. 2014. Efficient and generalized decentralized monitoring of regular languages. In Formal Techniques for Distributed Objects Components and Systems. 66--83.  Yli\u00e8s Falcone Tom Cornebize and Jean-Claude Fernandez. 2014. Efficient and generalized decentralized monitoring of regular languages. In Formal Techniques for Distributed Objects Components and Systems. 66--83.","DOI":"10.1007\/978-3-662-43613-4_5"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/SRDS.2018.00032"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/647762.735505"},{"key":"e_1_2_1_16_1","volume-title":"Introduction to Metamathematics. North-Holland","author":"Kleene Stephen Cole","unstructured":"Stephen Cole Kleene . 1952. Introduction to Metamathematics. North-Holland , Amsterdam . Stephen Cole Kleene. 1952. Introduction to Metamathematics. North-Holland, Amsterdam."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2015.95"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29860-8_23"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.226.20"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2014.6961843"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/998675.999446"},{"key":"e_1_2_1_24_1","volume-title":"First Order Logic","author":"Smullyan Raymond","unstructured":"Raymond Smullyan . 1968. First Order Logic . Springer-Verlag . Raymond Smullyan. 1968. First Order Logic. Springer-Verlag."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3358219","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3358219","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:23:07Z","timestamp":1750202587000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3358219"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,11]]},"references-count":23,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2019,10,31]]}},"alternative-id":["10.1145\/3358219"],"URL":"https:\/\/doi.org\/10.1145\/3358219","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,11]]},"assertion":[{"value":"2019-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-10-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}