Abstract
Updatable timed automata (UTAs) proposed by Bouyer et.al., is an extension of timed automata (TAs) having the extra ability to update clocks in a more elaborate way than simply reset them to zero. The reachability of UTAs is generally undecidable, which can be easily gained by regarding a pair of clocks as updatable counters. This paper investigates a subclass of UTAs by restricting the number of updatable clocks to be one. We will show that (1) the reachability of general UTAs with one updatable clock (UTA1s) is still undecidable, and (2) that of UTA1s under diagonal-free constraints is decidable, and the complexity is Pspace-complete. The former is achieved by encoding Minsky machines to the general UTA1s, where two counters are simulated by the updatable clock. The latter is gained by regarding a region of a UTA1 to be an unbounded digiword, and encoding sets of digiwords that are accepted by a one counter automaton where regions are generated as the value of the counter.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Alur R, Dill D L. A theory of timed automata. Theor Comput Sci, 1994, 126: 183–235
Bouyer P, Dufourd C, Fleury E, et al. Are timed automata updatable? In: Proceedings of the 12th International Conference on Computer Aided Verification, Chicago, 2000. 464–479
Bouyer P, Dufourd C, Fleury E, et al. Expressiveness of updatable timed automata. In: Proceedings of International Symposium on Mathematical Foundations of Computer, Bratislava, 2000. 232–242
Bouyer P, Dufourd C, Fleury E, et al. Updatable timed automata. Theor Comput Sci, 2004, 321: 291–345
Minsky M L. Computation: Finite and Infinite Machines. Upper Saddle River: Prentice-Hall, 1967
Bouyer P. Forward analysis of updatable timed automata. Form Method Syst Des, 2004, 24: 281–320
Fang B B, Li G Q, Fang L, et al. A refined algorithm for reachability analysis of updatable timed automata. In: Proceedings of IEEE International Conference on the Software Quality, Reliability and Security - Companion, Vancouver, 2015. 230–236
Henzinger T A, Kopke P W, Puri A, et al. What’s decidable about hybrid automata? J Comput Syst Sci, 1998, 57: 94–124
Wen Y Q, Li G Q, Yuen S. On reachability analysis of updatable timed automata with one updatable clock. In: Proceedings of International Workshop on Structured Object-Oriented Formal Language and Method, Pairs, 2015, 147–161
Abdulla P A, Atig M F, Stenman J. Dense-timed pushdown automata. In: Proceedings of 27th Annual IEEE Symposium on Logic in Computer Science, Dubrovnik, 2012. 35–44
Li G Q, Ogawa M, Yuen S. Nested timed automata with frozen clocks. In: Proceedings of International Conference on Formal Modeling and Analysis of Timed Systems, Madrid, 2015, 189–205
Jancar P, Kucera A, Moller F, et al. DP lower bounds for equivalence-checking and model-checking of one-counter automata. Inform Comput, 2004, 188: 1–19
Haase C, Kreutzer S, Ouaknine J, et al. Reachability in succinct and parametric one-counter automata. In: Proceedings of the International Conference on Concurrency Theory, Bologna, 2009. 369–383
Schwoon S. Model-checking pushdown system. Dissertation for Ph.D. Degree. Munich: Technical University of Munich, 2000
Demri S, Gascon R. The effects of bounding syntactic resources on presburger LTL. J Logic Comput, 2009, 19: 1541–1575
Fersman E, Krcal P, Pettersson P, et al. Task automata: schedulability, decidability and undecidability. Inform Comput, 2007, 205: 1149–1172
Ouaknine J, Worrell J. On the language inclusion problem for timed automata: closing a decidability gap. In: Proceedings of the 19th IEEE Symposium on Logic in Computer Science, Turku, 2004. 54–63
Abdulla P A, Jonsson B. Verifying networks of timed processes. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lisbon, 1998. 298–312
Abdulla P A, Jonsson B. Model checking of systems with many identical time processes. Theor Comput Sci, 2003, 290: 241–264
Li G Q, Cai X J, Ogawa M, et al. Nested timed automata. In: Proceedings of International Conference on Formal Modeling and Analysis of Timed Systems, Buenos Aires, 2013. 168–182
Choffrut C, Goldwurm M. Timed automata with periodic clock constraints. J Autom Lang Comb, 2000, 5: 371–404
Demichelis F, Zielonka W. Controlled timed automata. In: Proceedings of the 9th International Conference on Concurrency Theory, Nice, 1998. 455–469
Bouchy F, Finkel A, Sangnier A. Reachability in timed counter systems. Electr Notes Theor Comput Sci, 2009, 239: 167–178
Alur R, La Torre S, Pappas G J. Optimal paths in weighted timed automata. In: Proceedings of International Workshop on Hybrid Systems: Computation and Control, Rome, 2001, 49–62
Behrmann G, Fehnker A, Hune T, et al. Minimum-cost reachability for priced timed automata. In: Proceedings of the International Workshop on Hybrid Systems: Computation and Control, Rome, 2001, 147–161
Bouyer P, Chevalier F. On conciseness of extensions of timed automata. J Autom Lang Combin 2005, 10: 393–405
Suman P V, Pandya P K, Krishna S N, et al. Timed automata with integer resets: language inclusion and expressiveness. In: Proceedings of International Conference on Formal Modeling and Analysis of Timed Systems, Saint Malo, 2008. 78–92
Suman P V, Pandya P K. Determinization and expressiveness of integer reset timed automata with silent transitions. In: Proceedings of International Conference on Language and Automata Theory and Applications, Tarragona, 2009, 728–739
Trivedi A, Wojtczak D. Recursive timed automata. In: Proceedings of International Symposium on Automated Technology for Verification and Analysis, Singapore, 2010. 306–324
Wen Y Q, Li G Q, Yuen S J. An over-approximation forward analysis for nested timed automata. In: Proceedings of International Workshop on Structured Object-Oriented Formal Language and Method, Luxembourg, 2014. 62–80
Acknowledgments
This work was supported by NSFC-JSPS Bilateral Joint Research Project (Grant No. 61511140100), and National Natural Science Foundation of China (Grant Nos. 61472240, 61602224, 91318301).
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Li, G., Wen, Y. & Yuen, S. Updatable timed automata with one updatable clock. Sci. China Inf. Sci. 61, 012102 (2017). https://doi.org/10.1007/s11432-016-9027-y
Received:
Revised:
Accepted:
Published:
DOI: https://doi.org/10.1007/s11432-016-9027-y