Abstract
We prove the following property for safe conflict-free Petri nets and live and safe extended free-choice Petri nets:
Given two markings M 1 , M 2 of the reachability graph, if some path leads from M 1 to M 2, then some path of polynomial length in the number of transitions of the net leads from M 1 to M 2.
Work partly done within the Esprit Basic Research WG 6067: CALIBAN and within SFB 342, WG A3: SEMAFOR.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
T. van Aardenne-Ehrenfest and N.G. de Bruijn: Circuits and Trees in Oriented Linear Graphs, Simon Stevin 28, 203–217 (1951).
E. Best and J. Desel: Partial Order Behaviour and Structure of Petri Nets. Formal Aspects of Computing Vol. 2 No.2, 123–138 (1990).
E. Best and J. Esparza: Model Checking of Persistent Petri Nets. Computer Science Logic 91, E. Börger, G. Jäger, H. Kleine Büning and M.M. Richter (eds.), LNCS 626, 35–53 (1992).
E. Best and P.S. Thiagarajan: Some Classes of Live and Save Petri Nets. Concurrency, K. and Nets K., Voss H.J., Genrich G., Rozenberg G. (eds.), Advances in Petri Nets. — Berlin: Springer-Verlag, 71–94 (1987).
E. Best and K. Voss: Free Choice Systems have Home States. Acta Informatica 21, 89–100 (1984).
F. Commoner, A.W. Holt, S. Even and A. Pnueli: Marked Directed Graphs. Journal of Computer and System Science Vol. 5, 511–523 (1971).
J. Esparza: Model Checking Using net Unfoldings. Hildesheimer Informatik Fachbericht 14/92 (October 1992). To appear in the Proceedings of TAPSOFT'93.
H. Fleischner: Eulerian Graphs and Related Topics, Part 1, Volume 1. Annals of Discrete Mathematics Vol.45. North-Holland (1990).
H.J. Genrich and K. Lautenbach: Synchronisationsgraphen. Acta Informatica Vol. 2, 143–161 (1973).
M. Hack: Analysis of Production Schemata by Petri Nets. TR-94, MIT-MAC (1972). Corrections (1974).
R. Howell and L. Rosier: On questions of fairness and temporal logic for conflict-free Petri nets. Advances in Petri Nets 1988, G. Rozenberg (ed.), LNCS 340, 200–226 (1988).
L. Landweber and E. Robertson: Properties of Conflict-Free and Persistent Petri Nets. JACM, Vol. 25, No.3, 352–364 (1978).
K.L. McMillan: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. Proceedings of the 4th Workshop on Computer Aided Verification, Montreal, pp. 164–174 (1992).
P.S. Thiagarajan and K. Voss: A Fresh look at free-choice Nets. Information and Control, Vol. 61, No. 2, 85–113 (1984).
H. Yen: A polynomial time algorithm to decide pairwise concurrency of transitions for 1-bounded conflict-free Petri nets. Information Processing Letters 38, 71–76 (1991).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Desel, J., Esparza, J. (1993). Shortest paths in reachability graphs. In: Ajmone Marsan, M. (eds) Application and Theory of Petri Nets 1993. ICATPN 1993. Lecture Notes in Computer Science, vol 691. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56863-8_49
Download citation
DOI: https://doi.org/10.1007/3-540-56863-8_49
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56863-6
Online ISBN: 978-3-540-47759-4
eBook Packages: Springer Book Archive