Abstract
During the last years, timed automata have become a popular model for describing the behaviour of real-time systems. In particular, there has been much research on problems such as language inclusion and universality. It is well-known that the universality problem is undecidable for the class of timed automata with two or more clocks. Recently, it was shown that the problem becomes decidable if the automata are restricted to operate on a single clock variable. However, existing algorithms use a region-based constraint system and suffer from constraint explosion even for small examples. In this paper, we present a zone-based algorithm for solving the universality problem for single-clock timed automata. We apply the theory of better quasi-orderings, a refinement of the theory of well quasi-orderings, to prove termination of the algorithm. We have implemented a prototype based on our method, and checked universality for a number of timed automata. Comparisons with a region-based prototype confirm that zones are a more succinct representation, and hence allow a much more efficient implementation of the universality algorithm.
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
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
Alur, R., Madhusudan, P.: Decision problems for timed automata: A survey. In: Bernardo, M., Corradini, F. (eds.) Formal Methods for the Design of Real-Time Systems. LNCS, vol. 3185, Springer, Heidelberg (2004)
Alur, R., Fix, L., Henzinger, T.: Event-clock automata: A determinizable class of timed automata. Theoretical Computer Science 211, 253–273 (1999)
Alur, R., Torre, S.L., Madhusudan, P.: Perturbed timed automata. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, Springer, Heidelberg (2005)
Alur, R., Feder, T., Henzinger, T.: The benefits of relaxing punctually. Journal of the ACM 43, 116–146 (1996)
Henzinger, T., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, Springer, Heidelberg (1992)
Ouaknine, J., Worrell, J.: Universality and language inclusion for open and closed timed automata. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, Springer, Heidelberg (2003)
Ouaknine, J., Worrell, J.: On the language inclusion problem for timed automata: Closing a decidability gap. In: Proc. LICS 2004, 20th IEEE Int. Symp. on Logic in Computer Science, IEEE Computer Society Press, Los Alamitos (2004)
Abdulla, P.A., Deneux, J., Ouaknine, J., Worrell, J.: Decidability and complexity results for timed automata via channel machines. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, Springer, Heidelberg (2005)
Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Information and Computation 127(2), 91–101 (1996)
Abdulla, P.A., Nylén, A.: Timed Petri nets and BQOs. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol. 2075, pp. 53–70. Springer, Heidelberg (2001)
Yovine, S.: Kronos: A verification tool for real-time systems. Journal of Software Tools for Technology Transfer 1(1-2) (1997)
Larsen, K., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Software Tools for Technology Transfer 1(1-2) (1997)
Abdulla, P.A., Nylén, A.: Better is better than well: On efficient verification of infinite-state systems. In: Proc. LICS 2000, 16th IEEE Int. Symp. on Logic in Computer Science, pp. 132–140. IEEE Computer Society Press, Los Alamitos (2000)
Bengtsson, J., Larsson, F.: Uppaal a tool for automatic verification of real-time systems. Technical Report 96/97, DoCS, Uppsala University (1996)
Abdulla, P.A., Čerāns, K., Jonsson, B., Tsay, Y.K.: Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation 160, 109–127 (2000)
Marcone, A.: Foundations of bqo theory. Transactions of the American Mathematical Society 345(2) (1994)
Abdulla, P.A., Jonsson, B.: Verifying networks of timed processes. In: Steffen, B. (ed.) ETAPS 1998 and TACAS 1998. LNCS, vol. 1384, pp. 298–312. Springer, Heidelberg (1998)
Møller, J., Lichtenberg, J.: Difference decision diagrams. Master’s thesis, Department of Information Technology, Technical University of Denmark, Building 344, DK-2800 Lyngby, Denmark (1998)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abdulla, P.A., Ouaknine, J., Quaas, K., Worrell, J. (2007). Zone-Based Universality Analysis for Single-Clock Timed Automata. In: Arbab, F., Sirjani, M. (eds) International Symposium on Fundamentals of Software Engineering. FSEN 2007. Lecture Notes in Computer Science, vol 4767. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75698-9_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-75698-9_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75697-2
Online ISBN: 978-3-540-75698-9
eBook Packages: Computer ScienceComputer Science (R0)