Time Supervision of Concurrent Systems Using Symbolic Unfoldings of Time Petri Nets

  • Thomas Chatain
  • Claude Jard
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3829)


Monitoring real-time concurrent systems is a challenging task. In this paper we formulate (model-based) supervision by means of hidden state history reconstruction, from event (e.g. alarm) observations. We follow a so-called true concurrency approach using time Petri nets: the model defines explicitly the causal and concurrency relations between the observable events, produced by the system under supervision on different points of observation, and constrained by time aspects. The problem is to compute on-the-fly the different partial order histories, which are the possible explanations of the observable events. We do not impose that time is observable: the aim of supervision is to infer the partial ordering of the events and their possible firing dates. This is achieved by considering a model of the system under supervision, given as a time Petri net, and the on-the-fly construction of an unfolding, guided by the observations. Using a symbolic representation, this paper presents a new definition of the unfolding of time Petri nets with dense time.


Partial State Extended Process Concurrent System Extended Event Input Place 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Aura, T., Lilius, J.: Time processes for time Petri nets. In: ICATPN, pp. 136–155 (1997)Google Scholar
  2. 2.
    Benveniste, A., Fabre, E., Jard, C., Haar, S.: Diagnosis of asynchronous discrete event systems, a net unfolding approach. IEEE Transactions on Automatic Control 48(5), 714–727 (2003)CrossRefMathSciNetGoogle Scholar
  3. 3.
    Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE Trans. Software Eng. 17(3), 259–273 (1991)CrossRefMathSciNetGoogle Scholar
  4. 4.
    Berthomieu, B., Vernadat, F.: State class constructions for branching analysis of time Petri nets. In: TACAS, pp. 442–457 (2003)Google Scholar
  5. 5.
    Best, E.: Structure theory of Petri nets: the free choice hiatus. In: Proceedings of an Advanced Course on Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986-Part I, London, UK, pp. 168–205. Springer, Heidelberg (1987)CrossRefGoogle Scholar
  6. 6.
    Chatain, T., Jard, C.: Symbolic diagnosis of partially observable concurrent systems. In: FORTE, pp. 326–342 (2004)Google Scholar
  7. 7.
    Chatain, T., Jard, C.: Time supervision of concurrent systems using symbolic unfoldings of time petri nets. Technical Report RR-5076, Institut National de Recherche en Informatique et en Automatique, INRIA (2005)Google Scholar
  8. 8.
    Engelfriet, J.: Branching processes of Petri nets. Acta Inf. 28(6), 575–591 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Esparza, J., Römer, S., Vogler, W.: An improvement of McMillan’s unfolding algorithm. In: TACAS, pp. 87–106 (1996)Google Scholar
  10. 10.
    Fleischhack, H., Stehno, C.: Computing a finite prefix of a time Petri net. In: ICATPN, pp. 163–181 (2002)Google Scholar
  11. 11.
    Merlin, P.M., Farber, D.J.: Recoverability of communication protocols – implications of a theorical study. IEEE Transactions on Communications 24 (1976)Google Scholar
  12. 12.
    Pradin-Chézalviel, B., Valette, R., Künzle, L.A.: Scenario duration characterization of t-timed Petri nets using linear logic. In: IEEE PNPM, pp. 208–217 (1999)Google Scholar
  13. 13.
    Semenov, A., Yakovlev, A.: Verification of asynchronous circuits using time Petri net unfolding. In: DAC 1996: Proceedings of the 33rd annual conference on Design automation, pp. 59–62. ACM Press, New York (1996)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Thomas Chatain
    • 1
  • Claude Jard
    • 1
  1. 1.IRISA/ENS Cachan-BretagneRennesFrance

Personalised recommendations