Abstract
We introduce a model named nested updatable timed automata (NeUTAs), which can be regarded as a combination of nested timed automata (NeTAs) and updatable timed automata with one updatable clock (UTA1s). The model is suitable for soft real-time system analysis, since the updatable clock representing a deadline can be updated due to environments. A NeUTA behaves as a UTA1, in which all clocks can be tested/updated and a special clock can be incremented/decremented. It also behaves as a pushdown system, in which a UTA1 can be pushed to a stack or popped from a stack. When time elapses, all clocks (clocks in the current running UTA1 or in the stack) proceed uniformly. We show the termination and boundedness of NeUTAs are decidable.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Li, G., Cai, X., Ogawa, M., Yuen, S.: Nested timed automata. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 168–182. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40229-6_12
Li, G., Ogawa, M., Yuen, S.: Nested timed automata with frozen clocks. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS 2015. LNCS, vol. 9268, pp. 189–205. Springer, Cham (2015). doi:10.1007/978-3-319-22975-1_13
Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Updatable timed automata. Theoret. Comput. Sci. 321(2–3), 291–345 (2004)
Wen, Y., Li, G., Yuen, S.: On reachability analysis of updatable timed automata with one updatable clock. In: Liu, S., Duan, Z. (eds.) SOFL+MSVL 2015. LNCS, vol. 9559, pp. 147–161. Springer, Cham (2016). doi:10.1007/978-3-319-31220-0_11
Leroux, J., Praveen, M., Sutre, G.: Hyper-ackermannian bounds for pushdown vector addition systems. In: Proceeding of the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2014), pp. 63:1–63:10. ACM (2014)
Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183–235 (1994)
Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1993). doi:10.1007/3-540-57318-6_30
Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57, 94–124 (1998)
Henzinger, T.A.: The theory of hybrid automata. In: Inan, M.K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems. NATO ASI Series, vol. 170, pp. 265–292. Springer, Heidelberg (2000). doi:10.1007/978-3-642-59615-5_13
Abdulla, P.A., Atig, M.F., Stenman, J.: Dense-timed pushdown automata. In: Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science (LICS 2012), pp. 35–44. IEEE Computer Society (2012)
Bérard, B., Haddad, S., Sassolas, M.: Interrupt timed automata: verification and expressiveness. Formal Methods Syst. Des. 40(1), 41–87 (2012)
Bérard, B., Haddad, S.: Interrupt timed automata. In: Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 197–211. Springer, Heidelberg (2009). doi:10.1007/978-3-642-00596-1_15
Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Are timed automata updatable? In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 464–479. Springer, Heidelberg (2000). doi:10.1007/10722167_35
Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Expressiveness of updatable timed automata. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol. 1893, pp. 232–242. Springer, Heidelberg (2000). doi:10.1007/3-540-44612-5_19
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 (LICS 2004), pp. 54–63. IEEE Computer Society (2004)
Abdulla, P.A., Jonsson, B.: Verifying networks of timed processes. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 298–312. Springer, Heidelberg (1998). doi:10.1007/BFb0054179
Abdulla, P., Jonsson, B.: Model checking of systems with many identical time processes. Theoret. Comput. Sci. 290(1), 241–264 (2003)
Duan, Z.: Temporal Logic and Temporal Logic Programming. Science Press, Beijing (2005)
Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica 45(1), 43–78 (2008)
Duan, Z., Yang, X., Koutny, M.: Framed temporal logic programming. Sci. Comput. Program. 70(1), 31–61 (2008)
Tian, C., Duan, Z., Zhang, N.: An efficient approach for abstraction-refinement in model checking. Theoret. Comput. Sci. 461, 76–85 (2012)
Acknowledgements
This work is supported by National Natural Science Foundation of China with grant No. 61472240, 91318301, 61261130589, and the NSFC-JSPS bilateral joint research project with grant No. 61511140100.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Wang, Y., Tao, X., Li, G. (2017). On Termination and Boundedness of Nested Updatable Timed Automata. In: Liu, S., Duan, Z., Tian, C., Nagoya, F. (eds) Structured Object-Oriented Formal Language and Method. SOFL+MSVL 2016. Lecture Notes in Computer Science(), vol 10189. Springer, Cham. https://doi.org/10.1007/978-3-319-57708-1_2
Download citation
DOI: https://doi.org/10.1007/978-3-319-57708-1_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-57707-4
Online ISBN: 978-3-319-57708-1
eBook Packages: Computer ScienceComputer Science (R0)