Time Petri Nets: Theory, Tools and Applications
Time Petri nets (TPNs) extend Petri nets with temporal intervals associated
with transitions. Since their introduction by Merlin in 1974, they
are one of the prominent models proposed for the
specification and verification of time dependent systems.
Their ability to cope with a wide
variety of modeling problems, as well as
the availability of effective analysis methods certainly contributed to
their widespread use.
This advanced tutorial will review in a unified framework the
essentials results about Time Petri nets. It will cover the classical
results as well as recent state-of-the-art developments. Both theory
and applications will be addressed. A relationship to other time-dependent
modeling instruments - Timed automata, Timed Petri nets - will be examined.
Expected audience
This advanced tutorial is aimed at
- Researchers and Ph.D. students interested in fundamental issues
in modeling and verification of time dependent systems.
- Engineers interested in using analysis and verification methods for
complex systems in the areas of realtime systems, hardware components,
communication protocols or biochemical systems.
The attendees are expected to have a basic knowledge of Petri nets
(places, transitions, firing game) as well as some notions of linear
algebra.
Speakers
After a Doctoral degree obtained from the University of
Toulouse III and post-doctoral positions at Information Science
Institute (Marina del Rey) and the Bull Company,
Bernard Berthomieu
joined the Centre National de la Recherche Scientifique in 1982, at
the Laboratoire d'Architecture et d'Analyse des Systémes (LAAS),
Toulouse. He has studied specification and analysis techniques for
concurrent and real-time systems for over 20 years, using various
formal tools like Petri nets, Time Petri nets, Algebraic Data
Types, and Process Calculi. He authored a number of methods and tools
in these area and notably pioneered geometric analysis techniques for
real-time systems, by proposing the so-called state class method for
abstracting the behavior of Merlin's Time Petri nets. This work was
first presented at the 3rd European Workshop on Petri Nets, Varenna,
1982. This analysis technique has been has since incorporated in a
variety of tools and discussed and used in a number of works. He is
currently involved in a number of projects in the area of verification
of embedded systems.
Louchka Popova-Zeugmann
studied physics and mathematics, receiving her M.A. in
the latter. Her PhD and postdoctoral lecture qualification (Habilitation) were awarded in
Computer Science at the Berlin Humboldt University. Between 1979 and 1986,
while employed at the University of Economics in Berlin, optimization and
modeling were the focus of her work. Thereafter, she transferred to the
Humboldt University's department of Mathematics where she specialized in the
optimization of electrical power plant production. In 1990, she transferred to
the Department of Computer Science where she currently works as a researcher.
Her interests include the design and analysis of time-dependent PNs and the
design and modeling of time-sensitive systems. She created two methods for
reducing the state space of Merlin's TPNs, as well as several algorithms for
analyzing other time-dependent PNs like the ones that construct a time
dependent state equation for Ramchandani's time-dependent PNs or those that
translate time-dependent PNs into TPNs.
Contents
The tutorial will discuss the two most widely used analysis methods for Time Petri nets:
the "essential states" method by L. Popova-Zeugmann (1989) and the "state classes" method
by B. Berthomieu & M. Menasche (1982). The method by Popova-Zeugmann is based on particular
snapshots of the state space, while Berthomieu & Menasche utilize geometric
characterizations of temporal information to examine TPNs. Both methods will be
discussed by their author, respectively.
slides to Part II:
Part II
Part I. Essential states based methods - Louchka Popova-Zeugmann
1. TPN: An introduction
1.1. Basic notions, equivalence to the Turing machine
1.2. State space
1.2.1. Parametric representation
1.2.2. Reduction: essential states
1.2.3. Reachability graph
1.3. Comparison: TPN and timeless PN with respect to the
boundedness and the liveness
1.4. Quantitative evaluation
1.4.1. Algorithms for unbounded TPN
1.4.2. Algorithms for bounded TPN
2. Timed Petri nets
2.1. Short introduction, equivalence to the Turing
machine, transformation into TPN
2.2. Time-dependent state equation
2.3. Timed Petri nets with variable time durations
3. An application + tool demonstration: Evaluation of a biochemical network (cell division
cycle: cdc2 and cyclin interactions) modelled with a time-dependent Petri net using the tool
INA
Part II. State Classes based methods - Bernard Berthomieu
1. Background
1.1. Time Petri Nets
1.2. Dense semantics, state spaces
1.3. Representation of states -- firing domains, clocks
vectors
1.4. Basic theorems
1.5. logics
2. State Class graphs as abstract state spaces
2.1. State space abstractions
2.2. Properties
2.3. State class graphs
3. State Classes preserving markings and traces
3.1. Construction
3.2. Properties
3.3. Computing classes
3.4. Boundedness analysis
3.5. Marking reachability, LTL model checking
3.6. Variations
3.7. Illustrative examples
4. Preserving states and traces
4.1. Construction
4.2. Representing state sets, clock systems
4.3. Computing strong classes
4.4. Handling unbounded intervals
4.4. State reachability, LTL model checking
4.5. Variations
4.6. Illustrative examples
5. Preserving states and branching properties
5.1. Preserving branching properties
5.2. Partition refinement
5.3. Atomic state classe
5.4. Liveness analysis
5.5. Illustrative examples
6. Quantitative properties, Other techniques
6.1. Checking Timed properties, observers
6.2. Path Analysis, characterizing firing schedules
6.3. Alternative methods
6.4. State classes vs essential states
7. Subclasses, extensions, alternatives
7.1. Subclasses
7.2. Extensions and their analysis
7.2.1. Open time intervals
7.2.2. Inhibitor arcs, read arcs
7.2.3. Priorities
7.2.4. Stopwatches
7.2.5. High level notations - Time transition
systems
7.3. Other models for real-time systems
7.3.1. The variety of TPN's
7.3.2. Timed Automata
8. Application areas, tools
8.1. Applications areas
8.2. Some Tools using state classes
8.3. The TINA toolbox (http://www.laas.fr/tina)
Short bibliography
