More Web Proxy on the site http://driver.im/

research-article

Why Liveness for Timed Automata Is Hard, and What We Can Do About It

Authors:

Frédéric Herbreteau,

Thanh-Tung Tran,

Igor WalukiewiczAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 21, Issue 3

Article No.: 17, Pages 1 - 28

https://doi.org/10.1145/3372310

Published: 03 March 2020 Publication History

Abstract

The reachability problem for timed automata asks if a given automaton has a run leading to an accepting state, and the liveness problem asks if the automaton has an infinite run that visits accepting states infinitely often. Both of these problems are known to be Pspace-complete.

We show that if P ≠Pspace, the liveness problem is more difficult than the reachability problem; in other words, we exhibit a family of automata for which solving the reachability problem with the standard algorithm is in P but solving the liveness problem is Pspace-hard. This leads us to revisit the algorithmics for the liveness problem. We propose a notion of a witness for the fact that a timed automaton violates a liveness property. We give an algorithm for computing such a witness and compare it to existing solutions.

References

[1]

R. Alur and D. L. Dill. 1994. A theory of timed automata. Theoretical Computer Science 126, 2 (1994), 183--235.

Digital Library

[2]

G. Behrmann, P. Bouyer, E. Fleury, and K. G. Larsen. 2003. Static guard analysis in timed automata verification. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 254--270.

[3]

G. Behrmann, P. Bouyer, K. G. Larsen, and R. Pelánek. 2006. Lower and upper bounds in zone-based abstractions of timed automata. International Journal on Software Tools for Technology Transfer 8, 3 (2006), 204--215.

Digital Library

[4]

C. Daws and S. Tripakis. 1998. Model checking of real-time reachability properties using abstractions. In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, Vol. 1384. Springer, 313--329.

[5]

D. L. Dill. 1989. Timing assumptions and verification of finite-state concurrent systems. In Automatic Verification Methods for Finite State Systems. Lecture Notes in Computer Science, Vol. 407. Springer, 197--212.

[6]

F. Herbreteau and B. Srivathsan. 2013. Coarse abstractions make Zeno behaviours difficult to detect. Logical Methods in Computer Science 9, 1 (2013), 1--6.

[7]

F. Herbreteau, B. Srivathsan, T.-T. Tran, and I. Walukiewicz. 2016. Why liveness for timed automata is hard, and what we can do about it. In Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Article 48, 14 pages.

[8]

F. Herbreteau, B. Srivathsan, and I. Walukiewicz. 2012. Better abstractions for timed automata. In Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS’12). IEEE, Los Alamitos, CA, 375--384.

[9]

F. Herbreteau, B. Srivathsan, and I. Walukiewicz. 2012. Efficient emptiness check for timed Büchi automata. Formal Methods in System Design 40, 2 (2012), 122--146.

Digital Library

[10]

F. Herbreteau, B. Srivathsan, and I. Walukiewicz. 2013. Lazy abstractions for timed automata. In Computer Aided Verification. Lecture Notes in Computer Science, Vol. 8044. Springer, 990--1005.

[11]

Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. 2016. Better abstractions for timed automata. Information and Computation 251 (2016), 67--90.

Digital Library

[12]

F. Herbreteau and T.-T. Tran. 2015. Improving search order for reachability testing in timed automata. In Formal Modeling and Analysis of Timed Systems. Lecture Notes in Computer Science, Vol. 9268. Springer, 124--139.

[13]

A. Laarman, M. C. Olesen, A. E. Dalsgaard, K. G. Larsen, and J. van de Pol. 2013. Multi-core emptiness checking of timed Büchi automata using inclusion abstraction. In Computer Aided Verification. Lecture Notes in Computer Science, Vol. 8044. Springer, 968--983.

[14]

G. Li. 2009. Checking timed Büchi automata emptiness using LU-abstractions. In Formal Modeling and Analysis of Timed Systems. Lecture Notes in Computer Science, Vol. 5813. Springer, 228--242.

[15]

S. Tripakis. 2009. Checking timed Büchi automata emptiness on simulation graphs. ACM Transactions on Computational Logic 10, 3 (2009), 15.

Digital Library

[16]

S. Tripakis and S. Yovine. 2001. Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design 18, 1 (2001), 25--68.

Digital Library

[17]

S. Tripakis, S. Yovine, and A. Bouajjani. 2005. Checking timed Büchi automata emptiness efficiently. Formal Methods in System Design 26, 3 (2005), 267--292.

Digital Library

[18]

UPPAAL [n.d.]. UPPAAL CSMA/CD Model. Retrieved October 8, 2014 from https://www.it.uu.se/research/group/darts/uppaal/benchmarks/genCSMA_CD.awk.

Cited By

Srivathsan B(2022)Reachability in timed automataACM SIGLOG News10.1145/3559736.35597389:3(6-28)Online publication date: 25-Aug-2022
https://dl.acm.org/doi/10.1145/3559736.3559738
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: 12-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-15839-1_2
André ÉMarinho DPetrucci Lvan de Pol J(2022)Efficient Convex Zone Merging in Parametric Timed AutomataFormal Modeling and Analysis of Timed Systems10.1007/978-3-031-15839-1_12(200-218)Online publication date: 29-Aug-2022
https://doi.org/10.1007/978-3-031-15839-1_12
Show More Cited By

Index Terms

Why Liveness for Timed Automata Is Hard, and What We Can Do About It
1. Theory of computation
  1. Logic
    1. Verification by model checking

Recommendations

Interrupt Timed Automata: verification and expressiveness

We introduce the class of Interrupt Timed Automata (ITA), a subclass of hybrid automata well suited to the description of timed multi-task systems with interruptions in a single processor environment.

While the reachability problem is undecidable for ...
Presburger liveness verification of discrete timed automata

Using an automata-theoretic approach, we investigate the decidability of liveness properties (called Presburger liveness properties) for timed automata when Presburger formulas on configurations are allowed. While the general problem of checking a ...
Alternating timed automata

A notion of alternating timed automata is proposed. It is shown that such automata with only one clock have decidable emptiness problem over finite words. This gives a new class of timed languages that is closed under boolean operations and which has an ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 21, Issue 3

July 2020

407 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/3384674

Editor:
Orna Kupferman
School of Computer Science and Engineering, Hebrew University, Israel

Issue’s Table of Contents

Copyright © 2020 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 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: 03 March 2020

Accepted: 01 November 2019

Revised: 01 June 2019

Received: 01 June 2018

Published in TOCL Volume 21, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Infosys Foundation, India, Tata Consultancy Services, India, and the MATRICS project of the Science and Education Research Board, India
CNRS, Inria, and DST

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
225
Total Downloads

Downloads (Last 12 months)19
Downloads (Last 6 weeks)3

Reflects downloads up to 01 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Srivathsan B(2022)Reachability in timed automataACM SIGLOG News10.1145/3559736.35597389:3(6-28)Online publication date: 25-Aug-2022
https://dl.acm.org/doi/10.1145/3559736.3559738
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: 12-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-15839-1_2
André ÉMarinho DPetrucci Lvan de Pol J(2022)Efficient Convex Zone Merging in Parametric Timed AutomataFormal Modeling and Analysis of Timed Systems10.1007/978-3-031-15839-1_12(200-218)Online publication date: 29-Aug-2022
https://doi.org/10.1007/978-3-031-15839-1_12
Akshay SGastin PPrakash K(2021)Fast Zone-Based Algorithms for Reachability in Pushdown Timed AutomataComputer Aided Verification10.1007/978-3-030-81685-8_30(619-642)Online publication date: 15-Jul-2021
https://doi.org/10.1007/978-3-030-81685-8_30
André ÉArias JPetrucci LPol J(2021)Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed AutomataTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-72016-2_17(311-329)Online publication date: 20-Mar-2021
https://doi.org/10.1007/978-3-030-72016-2_17

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

HTML Format

View this article in HTML Format.

Media

Figures

Other

Tables

View Issue’s Table of Contents