Abstract
We propose a remedy to that part of the state-explosion problem for timed automata which is due to interleaving of actions. We prove the following quite surprising result: the union of all zones reached by different interleavings of the same set of transitions is convex. Consequently we can improve the standard reachability computation for timed automata by merging such zones whenever they are encountered. Since passage of time distributes over union, we can continue the successor computation from the new zone and eliminate completely the explosion due to interleaving.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126, 183–235 (1994)
Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial Order Reductions for Timed Systems. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 485–500. Springer, Heidelberg (1998)
Ben Salah, R., Bozga, M., Maler, O.: On Timing Analysis of Combinational Circuits. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 204–219. Springer, Heidelberg (2004)
Ben Salah, R., Bozga, M., Maler, O.: Automatic Abstraction of Timed Components (submitted, 2006)
Bozga, M., Graf, S., Mounier, L.: IF-2.0: A Validation Environment for Component-Based Real-Time Systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 343–348. Springer, Heidelberg (2002)
Dams, D., Gerth, R., Knaack, B., Kuiper, R.: Partial-order Reduction Techniques for Real-time Model Checking. Formal Aspects of Computing 10, 469–482 (1998)
Daws, C., Tripakis, S.: Model Checking of Real-Time Reachability Properties Using Abstractions. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 313–329. Springer, Heidelberg (1998)
Daws, C., Yovine, S.: Reducing the Number of Clock Variables of Timed Automata. In: RTSS 1996, pp. 73–81 (1996)
Diekert, V., Rozenberg, G. (eds.): The Book of Traces. World Scientific, Singapore (1995)
Hendriks, M., Behrmann, G., Larsen, K., Niebert, P., Vaandrager, F.: Adding Symmetry Reduction to Uppaal. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 46–59. Springer, Heidelberg (2004)
Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic Model-checking for Real-time Systems. Information and Computation 111, 193–244 (1994)
Lugiez, D., Niebert, P., Zennou, S.: A Partial Order Semantics Approach to the Clock Explosion Problem of Timed Automata. Theoretical Computer Science 345, 27–59 (2005)
Maler, O., Pnueli, A.: Timing Analysis of Asynchronous Circuits using Timed Automata. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987, pp. 189–205. Springer, Heidelberg (1995)
Minea, M.: Partial Order Reduction for Model Checking of Timed Automata. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 431–446. Springer, Heidelberg (1999)
Rokicki, T.G.: Representing and Modeling Digital Circuits. PhD Thesis, Stanford University (1994)
Tripakis, S.: The Analysis of Timed Systems in Practice, PhD Thesis, Université Joseph Fourier, Grenoble (1998)
Uppaal benchmarks, www.it.uu.se/research/group/darts/uppaal/benchmarks
Yoneda, T., Schlingloff, B.-H.: Efficient Verification of Parallel Real-Time Systems. Formal Methods in System Design, 11, 187–215 (1997)
Zennou, S., Yguel, M., Niebert, P.: ELSE: A New Symbolic State Generator for Timed Automata. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 273–280. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Salah, R.B., Bozga, M., Maler, O. (2006). On Interleaving in Timed Automata. In: Baier, C., Hermanns, H. (eds) CONCUR 2006 – Concurrency Theory. CONCUR 2006. Lecture Notes in Computer Science, vol 4137. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11817949_31
Download citation
DOI: https://doi.org/10.1007/11817949_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37376-6
Online ISBN: 978-3-540-37377-3
eBook Packages: Computer ScienceComputer Science (R0)