research-article

Timed automata with observers under energy constraints

Authors:

Patricia Bouyer,

Uli Fahrenberg,

Kim G. Larsen,

Nicolas MarkeyAuthors Info & Claims

HSCC '10: Proceedings of the 13th ACM international conference on Hybrid systems: computation and control

Pages 61 - 70

https://doi.org/10.1145/1755952.1755963

Published: 12 April 2010 Publication History

Get Access

Abstract

In this paper we study one-clock priced timed automata in which prices can grow linearly (dp/dt = k) or exponentially (dp/dt = kp), with discontinuous updates on edges. We propose EXPTIME algorithms to decide the existence of controllers that ensure existence of infinite runs or reachability of some goal location with non-negative observer value all along the run. These algorithms consist in computing the optimal delays that should be elapsed in each location along a run, so that the final observer value is maximized (and never goes below zero).

References

[1]

R. Alur, C. Courcoubetis, N. Halbwachs, Th. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theor. Comp. Science, 138(1):3--34, 1995.

Digital Library

Google Scholar

[2]

R. Alur, C. Courcoubetis, and Th. A. Henzinger. Computing accumulated delays in real-time systems. In Proc. 5th Intl Cond. Computer Aided Verification (CAV'93), volume 697 of Lecture Notes in Computer Science, pages 181--193. Springer, 1993.

Digital Library

Google Scholar

[3]

R. Alur, S. La Torre, and G. J. Pappas. Optimal paths in weighted timed automata. In Proc. 4th Intl Workshop Hybrid Systems: Computation and Control (HSCC'01), volume 2034 of Lecture Notes in Computer Science, pages 49--62. Springer, 2001.

Digital Library

Google Scholar

[4]

R. Alur, S. La Torre, and G. J. Pappas. Optimal paths in weighted timed automata. Theor. Comp. Science, 318(3):297--322, 2004.

Digital Library

Google Scholar

[5]

G. Behrmann, A. Fehnker, Th. Hune, K. G. Larsen, P. Pettersson, J. Romijn, and F. Vaandrager. Minimum-cost reachability for priced timed automata. In Proc. 4th Intl Workshop Hybrid Systems: Computation and Control (HSCC'01), volume 2034 of Lecture Notes in Computer Science, pages 147--161. Springer, 2001.

Digital Library

Google Scholar

[6]

P. Bouyer, U. Fahrenberg, K. G. Larsen, and N. Markey. Timed automata with observers under energy constraints. Research Report LSV-10-01, Lab. Specification & Verification, ENS Cachan, France, 2010.

Digital Library

Google Scholar

[7]

P. Bouyer, U. Fahrenberg, K. G. Larsen, N. Markey, and J. Srba. Infinite runs in weighted timed automata with energy constraints. In Proc. 6th Intl Conf. Formal Modeling and Analysis of Timed Systems (FORMATS'08), Lecture Notes in Computer Science, pages 33--47. Springer, 2008.

Digital Library

Google Scholar

[8]

P. Bouyer, K. G. Larsen, N. Markey, and J. I. Rasmussen. Almost optimal strategies in one-clock priced timed automata. In Proc. 26th Conf. Foundations of Software Technology and Theoretical Computer Science (FSTTCS'06), volume 4337 of Lecture Notes in Computer Science, pages 345--356. Springer, 2006.

Digital Library

Google Scholar

[9]

Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine. Decidable integration graphs. Inf. and Comp., 150(2):209--243, 1999.

Digital Library

Google Scholar

[10]

F. Laroussinie, N. Markey, and Ph. Schnoebelen. Model checking timed automata with one or two clocks. In Proc. 15th Intl Conf. Concurrency Theory (CONCUR'04), volume 3170 of Lecture Notes in Computer Science, pages 387--401. Springer, 2004.

Crossref

Google Scholar

Cited By

View all

Dziadek SFahrenberg USchlehuber P(2024)ω-Regular Energy ProblemsFormal Aspects of Computing10.1145/3678265Online publication date: 17-Jul-2024
https://doi.org/10.1145/3678265
Cuijpers PHansen JLarsen K(2024)Safe and Infinite Resource Scheduling Using Energy Timed AutomataTheoretical Aspects of Software Engineering10.1007/978-3-031-64626-3_5(73-90)Online publication date: 29-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-64626-3_5
Dziadek SFahrenberg USchlehuber-Caissier P(2023)Energy Büchi ProblemsFormal Methods10.1007/978-3-031-27481-7_14(222-239)Online publication date: 3-Mar-2023
https://doi.org/10.1007/978-3-031-27481-7_14
Show More Cited By

Index Terms

Timed automata with observers under energy constraints
1. Computer systems organization
  1. Embedded and cyber-physical systems
  2. Real-time systems

Recommendations

On model-checking timed automata with stopwatch observers

In this paper, we study the model-checking problem for weighted timed automata and the weighted CTL logic; we also study the finiteness of bisimulations of weighted timed automata. Weighted timed automata are timed automata extended with costs on both ...
Lower-bound-constrained runs in weighted timed automata

We investigate a number of problems related to infinite runs of weighted timed automata (with a single weight variable), subject to lower-bound constraints on the accumulated weight. Closing an open problem from Bouyer et al. (2008), we show that the ...
Lower-Bound Constrained Runs in Weighted Timed Automata
QEST '12: Proceedings of the 2012 Ninth International Conference on Quantitative Evaluation of Systems

We investigate a number of problems related to infinite runs of weighted timed automata, subject to lower-bound constraints on the accumulated weight. Closing an open problem from an earlier paper, we show that the existence of an infinite lower-bound-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

HSCC '10: Proceedings of the 13th ACM international conference on Hybrid systems: computation and control

April 2010

308 pages

ISBN:9781605589558

DOI:10.1145/1755952

General Chairs:
Karl Henrik Johansson
KTH, Sweden
,
Wang Yi
Uppsala University, Sweden

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 ACM 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

Published: 12 April 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

HSCC '10

Sponsor:

SIGBED

HSCC '10: The 13th ACM International Conference on Hybrid Systems: Computation and Control

April 12 - 15, 2010

Stockholm, Sweden

Acceptance Rates

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

33
Total Citations
View Citations
206
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)1

Reflects downloads up to 26 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Dziadek SFahrenberg USchlehuber P(2024)ω-Regular Energy ProblemsFormal Aspects of Computing10.1145/3678265Online publication date: 17-Jul-2024
https://doi.org/10.1145/3678265
Cuijpers PHansen JLarsen K(2024)Safe and Infinite Resource Scheduling Using Energy Timed AutomataTheoretical Aspects of Software Engineering10.1007/978-3-031-64626-3_5(73-90)Online publication date: 29-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-64626-3_5
Dziadek SFahrenberg USchlehuber-Caissier P(2023)Energy Büchi ProblemsFormal Methods10.1007/978-3-031-27481-7_14(222-239)Online publication date: 3-Mar-2023
https://doi.org/10.1007/978-3-031-27481-7_14
Bouyer PGastin PHerbreteau FSankur OSrivathsan B(2022)Zone-Based Verification of Timed Automata: Extrapolations, Simulations and What Next?Formal Modeling and Analysis of Timed Systems10.1007/978-3-031-15839-1_2(16-42)Online publication date: 29-Aug-2022
https://doi.org/10.1007/978-3-031-15839-1_2
Hélouët LMarkey NRaha R(2021)Reachability games with relaxed energy constraintsInformation and Computation10.1016/j.ic.2021.104806(104806)Online publication date: Oct-2021
https://doi.org/10.1016/j.ic.2021.104806
Blahoudek FBrázdil TNovotný POrnik MThangeda PTopcu U(2020)Qualitative Controller Synthesis for Consumption Markov Decision ProcessesComputer Aided Verification10.1007/978-3-030-53291-8_22(421-447)Online publication date: 14-Jul-2020
https://doi.org/10.1007/978-3-030-53291-8_22
Hélouët LMarkey NRaha R(2019)Reachability Games with Relaxed Energy ConstraintsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.305.2305(17-33)Online publication date: 13-Sep-2019
https://doi.org/10.4204/EPTCS.305.2
Fahrenberg ULegay A(2019)Quantitative properties of featured automataInternational Journal on Software Tools for Technology Transfer10.1007/s10009-019-00538-yOnline publication date: 23-Sep-2019
https://doi.org/10.1007/s10009-019-00538-y
Bacci GBouyer PFahrenberg ULarsen KMarkey NReynier P(2018)Optimal and Robust Controller SynthesisFormal Methods10.1007/978-3-319-95582-7_12(203-221)Online publication date: 12-Jul-2018
https://doi.org/10.1007/978-3-319-95582-7_12
Fahrenberg ULegay AGnesi SPlat NMelgratti H(2017)Featured weighted automataProceedings of the 5th International FME Workshop on Formal Methods in Software Engineering10.5555/3101290.3101304(51-57)Online publication date: 20-May-2017
https://dl.acm.org/doi/10.5555/3101290.3101304
Show More Cited By

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.

Cited By

Index Terms

Recommendations

On model-checking timed automata with stopwatch observers

Lower-bound-constrained runs in weighted timed automata

Lower-Bound Constrained Runs in Weighted Timed Automata