Typesetting Petri Nets

18 February 2010

Donal asked about typesetting Petri nets. I’m using the LaTeX style PGF/TikZ; this renders things well, and plays nicely with the beamer class for creating slides. These are ridiculously extensive packages, both written by Till Tantau — I cannot imagine how he finds the time.

TikZ works with moderately high-level descriptions of diagrams: for Petri nets, once the location of places and transitions are set it will draw the links between them, according to suitable styling instructions. It also works entirely within TeX, which is a help for portability. (We’ll leave aside the issue of whether trigonometric computation is a sensible task to attempt in a language designed for text preparation.)

Browse the gallery of TikZ examples to see what can be done. There are even PDF animations, like this one of set intersection (source code).

I have no plans to animate my Petri nets, although I’m sure it could be done.

Chris said he had experience with dot2tex, which I have not used.

Any other suggestions on good ways to draw Petri nets?

1 Comment | Uncategorized | Tagged: , , , | Permalink
Posted by Ian Stark

Lecture 9: Continuous time

8 February 2010

Note: The slides have been revised since the lecture, removing some untruths, adding more about BDDs and exponential distribution, and providing further references.

Symbolic Model Checking: How advanced algorithms test assertions on systems with states than you can imagine possible.

Road Map Review: Shifting between high-level intuitive models and low-level mathematical ones, with multiple choices and analyses.

Continuous Time: Negative exponential distributions and why we use it; starting with Stochastic Petri Nets.

Link: Slides (updated)

Homework

Read the following short articles for Thursday.

Comments Off on Lecture 9: Continuous time | Lecture Log | Tagged: , , | Permalink
Posted by Ian Stark

Lecture 5: Linear Temporal Logic

25 January 2010

The slides for this lecture review the notions of labelled transition systems, runs and traces, and give examples of the expansion of Petri net behaviour into labelled transition systems.

Boardwork then gave definitions of LTL formula, their meaning, and some small examples of application to LTS runs and Petri net behaviours.

Heiner et al. discuss how even finite reachability graphs for Petri nets may blow up very fast (§4(5)). However, they then jump straight to branching-time with CTL.

Huth and Ryan present the syntax and semantics of LTL (§3(2)) as well as some motivation on model checking.

The SPIN tool is based on LTL model checking.

Comments Off on Lecture 5: Linear Temporal Logic | Lecture Log | Tagged: , , | Permalink
Posted by Ian Stark

Some Petri Net reading

25 January 2010

Here are some reading indications for the material we have covered so far: Petri Nets, matrix representation, {T,P}-invariants, and the conversion to labelled transition systems.

Plotkin
Lecture notes set 1 and set 2 from a previous iteration of MLCSB cover these topics and include some extra examples.

Wilkinson
Chapter 1 introduces and motivates biological modelling in general. Chapter 2 sections 2.1–2.3 describe Petri Nets; the remainder of Chapter 2 discusses representation in the Systems Biology Markup Language (SBML). Wilkinson does not cover logical and model-checking, but does treat probabilistic and stochastic models, which we shall return to later.

Heiner et al.
Sections 1–3 give an overview and some context to modelling in systems biology. Section 4 covers all the Petri Net material we have done so far, and in considerable depth. Read it to see just how detailed these analyses can get.

There are some accompanying slides from this summer school, which you may find helpful.

Comments Off on Some Petri Net reading | Reading | Tagged: , | Permalink
Posted by Ian Stark