Symbolic Diagnosis of Partially Observable Concurrent Systems

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


Monitoring large distributed concurrent systems is a challenging task. In this paper we formulate (model-based) diagnosis by means of hidden state history reconstruction, from event (e.g. alarm) observations. We follow a so-called true concurrency approach: the model defines explicitly the causal and concurrency relations between the observable events, produced by the system under supervision on different points of observation. The problem is to compute on-the-fly the different partial order histories, which are the possible explanations of the observable events. In this paper we extend our first method based on Petri nets unfolding to high-level parameterized Petri nets. This allows the designer to model data aspects (even on infinite domains) and non deterministic actions. The observation of such an action gives only partial information and the supervisor has to introduce parameters to represent the hidden aspects of the reached state. This supposes that the possible values for the parameters are symbolically computed and refined during supervision. In practice, non deterministic actions can also be used as an approximation to deal with incomplete information about the system. In this case the refinement of the parameters during supervision improves the knowledge of the model.


Discrete Event System Symbolic Execution Input Place Deterministic Action Presburger Arithmetic 
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.


  1. 1.
    Benveniste, A., Fabre, E., Jard, C., Haar, S.: Diagnosis of asynchronous discrete event systems, a net unfolding approach. IEEE Trans. on Automatic Control 48(5), 714–727 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Cassandras, C., Lafortune, S.: Introduction to discrete event systems. Kluwer Academic Publishers, Dordrecht (1999)CrossRefzbMATHGoogle Scholar
  3. 3.
    Engelfriet, J.: Branching processes of Petri nets. Acta Informatica 28, 575–591 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Desel, J., Esparza, J.: Free choice Petri nets. Cambridge University Press, Cambridge (1995)CrossRefzbMATHGoogle Scholar
  5. 5.
    Esparza, J., Römer, S., Vogler, W.: An improvement of McMillan’s unfolding algorithm. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 2–20. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  6. 6.
    Esparza, J., Römer, S.: An unfolding algorithm for synchronous products of transition systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, p. 2. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  7. 7.
    Fabre, E.: Monitoring distributed systems with distributed algorithms. In: Proc. of the 2002 IEEE Conf. on Decision and Control, pp. 411–416 (2002)Google Scholar
  8. 8.
    Goodwin, G.C., Sin, K.S.: Adaptive filtering, prediction, and control. Prentice-Hall, Upper Sadle River (1984)zbMATHGoogle Scholar
  9. 9.
    Jensen, K.: Coloured Petri nets. Basic concepts, analysis methods and practical use. EATCS Monographs on Theoretical Computer Science. Springer, Heidelberg (1992)CrossRefzbMATHGoogle Scholar
  10. 10.
    Khomenko, V., Koutny, M.: Branching processes of high-level Petri nets. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 458–472. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  11. 11.
    Kozura, V.E.: Unfolding of coloured Petri nets. Technical Report 80, A.P. Ershov Institute of Informatics Systems (2000)Google Scholar
  12. 12.
    Presburger, M.: Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Comptes Rendus du Premier Congrès des Mathématiciens des Pays Slaves 395, 92–101 (1927)zbMATHGoogle Scholar
  13. 13.
    Rabiner, L.R., Juang, B.H.: An introduction to hidden Markov models. IEEE ASSP magazine 3, 4–16 (1986)CrossRefGoogle Scholar
  14. 14.
    Reisig, W.: Petri Net: an introduction. ETACS Monographs on Theoretical Computer Science, vol. 4. Springer, Heidelberg (1985)CrossRefzbMATHGoogle Scholar
  15. 15.
    Sampath, M., Sengupta, R., Sinnamohideen, K., Lafortune, S., Teneketzis, D.: Failure diagnosis using discrete event models. IEEE Trans. on Systems Technology 4(2), 105–124 (1996)CrossRefzbMATHGoogle Scholar
  16. 16.
    Vernier, I.: Symbolic executions of symmetrical parallel programs. In: Proc. of 4th Euromicro Workshop on Parallel and Distributed Processing, Braga, Portugal, pp. 327–334 (1996)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2004

Authors and Affiliations

  • Thomas Chatain
    • 1
  • Claude Jard
    • 1
  1. 1.IRISA/ENS Cachan-Bretagne Campus de BeaulieuRennes cedexFrance

Personalised recommendations