Abstract
The paper presents a partial order reduction method applicable to networks of timed automata. The advantage of the method is that it reduces both the number of explored control states and the number of generated time zones. The approach is based on a local-time semantics for networks of timed automata defined by Bengtsson et al. [1998], and used originally for local reachability analysis. In this semantics, each component automaton executes asynchronously, in its own local time scale, which is tracked by an auxiliary reference clock. On communication transitions, the automata synchronize their time scales. We show how this model can be used to perform model checking for an extension of linear temporal logic, which can express timing relations between events. We also show how for a class of timed automata, the local-time model can be implemented using difference bound matrices without any space penalty, despite the need to represent local time. Furthermore, we analyze the dependence relation between transitions in the new model and give practical conditions for selecting a reduced set of transitions.
This research was sponsored in part by the Semiconductor Research Corporation (SRC), the National Science Foundation (NSF), and the Defense Advanced Research Projects Agency (DARPA).
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.
Similar content being viewed by others
References
R. Alur and D. Dill. Automata for modeling real-time systems. In Automata, Languages, and Programming. 17th Int. Colloquium Proc., LNCS v. 443, pp. 322–35, Coventry, UK, July 1990. Springer.
J. Bengtsson, B. Jonsson, J. Lilius, and Wang Yi. Partial order reductions for timed systems. In CONCUR’98: Concurrency Theory. 8th Int. Conf. Proc., LNCS v. 1466, pp. 485–500, Nice, France, September 1998. Springer.
W. Belluomini and C. J. Myers. Verification of timed systems using POSETs. In Computer Aided Verification. 10th Int. Conf., CAV’98. Proc., LNCS v. 1427, pp. 403–15, Vancouver, BC, Canada, June 1998. Springer.
Computer Aided Verification. 2nd Int. Conf., CAV’90. Proc., LNCS v. 531, New Brunswick, NJ, USA, June 1990. Springer.
E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. Logic of Programs: Workshop, Yorktown Heights, NY, LNCS v. 131, pp. 52–71. Springer, May 1981.
D. Dams, R. Gerth, B. Knaack, and R. Kuiper. Partial-order reduction techniques for real-time model checking. In Proc. 3rd Int. Workshop on Formal Methods for Industrial Critical Systems, pp. 157–69, Amsterdam, The Netherlands, May 1998.
D. L. Dill. Timing assumptions and verification of finite-state concurrent systems. Proc. Int. Workshop Automatic Verification Methods for Finite State Systems., LNCS v. 407, pp. 197–212, Grenoble, June 1989. Springer.
P. Godefroid. Using partial orders to improve automatic verification methods. In [4], pp. 176–85.
T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. In Proc. Seventh Ann. IEEE Symp. on Logic in Computer Science, pp. 394–406, Santa Cruz, CA, USA, June 1992. IEEE Comp. Soc. Press.
J. Lilius. Efficient state space search for time Petri nets. In Proc. MFCS’98 Workshop on Concurrency, Brno, Czech Republic, August 1998. Elsevier.
K. G. Larsen, P. Pettersson, and Wang Yi. Compositional and symbolic modelcheking of real-time systems. In Proc. 16th IEEE Real-Time Systems Symp., pp. 76–87, Pisa, Italy, Dec. 1995. IEEE Comp. Soc. Press.
F. Pagani. Partial orders and verification of real-time systems. In Formal Techniques in Real-Time and Fault-Tolerant Systems. 4th Int. Symp. Proc., LNCS v. 1135, pp. 327–46, Uppsala, September 1996. Springer.
F. Pagani. Ordres partiels pour la vérification de systémes temps réel (Partial orders for verification of real-time systems). PhD thesis, Centre d’études et de Recherches de Toulouse, September 1997.
D. Peled. All from one, one for all: on model checking using representatives. In Computer Aided Verification. 5th Int. Conf., CAV’93. Proc., LNCS v. 697, pp. 409–23, Elounda, Greece, June 1993. Springer.
A. Valmari. A stubborn attack on state explosion. In [4], pp. 156–65.
M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. Symp. on Logic in Computer Science, pp. 332–44, Cambridge, MA, USA, June 1986. IEEE Comp. Soc. Press.
H. Wong-Toi. Symbolic Approximations for Verifying Real-Time Systems. PhD thesis, Stanford University, December 1994.
T. Yoneda and B.-H. Schlingloff. Efficient verification of parallel real-time systems. Formal Methods in System Design, 11(2):197–215, August 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Minea, M. (1999). Partial Order Reduction for Model Checking of Timed Automata. In: Baeten, J.C.M., Mauw, S. (eds) CONCUR’99 Concurrency Theory. CONCUR 1999. Lecture Notes in Computer Science, vol 1664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48320-9_30
Download citation
DOI: https://doi.org/10.1007/3-540-48320-9_30
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66425-3
Online ISBN: 978-3-540-48320-5
eBook Packages: Springer Book Archive