{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:59:46Z","timestamp":1750309186255,"version":"3.41.0"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2024,12,26]],"date-time":"2024-12-26T00:00:00Z","timestamp":1735171200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ANR","award":["ANR-19-CE48-0019"],"award-info":[{"award-number":["ANR-19-CE48-0019"]}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"crossref","award":["431183758"],"award-info":[{"award-number":["431183758"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2025,3,31]]},"abstract":"<jats:p>\n            We show how to efficiently solve problems involving a quantitative measure, here called\n            <jats:italic>energy<\/jats:italic>\n            , as well as a qualitative acceptance condition, expressed as a B\u00fcchi or Parity objective, in finite weighted automata and in one-clock weighted timed automata. Solving the former problem and extracting the corresponding witness is our main contribution and is handled by a modified version of the Bellman-Ford algorithm interleaved with Couvreur\u2019s algorithm. The latter problem is handled via a reduction to the former relying on the corner-point abstraction. All our algorithms are freely available and implemented in a tool based on the open-source platforms TChecker and Spot.\n          <\/jats:p>","DOI":"10.1145\/3678265","type":"journal-article","created":{"date-parts":[[2024,7,18]],"date-time":"2024-07-18T04:06:53Z","timestamp":1721275613000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["\u03c9-Regular Energy Problems"],"prefix":"10.1145","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6767-7751","authenticated-orcid":false,"given":"Sven","family":"Dziadek","sequence":"first","affiliation":[{"name":"Inria, Paris, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9094-7625","authenticated-orcid":false,"given":"Uli","family":"Fahrenberg","sequence":"additional","affiliation":[{"name":"EPITA Research Laboratory (LRE), Rennes, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6611-9659","authenticated-orcid":false,"given":"Philipp","family":"Schlehuber","sequence":"additional","affiliation":[{"name":"EPITA Research Laboratory (LRE), Le Kremlin-Bicetre, France"}]}],"member":"320","published-online":{"date-parts":[[2024,12,26]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-020-00521-4"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45351-2_15"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1090\/qam\/102435"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_34"},{"key":"e_1_3_3_7_2","first-page":"61","volume-title":"HSCC","author":"Bouyer Patricia","year":"2010","unstructured":"Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, and Nicolas Markey. 2010. Timed automata with observers under energy constraints. In HSCC, Karl Henrik Johansson and Wang Yi (Eds.). ACM, 61\u201370."},{"key":"e_1_3_3_8_2","first-page":"33","volume-title":"FORMATS (Lecture Notes in Computer Science)","author":"Bouyer Patricia","year":"2008","unstructured":"Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey, and Ji\u0159\u00ed Srba. 2008. Infinite runs in weighted timed automata with energy constraints. In FORMATS (Lecture Notes in Computer Science), Franck Cassez and Claude Jard (Eds.), Vol. 5215. Springer, Berlin, 33\u201347."},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2013.11.002"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70564-6"},{"issue":"2","key":"e_1_3_3_11_2","article-title":"An  \\(\\omega\\) -Algebra for real-time energy problems","volume":"15","author":"Cachera David","year":"2019","unstructured":"David Cachera, Uli Fahrenberg, and Axel Legay. 2019. An \\(\\omega\\) -Algebra for real-time energy problems. Logical Methods in Computer Science 15, 2 (2019). https:\/\/lmcs.episciences.org\/5507","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.07.038"},{"key":"e_1_3_3_13_2","first-page":"505","volume-title":"FSTTCS (Leibniz International Proceedings in Informatics)","volume":"8","author":"Chatterjee Krishnendu","year":"2010","unstructured":"Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-Fran\u00e7ois Raskin. 2010. Generalized mean-payoff and energy games. In FSTTCS (Leibniz International Proceedings in Informatics), Kamal Lodaya and Meena Mahajan (Eds.), Vol. 8. 505\u2013516."},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48119-2_16"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_14"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.14232\/actacyb.23.1.2017.13"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.14232\/actacyb.23.1.2017.14"},{"key":"e_1_3_3_19_2","first-page":"95","volume-title":"ICTAC (Lecture Notes in Computer Science)","author":"Fahrenberg Uli","year":"2011","unstructured":"Uli Fahrenberg, Line Juhl, Kim G. Larsen, and Ji\u0159\u00ed Srba. 2011. Energy games in multiweighted automata. In ICTAC (Lecture Notes in Computer Science), Antonio Cerone and Pekka Pihlajasaari (Eds.), Vol. 6916. Springer, Berlin, 95\u2013115."},{"key":"e_1_3_3_20_2","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1145\/2380356.2380386","volume-title":"EMSOFT","author":"Falk Heiko","year":"2012","unstructured":"Heiko Falk, Kevin Hammond, Kim G. Larsen, Bj\u00f6rn Lisper, and Stefan M. Petters. 2012. Code-level timing analysis of embedded software. In EMSOFT, Ahmed Jerraya, Luca P. Carloni, Florence Maraninchi, and John Regehr (Eds.). ACM, 163\u2013164."},{"key":"e_1_3_3_21_2","volume-title":"Network Flow Theory.","author":"Ford Lester R.","year":"1956","unstructured":"Lester R. Ford. 1956. Network Flow Theory.RAND Corporation, Santa Monica, CA."},{"key":"e_1_3_3_22_2","first-page":"115","volume-title":"ICTSS (Lecture Notes in Computer Science)","author":"Frehse Goran","year":"2011","unstructured":"Goran Frehse, Kim G. Larsen, Marius Miku\u010dionis, and Brian Nielsen. 2011. Monitoring dynamical signals while testing timed aspects of a system. In ICTSS (Lecture Notes in Computer Science), Burkhart Wolff and Fatiha Za\u00efdi (Eds.), Vol. 7019. Springer, Berlin, 115\u2013130."},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_6"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(1:6)2013"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2016.07.004"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_25"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"e_1_3_3_28_2","first-page":"175","volume-title":"ISoLA (2) (Lecture Notes in Computer Science)","author":"Miku\u010dionis Marius","year":"2010","unstructured":"Marius Miku\u010dionis, Kim G. Larsen, Jacob Illum Rasmussen, Brian Nielsen, Arne Skou, Steen Ulrik Palm, Jan Storbank Pedersen, and Poul Hougaard. 2010. Schedulability analysis using Uppaal: Herschel-Planck case study. In ISoLA (2) (Lecture Notes in Computer Science), Tiziana Margaria and Bernhard Steffen (Eds.), Vol. 6416. Springer, Berlin, 175\u2013190."},{"key":"e_1_3_3_29_2","first-page":"452","volume-title":"LATA (Lecture Notes in Computer Science)","author":"Quaas Karin","year":"2011","unstructured":"Karin Quaas. 2011. On the interval-bound problem for weighted timed automata. In LATA (Lecture Notes in Computer Science), Adrian Horia Dediu, Shunsuke Inenaga, and Carlos Mart\u00edn-Vide (Eds.), Vol. 6638. Springer, Berlin, 452\u2013464."},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59152-6_7"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.03.001"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1983.51"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00009-7"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3678265","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3678265","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:09Z","timestamp":1750287249000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3678265"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,26]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,3,31]]}},"alternative-id":["10.1145\/3678265"],"URL":"https:\/\/doi.org\/10.1145\/3678265","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2024,12,26]]},"assertion":[{"value":"2024-02-18","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-05-30","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-12-26","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}