Abstract
Recently, a new approach to the symbolic model checking of timed automata based on a partial order semantics was introduced, which relies on event zones that use vectors of event occurrences instead of clock zones that use vectors of clock values grouped in polyhedral clock constraints. Symbolic state exploration with event zones rather than clock zones can result in significant reductions in the number of symbolic states explored. In this work, we show how to extend the event zone approach to networks of automata with local state invariants, an important feature for modeling complex timed systems. To avoid formalizing local states, we attach to each transition an urgency constraint, that allows to code local state invariants. We have integrated the extension into a prototype tool with event zones and reported very promising experimental results.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
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.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.G.: Static guard analysis in timed automata verification. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, pp. 254–277. Springer, Heidelberg (2003)
Behrmann, G., David, A., Larsen, K.G., Moeller, O., Pettersson, P., Yi, W.: UPPAAL - present and future. In: Proc. of 40th IEEE Conference on Decision and Control. IEEE Computer Society Press, Los Alamitos (2001)
Behrmann, G., Larsen, K., Pearson, J., Weise, C., Yi, W., Lind-Nielsen, J.: Efficient timed reachability analysis using clock difference diagrams. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 341–353. Springer, Heidelberg (1999)
Belluomini, W., Myers, C.: Verification of timed systems using POSETs. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 403–415. Springer, Heidelberg (1998)
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)
Daws, C., Tripakis, S.: Model checking of real-time reachability properties using abstractions. In: Steffen, B. (ed.) ETAPS 1998 and TACAS 1998. LNCS, vol. 1384, p. 313. Springer, Heidelberg (1998)
Daws, C., Yovine, S.: Reducing the number of clock variables of timed automata. In: IEE Real-Time Systems Symposium, pp. 73–81 (December 1996)
Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Information and Computation 111, 193–244 (1994)
Larsen, K., Pettersson, P., Yi, W.: Model-checking for real-time systems. In: Reichel, H. (ed.) FCT 1995. LNCS, vol. 965, pp. 62–88. Springer, Heidelberg (1995)
Lugiez, D., Niebert, P., Zennou, S.: A partial order semantics approach to the clock explosion problem of timed automata. Theoretical Computer Science 345(1), 27–59 (2005)
Ben Salah, R., Bozga, M., Maler, O.: On interleaving in timed automata. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 465–476. Springer, Heidelberg (2006)
Yovine, S.: Kronos: A verification tool for real-time systems. Software Tools for Technology Transfer 1(1), 123–133 (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
Niebert, P., Qu, H. (2006). Adding Invariants to Event Zone Automata. In: Asarin, E., Bouyer, P. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2006. Lecture Notes in Computer Science, vol 4202. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11867340_21
Download citation
DOI: https://doi.org/10.1007/11867340_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-45026-9
Online ISBN: 978-3-540-45031-3
eBook Packages: Computer ScienceComputer Science (R0)