research-article

Abstractions for the local-time semantics of timed automata: a foundation for partial-order methods

Authors:

Frédéric Herbreteau,

Igor WalukiewiczAuthors Info & Claims

LICS '22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science

Article No.: 24, Pages 1 - 14

https://doi.org/10.1145/3531130.3533343

Published: 04 August 2022 Publication History

Abstract

A timed network is a parallel composition of timed automata synchronizing on common actions. We develop a methodology that allows to use partial-order methods when solving the reachability problem for timed networks. It is based on a local-time semantics proposed by [Bengtsson et al. 1998]. A new simulation based abstraction of local-time zones is proposed. The main technical contribution is an efficient algorithm for testing subsumption between local-time zones with respect to this abstraction operator. The abstraction is not finite for all networks. It turns out that, under relatively mild conditions, there is no finite abstraction for local-time zones that works for arbitrary timed networks. To circumvent this problem, we introduce a notion of a bounded-spread network. The spread of a network is a parameter that says how far the local times of individual processes need to diverge. For bounded-spread networks, we show that it is possible to use subsumption and partial-order methods at the same time.

References

[1]

Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2014. Optimal dynamic partial order reduction. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, Suresh Jagannathan and Peter Sewell (Eds.). ACM, 373–384. https://doi.org/10.1145/2535838.2535845

Digital Library

[2]

Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2017. Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction. J. ACM 64, 4 (2017), 25:1–25:49. https://doi.org/10.1145/3073408

Digital Library

[3]

Rajeev Alur and David L. Dill. 1994. A Theory of Timed Automata. Theor. Comput. Sci. 126, 2 (1994), 183–235. https://doi.org/10.1016/0304-3975(94)90010-8

Digital Library

[4]

Gilles Audemard, Alessandro Cimatti, Artur Kornilowicz, and Roberto Sebastiani. 2002. Bounded Model Checking for Timed Systems. In Formal Techniques for Networked and Distributed Systems - FORTE 2002, 22nd IFIP WG 6.1 International Conference Houston, Texas, USA, November 11-14, 2002, Proceedings(Lecture Notes in Computer Science, Vol. 2529), Doron A. Peled and Moshe Y. Vardi (Eds.). Springer, 243–259. https://doi.org/10.1007/3-540-36135-9_16

[5]

Bahareh Badban and Martin Lange. 2011. Exact Incremental Analysis of Timed Automata with an SMT-Solver. In Formal Modeling and Analysis of Timed Systems - 9th International Conference, FORMATS 2011, Aalborg, Denmark, September 21-23, 2011. Proceedings(Lecture Notes in Computer Science, Vol. 6919), Uli Fahrenberg and Stavros Tripakis (Eds.). Springer, 177–192. https://doi.org/10.1007/978-3-642-24310-3_13

[6]

Gerd Behrmann, Patricia Bouyer, Kim Guldstrand Larsen, and Radek Pelánek. 2006. Lower and upper bounds in zone-based abstractions of timed automata. Int. J. Softw. Tools Technol. Transf. 8, 3 (2006), 204–215.

Digital Library

[7]

Gerd Behrmann, Kim Guldstrand Larsen, Justin Pearson, Carsten Weise, and Wang Yi. 1999. Efficient Timed Reachability Analysis Using Clock Difference Diagrams. In Computer Aided Verification, 11th International Conference, CAV ’99, Trento, Italy, July 6-10, 1999, Proceedings(Lecture Notes in Computer Science, Vol. 1633), Nicolas Halbwachs and Doron A. Peled (Eds.). Springer, 341–353. https://doi.org/10.1007/3-540-48683-6_30

[8]

Johan Bengtsson, Bengt Jonsson, Johan Lilius, and Wang Yi. 1998. Partial Order Reductions for Timed Systems. In CONCUR(Lecture Notes in Computer Science, Vol. 1466). 485–500.

[9]

Frederik M. Bønneland, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marco Muñiz, and Jirí Srba. 2018. Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I(Lecture Notes in Computer Science, Vol. 10981), Hana Chockler and Georg Weissenbacher (Eds.). Springer, 527–546. https://doi.org/10.1007/978-3-319-96145-3_28

[10]

Frederik M. Bønneland, Peter Gjøl Jensen, Kim G. Larsen, Marco Muñiz, and Jirí Srba. 2021. Stubborn Set Reduction for Timed Reachability and Safety Games. In Formal Modeling and Analysis of Timed Systems - 19th International Conference, FORMATS 2021, Paris, France, August 24-26, 2021, Proceedings(Lecture Notes in Computer Science, Vol. 12860), Catalin Dima and Mahsa Shirmohammadi (Eds.). Springer, 32–49. https://doi.org/10.1007/978-3-030-85037-1_3

Digital Library

[11]

Frederik Meyer Bønneland, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marco Muñiz, and Jirí Srba. 2021. Stubborn Set Reduction for Two-Player Reachability Games. Log. Methods Comput. Sci. 17, 1 (2021). https://lmcs.episciences.org/7278

[12]

Patricia Bouyer, Serge Haddad, and Pierre-Alain Reynier. 2006. Timed Unfoldings for Networks of Timed Automata. In Automated Technology for Verification and Analysis, 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006(Lecture Notes in Computer Science, Vol. 4218), Susanne Graf and Wenhui Zhang (Eds.). Springer, 292–306. https://doi.org/10.1007/11901914_23

Digital Library

[13]

Franck Cassez, Thomas Chatain, and Claude Jard. 2006. Symbolic Unfoldings for Networks of Timed Automata. In Automated Technology for Verification and Analysis, 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006(Lecture Notes in Computer Science, Vol. 4218), Susanne Graf and Wenhui Zhang (Eds.). Springer, 307–321. https://doi.org/10.1007/11901914_24

Digital Library

[14]

Krishnendu Chatterjee, Andreas Pavlogiannis, and Viktor Toman. 2019. Value-centric dynamic partial order reduction. Proc. ACM Program. Lang. 3, OOPSLA (2019), 124:1–124:29. https://doi.org/10.1145/3360550

Digital Library

[15]

Edmund M. Clarke, Orna Grumberg, Marius Minea, and Doron A. Peled. 1999. State Space Reduction Using Partial Order Techniques. Int. J. Softw. Tools Technol. Transf. 2, 3 (1999), 279–287. https://doi.org/10.1007/s100090050035

[16]

Dennis Dams, Rob Gerth, Bart Knaack, and Ruurd Kuiper. 1998. Partial-order Reduction Techniques for Real-time Model Checking. Formal Aspects Comput. 10, 5-6 (1998), 469–482. https://doi.org/10.1007/s001650050028

Digital Library

[17]

Conrado Daws and Stavros Tripakis. 1998. Model Checking of Real-Time Reachability Properties Using Abstractions. In TACAS(Lecture Notes in Computer Science, Vol. 1384). Springer, 313–329.

[18]

Rüdiger Ehlers, Daniel Fass, Michael Gerke, and Hans-Jörg Peter. 2010. Fully Symbolic Timed Model Checking Using Constraint Matrix Diagrams. In Proceedings of the 31st IEEE Real-Time Systems Symposium, RTSS 2010, San Diego, California, USA, November 30 - December 3, 2010. IEEE Computer Society, 360–371. https://doi.org/10.1109/RTSS.2010.36

Digital Library

[19]

Cormac Flanagan and Patrice Godefroid. 2005. Dynamic partial-order reduction for model checking software. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005, Jens Palsberg and Martín Abadi (Eds.). ACM, 110–121. https://doi.org/10.1145/1040305.1040315

Digital Library

[20]

Patrice Godefroid. 1996. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. Lecture Notes in Computer Science, Vol. 1032. Springer. https://doi.org/10.1007/3-540-60761-7

[21]

Patrice Godefroid. 1997. Model Checking for Programming Languages using Verisoft. In Conference Record of POPL’97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, Paris, France, 15-17 January 1997, Peter Lee, Fritz Henglein, and Neil D. Jones (Eds.). ACM Press, 174–186. https://doi.org/10.1145/263699.263717

Digital Library

[22]

Patrice Godefroid and Pierre Wolper. 1994. A Partial Approach to Model Checking. Inf. Comput. 110, 2 (1994), 305–326. https://doi.org/10.1006/inco.1994.1035

Digital Library

[23]

R. Govind, Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. 2019. Revisiting Local Time Semantics for Networks of Timed Automata. In CONCUR(LIPIcs, Vol. 140). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 16:1–16:15.

[24]

Henri Hansen, Shang-Wei Lin, Yang Liu, Truong Khanh Nguyen, and Jun Sun. 2014. Diamonds Are a Girl’s Best Friend: Partial Order Reduction for Timed Automata with Abstractions. In CAV(Lecture Notes in Computer Science, Vol. 8559). Springer, 391–406.

[25]

Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. 2013. Lazy Abstractions for Timed Automata. In CAV(Lecture Notes in Computer Science, Vol. 8044). Springer, 990–1005.

[26]

Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. 2016. Better abstractions for timed automata. Inf. Comput. 251(2016), 67–90. https://doi.org/10.1016/j.ic.2016.07.004

Digital Library

[27]

Shmuel Katz and Doron A. Peled. 1992. Verification of Distributed Programs Using Representative Interleaving Sequences. Distributed Comput. 6, 2 (1992), 107–120. https://doi.org/10.1007/BF02252682

Digital Library

[28]

Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, and Viktor Vafeiadis. 2022. Truly Stateless, Optimal Dynamic Partial Order Reduction. Proc. ACM Program. Lang. 6, POPL, Article 49 (Jan 2022), 28 pages. https://doi.org/10.1145/3498711

Digital Library

[29]

Kim Guldstrand Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. 2003. Compact Data Structures and State-Space Reduction for Model-Checking Real-Time Systems. Real Time Syst. 25, 2-3 (2003), 255–275. https://doi.org/10.1023/A:1025132427497

Digital Library

[30]

Kim G. Larsen, Marius Mikucionis, Marco Muñiz, and Jirí Srba. 2020. Urgent Partial Order Reduction for Extended Timed Automata. In Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings(Lecture Notes in Computer Science, Vol. 12302), Dang Van Hung and Oleg Sokolsky (Eds.). Springer, 179–195. https://doi.org/10.1007/978-3-030-59152-6_10

Digital Library

[31]

Denis Lugiez, Peter Niebert, and Sarah Zennou. 2005. A partial order semantics approach to the clock explosion problem of timed automata. Theor. Comput. Sci. 345, 1 (2005), 27–59. https://doi.org/10.1016/j.tcs.2005.07.023

Digital Library

[32]

Marius Minea. 1999. Partial Order Reduction for Model Checking of Timed Automata. In CONCUR(Lecture Notes in Computer Science, Vol. 1664). Springer, 431–446.

[33]

Jesper B. Møller, Jakob Lichtenberg, Henrik Reif Andersen, and Henrik Hulgaard. 1999. Fully Symbolic Model Checking of Timed Systems using Difference Decision Diagrams. Electron. Notes Theor. Comput. Sci. 23, 2 (1999), 88–107. https://doi.org/10.1016/S1571-0661(04)80671-6

[34]

Peter Niebert, Moez Mahfoudh, Eugene Asarin, Marius Bozga, Oded Maler, and Navendu Jain. 2002. Verification of Timed Automata via Satisfiability Checking. In Formal Techniques in Real-Time and Fault-Tolerant Systems, 7th International Symposium, FTRTFT 2002, Co-sponsored by IFIP WG 2.2, Oldenburg, Germany, September 9-12, 2002, Proceedings(Lecture Notes in Computer Science, Vol. 2469), Werner Damm and Ernst-Rüdiger Olderog (Eds.). Springer, 225–244. https://doi.org/10.1007/3-540-45739-9_15

[35]

Doron A. Peled. 1993. All from One, One for All: on Model Checking Using Representatives. In Computer Aided Verification, 5th International Conference, CAV ’93, Elounda, Greece, June 28 - July 1, 1993, Proceedings(Lecture Notes in Computer Science, Vol. 697), Costas Courcoubetis (Ed.). Springer, 409–423. https://doi.org/10.1007/3-540-56922-7_34

[36]

Doron A. Peled, Antti Valmari, and Ilkka Kokkarinen. 2001. Relaxed Visibility Enhances Partial Order Reduction. Formal Methods Syst. Des. 19, 3 (2001), 275–289. https://doi.org/10.1023/A:1011202615884

Digital Library

[37]

Antti Valmari. 1989. Stubborn sets for reduced state space generation. In Advances in Petri Nets 1990 [10th International Conference on Applications and Theory of Petri Nets, Bonn, Germany, June 1989, Proceedings](Lecture Notes in Computer Science, Vol. 483), Grzegorz Rozenberg (Ed.). Springer, 491–515. https://doi.org/10.1007/3-540-53863-1_36

[38]

Antti Valmari. 1992. A Stubborn Attack on State Explosion. Formal Methods Syst. Des. 1, 4 (1992), 297–322. https://doi.org/10.1007/BF00709154

Digital Library

[39]

Farn Wang. 2001. Symbolic Verification of Complex Real-Time Systems with Clock-Restriction Diagram. In Formal Techniques for Networked and Distributed Systems, FORTE 2001, IFIP TC6/WG6.1 - 21st International Conference on Formal Techniques for Networked and Distributed Systems, August 28-31, 2001, Cheju Island, Korea(IFIP Conference Proceedings, Vol. 197), Myungchul Kim, Byoungmoon Chin, Sungwon Kang, and Danhyung Lee (Eds.). Kluwer, 235–250.

[40]

Naling Zhang, Markus Kusano, and Chao Wang. 2015. Dynamic partial order reduction for relaxed memory models. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, David Groveand Stephen M. Blackburn (Eds.). ACM, 250–259. https://doi.org/10.1145/2737924.2737956

Digital Library

Cited By

Ho HMadnani K(2025)Metric Quantifiers and Counting in Timed Logics and AutomataInformation and Computation10.1016/j.ic.2025.105268(105268)Online publication date: Jan-2025
https://doi.org/10.1016/j.ic.2025.105268
Mukund MRoy ASrivathsan B(2023)A Local-Time Semantics for NegotiationsFormal Modeling and Analysis of Timed Systems10.1007/978-3-031-42626-1_7(105-121)Online publication date: 29-Aug-2023
https://doi.org/10.1007/978-3-031-42626-1_7

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 ...
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 ...
Undecidable problems about timed automata
FORMATS'06: Proceedings of the 4th international conference on Formal Modeling and Analysis of Timed Systems

We solve some decision problems for timed automata which were raised by S. Tripakis in [Tri04] and by E. Asarin in [Asa04]. In particular, we show that one cannot decide whether a given timed automaton is determinizable or whether the complement of a ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

LICS '22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science

August 2022

817 pages

ISBN:9781450393515

DOI:10.1145/3531130

Editor:
Christel Baier

Copyright © 2022 ACM.

Publication rights licensed to ACM. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of a national government. As such, the Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.

Sponsors

SIGLOG: ACM Special Interest Group on Logic and Computation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 August 2022

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Funding Sources

Agence Nationale de la Recherche

Conference

LICS '22

Sponsor:

SIGLOG

LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science

August 2 - 5, 2022

Haifa, Israel

Acceptance Rates

Overall Acceptance Rate 215 of 622 submissions, 35%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
88
Total Downloads

Downloads (Last 12 months)30
Downloads (Last 6 weeks)2

Reflects downloads up to 20 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Ho HMadnani K(2025)Metric Quantifiers and Counting in Timed Logics and AutomataInformation and Computation10.1016/j.ic.2025.105268(105268)Online publication date: Jan-2025
https://doi.org/10.1016/j.ic.2025.105268
Mukund MRoy ASrivathsan B(2023)A Local-Time Semantics for NegotiationsFormal Modeling and Analysis of Timed Systems10.1007/978-3-031-42626-1_7(105-121)Online publication date: 29-Aug-2023
https://doi.org/10.1007/978-3-031-42626-1_7

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 Publication

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 Table of Contents