research-article

Clock Allocation in Timed Automata and Graph Colouring

Authors:

Neda Saeedloei,

Feliks KluźniakAuthors Info & Claims

HSCC '18: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)

Pages 71 - 80

https://doi.org/10.1145/3178126.3178138

Published: 11 April 2018 Publication History

Abstract

We consider the problem of optimal clock allocation for a fairly general class of timed automata, TAS, under the safe assumption that all locations are reachable. Techniques similar to those used in compiler technology allow us to construct an interference graph: the problem of clock allocation for timed automata in TAS can be reduced to that of colouring this graph. We then describe a class of timed automata, TADS ⊊ TAS, for which optimal clock allocation can be computed in polynomial time, because the corresponding interference graphs are perfect. Finally, we discuss some of the difficulties in applying similar techniques to timed automata outside TAS.

References

[1]

Rajeev Alur, Costas Courcoubetis, and David Dill. 1993. Model-Checking in Dense Real-time. INFORMATION AND COMPUTATION 104 (1993), 2--34.

Digital Library

[2]

Rajeev Alur and David L. Dill. 1994. A theory of timed automata. Theor. Comput. Sci. 126, Article 2 (April 1994), 53 pages.

Digital Library

[3]

Rajeev Alur, Limor Fix, and Thomas A. Henzinger. 1999. Event-Clock Automata: A Determinizable Class of Timed Automata. Theor. Comput. Sci. 211, 1-2 (1999), 253--273.

Digital Library

[4]

Gerd Behrmann, Alexandre David, and Kim G. Larsen. 2004. A Tutorial on Uppaal. In Formal Methods for the Design of Real-Time Systems: 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004 (LNCS), Marco Bernardo and Flavio Corradini (Eds.). Springer-Verlag, 200--236.

[5]

G. J. Chaitin. 1982. Register Allocation & Spilling via Graph Coloring. SIGPLAN Not. 17, Article 6 (June 1982), 4 pages.

Digital Library

[6]

Conrado Daws and Sergio Yovine. 1996. Reducing the number of clock variables of timed automata. In Proceedings of the 17th IEEE Real-Time Systems Symposium (RTSS '96), December 4-6, 1996, Washington, DC, USA. IEEE Computer Society, 73--81.

Digital Library

[7]

Olivier Finkel. 2006. Undecidable Problems About Timed Automata. In FOR-MATS'06 (Lecture Notes in Computer Science, Volume 4202.), Eugene Asarin and Patricia Bouyer (Eds.). Springer, France, 187--199. https://hal.archives-ouvertes.fr/hal-00121529

Digital Library

[8]

Fanica Gavril. 1972. Algorithms for Minimum Coloring, Maximum Clique, Minimum Covering by Cliques, and Maximum Independent Set of a Chordal Graph. SIAM J. Comput. 1, 2 (1972), 180--187.

Digital Library

[9]

Martin Grötschel, Lászlo Lovász, and Alexander Schrijver. 1988. Geometric Algorithms and Combinatorial Optimization. Algorithms and Combinatorics, Vol. 2. Springer.

[10]

Shibashis Guha, Chinmay Narayan, and S. Arun-Kumar. 2014. Reducing Clocks in Timed Automata while Preserving Bisimulation. In CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings. Springer, 527--543.

[11]

Thomas A. Henzinger. 1992. Sooner is Safer Than Later. Inf. Process. Lett. 43, 3 (1992), 135--141.

Digital Library

[12]

Thomas Lengauer and Robert Endre Tarjan. 1979. A Fast Algorithm for Finding Dominators in a Flowgraph. ACM Trans. Program. Lang. Syst. 1, Article 1 (Jan. 1979), 21 pages.

Digital Library

[13]

Gabriela Nicolescu and Pieter J. Mosterman. 2009. Model-Based Design for EmbeddedSystems(1sted.). CRCPress, Inc., Boca Raton, FL, USA.

Digital Library

[14]

Fernando Magno Quintão Pereira and Jens Palsberg. 2005. Register Allocation Via Coloring of Chordal Graphs. In Programming Languages and Systems, Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2-5, 2005, Proceedings. Springer, 315--329.

Digital Library

[15]

Massimiliano Poletto and Vivek Sarkar. 1999. Linear Scan Register Allocation. ACM Trans. Program. Lang. Syst. 21, Article 5 (Sept. 1999), 19 pages.

Digital Library

[16]

Neda Saeedloei and Feliks Kluzniak. 2017. From Scenarios to Timed Automata. In Formal Methods: Foundations and Applications - 20th Brazilian Symposium, SBMF 2017, Recife, Brazil, November 29-December 1, 2017, Proceedings. 33--51.

[17]

Neda Saeedloei and Feliks Kluźniak. 2017. Optimal Clock Allocation for a Class of Timed Automata. http://www2.cs.siu.edu/~neda/report2.pdf. (2017). Technical Report.

Cited By

Saeedloei NKluźniak F(2024)Synthesizing Timed Automata with Minimal Numbers of Clocks from Optimised Timed ScenariosFormal Techniques for Distributed Objects, Components, and Systems10.1007/978-3-031-62645-6_8(136-154)Online publication date: 17-Jun-2024
https://dl.acm.org/doi/10.1007/978-3-031-62645-6_8
Saeedloei NKluźniak F(2022)An Efficient Customized Clock Allocation Algorithm for a Class of Timed AutomataFormal Methods: Foundations and Applications10.1007/978-3-031-22476-8_1(3-21)Online publication date: 1-Dec-2022
https://doi.org/10.1007/978-3-031-22476-8_1
Saeedloei NKluźniak F(2022)Untangling the Graphs of Timed Automata to Decrease the Number of ClocksIntegrated Formal Methods10.1007/978-3-031-07727-2_10(168-187)Online publication date: 1-Jun-2022
https://doi.org/10.1007/978-3-031-07727-2_10
Show More Cited By

Index Terms

Clock Allocation in Timed Automata and Graph Colouring
1. Computer systems organization
  1. Dependable and fault-tolerant systems and networks
    1. Redundancy
  2. Embedded and cyber-physical systems
    1. Embedded systems
    2. Robotics
2. Networks
  1. Network properties
    1. Network reliability

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

HSCC '18: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)

April 2018

296 pages

ISBN:9781450356428

DOI:10.1145/3178126

Copyright © 2018 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].

Sponsors

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 April 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

HSCC '18

Sponsor:

SIGBED

HSCC '18: 21st International Conference on Hybrid Systems: Computation and Control

April 11 - 13, 2018

Porto, Portugal

Acceptance Rates

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
108
Total Downloads

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

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Saeedloei NKluźniak F(2024)Synthesizing Timed Automata with Minimal Numbers of Clocks from Optimised Timed ScenariosFormal Techniques for Distributed Objects, Components, and Systems10.1007/978-3-031-62645-6_8(136-154)Online publication date: 17-Jun-2024
https://dl.acm.org/doi/10.1007/978-3-031-62645-6_8
Saeedloei NKluźniak F(2022)An Efficient Customized Clock Allocation Algorithm for a Class of Timed AutomataFormal Methods: Foundations and Applications10.1007/978-3-031-22476-8_1(3-21)Online publication date: 1-Dec-2022
https://doi.org/10.1007/978-3-031-22476-8_1
Saeedloei NKluźniak F(2022)Untangling the Graphs of Timed Automata to Decrease the Number of ClocksIntegrated Formal Methods10.1007/978-3-031-07727-2_10(168-187)Online publication date: 1-Jun-2022
https://doi.org/10.1007/978-3-031-07727-2_10
Westphal B(2021)Quasi-Equal Clock Reduction On-the-FlyNASA Formal Methods10.1007/978-3-030-76384-8_23(375-391)Online publication date: 19-May-2021
https://doi.org/10.1007/978-3-030-76384-8_23
Saeedloei NKluźniak F(2020)Optimization of Timed ScenariosFormal Methods: Foundations and Applications10.1007/978-3-030-63882-5_8(119-136)Online publication date: 19-Nov-2020
https://doi.org/10.1007/978-3-030-63882-5_8
Saeedloei NKluźniak F(2020)Synthesizing Clock-Efficient Timed AutomataIntegrated Formal Methods10.1007/978-3-030-63461-2_15(276-294)Online publication date: 13-Nov-2020
https://doi.org/10.1007/978-3-030-63461-2_15
Yalcinkaya BGol EGnesi SPlat NDay NRossi M(2019)Clock reduction in timed automata while preserving design parametersProceedings of the 7th International Workshop on Formal Methods in Software Engineering10.1109/FormaliSE.2019.00010(11-20)Online publication date: 27-May-2019
https://dl.acm.org/doi/10.1109/FormaliSE.2019.00010

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.

Figures

Tables

Media

View Table of Conten