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 k-bounded, 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? (Free-choice Net, Well-Formed 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

pn-images/invariant-example.png

Place invariants

If a vector YT is a solution of YT * C = 0 then YT is a structural place invariant. For example, YT = (1 1 1 0 0 0 0) is a structural place invariant. System place invariants are defined by the equation: YTM = YTM0. For example:

pn-images/system-p-invariant.png

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 Vs is equal X, e.g. s1 = t1t2t3t4t5t6 or s2 = t4t5t6t1t2t3 are system transition invariants while, for example, sF = t1t3t2t4t5t6 is not system transition invariant because it is not realizable from any reachable marking.

Fundamental equation

M' = M + C * Vs

Vs is a characteristic vector of an arbitrary transition sequence s. The product of C * Vs 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 = M0 and Vs as the characteristic vector of an arbitrary system transition invariant s, then M' has to equal M0. 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; pn-images/omega-markings.png

      • ⇒ 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 m0.

      • 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?