Advertisement

Fault Diagnosis for Timed Automata

  • Stavros Tripakis
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2469)

Abstract

We study the problem of fault-diagnosis in the context of dense-time automata. The problem is, given the model of a plant as a timed automaton with a set of observable events and a set of unobserv-able events, including a special event modeling faults, to construct a deterministic machine, the diagnoser, which reacts to observable events and time delays, and announces a fault within a delay of at most Δ time units after the fault occurred. We define what it means for a timed automaton to be diagnosable, and provide algorithms to check diagnosability. The algorithms are based on standard reachability analyses in search of accepting states or non-zeno runs. We also show how to construct a di-agnoser for a diagnosable timed automaton, and how the diagnoser can be implemented using data structures and algorithms similar to those used in most timed-automata verification tools.

Keywords

Fault diagnosis Partial observability Timed Automata 

References

  1. 1.
  2. 2.
    Esterel web-site: http://www.esterel.org.
  3. 3.
    R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Rajeev Alur. Techniques for Automatic Verification of Real-Time Systems. PhD thesis, Department of Computer Science, Stanford University, 1991.Google Scholar
  5. 5.
    E. Asarin, O. Maler, A. Pnueli, and J. Sifakis. Controller synthesis for timed automata. In Proc. IFAC Symposium on System Structure and Control. Elsevier, 1998.Google Scholar
  6. 6.
    A. Balluchi, L. Benvenuti, M. Di Benedetto, and A. Sangiovanni-Vincentelli. Design of observers for hybrid systems. In Hybrid Systems: Computation and Control, 2002. To appear.Google Scholar
  7. 7.
    P. Baroni, G. Lamperti, P. Pogliano, and M. Zanella. Diagnosis of large active systems. Artificial Intelligence, 110, 1999.Google Scholar
  8. 8.
    A. Bouajjani, S. Tripakis, and S. Yovine. On-the-fly symbolic model checking for real-time systems. In Proc. of the 18th IEEE Real-Time Systems Symposium, San Francisco, CA, pages 232–243. IEEE, December 1997.Google Scholar
  9. 9.
    M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine. Kronos: a model-checking tool for real-time systems. In Proc. of the 10th Conference on Computer-Aided Verification, CAV’98. LNCS 1427, Springer-Verlag, 1998.CrossRefGoogle Scholar
  10. 10.
    B.A. Brandin and W.M. Wonham. Supervisory control of timed discrete-event systems. IEEE Transactions on Automatic Control, 39(2), 1994.Google Scholar
  11. 11.
    Yi-Liang Chen and Gregory Provan. Modeling and diagnosis of timed discrete event systems-a factory automation example. In ACC, 1997.Google Scholar
  12. 12.
    D.D. Cofer and V.K. Garg. On controlling timed discrete event systems. In Hybrid Systems III: Verification and Control. LNCS 1066, Springer-Verlag, 1996.Google Scholar
  13. 13.
    D.L. Dill. Timing assumptions and verification of finite-state concurrent systems. In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science 407, pages 197–212. Springer-Verlag, 1989.Google Scholar
  14. 14.
    N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language Lustre. Proceedings of the IEEE, 79(9), September 1991.Google Scholar
  15. 15.
    T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193–244, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    L.E. Holloway and S. Chand. Time templates for discrete event fault monitoring in manufacturing systems. In Proc. of the 1994 American Control Conference, 1994.Google Scholar
  17. 17.
    S. Narasimhan and G. Biswas. An approach to model-based diagnosis of hybrid systems. In Hybrid Systems: Computation and Control, 2002. To appear.Google Scholar
  18. 18.
    J. Raisch and S. O’Young. A DES approach to control of hybrid dynamical systems. In Hybrid Systems III: Verification and Control. LNCS 1066, Springer-Verlag, 1996.Google Scholar
  19. 19.
    P. Ramadge and W. Wonham. Supervisory control of a class of discrete event processes. SIAM J. Control Optim., 25(1), January 1987.Google Scholar
  20. 20.
    Amit Kumar Ray and R. B. Misra. Real-time fault diagnosis-using occupancy grids and neural network techniques. In Industrial and Engineering Applications of Artificial Intelligence and Expert Systems, IEA/AIE. LNCS 604, Springer-Verlag, 1992.CrossRefGoogle Scholar
  21. 21.
    M. Sampath, R. Sengupta, S. Lafortune, K. Sinnamohideen, and D. Teneketzis. Diagnosability of discrete event systems. IEEE Transactions on Automatic Control, 40(9), September 1995.Google Scholar
  22. 22.
    M. Sampath, R. Sengupta, S. Lafortune, K. Sinnamohideen, and D. Teneketzis. Failure diagnosis using discrete event models. IEEE Transactions on Control Systems Technology, 4(2), March 1996.Google Scholar
  23. 23.
    J. Sztipanovits, R. Carnes, and A. Misra. Finite state temporal automata modeling for fault diagnosis. In 9th AIAA Conference on Computing in Aerospace, 1993.Google Scholar
  24. 24.
    J. Sztipanovits and A. Misra. Diagnosis of discrete event systems using ordered binary decision diagrams. In 7th Intl. Workshop on Principles of Diagnosis, 1996.Google Scholar
  25. 25.
    C. Tomlin, J. Lygeros, and S. Sastry. Synthesizing controllers for nonlinear hybrid systems. In Hybrid Systems: Computation and Control. LNCS 1386, Springer-Verlag, 1998.Google Scholar
  26. 26.
    S. Tripakis. The formal analysis of timed systems in practice. PhD thesis, Université Joseph Fourrier de Grenoble, 1998.Google Scholar
  27. 27.
    S. Tripakis. Verifying progress in timed systems. In ARTS’99, LNCS 1601, 1999.Google Scholar
  28. 28.
    S. Tripakis and S. Yovine. Analysis of timed systems using time-abstracting bisim-ulations. Formal Methods in System Design, 18(1):25–68, January 2001.Google Scholar
  29. 29.
    J.N. Tsitsiklis. On the control of discrete event dynamical systems. Mathematics of Control, Signals and Systems, 2(2), 1989.Google Scholar
  30. 30.
    H. Wong-Toi. The synthesis of controllers for linear hybrid automata. In Proc. of IEEE Conference on Decision and Control, 1997.Google Scholar
  31. 31.
    H. Wong-Toi and G. Hoffmann. The control of dense real-time discrete event systems. In Proc. of the 30th IEEE Conference on Decision and Control, 1991.Google Scholar
  32. 32.
    S. Hashtrudi Zad, R.H. Kwong, and W.M. Wonham. Fault diagnosis in finite-state automata and timed discrete-event systems. In 38th IEEE Conference on Decision and Control, 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Stavros Tripakis
    • 1
  1. 1.VERIMAGCentre EquationGiéresFrance

Personalised recommendations