Advertisement

Frequencies in Forgetful Timed Automata

  • Amélie Stainer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7595)

Abstract

A quantitative semantics for infinite timed words in timed automata based on the frequency of a run is introduced in [6]. Unfortunately, most of the results are obtained only for one-clock timed automata because the techniques do not allow to deal with some phenomenon of convergence between clocks. On the other hand, the notion of forgetful cycle is introduced in [4], in the context of entropy of timed languages, and seems to detect exactly these convergences. In this paper, we investigate how the notion of forgetfulness can help to extend the computation of the set of frequencies to n-clock timed automata.

Keywords

Model Check Simple Cycle Time Automaton Single Clock Orbit Graph 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  2. 2.
    Alur, R., La Torre, S., Pappas, G.J.: Optimal Paths in Weighted Timed Automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 49–62. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  3. 3.
    Baier, C., Bertrand, N., Bouyer, P., Brihaye, Th., Größer, M.: Almost-sure model checking of infinite paths in one-clock timed automata. In: Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science (LICS 2008), pp. 217–226. IEEE (2008)Google Scholar
  4. 4.
    Basset, N., Asarin, E.: Thin and Thick Timed Regular Languages. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 113–128. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  5. 5.
    Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.M.T., Vaandrager, F.W.: 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)CrossRefGoogle Scholar
  6. 6.
    Bertrand, N., Bouyer, P., Brihaye, T., Stainer, A.: Emptiness and Universality Problems in Timed Automata with Positive Frequency. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 246–257. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  7. 7.
    Bouyer, P., Brinksma, E., Larsen, K.G.: Optimal infinite scheduling for multi-priced timed automata. Formal Methods in System Design 32(1), 3–23 (2008)zbMATHCrossRefGoogle Scholar
  8. 8.
    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)CrossRefGoogle Scholar
  9. 9.
    Kwiatkowska, M.Z., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science 282, 101–150 (2002)MathSciNetzbMATHCrossRefGoogle Scholar
  10. 10.
    Laroussinie, F., Markey, N., Schnoebelen, P.: Model Checking Timed Automata with One or Two Clocks. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 387–401. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  11. 11.
    Ouaknine, J., Worrell, J.: On the language inclusion problem for timed automata: Closing a decidability gap. In: Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004), pp. 54–63. IEEE (2004)Google Scholar
  12. 12.
    Puri, A.: Dynamical properties of timed automata. Discrete Event Dynamic Systems 10(1-2), 87–113 (2000)MathSciNetzbMATHCrossRefGoogle Scholar
  13. 13.
    Stainer, A.: Frequencies in forgetful timed automata. Research Report 8009, INRIA, Rennes, France (July 2012), http://hal.inria.fr/hal-00714262

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Amélie Stainer
    • 1
  1. 1.University of Rennes 1RennesFrance

Personalised recommendations