Coordinating Functional Processes using Petri Nets
Claus Aßmann

Dept of Computer Science, University of Kiel, 24105 Kiel, Germany,
e-mail: ca@informatik.uni-kiel.de

Abstract. Functional programs are well suited for concurrent execu-
tion due to the Church-Rosser property. However, for many applications
there is still need to explicitly specify process systems instead of rely-
ing on compilers. Coordination languages provide one viable solution to
the problem of specifying concurrent process systems, since they do not
interfere with the properties of the language used for the algorithmic
specification of the processes. The coordination language K2 to be pro-
posed in this paper is based on a variant of colored Petri nets. It primarily
defines process systems with deterministic behavior, but also allows for
controlled forms of non-determinism. Specifications based on Petri nets
offer several advantages. An underlying net calculus facilitates formal
analysis and verification of basic safety and liveness properties. Graphi-
cal representations clearly expose structural dependencies among system
components. Our variant of colored Petri nets provides several forms of
net abstractions which facilitate the systematic construction of complex
systems from small subsystems by composition. Recursive specifications
can be used to adapt the structure of a process system to actual problem
sizes or to varying input parameters.