Skip to main content

Predictability of Event Occurrences in Timed Systems

  • Conference paper
Formal Modeling and Analysis of Timed Systems (FORMATS 2013)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8053))

Abstract

We address the problem of predicting events’ occurrences in partially observable timed systems modelled by timed automata. Our contribution is many-fold: 1) we give a definition of bounded predictability, namely k-predictability, that takes into account the minimum delay between the prediction and the actual event’s occurrence; 2) we show that 0-predictability is equivalent to the original notion of predictability of S. Genc and S. Lafortune; 3) we provide a necessary and sufficient condition for k-predictability (which is very similar to k-diagnosability) and give a simple algorithm to check k-predictability; 4) we address the problem of predictability of events’ occurrences in timed automata and show that the problem is PSPACE-complete.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 49.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Sampath, M., Sengupta, R., Lafortune, S., Sinnamohideen, K., Teneketzis, D.: Diagnosability of discrete event systems. IEEE Trans. on Auto. Cont. 40(9) (1995)

    Google Scholar 

  2. Yoo, T.S., Lafortune, S.: Polynomial-time verification of diagnosability of partially-observed discrete-event systems. IEEE Trans. on Auto. Cont. 47(9), 1491–1495 (2002)

    Article  MathSciNet  Google Scholar 

  3. Jiang, S., Huang, Z., Chandra, V., Kumar, R.: A polynomial algorithm for testing diagnosability of discrete event systems. IEEE Trans. on Auto. Cont. 46(8) (2001)

    Google Scholar 

  4. Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  5. Genc, S., Lafortune, S.: Predictability of event occurrences in partially-observed discrete-event systems. Automatica 45(2), 301–311 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  6. Genc, S., Lafortune, S.: Predictability in discrete-event systems under partial observation. In: IFAC Symp. on Fault Detection, Supervision and Safety of Technical Processes, Beijing, China. IEEE (2006)

    Google Scholar 

  7. Jéron, T., Marchand, H., Genc, S., Lafortune, S.: Predictability of sequence patterns in discrete event systems. In: IFAC WC, Seoul, Korea, pp. 537–543 (2008)

    Google Scholar 

  8. Brandán Briones, L., Madalinski, A.: Bounded predictability for faulty discrete event systems. In: 30th Int. Conf. of the Chilean Computer Science Society (2011)

    Google Scholar 

  9. Tripakis, S.: Fault diagnosis for timed automata. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 205–224. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  10. Bouyer, P., Chevalier, F., D’Souza, D.: Fault diagnosis using timed automata. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 219–233. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  11. Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. STTT 1(1-2), 134–152 (1997)

    Article  MATH  Google Scholar 

  12. Cassez, F., Grastien, A.: Predictability of Event Occurrences in Timed Systems. CoRR/abs arXiv:1306.0662 [cs.SY] (2013), http://arxiv.org/abs/1306.0662

  13. Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.: Minimum-cost reachability for priced timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 147–161. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  14. Courcoubetis, C., Yannakakis, M.: Minimum and maximum delay problems in real-time systems. Formal Methods in System Design 1(4), 385–415 (1992)

    Article  MATH  Google Scholar 

  15. De Wulf, M., Doyen, L., Raskin, J.-F.: Almost ASAP semantics: From timed models to timed implementations. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 296–310. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  16. Cassez, F., Henzinger, T.A., Raskin, J.-F.: A Comparison of Control Problems for Timed and Hybrid Systems. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 134–148. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  17. Cassez, F., Tripakis, S.: Fault diagnosis with static and dynamic diagnosers. Fundamenta Informaticae 88(4), 497–540 (2008)

    MathSciNet  MATH  Google Scholar 

  18. Cassez, F., Dubreil, J., Marchand, H.: Synthesis of opaque systems with static and dynamic masks. Formal Methods in System Design 40(1), 88–115 (2012)

    Article  MATH  Google Scholar 

  19. Cassez, F., Tripakis, S., Altisen, K.: Sensor minimization problems with static or dynamic observers for fault diagnosis. In: ACSD 2007, pp. 90–99. IEEE Comp. Soc. (2007)

    Google Scholar 

  20. Cassez, F., Dubreil, J., Marchand, H.: Dynamic observers for the synthesis of opaque systems. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 352–367. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  21. Cassez, F., Tripakis, S., Altisen, K.: Synthesis of optimal-cost dynamic observers for fault diagnosis of discrete-event systems. In: TASE 2007, pp. 316–325. IEEE Comp. Soc. (2007)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cassez, F., Grastien, A. (2013). Predictability of Event Occurrences in Timed Systems. In: Braberman, V., Fribourg, L. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2013. Lecture Notes in Computer Science, vol 8053. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40229-6_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-40229-6_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-40228-9

  • Online ISBN: 978-3-642-40229-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics