Abstract
The intention of the paper is to develop an algorithm for timing behaviour analysis of concurrent and real time systems. To this purpose we introduce a notion of the parametric time net that is a mod- ification of the time Petri net [4], [7] by using parameter variables in spec- ification of timing constraints on transition firings. A property of the system is given as a formula of Parametric TCTL (PTCTL), a real time branching time temporal logic with timing parameter variables in its operators [6]. Timing behaviour analysis consists in finding necessary and sufficient conditions on parameter values under which the checked PTCTL-formula is valid in the given system. Thus the approach allows ‘mutual adjustment’ of timing specifications of both the system and the property via a single execution of verification procedure. It is further shown the correctness and evaluated the complexity of the algorithm proposed.
This work is supported in part by the Russian State Committee of Higher Education for Basic Research in Mathematics.
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.
References
Alur, R., Dill, D. A theory of timed automata. Theoretical Computer Science 126 (1994) 183–235.
Alur, R., Henzinger, T., Vardi, M. Parametric real time reasoning. Proc. 25th ACM STOC (1993) 592–601.
Bengtsson, J., Jonsson, B., Lilius, J., Yi, W. Partial order reductions for timed systems. Proc. CONCUR’98 (1998) 485–496.
Merlin, P., Faber, D. J. Recoverability of communication protocols. IEEE Trans. of Communication COM-24(9) (1976).
Virbitskaite, I. B., Pokozy, E. A. Towards efficient verification of time Petri nets. Logical Journal of IGPL 5(6) (1997) 921–924.
Wang F. Timing behavior analysis for real-time systems. Proc. 10th IEEE LICS (1995) 112–122.
Yoneda, T., Shibayama, A., Schlingloff, B. H., Clarke, E. M. Efficient verification of concurrent real-time systems. Lecture Notes in Computer Science 697 (1993) 321–333.
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
Virbitskaite, I.B., Pokozy, E.A. (1999). Parametric Behaviour Analysis for Time Petri Nets* . In: Malyshkin, V. (eds) Parallel Computing Technologies. PaCT 1999. Lecture Notes in Computer Science, vol 1662. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48387-X_14
Download citation
DOI: https://doi.org/10.1007/3-540-48387-X_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66363-8
Online ISBN: 978-3-540-48387-8
eBook Packages: Springer Book Archive