Abstract
We present a method for specifying and implementing algorithms for the analysis of Petri nets. It is formally grounded in relational algebra. Specifications are written in ordinary predicate logic and then transformed systematically into relational programs which can be executed directly in RELVIEW, a graphical computer system for calculating with relations. Our method yields programs that are correct by construction. Its simplicity and efficiency is illustrated in many examples.
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
Berghammer R., Zierer H.: Relational algebraic semantics of deterministic and nondeterministic programs. Theoret. Comput. Sci. 43, 123–147 (1986)
Berghammer R., Gritzner T., Schmidt G.: Prototyping relational specifications using higher-order objects. In: Heering, J., Meinke, K., Möller, B., Nipkow, T. (eds.): Proc. Int. Workshop on Higher Order Algebra, Logic and Term Rewriting (HOA 93), Amsterdam, The Netherlands, Sept. 1993, LNCS 816, Springer, 56–75 (1994)
Berghammer R., von Karger B.: Algorithms from relational specification. In: Brink C., Schmidt G., Albrecht R. (eds.): Relational methods in Computer Science, Supplement volume of Computing (to appear 1996)
Berghammer R., Schmidt G.: RELVIEW — A computer system for the manipulation of relations. In: Nivat M., Rattray C., Rus T., Scollo G. (eds.): Proc. 3rd Conf. on Algebraic Methodology and Software Technology (AMAST 93), University of Twente, The Netherlands, June 1993, Workshops in Computing, Springer, 405–406 (1993)
Dijkstra E.W.: Hierarchical ordering of sequential processes. Acta Informatica 1, 115–138 (1971)
Genrich H.J., Lautenbach K.: Synchronisationsgraphen. Acta Informatica 2, 143–161 (1973)
Hack M.: Analysis of production schemata by Petri nets. TR-94, MIT-MAC (1972)
Lautenbach K.: Liveness in Petri nets. Bericht 02.1/75-7-29, Gesellschaft für Mathematik und Datenverarbeitung, St. Augustin (1975)
Reisig W.: Petri nets — An introduction. EATCS Monographs on Theoret. Comput. Sci., Springer (1985)
Olderog E.-R.: Nets, terms and formulas. Cambridge Tracts in Theoret. Comput. Sci., Cambridge University Press (1991)
Petri C.A.: Non-sequential processes. Bericht GMD-ISF-77-5, Gesellschaft für Mathematik und Datenverarbeitung, St. Augustin (1977)
Schmidt G., Ströhlein T.: Relations and graphs. Discrete Mathematics for Computer Scientists, EATCS Monographs on Theoret. Comput. Sci., Springer (1993)
Tarski A.: On the calculus of relations. J. Symbolic Logic 6, 73–89 (1941)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Berghammer, R., von Karger, B., Ulke, C. (1996). Relation-algebraic analysis of Petri nets with RELVIEW. In: Margaria, T., Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1996. Lecture Notes in Computer Science, vol 1055. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61042-1_38
Download citation
DOI: https://doi.org/10.1007/3-540-61042-1_38
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61042-7
Online ISBN: 978-3-540-49874-2
eBook Packages: Springer Book Archive