{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:34:34Z","timestamp":1750221274630,"version":"3.41.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2017,10,31]],"date-time":"2017-10-31T00:00:00Z","timestamp":1509408000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Austrian Science Fund","award":["S11402-N23 (RiSE), Z211-N23 (Wittgenstein Award)"],"award-info":[{"award-number":["S11402-N23 (RiSE), Z211-N23 (Wittgenstein Award)"]}]},{"name":"ERC","award":["279307: Graph Games"],"award-info":[{"award-number":["279307: Graph Games"]}]},{"name":"Microsoft faculty fellows award"},{"name":"European Research Council","award":["267989 (QUAREM)"],"award-info":[{"award-number":["267989 (QUAREM)"]}]},{"DOI":"10.13039\/501100004442","name":"National Science Centre","doi-asserted-by":"crossref","award":["2014\/15\/D\/ST6\/04543"],"award-info":[{"award-number":["2014\/15\/D\/ST6\/04543"]}],"id":[{"id":"10.13039\/501100004442","id-type":"DOI","asserted-by":"crossref"}]},{"name":"FWF NFN","award":["S11407-N23 (RiSE)"],"award-info":[{"award-number":["S11407-N23 (RiSE)"]}]},{"name":"FWF","award":["P23499-N23"],"award-info":[{"award-number":["P23499-N23"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2017,10,31]]},"abstract":"<jats:p>Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata or in any other known decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata, which makes it possible to express important quantitative properties such as average response time. In nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in runtime verification. We establish an almost-complete decidability picture for the basic decision problems about nested weighted automata and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties.<\/jats:p>","DOI":"10.1145\/3152769","type":"journal-article","created":{"date-parts":[[2017,12,15]],"date-time":"2017-12-15T13:39:24Z","timestamp":1513345164000},"page":"1-44","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Nested Weighted Automata"],"prefix":"10.1145","volume":"18","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[{"name":"IST Austria, Klosterneuburg, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[{"name":"IST Austria, Klosterneuburg, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Otop","sequence":"additional","affiliation":[{"name":"University of Wroc\u0142aw, Wroc\u0142aw, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,12,14]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/2050917.2050958"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_31"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2039346.2039347"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.65"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1516512.1516518"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629686"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/1880999.1881063"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1887654.1887673"},{"volume-title":"Proceedings of the 17th International Symposium Fundamentals of Computation Theory (FCT\u201909)","author":"Chatterjee Krishnendu","key":"e_1_2_1_9_1","unstructured":"Krishnendu Chatterjee , Laurent Doyen , and Thomas A. Henzinger . 2009. Alternating weighted automata . In Proceedings of the 17th International Symposium Fundamentals of Computation Theory (FCT\u201909) . Springer, 3--13. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. 2009. Alternating weighted automata. In Proceedings of the 17th International Symposium Fundamentals of Computation Theory (FCT\u201909). Springer, 3--13."},{"key":"e_1_2_1_10_1","volume-title":"Henzinger","author":"Chatterjee Krishnendu","year":"2010","unstructured":"Krishnendu Chatterjee , Laurent Doyen , and Thomas A . Henzinger . 2010 b. Expressiveness and closure properties for quantitative languages. Logic. Methods Comput. Sci . 6, 3 (2010). Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. 2010b. Expressiveness and closure properties for quantitative languages. Logic. Methods Comput. Sci. 6, 3 (2010)."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1805950.1805953"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.72"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.30"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1887459.1887483"},{"key":"e_1_2_1_15_1","volume-title":"Handbook of Weighted Automata","author":"Droste Manfred","unstructured":"Manfred Droste , Werner Kuich , and Heiko Vogler . 2009. Handbook of Weighted Automata ( 1 st ed.). Springer Publishing Company, Inc orporated. Manfred Droste, Werner Kuich, and Heiko Vogler. 2009. Handbook of Weighted Automata (1st ed.). Springer Publishing Company, Incorporated.","edition":"1"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.10.001"},{"volume-title":"Competitive Markov Decision Processes","author":"Filar Jerzy","key":"e_1_2_1_17_1","unstructured":"Jerzy Filar and Koos Vrieze . 1996. Competitive Markov Decision Processes . Springer-Verlag , New York, NY . Jerzy Filar and Koos Vrieze. 1996. Competitive Markov Decision Processes. Springer-Verlag, New York, NY."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_11"},{"volume-title":"TACAS. LNCS 2280","author":"Havelund Klaus","key":"e_1_2_1_19_1","unstructured":"Klaus Havelund and Grigore Rosu . 2002. Synthesizing monitors for safety properties . In TACAS. LNCS 2280 , Springer , 342--356. Klaus Havelund and Grigore Rosu. 2002. Synthesizing monitors for safety properties. In TACAS. LNCS 2280, Springer, 342--356."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.nahs.2016.09.001"},{"key":"e_1_2_1_21_1","unstructured":"J. E. Hopcroft R. Motwani and J. D. Ullman. 2014. Introduction to Automata Theory Languages and Computation. Pearson Education.   J. E. Hopcroft R. Motwani and J. D. Ullman. 2014. Introduction to Automata Theory Languages and Computation. Pearson Education."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.16"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218196794000063"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90321-R"},{"key":"e_1_2_1_25_1","volume-title":"Weighted logics for nested words and algebraic formal power series. Logic. Methods Comput. Sci. 6, 1","author":"Mathissen Christian","year":"2010","unstructured":"Christian Mathissen . 2010. Weighted logics for nested words and algebraic formal power series. Logic. Methods Comput. Sci. 6, 1 ( 2010 ), 5:1--5:34. Christian Mathissen. 2010. Weighted logics for nested words and algebraic formal power series. Logic. Methods Comput. Sci. 6, 1 (2010), 5:1--5:34."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90049-5"},{"key":"e_1_2_1_27_1","first-page":"321","article-title":"Semiring frameworks and algorithms for shortest-distance problems","volume":"7","author":"Mohri Mehryar","year":"2002","unstructured":"Mehryar Mohri . 2002 . Semiring frameworks and algorithms for shortest-distance problems . J. Autom. Lang. Comb. 7 , 3 (2002), 321 -- 350 . Mehryar Mohri. 2002. Semiring frameworks and algorithms for shortest-distance problems. J. Autom. Lang. Comb. 7, 3 (2002), 321--350.","journal-title":"J. Autom. Lang. Comb."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69850-0_11"},{"volume-title":"Handbook of Theoretical Computer Science (Vol. B), Jan van Leeuwen (Ed.)","author":"Thomas Wolfgang","key":"e_1_2_1_29_1","unstructured":"Wolfgang Thomas . 1990. Automata on infinite objects . In Handbook of Theoretical Computer Science (Vol. B), Jan van Leeuwen (Ed.) . MIT Press , Cambridge, MA ,133--191. Wolfgang Thomas. 1990. Automata on infinite objects. In Handbook of Theoretical Computer Science (Vol. B), Jan van Leeuwen (Ed.). MIT Press, Cambridge, MA,133--191."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3152769","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3152769","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:09Z","timestamp":1750212669000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3152769"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,31]]},"references-count":29,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,10,31]]}},"alternative-id":["10.1145\/3152769"],"URL":"https:\/\/doi.org\/10.1145\/3152769","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2017,10,31]]},"assertion":[{"value":"2016-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-12-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}