Skip to main content

Unfolding and finite prefix for nets with read arcs

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1466))

Abstract

Petri nets with read arcs are investigated w.r.t their unfolding, where read arcs model reading without consuming, which is often more adequate than the destructive-read-and-rewrite modelled with loops in ordinary nets. The paper redefines the concepts of a branching process and unfolding for nets with read arcs and proves that the set of reachable markings of a net is completely represented by its unfolding. The specific feature of branching processes of nets with read arcs is that the notion of a co-set is no longer based only on the binary concurrency relation between the elements of the unfolding, contrary to ordinary nets. It is shown that the existing conditions for finite prefix construction (McMillan's one and its improvement by Esparza et al.) can only be applied for a subclass of nets with read arcs, the so-called read-persistent nets. Though being restrictive, this subclass is sufficiently practical due to its conformance to the notion of hazard-freedom in logic circuits. The latter appear to be one of the most promising applications for nets with read arcs.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P. Baldan, A. Corradini and U. Montanari. An event structure semantics for P/T contextual nets: asymmetric event structures. to appear in Proc. FoSSaCS'98, April 1998, Lisbon.

    Google Scholar 

  2. N. Busi and R. Gorrieri. A Petri net semantics for π-calculus. In L. Insup and S. Smolka, editors, CONCUR 95, Lect. Notes Comp. Sci. 962, 145–159. Springer, 1995.

    Google Scholar 

  3. N. Busi and M. Pinna. Non-sequential semantics for contextual P/T-nets. In J. Billington and W. Reisig, editors, Applications and Theory of Petri Nets 1996, Lect. Notes Comp. Sci. 1091, 113–132. Springer, 1996.

    Google Scholar 

  4. S. Christensen and N.D. Hansen. Coloured Petri nets extended with place capacities, test arcs, and inhibitor arcs. In M. Ajmone-Marsan, editor, Applications and Theory of Petri Nets 1993, Lect. Notes Comp. Sci. 691, 186–205. Springer, 1993.

    Google Scholar 

  5. J. Engelfriet. Branching processes of Petri nets. Acta Informatica, 28:575–591, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  6. J. Esparza and G. Bruns. Trapping mutual exclusion in the box calculus. Theor. Comput. Sci., 153:95–128, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  7. J. Esparza and S. Melzer. Model Checking LTL Using Constraint Programming In P. Azema and G. Balbo, editors, Applications and Theory of Petri Nets 1997, Lect. Notes Comp. Sci. 1248, 1–20. Springer, 1997.

    Google Scholar 

  8. J. Esparza, S. Römer, and W. Vogler. An improvement of McMillan's unfolding algorithm. In T. Margaria and B. Steffen, editors, TACAS 96, Lect. Notes Comp. Sci. 1055, 87–106. Springer, 1996.

    Google Scholar 

  9. R. Janicki and M. Koutny. Semantics of inhibitor nets. Information and Computation, 123:1–16, 1995.

    Article  MathSciNet  Google Scholar 

  10. K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, 1993.

    Google Scholar 

  11. U. Montanari and F. Rossi. Contextual nets. Acta Informatica, 32:545–596, 1995.

    MATH  MathSciNet  Google Scholar 

  12. M. Nielsen, G.D. Plotkin, and G. Winskel. Petri nets, event structures and domains I. Theor. Comput. Sci., 13:85–108, 1981.

    Article  MATH  MathSciNet  Google Scholar 

  13. A. Semenov and A. Yakovlev. Contextual net unfolding and asynchronous circuit verification Technical Report Series No. 572, Computing Science, University of Newcastle upon Tyne, April 1997. See http://www.cs.ncl.ac.uk/research/trs/lists/97.html.

    Google Scholar 

  14. W. Vogler. Executions: A New Partial Order Semantics of Petri Nets. Theor. Comput. Sci., 91:205–238, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  15. W. Vogler. Partial order semantics and read arcs. Technical Report 1997-1, Inst. f. Informatik, Univ. Augsburg, 1997. See http://www.math.uni-augsburg.de/~vogler/; extended abstract in MFCS 97, LNCS 1295, 508–517.

    Google Scholar 

  16. W. Vogler, A. Semenov and A. Yakovlev. Unfolding and finite prefix for nets with read arcs. 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/).

    Google Scholar 

  17. A. Yakovlev, A.M. Koelmans, A. Semenov and D.J. Kinniment. Modelling, analysis and synthesis of asynchronous control circuits using Petri nets. INTEGRATION: the VLSI Journal, 21:143–170, 1996.

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Davide Sangiorgi Robert de Simone

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Vogler, W., Semenov, A., Yakovlev, A. (1998). Unfolding and finite prefix for nets with read arcs. 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/BFb0055644

Download citation

  • DOI: https://doi.org/10.1007/BFb0055644

  • 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

Publish with us

Policies and ethics