Also see the following alternative models of complex dynamic systems: General Systems theory and automata: [ math_71_Auto...Systems.html ] , Systems algebras: [ math_72_Systems_Algebra.html ] , Process Algebras: [ math_73_Process_algebra.html ] , and theories of programs: [ math_75_Programs.html ]

Computation Graphs

The grand-daddy of all parallel computation schemes: [KarpMiller66]. These are equivalent to the marked directed graphs described later in this page.
1. computation_graph::=following,
   Net
   1. N::Finite=given, Nodes.
   2. BRANCH::=Net{from, to: N}, each branch connects one node to another.
   3. D::Finite($ 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.
   4. 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.
   5. A::D->Nat0=given,
   6. For d:D, A(d)=number of words in d at start of the computation.
   7. U::D->Nat0=given,
   8. For d:D, U(d) = number of words output from d into d.from.
   9. W::D->Nat0=given,
   10. For d, W(d)=number of words removed from d and input into d.to.
   11. T::D->Nat0=given,
   12. For d, T(d) =the threshold of number of words needed in d for d.to to be initiated.
   13. For all d:D, T(d)>=W(d).
   14. S::=D->#Data, set of states.
   15. A node n:N is eligible for initiation iff for all d:n./to (number of words in queue d >=T(d)).
   16. For n:N, s:S, eligible(n,s)::@= for all d:n./to (s(d) >=T(d)).
   17. No two performances of a node can be simultaneously initiated.
   18. After n is initiated, W(d) words are removed from each d:n./to, and operation Op(n) is performed.
   19. When Op(n) terminates, U(d) words are placed in each queue d : n./from.

   20. Whole graph terminates when every node has at least on incoming edge that has too few words to let it initiate.

   21. 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.

       
       

   22. |-the computation is determinate.

   
   (End of Net)
   
   

. . . . . . . . . ( end of section Computation Graphs) <<Contents | End>>

Petri Nets

There is an excellent World Wide Web page for all work being done on Petri Nets: [ http://www.daimi.au.dk/PetriNets/ ] and a mailing list 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).

1. 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.

   • PETRI
   • SIMPLE_PETRI_NET
   • SAFE_BOOLEAN_PETRI_NET
   • NON_DESTRUCTIVE_SIMPLE_PETRI_NET
   • WEIGHTED_PETRI_NET

   Sources

   Mike Elstob & Andrew Rae & James Sit Yuen Foo & Arthur Kaletski etc, Automata Group Meetings, Brunel University, October 1973..February 1974.

   "Integration and analysis of use cases using modular Petri nets in requirements engineering" by Lee, Woo J.; Cha, Sung D.; and Kwon, Yong R. (IEEE Trans Softw Eng V24 n12 (Dec 1998)pp1115-1130

   Definition

2. PETRI::=following,
   Net
   1. Places::Sets=given

      Each place typically 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.

   2. Transitions::Sets=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.

      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:

   3. P:=Places.
   4. T:=Transitions.
   5. For p:Places, t:Transitions.

   6. Arcs::@(Places><Transitions) | @(Transitions><Places)=given.

      Arcs are drawn as lines with arrow heads. Notice that an arc can go from a place to a transition (an input) or from a transition to a place (an output) 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 a double headed arrow is drawn.

      To save space and time, a will always represent an arc:

   7. For a:Arcs.

   8. Nodes::Sets=Places|Transitions, a Petri Net is a directed graph with the property that no place is a transition and no transition is a place and so the Nodes are partitioned into Places and Transitions:
      
   9. |- (bipartite): Nodes >== { Places, Transitions }

      The following are short hand notations allowing us to write about the behavior of transitions. We define the relationship between a transition and a place as being None, In, Out, and Inout arcs:

   10. Inout::@(Transitions, Places) = rel[t,p]( (p,t) and (t,p) in Arcs ),
   11. In::@(Transitions, Places) =rel[t,p]( (p,t) in Arcs and (t,p) not_in Arcs ).
   12. Out::@(Transitions, Places)=rel[t,p]( (t,p) in Arcs and (p,t) not_in Arcs).
   13. None::=@(Transitions, Places)=rel[t,p]( (t,p) notin Arcs and (p,t) not_in Arcs).

       
       

   14. (None, In, Inout, Out)|-@(Transitions><Places) >== {None, In, Out, Inout }.

       Notice that in the MATHS notation relations can be used as follows:
       

   15. (In)|-t.In = In(t) = { p || t In p } = { (p,t) in Arcs and (t,p) not_in Arcs }, and
       
   16. (Out)|-t.Out = Out(t) = { p || t Out p } = { (t,p) in Arcs and (p,t) not_in Arcs }.

   17. 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 [ 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..

   18. 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:

   19. output::Out-> ( Tokens <-> Tokens )=given.
   20. 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. 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).

   21. 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:

   22. 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:

   23. 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.

       Arc	Operation
       None	do nothing
       In	given
       Out	given
       Inout	do nothing

       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:
       

   24. |-for all x:In, empty not_in pre(x.op).
       
   25. |-for all x:Out, empty in pre(x.op).

       
       

   26. (above)|-for all x:@(Transitions,Places), all T:Tokens, | (x.op)(T) | in 0..1.

   27. Markings::=Places->Tokens, each place is given a marking.

   28. 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.

   29. initial::Markings= Initial|+>empty.

       (The "f|+>x" notation for completing a partial map is in STANDARD)

       We will use m to indicate a marking:

   30. 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

   31. ((t,p).op)(m(p)) if there is such an element.

       We write

   32. Enabled(m)::={t || for all p ( some ((t,p).op)(m(p)) ) }.

       
       

   33. (above)|-For m:Markings, t:Enabled(m), x:@(Transitions,Places), one (x.op)(m).
       
   34. (above)|-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)) ).

       
       

   35. (above)|-m becomes m' = for some t:Enabled(m), all p, following,

       If	then
       (t,p) in In	m'(p) = the ((t,p).op)(m(p))
       (t,p) in Out	m'(p) = the ((t,p).op)(m(p))
       (t,p) in Inout	m'(p) = m(p)
       (t,p) in None	m'(p) = m(p)

       This is then repeated to generate a sequence of new markings:

   36. initial becomes m1 becomes m2 becomes m3 becomes...

       We have defined a state determined mechanism:

   37. mechanism::=the Mechanism with State=Markings & Transitions=becomes.

       Properties

   38. 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.

   39. 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

   40. Sources::@Transitions= {t || In(t)={} }.
   41. Sinks::@Transitions= {t || Out(t)={} }.

       Places with no outgoing transitions:

   42. {p || no t ((p,t) in Arcs)} are places where Tokens can accumulate. Places with no incoming transitions:
   43. {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.

   
   (End of Net PETRI)
   
   

   Special Versions

   The different versions can be distinguished by the model used for Tokens.
3. 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:

   1. put::Tokens<->Tokens=given, note that put is a partial one-to-one function.
   2. take::Tokens<->Tokens= /put, take is the inverse or converse of put.

      Now use them to make the net:
      

   3. |-PETRI( input=> fun[x](take), output=>fun[x](put) )

      Define the folowing terms:

   4. marked::=pre(take), the pre-image or domain of definition of take.
   5. safe::=pre(put), places where it safe to put things down.
   6. unmarked::=Tokens~marked.
   7. unsafe::=Tokens~safe.

      The following properties follow:

      
      

   8. (above)|-take;put and put;take ==> Id.
      
   9. (above)|-marked = post(put).
      
   10. (above)|-safe = post(take).
       
   11. (PETRI)|-empty in unmarked & safe.

   
   }=::SIMPLE_PETRI_NET.

   A SIMPLE_PETRI_NET with single place can exhibit complex behaviors. For example

4. hailstone::=$ SIMPLE_PETRI_NET(Places=p, Transition=(0,1), In=Transitions><Places, Out=transitions><Places,Tokens=>(1..), empty=0, put=odd;(_)*3+1;(_)/2, take=even;(_)/2).

5. 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.

   
   

   1. |-SIMPLE_PETRI_NET( TOKENS=>{false, true}, put=(false+>true), empty=false).
      
   2. (above)|-take=(true+>false).

      We can never fire a transition that outputs true onto true.
      

   3. (above)|-marked=unsafe={true} and unmarked=safe={false}.

   
   }=::SAFE_BOOLEAN_PETRI_NET.

   Notice that the following formula

6. 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 [click here if you can fill this hole] the rewriting of SIMPLE_PETRI_NET so that the following become valid:

7. put=(true+>true | false+>true),
8. 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:

9. SIMPLE_PETRI_NET( Tokens=>{false, true}, put=not, empty=false).

10. NON_DESTRUCTIVE_SIMPLE_PETRI_NET::=
    Net{

    
    
    1. |-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:
       

    2. |- (nondestructive): for all i,j:0.., if for some t(put^i(t) = put^j(t)) then i=j.

       For example:

    3. 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.

11. WEIGHTED_PETRI_NET::=
    Net{

    
    
    1. |-ADDITIVE_GROUP(Tokens, +, 0, -).
       
    2. |-PETRI(empty=0).
    3. weight::(In|Out)->Tokens=given.
       
    4. |-for x:In, op(x)(T)=T+weight(x).
       
    5. |-for x:Out, op(x)(T)=T-weight(x).

       The commonest case is when

    6. Tokens=Nat0, the natural numbers from 0 upward.

       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

    • Tokens are a Bag of elementary tokens, taking removes one item from the bag and put add on 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. [click here if you can fill this hole]

    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.

    F Commoner & A W Holt & A even & A Pnueli, Marked Directed Graphs, Journal of Computer and Systems Science V5 (1971) pp511-523.

    However they are are not capable of expressing conditional execution, see Conditions below.

    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.
    1. 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).

    . . . . . . . . . ( end of section Design Patterns) <<Contents | End>>

. . . . . . . . . ( end of section Petri Nets) <<Contents | End>>

Event Structures

After Vaandrager 91, Fritz Vaandrager, Determinism \implies (event structure isomorphism ≡ step sequence equivalence), Theoretical Comp Sci. V79Bn2(Feb 91)pp275-294 who refers to Nielsen & Plotkin & Winskal, Petrie Nets, Event structures & Domains Part I, Theoretical Comp Sci. V13(1981) pp85-108).
1. EVENT_STRUCTURE::=
   Net{

   1. E::=events::Sets.
   2. POSET(E, (<=),...).
   3. preceeds::E->@E=fun[e]{e':E || e'<=e}.

      Add a binary conflict relationship:

   4. #::=conflicts_with::@(E,E) & irreflexive & symmetric.
      
   5. |-for all events e1,e2,e3, if e1 conflicts_with e2 <= e3 then e1 conflicts_with e3.
   6. \high_cup::=concurrent_with::@(E,E)~(<=|>=|#).
      
   7. |-E><E >== { <, \high_cup, >, #}.

   
   }=::EVENT_STRUCTURE.

2. PRIME_EVENT_STRUCTURE::=EVENT_STRUCTURE and for all e:E(preceeds(e) is Finite).

3. LABELED_EVENT_STRUCTURE::=EVENT_STRUCTURE and Net{ A:=labels:Sets, l:E->A}.

4. LABELED_PRIME_EVENT_STRUCTURE::=PRIME_EVENT_STRUCTURE and Net{ A:=labels:Sets, l:E->A}.

   See Also

5. map_expressions::= See http://www.csci.csusb.edu/dick/maths/logic_5_Maps.html#Map expressions.

6. Mechanism::= See http://www.csci.csusb.edu/dick/maths/math_71_Auto...Systems.html#M echanism.

7. POSET::= See http://www.csci.csusb.edu/dick/maths/math_21_Order.html#POSET.

8. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html.

. . . . . . . . . ( end of section Theories of Concurrency) <<Contents | End>>

Notes on MATHS Notation

Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle = Net{radius:Positive Real, center:Point}.

For a complete listing of pages in this part of my site by topic see [ home.html ]

Notes on the Underlying Logic of MATHS

For a more rigorous description of the standard notations see