There are information related to the seminars.
Tools

GreatSPN editor on GreatSPN home page, an editor which provides a pleasant way of drawing nets with a nice simulation. It supports all constructs that we use in the course (discrete places, immediate transitions, normal arcs, inhibitor arcs, transitions with priorities).

CPN Tools, a complex tool which provides a wide variety of functions, mainly intended for Coloured Petr nets.
Project specification [CZE]
For the project you can use GreatSPN editor or CPN Tools. One part of the submission is presentation of your project. The presentation will be personal, most likely, during the exam period. Presentation before Christmas Holiday will be possible as well. No presentation slides are needed!
The project should match all the following conditions:

The project is consisted of at least 15 elements (the sum of places and transitions).

There are at least two places which are kbounded, where k >= 2.

All places and transition have reasonable names.

Analyze your Petri net.

What properties your system meet? (liveness, boundedness, reversibility, …)

What those properties say about your system? Try to interpret them in terms of your system.

Is your Petri net of one of the specific types? (Freechoice Net, WellFormed System Net, …)

All analyzes should be supported by some of the standard methods.

Notes from seminars
15.12.2014
Test  at the lecture
Presentation of projects  at the seminar. It is optional, for students who want to get a feedback or close their project :).
8.12.2014
Revision, preparation for test
1.12.2014
Hierarchical synthesis of Petri nets
10.  24.11.2014

Structural analysis of P/T Petri nets

Incidence matrix, C

Place/Transition invariants

Structural, based on the structure of a P/T Petri net

System, includes marking


Fundamental equation

Traps and Cotraps

Example: Mutual exclusion
Place invariants
If a vector Y^{T} is a solution of Y^{T} * C = 0 then Y^{T} is a structural place invariant. For example, Y^{T} = (1 1 1 0 0 0 0) is a structural place invariant. System place invariants are defined by the equation: Y^{T}M = Y^{T}M_{0}. For example:
Transition invariants
If a vector X is a solution of C * X = 0 then X is a structural transition invariant. For example, X = (1 1 1 1 1 1) is a structural transition invariant. A system transition invariant is a sequence s of transitions which is realizable from a reachable marking M and its characteristic vector V_{s} is equal X, e.g. s_{1} = t_{1}t_{2}t_{3}t_{4}t_{5}t_{6} or s_{2} = t_{4}t_{5}t_{6}t_{1}t_{2}t_{3} are system transition invariants while, for example, s_{F} = t_{1}t_{3}t_{2}t_{4}t_{5}t_{6} is not system transition invariant because it is not realizable from any reachable marking.
Fundamental equation
M' = M + C * V_{s}
V_{s} is a characteristic vector of an arbitrary transition sequence s. The product of C * V_{s} is a vector which says the change of marking M, so a new marking M' arises as sum of the product and current marking M. Let’s take M = M_{0} and V_{s} as the characteristic vector of an arbitrary system transition invariant s, then M' has to equal M_{0}. If it is not, then s is not a system transition invariant.
3.11.2014

Other properties of Petri nets

Termination

Weak liveness

Deadlock free


Marking (Reachability) vs. Covering graphs

Covering graphs, a finite representation of (in)finite marking graphs;

⇒ What does it mean that one marking covers another one?



Relation between properties of Petri nets and graph properties of marking graph.

Boundedness:

PN: There exists a number b such that each place contains at most b tokens.

MG: Marking graph is finite.


Liveness:

PN: For each reachable marking m and each transition t there exists a marking m' which is reachable from m and enables t.

MG: For each transition t there exists a path starting in each vertex of marking graph such that t occurs on that path. (each transition t will always be enabled in the future)


Reversibility:

PN: From each marking m is always reachable the initial marking m_{0}.

MG: Marking graph forms one strongly connected component.


…

27.10.2014
Dean’s day off
20.10.2014

Marking (reachability) graphs

Covering graphs

Properties of Petri nets Each two of the following properties are mutually independent.

Liveness (transitions)

Boundedness (places)

Reversibility (markings)

Home work: Find a net which is bounded, live, and not reversible. Hint: What is the minimal number of tokens you need?