Just Accepted
ω-Regular Energy Problems
Abstract
We show how to efficiently solve problems involving a quantitative measure, here called energy, as well as a qualitative acceptance condition, expressed as a Büchi 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’s 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.
References
[1]
Rajeev Alur and David L. Dill. 1994. A Theory of Timed Automata. Theoretical Computer Science 126, 2 (1994), 183–235.
[2]
Giovanni Bacci, Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey, and Pierre-Alain Reynier. 2021. Optimal and robust controller synthesis using energy timed automata with uncertainty. Formal Aspects of Computing 33, 1 (2021), 3–25. 10.1007/s00165-020-00521-4
[3]
Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim G. Larsen, Paul Pettersson, Judi Romijn, and Frits W. Vaandrager. 2001. Minimum-Cost Reachability for Priced Timed Automata. In HSCC (Lecture Notes in Computer Science, Vol. 2034), Maria Domenica Di Benedetto and Alberto L. Sangiovanni-Vincentelli (Eds.). Springer, 147–161. 10.1007/3-540-45351-2_15
[4]
Richard Bellman. 1958. On a routing problem. Quart. Appl. Math. 16, 1 (1958), 87–90. 10.1090/qam/102435
[5]
Morten Bisgaard, David Gerhardt, Holger Hermanns, Jan Krčál, Gilles Nies, and Marvin Stenger. 2016. Battery-Aware Scheduling in Low Orbit: The GomX-3 Case. In FM(Lecture Notes in Computer Science, Vol. 9995), John S. Fitzgerald, Constance L. Heitmeyer, Stefania Gnesi, and Anna Philippou (Eds.). Springer, 559–576. 10.1007/978-3-319-48989-6_34
[6]
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–70.
[7]
Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey, and Jiří Srba. 2008. Infinite Runs in Weighted Timed Automata with Energy Constraints. In FORMATS(Lecture Notes in Computer Science, Vol. 5215), Franck Cassez and Claude Jard (Eds.). Springer, 33–47.
[8]
Patricia Bouyer, Kim G. Larsen, and Nicolas Markey. 2014. Lower-bound-constrained runs in weighted timed automata. Performance Evaluation 73 (2014), 91–109. 10.1016/j.peva.2013.11.002
[9]
J. Richard Büchi. 1966. On a Decision Method in Restricted Second Order Arithmetic. In Logic, Methodology and Philosophy of Science. Studies in Logic and the Foundations of Mathematics, Vol. 44. Elsevier, 1–11. 10.1016/S0049-237X(09)70564-6
[10]
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
[11]
Krishnendu Chatterjee and Laurent Doyen. 2012. Energy parity games. Theoretical Computer Science 458 (2012), 49–60. 10.1016/j.tcs.2012.07.038
[12]
Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. 2010. Generalized Mean-payoff and Energy Games. In FSTTCS(Leibniz International Proceedings in Informatics, Vol. 8), Kamal Lodaya and Meena Mahajan (Eds.). 505–516.
[13]
Jean-Michel Couvreur. 1999. On-the-Fly Verification of Linear Temporal Logic. In FM(Lecture Notes in Computer Science, Vol. 1708), Jeannette M. Wing, Jim Woodcock, and Jim Davies (Eds.). Springer, 253–271. 10.1007/3-540-48119-2_16
[14]
Alexandre Duret-Lutz, Étienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, and Henrich Lauko. 2022. From Spot 2.0 to Spot 2.10: What’s New?. In CAV(Lecture Notes in Computer Science, Vol. 13372). Springer, 174–187. 10.1007/978-3-031-13188-2_9
[15]
Sven Dziadek, Uli Fahrenberg, and Philipp Schlehuber-Caissier. 2023. Energy Büchi Problems. In FM(Lecture Notes in Computer Science, Vol. 14000), Marsha Chechik, Joost-Pieter Katoen, and Martin Leucker (Eds.). Springer, 222–239. 10.1007/978-3-031-27481-7_14
[16]
Zoltán Ésik, Uli Fahrenberg, Axel Legay, and Karin Quaas. 2017. An Algebraic Approach to Energy Problems I: \({}^*\) -Continuous Kleene \(\omega\) -Algebras. Acta Cybyernetica 23, 1 (2017), 203–228. 10.14232/actacyb.23.1.2017.13
[17]
Zoltán Ésik, Uli Fahrenberg, Axel Legay, and Karin Quaas. 2017. An Algebraic Approach to Energy Problems II: The Algebra of Energy Functions. Acta Cybyernetica 23, 1 (2017), 229–268. 10.14232/actacyb.23.1.2017.14
[18]
Uli Fahrenberg, Line Juhl, Kim G. Larsen, and Jiří Srba. 2011. Energy Games in Multiweighted Automata. In ICTAC(Lecture Notes in Computer Science, Vol. 6916), Antonio Cerone and Pekka Pihlajasaari (Eds.). Springer, 95–115.
[19]
Heiko Falk, Kevin Hammond, Kim G. Larsen, Björn 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–164.
[20]
Lester R. Ford. 1956. Network Flow Theory.RAND Corporation, Santa Monica, CA.
[21]
Goran Frehse, Kim G. Larsen, Marius Mikučionis, and Brian Nielsen. 2011. Monitoring Dynamical Signals While Testing Timed Aspects of a System. In ICTSS(Lecture Notes in Computer Science, Vol. 7019), Burkhart Wolff and Fatiha Zaïdi (Eds.). Springer, 115–130.
[22]
Paul Gastin and Denis Oddoux. 2001. Fast LTL to Büchi Automata Translation. In CAV(Lecture Notes in Computer Science, Vol. 2102), Gérard Berry, Hubert Comon, and Alain Finkel (Eds.). Springer, 53–65. 10.1007/3-540-44585-4_6
[23]
Frédéric Herbreteau and B. Srivathsan. 2011. Coarse abstractions make Zeno behaviours difficult to detect. Logical Methods in Computer Science 9, 1 (2011). 10.2168/LMCS-9(1:6)2013
[24]
Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. 2016. Better abstractions for timed automata. Information and Computation 251 (2016), 67–90. 10.1016/j.ic.2016.07.004
[25]
François Laroussinie, Nicolas Markey, and Philippe Schnoebelen. 2004. Model Checking Timed Automata with One or Two Clocks. In CONCUR(Lecture Notes in Computer Science, Vol. 3170), Philippa Gardner and Nobuko Yoshida (Eds.). Springer, 387–401. 10.1007/978-3-540-28644-8_25
[26]
Kim G. Larsen, Paul Pettersson, and Wang Yi. 1997. UPPAAL in a Nutshell. Software Tools for Technology Transfer 1, 1-2 (1997), 134–152.
[27]
Marius Mikučionis, 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, Vol. 6416), Tiziana Margaria and Bernhard Steffen (Eds.). Springer, 175–190.
[28]
Karin Quaas. 2011. On the Interval-Bound Problem for Weighted Timed Automata. In LATA(Lecture Notes in Computer Science, Vol. 6638), Adrian Horia Dediu, Shunsuke Inenaga, and Carlos Martín-Vide (Eds.). Springer, 452–464.
[29]
Florian Renkin, Alexandre Duret-Lutz, and Adrien Pommellet. 2020. Practical “Paritizing” of Emerson–Lei Automata. In ATVA(Lecture Notes in Computer Science, Vol. 12302). Springer, 127–143. 10.1007/978-3-030-59152-6_7
[30]
Yaron Velner, Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Alexander Moshe Rabinovich, and Jean-François Raskin. 2015. The complexity of multi-mean-payoff and multi-energy games. Information and Computation 241 (2015), 177–196. 10.1016/j.ic.2015.03.001
[31]
Pierre Wolper, Moshe Y. Vardi, and A. Prasad Sistla. 1983. Reasoning about Infinite Computation Paths. In FOCS. IEEE Computer Society, 185–194. 10.1109/SFCS.1983.51
[32]
Wiesław Zielonka. 1998. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science 200, 1 (1998), 135–183. 10.1016/S0304-3975(98)00009-7
Recommendations
Energy Büchi Problems
Formal MethodsAbstractWe show how to efficiently solve energy Büchi problems in finite weighted automata and in one-clock weighted timed automata. Solving the former problem is our main contribution and is handled by a modified version of Bellman-Ford interleaved with ...
An improved algorithm for determinization of weighted and fuzzy automata
For a given weighted finite automaton over a strong bimonoid we construct its reduced Nerode automaton, which is crisp-deterministic and equivalent to the original weighted automaton with respect to the initial algebra semantics. We show that the ...
Complexity of Topological Properties of Regular ω-Languages
We determine the complexity of topological properties (i.e., properties closed under the Wadge equivalence) of regular ω-languages by showing that they are typically NL-complete (PSPACE-complete) for the deterministic Muller, Mostowski and Büchi ...
Comments
Information & Contributors
Information
Published In
EISSN:1433-299X
Table of ContentsCopyright © 2024 Copyright held by the owner/author(s). Publication rights licensed to ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Online AM: 17 July 2024
Check for updates
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 69Total Downloads
- Downloads (Last 12 months)69
- Downloads (Last 6 weeks)29
Reflects downloads up to 10 Sep 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in