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.

- 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.

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.

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.

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

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

Bernard Berthomieu and Louchka Popova-Zeugmann