Abstract
We introduce partial S-invariants of Petri nets, which can help to determine invariants and to prove safety if large nets are built from smaller ones using parallel composition withsync hronous communication. Partial S-invariants can support compositional reduction and, in particular, the fixed-point approach, used for verifying infinite parameterized families of concurrent systems. Withpartial S-invariants and the fixed-point approach we prove the correctness of two solutions to the MUTEX-problem based on token rings; for this, we only have to prove liveness of a simplified version due to previous results.
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
P. Baldan, N. Busi, A. Corradini, and M. Pinna. Functional concurrent semantics for Petri nets withread and inhibitor arcs. In C. Palamidessi, editor, CONCUR 2000, Lect. Notes Comp. Sci. 1877, 442–457. Springer, 2000.
E. Bihler and W. Vogler. Efficiency of token-passing MUTEX-solutions-some experiments. In J. Desel et al., editors, Applications and Theory of Petri Nets 1998, Lect. Notes Comp. Sci. 1420, 185–204. Springer, 1998.
E.M. Clarke, O. Grumberg, and S. Jha. Verifying parameterized networks using abstraction and regular languages. In I. Lee and S. Smolka, editors, CONCUR 95, Lect. Notes Comp. Sci. 962, 395–407. Springer, 1995.
E.W. Dijkstra. Invariance and non-determinacy. In C.A.R. Hoare and J.C. Sheperdson, editors, Mathematical Logic and Programming Languages, 157–165. Prentice-Hall, 1985.
S. Graf, B. Steffen, and G. Lüttgen. Compositional minimisation of finite state systems using interface specifications. Formal Aspects of Computing, 8:607–616, 1996.
R. Janicki and M. Koutny. Semantics of inhibitor nets. Information and Computation, 123:1–16, 1995.
R. Kaivola. Using compositional preorders in the verification of sliding window protocol. In CAV 97, Lect. Notes Comp. Sci. 1254, 48–59. Springer, 1997.
E. Kindler. Modularer Entwurf verteilter Systeme mit Petrinetzen. PhD thesis, Techn. Univ. München, Bertz-Verlag, 1995.
U. Montanari and F. Rossi. Contextual nets. Acta Informatica, 32:545–596, 1995.
W. Reisig. Partial order semantics versus interleaving semantics for CSP-like languages and its impact on fairness. In J. Paredaens, editor, Automata, Languages and Programming, Lect. Notes Comp. Sci. 172, 403–413. Springer, 1984.
A. Valmari and Kokkarinen. Unbounded verification results by finite-state compositional technique: 10any states and beyond. In Int. Conf. Application of Concurrency to System Design, 1998, Fukushima, Japan, 75–87. IEEE Computer Society, 1998.
W. Vogler. Fairness and partial order semantics. Information Processing Letters, 55:33–39, 1995.
W. Vogler. Efficiency of asynchronous systems and read arcs in Petri nets. In P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, editors, ICALP 97, Lect. Notes Comp. Sci. 1256, 538–548. Springer, 1997. Full version at http://www.informatik.uni-augsburg.de/~vogler/ under the title ‘Efficiency of Asynchronous Systems, Read Arcs, and the MUTEX-Problem’.
W. Vogler, A. Semenov, and A. Yakovlev. Unfolding and finite prefix for nets with read arcs. In D. Sangiorgi and R. de Simone, editors, CONCUR 98, Lect. Notes Comp. Sci. 1466, 501–516. Springer, 1998. Full version as Technical Report Series No. 634, Computing Science, University of Newcastle upon Tyne, February 1998; can be obtained from: ftp://sadko.ncl.ac.uk/pub/incoming/TRs/.
P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. In Automatic Verification Methods for Finite Systems, Lect. Notes Comp. Sci. 407, 68–80. Springer, 1989.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Vogler, W. (2001). Partial S-Invariants for the Verification of Infinite Systems Families. In: Colom, JM., Koutny, M. (eds) Applications and Theory of Petri Nets 2001. ICATPN 2001. Lecture Notes in Computer Science, vol 2075. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45740-2_22
Download citation
DOI: https://doi.org/10.1007/3-540-45740-2_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42252-5
Online ISBN: 978-3-540-45740-4
eBook Packages: Springer Book Archive