Abstract
This paper presents an efficient model checking algorithm for one-safe time Petri nets and a timed temporal logic. The approach is based on the idea of (1) using only differences of timing variables to be able to construct a finite representation of the set of all reachable states and (2) further reducing the size of this representation by exploiting the concurrency in the net, i.e. only one of several equivalent interleavings being generated for the evaluation of the given formula. This reduction of the state space is possible, because the considered linear-time temporal logic is stuttering invariant. In this paper the concrete model checking algorithm is developed and some experimental results which demonstrate the efficiency of the method are given.
Chapter PDF
Similar content being viewed by others
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.
References
R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. Proc. 5th IEEE LICS, 1990.
R. Alur, T. Henzinger. A really temporal logic. Proc. 30th FOCS, 1989.
B. Berthomieu, M. Diaz. Modeling and verification of time dependent systems using time Petri nets. IEEE Trans. on Soft. Eng., 17(3):259–273, 1991.
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. on Programming Languages and Systems, 8(2):244–263, 1986.
P. Godefroid. Using partial orders to improve automatic verification methods. Proc. 1st CAV, 1990.
F. Jahanian and A. K. Mok. A graph-theoretic approach for timing analysis and its implementation. IEEE Trans. Comput., C-36(8):961–975, 1987.
S. Katz and D. Peled. Defining conditional independence using collapses. Semantics for concurrency, BCS-FACS Workshop, Springer, 1990.
O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. Proc. 12th POPL, 1985.
P. Merlin and D. J. Faber. Recoverability of communication protocols. IEEE Trans. on Communication, COM-24(9), 1976.
J-L. Roux and B. Berthomieu. Verification of a local area network protocol with Tina, a software package for time Petri nets. 7th European Workshop on Application and Theory of Petri Nets, pages 183–205, 1986.
A. Valmari. A stubborn attack on state explosion. Proc. 1st CAV, 1990.
T. Yoneda, Y. Tohma, Y. Kondo. Acceleration of timing verification method based on time Petri nets. Syst. and Computers in Japan, 22(12):37–52, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yoneda, T., Shibayama, A., Schlingloff, BH., Clarke, E.M. (1993). Efficient verification of parallel real-time systems. In: Courcoubetis, C. (eds) Computer Aided Verification. CAV 1993. Lecture Notes in Computer Science, vol 697. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56922-7_27
Download citation
DOI: https://doi.org/10.1007/3-540-56922-7_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56922-0
Online ISBN: 978-3-540-47787-7
eBook Packages: Springer Book Archive