.Open Theories of Concurrency
Also see the following alternative models of complex dynamic systems:
General Systems theory and automata:
.See http://www/dick/maths/math_71_Auto...Systems.html
, Systems algebras:
.See http://www/dick/maths/math_72_Systems_Algebra.html
, Process Algebras:
.See http://www/dick/maths/math_73_Process_algebra.html
, and theories of programs:
.See http://www/dick/maths/math_75_Programs.html
.Open Computation Graphs
The grand-daddy of all parallel computation schemes:
.See [KarpMiller66].
These are equivalent to the marked directed graphs described later in this page.
computation_graph::=following,
.Net
N::Sets=given, Nodes.
|- finite N.
BRANCH::=Net{from, to: N}, each branch connects one node to another.
D::Finite_sets($ $BRANCH)=given, a finite set of branches.
Each branch d:D has a FIFO queue of data words in it that are input to `d`.to and output from `d`.from.
Each node n:N inputs a fixed number of data words from each of the branches going to it, and outputs a fixed number of words into the queue leading from it that depend only on the data input.
A::D->Nat0=given,
For d:D, A(d)=number of words in d at start of the computation.
U::D->Nat0=given,
For d:D, U(d) = number of words output from d into d.from.
W::D->Nat0=given,
For d, W(d)=number of words removed from d and input into d.to.
T::D->Nat0=given,
For d, T(d) =the threshold of number of words needed in d for d.to to be initiated.
For all d:D, T(d)>=W(d).
S::=D->#Data, set of states.
A node n:N is eligible for initiation iff for all d:n./to (number of words in queue d >=T(d)).
For n:N, s:S, eligible(n,s)::@= for all d:n./to (s(d) >=T(d)).
No two performances of a node can be simultaneously initiated.
After n is initiated, W(d) words are removed from each d:n./to, and operation Op(n) is performed.
When Op(n) terminates, U(d) words are placed in each queue d : n./from.
Whole graph terminates when every node has at least on incoming edge that has too few words to let it initiate.
Note. A loop d:D such that d.from=d.to will act as a state for the node d.from as long as d.A=d.U=d.W.
|- the computation is determinate.
.Close.Net
.Close Computation Graphs
.Open Petri Nets
There is an excellent World Wide Web page for all work being done
on Petri Nets:
.See http://www.daimi.au.dk/PetriNets/
and a mailing list
.See mailto:PetriNet-request@daimi.au.dk
you can subscribe to. The Petri net home page (above)
has a pointer to the home page of the inventor
Prof. Dr. Carl Adam Petri of the original net.
The original Petri net was a designed in response to the theory
of automata. Initially it was an overly general model of a collection
of interacting parts. Modern Petri nets are some variation of the
simpler
P/T or Place/Transition net defined here.
Petri Nets are a way to model many kinds of systems that are both
non-determinstic and/or concurrent. When many things can happen
independently, and these event also tend to control what happens
next to some extent, then a Petri Net may provide a good model.
Petri nets do not necessarily
evolve in a deterministic way. Several different events($Transitions) are
possible($Enabled) at any given time. One of the enabled transitions occurs.
The state of the system is represented by the marks($Marking) made by
putting special
objects ($Tokens) in special icons called places($Places).
PN::abbreviation="Petri Net".
Here is a list of the different kinds of Petri Net defined here.
You can, if you wish, jump to the more specific models and return
to the general ones, top-down by following links.
.Set
$PETRI
$SIMPLE_PETRI_NET
$SAFE_BOOLEAN_PETRI_NET
$NON_DESTRUCTIVE_SIMPLE_PETRI_NET
$WEIGHTED_PETRI_NET
.Close.Set
.Source $ElstobEtAl74, $WooEtAl98
. Definition
PETRI::=following,
.Net
Nodes::Sets, a Petri Net is a directed graph. The nodes are classified
as Places (where tokens are stored) and Transitions (where
things happen).
Places::@Nodes=`given`
Each place is a node that
models a property of the system or a component of the system's state.
Places are normally shown by circles, sometimes with a label next
to the circle. The circle doesn't have a label inside because
its state is shown by "marking" the inside of the circle.
Transitions::@Nodes=`given`.
Transitions model the dynamics of the system, the possible changes.
Transitions are shown as a thin rectangle. If labeled the label is
written beside them.
Nodes are partitioned into Places and Transitions:
|-(bipartite): $Nodes >== { $Places, $Transitions }
(bipartitie)|- (cover): $Nodes = $Places | $Transitions.
(bipartitie)|- (disjoint): No $Places & Transitions.
To save space and typing many mathematicians use P for Places and T
for Transitions and the variable `p` always refers to a place, and
`t` refers to a Transition:
P:=$Places.
T:=$Transitions.
For p:$Places, t:$Transitions.
Arcs::@($Places><$Transitions) | @($Transitions><$Places)=`given`.
The above declaration needs a defence because when you write `A | B` you
must know that `A` and `B` are sets of the same type. In the above declaration
$Places and $Transitions are of type `@$Nodes` and so the type of `$Arcs` is
`@($Nodes><$Nodes)`.
To save space and time, `a` will always represent an arc:
For a:$Arcs.
$Arcs are drawn
as lines with arrow heads. Notice that an arc can go from a place
to a transition or from a transition to a place
but never from a place to a place or a transition to a transition. It
is possible for an arc to go from place `p` to transition `t` and also
another arc can go from `t` to `p`. In this case an arrowhead is drawn
at both ends of a single arc.
When an arrow goes from a place `p` to a transition `t` it is said to be an
input to `t`.
When an arrow goes from a transition `t` to a place `p` it is said to be an
output from `t`.
The following are short hand notations allowing us to write about
the behavior of transitions.
We define the relationship between a transition `t` and a place `p` as being
`None`, `In`, `Out`, and `Inout` arcs:
Inout::@(Transitions, Places) = rel[t,p]( (p,t) and (t,p) in Arcs ),
In::@(Transitions, Places) =rel[t,p]( (p,t) in Arcs and (t,p) not_in Arcs ).
Out::@(Transitions, Places)=rel[t,p]( (t,p) in Arcs and (p,t) not_in Arcs).
None::=@(Transitions, Places)=rel[t,p]( (t,p) notin Arcs and (p,t) not_in Arcs).
(None, In, Inout, Out)|- @(Transitions>== {None, In, Out, Inout }.
Notice that in the MATHS notation relations can be used as follows:
(In)|- t.In = In(t) = { p || t In p } = { (p,t) in Arcs and (t,p) not_in Arcs },
and
(Out)|- t.Out = Out(t) = { p || t Out p } = { (t,p) in Arcs and (p,t) not_in Arcs }.
Tokens::Sets=`given`.
Tokens are used to mark the places and so record their state.
If a Petri net models a computer system then these tokens tend associated with
threads of execution. In a model of a physical system (for example
making coffee) the tokens tend to be associated with physical
resources like (for example) beans, pots, cups, water, boiler, ...
However in some models one token can stand for several (combined)
resources: for example a cup of hot black coffee might be a single
token `cup_black_coffee` even through you might argue that it is a
`cup+hot water+coffee` combination.
Tokens can also be the two possible values for a condition: true and false.
The following is my personal abstraction from several common
models of Petri nets. See
.See Special Versions
below for some specialized and so more applicable kinds of
Petri nets -- nets with conditions on the places, nets which keep
a count of the number of tokens, etc..
empty::Tokens=`given`.
There is a special value for Tokens called `empty`. This is shown
as a place with nothing inside it -- a blank circular icon. It is
also a value that doesn't get listed when describing a marking in a net.
Associated with every transition and place there is an operation that
describes the effect of the transition on that place. If there is no arc
then the transition has no effect. If there is an output arc is then the
operation the puts tokens onto it.
Each input needs an operation that takes tokens. By changing the effect of
input and output we create different versions of a Petri Net.
These operations are always
one-to-one operations. Sometimes operations can not be
carried out -- for example taking a token from an empty place:
output::Out-> ( Tokens <-> Tokens )=`given`.
input::In-> (Tokens <-> Tokens)=`given`.
Note. If the input was not one-to-one then the operation has a choice
about what is consumed. This complicates the analysis of the net's
behavior. It alloes it to model more complex
systems. If empty is some thing that can be input then we have an
optional input. A normal $PN can simulate actions with choices by
having one action for each possible combination of choices instead.
Petri nets evolve by taking tokens from places and putting them
on places. In some versions can destroy and create tokens.
Some versions only allow tokens to be put on places that don't have tokens.
These differences are set up by changing the operations on the arcs($op).
op:: (In|Out)->(Tokens <-> Tokens) = input | output.
I extend the `op` so that it doesn't do anything to places that have no
connection to a transtion:
op::None->(Tokens <-> Tokens) = Id, the do nothing identity function x+>x.
I choose to allow the effect of putting and taking to be allways
possible, and to alows do nothing:
op::Inout->(Tokens <-> Tokens) = Id.
Notice that `op` is well-defined. When these operations are
carried out they have a well-determined effect -- removing a bean
from a non-empty can reduces the number of beans in the can by one.
.Table Arc Operation
.Row None do nothing
.Row In given
.Row Out given
.Row Inout do nothing
.Close.Table
Notice that these operations can not always be carried out -- you can't
get a bean from an empty coffee can. If a place is
empty then you can not take a token from it, and you can certainly
put a token on it:
|- for all x:In, empty not_in pre(x.op).
|- for all x:Out, empty in pre(x.op).
()|- for all x:@(Transitions,Places), all T:Tokens, | (x.op)(T) | in 0..1.
Markings::=Places->Tokens, each place is given a marking.
Initial::Places<>->Tokens=`given`.
Notice that
`Initial` is only a partial map. This makes it
easier to describe typical Petri nets. Normally most places are empty so
this allows a net to described by just listing the non_empty
(marked) places. So the `initial` (lower case) map is defined
as `Initial` (Upper Case) plus the empty Places.
initial::Markings= Initial|+>empty.
(The "f|+>x" notation for completing a partial map is in $STANDARD)
We will use `m` to indicate a marking:
For m:Markings.
Now a given transition `t` can sometimes `fire` depending on the marking `m`.
The effect depends on the operations placed on
the arcs as tabulated in the $op mapping. The result is a new
value ( m'(p) ) represented by the element in the set
((t,p).op)(m(p))
if there is such an element.
We write
Enabled(m) ::={t || for all p ( some ((t,p).op)(m(p)) ) }.
()|- For m:Markings, t:Enabled(m), x:@(Transitions,Places), one (x.op)(m).
()|- For m:Markings, t:Transitions~Enabled(m), x:@(Transitions,Places), no
(x.op)(m).
So if the effect of a transition `t` is described by changing `m` to `m'` then
the relation between a current state and a possible next state as
m becomes m' ::= for some t:$Enabled(m), all p ( m'(p) = the ((t,p).op)(m(p))
).
()|- m becomes m' = for some t:$Enabled(m), all p, following,
.Table If then
.Row (t,p) in In m'(p) = the ((t,p).op)(m(p))
.Row (t,p) in Out m'(p) = the ((t,p).op)(m(p))
.Row (t,p) in Inout m'(p) = m(p)
.Row (t,p) in None m'(p) = m(p)
.Close.Table
This is then repeated to generate a sequence
of new markings:
initial becomes m1 becomes m2 becomes m3 becomes...
We have defined
a state determined mechanism:
mechanism::=the $Mechanism with State=Markings & Transitions=becomes.
. Properties
Live::@Markings={m|| | m.becomes| >= 1 }.
Notice that when a place has a token, and several arcs going to
transitions, that token can only fire one transition. There is
an implicit choice point in every place. However, unlike
flowcharts and start charts there is no explicit condition determining
which happens. This introduces non-determinacy. It is useful
because it can model users making choices. For example, if you
telephone someone their phone starts ringing. They may answer,
or you may hang up. This is not a choice made by the telephone
system and so is naturally shown as a place with two outgoing
arcs.
Deterministic::@Markings={m|| | m.becomes | <= 1 }.
On the other hand, when a transition has two or more outgoing
arcs all the place that they go to get a token. This means
that transitions can create concurrent threads of control.
Similarly they can absorb or join two or more threads.
On the other hand when a Place has more than outgoing arrow
then more than one transition can be enabled. The system can choose
one or the other. Places embody choices and decisions in the net.
. Special Transitions and Places
Sources::@Transitions= {t || In(t)={} }.
Sinks::@Transitions= {t || Out(t)={} }.
Places with no outgoing transitions:
{p || no t ((p,t) in Arcs)}
are places where Tokens can accumulate. Places with no
incoming transitions:
{p || no t ( (t,p) in Arcs )}
tend to become depleted and then freeze activity in their
dependent transactions.
In modeling requirements Sources and Sinks are rare.
.Close.Net PETRI
. Special Versions
The different versions can be distinguished by the model used for
Tokens.
SIMPLE_PETRI_NET::=Net{
In the simplest case all outputs have the same operation($take)
and all input arcs have the converse operation ($put). This simplifies
the analysis of the net and prediction of how it behaves. It also fits a
large number of useful cases.
We start by defining the two functions:
put::Tokens<->Tokens=`given`, note that `put` is a partial one-to-one
function.
take::Tokens<->Tokens= /put, `take` is the inverse or converse of `put`.
Now use them to make the net:
|- $PETRI( input=> fun[x]($take), output=>fun[x]($put) )
Define the folowing terms:
marked::=pre(take), the pre-image or domain of definition of take.
safe::=pre(put), places where it safe to put things down.
unmarked::=Tokens~marked.
unsafe::=Tokens~safe.
The following properties follow:
()|- take;put and put;take ==> Id.
()|- marked = post(put).
()|- safe = post(take).
(PETRI)|- empty in unmarked & safe.
}=::SIMPLE_PETRI_NET.
A $SIMPLE_PETRI_NET with single place can exhibit complex behaviors. For
example
hailstone::=$ $SIMPLE_PETRI_NET(Places=p, Transition=(0,1),
In=Transitions>(1..), empty=0,
put=odd;(_)*3+1;(_)/2, take=even;(_)/2).
SAFE_BOOLEAN_PETRI_NET::=Net{
Use this model when transitions set only false conditions to true but
can not fire of the condition is already true. An example is that we don't
want to add water to a cup that is already full.
|- $SIMPLE_PETRI_NET( TOKENS=>{false, true}, put=(false+>true), empty=false).
()|- take=(true+>false).
We can never fire a transition that outputs true onto true.
()|-marked=unsafe={true} and unmarked=safe={false}.
}=::SAFE_BOOLEAN_PETRI_NET.
Notice that the following formula
$SIMPLE_PETRI_NET( Tokens=>{false, true}, put=(true+>true|false+>true),
empty=false),
is not correct because `put` is not one-to-one and so `take` is not
definable. I'll leave as an exercise
.Hole
the rewriting of $SIMPLE_PETRI_NET
so that the following become valid:
put=(true+>true | false+>true),
take= (true+>false).
The resulting assumptions model a situation where tokens are destroyed
as they enter places. It shouldn't be possible to destroy a token on a place
by adding another
token. In a simple $PN this is still possible. Here is an example:
$SIMPLE_PETRI_NET( Tokens=>{false, true}, put=not, empty=false).
NON_DESTRUCTIVE_SIMPLE_PETRI_NET::=Net{
|- $SIMPLE_PETRI_NET.
A neat formulation of this is to make sure that `put` doesn't
lead to a fewer number of tokens, or that the sequence t, put(t), put^2(t),...
never repeats itself:
|-(nondestructive):for all i,j:0.., if for some t(put^i(t) = put^j(t)) then i=j.
For example:
Integer::= Net{ Tokens=Nat0, put= (_)+1, empty=0 }.
Exercise.
Show that in this model $Sources can continuously generate new tokens and
$Sinks can continuously absorb any incoming tokens.
}=::NON_DESTRUCTIVE_SIMPLE_PETRI_NET.
In a more complex model the Tokens can be items of data, the places
queues, and the transitions have functions or processes
that indicate how input tokens are used to produce output tokens.
A very common form puts a different weight on each arc but has the
same operation.
WEIGHTED_PETRI_NET::=Net{
|-$ADDITIVE_GROUP(Tokens, +, 0, -).
|-$PETRI(empty=0).
weight::(In|Out)->Tokens=`given`.
|- for x:In, op(x)(T)=T+weight(x).
|- for x:Out, op(x)(T)=T-weight(x).
This means that when transition `t` fires place `p` changes by the
difference between the outputs from `t` asnd the sum of the inputs to `t`.
The commonest case is when
Tokens=Nat0, the natural numbers from 0 upward.
Typcially the weights are either 1 or 0 as well.
Notice that when Tokens =Nat0 it is easy to create Petri Nets where
the number of tokens on a place grow without limit. An example
being any net where a single input produces two outputs that in turn
lead to input back into the original place.
}=::WEIGHTED_PETRI_NET.
A variation of $WEIGHTED_PETRI_NET is when the weights are an action on
some group or monoid. The commonest forms are
.Set
Tokens are a Bag of elementary tokens, taking removes one item from the
bag and puttung adds one token. These are colored petri nets.
Places as Queues. The Tokens are a free Monoid over a set of elementary
items. Items are prefixed by put and `popped` by removing the tail. Here we have the basis
for the piped architectural style and JSP/JSD programs.
My own `floset` should be applicable as well.
.Hole
.Close.Set
. Marked Directed Graphs
If each place in a $PETRI net has precisely one input and one output
then it can be modelled by a `marked directed graph`. The places
become edges in the new graph and the transitions become vertices.
Some powerful results have proved about the liveness and safety of these nets.
.Source $CommonerHoltPnueli71
However they are are not capable of expressing conditional execution, see
$Conditions below.
.Open Design Patterns
. Conditions
A condition is represented by two places with the property that
only one is marked at a time. Other transitions can be turned
on (or off) by taking an input from a condition, and putting it
back afterward. These conditions can be used to reduce the nondeterminancy
of the net. Initially only one of the two places is marked.
The marked place is the condition that is true initially.
As an example a phone can be on-hook, so we have two places:
on_hook and off_hook. A couple of transitions can show that
we can put the phone on_hook and take it off_hook. By only
putting a token on one of them, we make sure that only one
can be true at a time. This gives us a $Toggle.
One can have non-boolean conditions as well.
. Toggle
Toggles are a collection of transitions that can flip a
condition. Each one must take input from one place and put it
on the other place. Typically each toggle has another one that reverses
it.
For example, you raise a telephone and it becomes off_hook (not on_hook).
Putting the phone back puts the phone on-hook and not off-hook.
. Example: a simple toggle
An example is a simple toggle which can move between being on and off
as the `transitions` turn_on and turn_off occur.
toggle::=the NON_DESTRUCTIVE_SIMPLE_PETRI_NET
( Places=>(on,off), Transitions=>(turn_on, turn_off), Integer, empty=0,
Arcs=>{(turn_on,on),(on,turn_off),(turn_off,off), (off, turn_on),
Initial=>off+>1).
.Close Design Patterns
.Close Petri Nets
. Event Structures
After $Vaandrager91, who refers to $NielsenEtAl81
EVENT_STRUCTURE::=Net{
events::Setsgiven.
E:=events.
|- $POSET(E, (<=),...).
preceeds::E->@E=fun[e]{e':E || e'<=e}.
Add a binary conflict relationship:
conflicts_with::@(E,E) & irreflexive & symmetric.
#::=conflists_with.
|- for all events e1,e2,e3, if e1 conflicts_with e2 <= e3 then e1 conflicts_with e3.
concurrent_with::@(E,E)~(<=|>=|#).
\high_cup::=concurrent_with.
|- E>== { <, \high_cup, >, #}.
}=::EVENT_STRUCTURE.
PRIME_EVENT_STRUCTURE::=$EVENT_STRUCTURE and for all e:E(finite preceeds(e)).
LABELED_EVENT_STRUCTURE::=$EVENT_STRUCTURE and Net{ A:=labels:Sets, l:E->A}.
LABELED_PRIME_EVENT_STRUCTURE::=$PRIME_EVENT_STRUCTURE and
Net{ A:=labels:Sets, l:E->A}.
. See Also
map_expressions::=http://www.csci.csusb.edu/dick/maths/logic_5_Maps.html#Map
expressions.
Mechanism::=http://www.csci.csusb.edu/dick/maths/math_71_Auto...Systems.html#M
echanism.
POSET::=http://www.csci.csusb.edu/dick/maths/math_21_Order.html#POSET.
STANDARD::=http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html.
.Close Theories of Concurrency
.Bibliography
(CommonerHoltPnueli71): F Commoner & A W Holt & A even & A Pnueli, Marked Directed Graphs, Journal of Computer and Systems Science V5 (1971) pp511-523.
(ElstobEtAl74): Mike Elstob & Andrew Rae & James Sit Yuen Foo & Arthur Kaletski etc, Automata Group Meetings, Brunel University, October 1973..February 1974.
(NielsenEtAl81): Nielsen & Plotkin & Winskal, Petrie Nets, Event structures & Domains Part I, Theoretical Comp Sci. V13(1981) pp85-108).
(Vaandrager92): Fritz Vaandrager, Determinism \implies (event structure isomorphism \equiv step sequence equivalence), Theoretical Comp Sci. V79Bn2(Feb 91)pp275-294
(WooEtAl98): Lee, Woo J.; Cha, Sung D.; and Kwon, Yong R.,"Integration and analysis of use cases using modular Petri nets in requirements engineering", IEEE Trans Softw Eng V24 n12 (Dec 1998)pp1115-1130