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 adressed. A relationship to other time-dependent
modelling instruments - Timed automata, Timed Petri nets - will be examined.
Expected audience
This advanced tutorial is aimed at
- Researchers and Ph.D. students interested in foundamental issues
in modeling and verification of time dependant systems.
- Engineers interested in using analysis and verification methods for
complex systems in the areas of realtime systems, hardware components,
communication protocols or bio-chemical 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 and inequatoin systems.
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{\`e}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 Europen 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
1. TPN: An introduction
1.1. Basic notions, equivalence to the Turing machine
1.2. State space
1.2.1. Parametric represantation
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
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: Evaluation of a biochemical network (cell division
cycle: cdc2 and cyclin interactions) modelled with time-dependent Petri nets
