Abstract
In this paper, we present a partial-order reduction method for timed systems based on a local-time semantics for networks of timed automata. The main idea is to remove the implicit clock synchronization between processes in a network by letting local clocks in each process advance independently of clocks in other processes, and by requiring that two processes resynchronize their local time scales whenever they communicate. A symbolic version of this new semantics is developed in terms of predicate transformers, which enjoys the desired property that two predicate transformers are independent if they correspond to disjoint transitions in different processes. Thus we can apply standard partial order reduction techniques to the problem of checking reachability for timed systems, which avoid exploration of unnecessary interleavings of independent transitions. The price is that we must introduce extra machinery to perform the resynchronization operations on local clocks. Finally, we present a variant of DBM representation of symbolic states in the local time semantics for efficient implementation of our method.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R. Alur and D. Dill. Automata for Modelling Real-Time Systems. In Proc. of of International Colloquium on Algorithms, Languages and Programming, vol. 443 of LNCS, pp. 322–335. Springer Verlag, 1990.
B. Berthomieu and M. Diaz. Modelling and verification of time dependent systems using time Petri nets. IEEE Transactions on Software Engineering, 17(3):259–273, 1991.
R. Bellman. Dynamic Programming. Princeton University Press, 1957.
J. Bengtsson, D. Griffioen, K. Kristoffersen, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. Verification of an Audio Protocol with Bus Collision Using Uppaal. In Proc. of 9th Int. Conf. on Computer Aided Verification, vol. 1102 of LNCS, pp. 244–256. Springer Verlag, 1996.
J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. Uppaal in 1995. In Proc. of the 2nd Workshop on Tools and Algorithms for the Construction and Analysis of Systems, vol. 1055 of Lecture Notes in Computer Science, pp. 431–434. Springer Verlag, 1996.
C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool kronos. In Proc. of Workshop on Verification and Control of Hybrid Systems III, vol. 1066 of LNCS, pp. 208–219. Springer Verlag, 1995.
R. M. Fujimoto. Parallel discrete event simulation. Communications of the ACM, 33(10):30–53, Oct. 1990.
P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem, vol. 1032 of LNCS. Springer Verlag, 1996.
P. Godefroid and P. Wolper. Using partial orders to improve automatic verification methods. In Proc. of Workshop on Computer Aided Verification, 1990.
T. A. Henzinger and P.-H. Ho. HyTech: The Cornell HYbrid TECHnology Tool. Proc. of Workshop on Tools and Algorithms for the Construction and Analysis of Systems, 1995. BRICS report series NS-95-2.
G. J. Holzmann and D. A. Peled. An improvement in formal verification. In Proc. of the 7th International Conference on Formal Description Techniques, pp. 197–211, 1994.
F. Larsson, K. G. Larsen, P. Pettersson, and W. Yi. Efficient Verification of Real-Time Systems: Compact Data Structures and State-Space Reduction. In Proc. of the 18th IEEE Real-Time Systems Symposium, pp. 14–24, December 1997.
K. G. Larsen, P. Pettersson, and W. Yi. Compositional and Symbolic Model-Checking of Real-Time Systems. In Proc. of the 16th IEEE Real-Time Systems Symposium, pp. 76–87, December 1995.
W. Overman. Verification of Concurrent Systems: Function and Timing. PhD thesis, UCLA, Aug. 1981.
F. Pagani. Partial orders and verification of real-time systems. In Proc. of Formal Techniques in Real-Time and Fault-Tolerant Systems, vol. 1135 of LNCS, pp. 327–346. Springer Verlag, 1996.
D. Peled. All from one, one for all, on model-checking using representatives. In Proc. of 5th Int. Conf. on Computer Aided Verification, vol. 697 of LNCS, pp. 409–423. Springer Verlag, 1993.
A. Valmari. Stubborn sets for reduced state space generation. In Advances in Petri Nets, vol. 483 of LNCS, pp. 491–515. Springer Verlag, 1990.
A. Valmari. On-the-fly verification with stubborn sets. In Proc. of 5th Int. Conf. on Computer Aided Verification, vol. 697 of LNCS, pp. 59–70, 1993.
W. Yi, P. Pettersson, and M. Daniels. Automatic Verification of Real-Time Communicating Systems By Constraint-Solving. In Proc. of the 7th International Conference on Formal Description Techniques, 1994.
T. Yoneda and H. Schlingloff. Efficient verification of parallel real-time systems. Journal of Formal Methods in System Design, 11(2):187–215, 1997.
T. Yoneda, A. Shibayama, B.-H. Schlingloff, and E. M. Clarke. Efficient verification of parallel real-time systems. In Proc. of 5th Int. Conf. on Computer Aided Verification, vol. 697 of LNCS, pp. 321–332. Springer Verlag, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bengtsson, J., Jonsson, B., Lilius, J., Yi, W. (1998). Partial order reductions for timed systems. In: Sangiorgi, D., de Simone, R. (eds) CONCUR'98 Concurrency Theory. CONCUR 1998. Lecture Notes in Computer Science, vol 1466. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055643
Download citation
DOI: https://doi.org/10.1007/BFb0055643
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64896-3
Online ISBN: 978-3-540-68455-8
eBook Packages: Springer Book Archive