logo

SCIENCE CHINA Information Sciences, Volume 61, Issue 1: 012102(2018) https://doi.org/10.1007/s11432-016-9027-y

Updatable timed automata with one updatable clock

More info
  • ReceivedNov 7, 2016
  • AcceptedFeb 9, 2017
  • PublishedSep 1, 2017

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.


Acknowledgment

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).


References

[1] Alur R, Dill D L. A theory of timed automata. Theor Comput Sci 1994, 126: 183--235. Google Scholar

[2] 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. Google Scholar

[3] 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. Google Scholar

[4] Bouyer P, Dufourd C, Fleury E, et al. Updatable timed automata. Theor Comput Sci 2004, 321: 291--345. Google Scholar

[5] Minsky M L. Computation: Finite and Infinite Machines Upper Saddle River: Prentice-Hall, 1967. Google Scholar

[6] Bouyer P. Forward analysis of updatable timed automata. Form Method Syst Des 2004, 24: 281--320. Google Scholar

[7] 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. Google Scholar

[8] Henzinger T A, Kopke P W, Puri A, et al. Whats decidable about hybrid automata? J Comput Syst Sci 1998, 57: 94--124. Google Scholar

[9] Wen Y Q, Li G Q, Yuen S. On reachability analysis of updatable timed automata with one updatable clock.łinebreak In: Proceedings of International Workshop on Structured Object-Oriented Formal Language and Method Pairs, 2015, 147--161. Google Scholar

[10] 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. Google Scholar

[11] 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. Google Scholar

[12] 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. Google Scholar

[13] Haase C, Kreutzer S, Ouaknine J, et al. Reachability in succinct and parametric one-counter automata. In: Pro-łinebreak ceedings of the International Conference on Concurrency Theory Bologna, 2009. 369--383. Google Scholar

[14] Schwoon S. Model-checking pushdown system Dissertation for Ph.D. Degree. Munich: Technical University of Munich, 2000. Google Scholar

[15] Demri S, Gascon R. The effects of bounding syntactic resources on presburger LTL J Logic Comput 2009, 19: 1541--1575. Google Scholar

[16] Fersman E, Krcal P, Pettersson P, et al. Task automata: schedulability, decidability and undecidability. Inform Comput 2007, 205: 1149--1172. Google Scholar

[17] Ouaknine J, Worrell J. On the language inclusion problem for timed automata: closing a decidability gap. In: Pro-łinebreak ceedings of the 19th IEEE Symposium on Logic in Computer Science Turku, 2004. 54--63. Google Scholar

[18] 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. Google Scholar

[19] Abdulla P A, Jonsson B. Model checking of systems with many identical time processes. Theor Comput Sci 2003, 290: 241--264. Google Scholar

[20] 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. Google Scholar

[21] Choffrut C, Goldwurm M. Timed automata with periodic clock constraints. J Autom Lang Comb 2000, 5: 371--404. Google Scholar

[22] Demichelis F, Zielonka W. Controlled timed automata. In: Proceedings of the 9th International Conference on Concurrency Theory Nice, 1998. 455--469. Google Scholar

[23] Bouchy F, Finkel A, Sangnier A. Reachability in timed counter systems. Electr Notes Theor Comput Sci 2009, 239: 167--178. Google Scholar

[24] 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. Google Scholar

[25] 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. Google Scholar

[26] Bouyer P, Chevalier F. On conciseness of extensions of timed automata. J Autom Lang Combin 2005, 10: 393--405. Google Scholar

[27] 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. Google Scholar

[28] 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. Google Scholar

[29] Trivedi A, Wojtczak D. Recursive timed automata. In: Proceedings of International Symposium on Automated Technology for Verification and Analysis Singapore, 2010. 306--324. Google Scholar

[30] 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. Google Scholar

Copyright 2020 Science China Press Co., Ltd. 《中国科学》杂志社有限责任公司 版权所有

京ICP备18024590号-1