Skip to main content
SpringerLink
Log in

On the Supports of Recognizable Timed Series

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

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

  • 434 Accesses

Abstract

Recently, the model of weighted timed automata has gained interest within the real-time community. In a previous work, we built a bridge to the theory of weighted automata and introduced a general model of weighted timed automata defined over a semiring and a family of cost functions. In this model, a weighted timed automaton recognizes a timed series, i.e., a function mapping to each timed word a weight taken from the semiring. Continuing in this spirit, the aim of this paper is to investigate the support and cut languages of recognizable timed series. We present results that lead to the decidability of weighted versions of classical decidability problems as e.g. the emptiness problem. Our results may also be used to check whether weighted timed systems satisfy specifications restricting the consumption of a resource.

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

Access this chapter

Log in via an institution
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 54.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. Abdeddaïm, Y., Maler, O.: Preemptive job-shop scheduling using stopwatch automata. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 113–126. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  3. 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)

    Chapter  Google Scholar 

  4. Alur, R., Madhusudan, P.: Decision problems for timed automata: A survey. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 1–24. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  5. Behrmann, G., Fehnker, A.: Efficient guiding towards cost-optimality in Uppaal. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 174–188. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  6. Behrmann, G., Fehnker, A., Hune, T., Larsen, K., 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 

  7. Berstel, J., Reutenauer, C.: Rational series and their languages. Current online version of the book of the same name from 1988 (February 2007)

    Google Scholar 

  8. Bouyer, P.: Weighted timed automata: Model-checking and games. In: MFPS 2006. ENTCS, vol. 158, pp. 3–17. Elsevier Science Publishers, Amsterdam (2006)

    Google Scholar 

  9. Bouyer, P., Brihaye, T., Bruyère, V., Raskin, J.-F.: On the optimal reachability problem on weighted timed automata. Formal Methods in System Design 31(2), 135–175 (2007)

    Article  MATH  Google Scholar 

  10. Bouyer, P., Brihaye, T., Markey, N.: Improved undecidability results on weighted timed automata. Inf. Process. Lett. 98(5), 188–194 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  11. 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)

    Article  MATH  Google Scholar 

  12. Bouyer, P., Markey, N.: Costs are expensive! In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 53–68. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  13. Brihaye, T., Bruyère, V., Raskin, J.-F.: On optimal timed strategies. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 49–64. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  14. Brihaye, T., Bruyère, V., Raskin, J.-F.: On model-checking timed automata with stopwatch observers. Inf. Comput. 204(3), 408–433 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  15. Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 385–400. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  16. Droste, M., Quaas, K.: A Kleene-Schützenberger Theorem for Weighted Timed Automata. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 142–156. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  17. Fichtner, I.: Characterizations of Recognizable Picture Series. PhD thesis, Universität Leipzig, Institut für Informatik, Abteilung Automaten und Sprachen (2006)

    Google Scholar 

  18. Kirsten, D.: The support of a recognizable series over a zero-sum free, commutative semiring is recognizable. In: DLT 2009. LNCS, vol. 5583, pp. 326–333. Springer, Heidelberg (2009)

    Google Scholar 

  19. Larsen, K.G., Rasmussen, J.I.: Optimal reachability for multi-priced timed automata. Theor. Comput. Sci. 390(2-3), 197–213 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  20. Ouaknine, J., Worrell, J.: On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap. In: LICS, pp. 54–63. IEEE Computer Society Press, Los Alamitos (2004)

    Google Scholar 

  21. Quaas, K.: Weighted Timed MSO Logics. In: DLT 2009. LNCS, vol. 5583, pp. 419–430. Springer, Heidelberg (2009)

    Google Scholar 

  22. Rahonis, G.: Fuzzy languages. In: Droste, Kuich, Vogler (eds.) Handbook of Weighted Automata. Springer, Heidelberg (to appear, 2009)

    Google Scholar 

  23. Sakarovitch, J.: Rational and recognisable power series. In: Droste, Kuich, Vogler (eds.) Handbook of Weighted Automata. Springer, Heidelberg (To appear, 2009)

    Google Scholar 

  24. Salomaa, A., Soittola, M.: Automata-Theoretic Aspects of Formal Power Series. Springer, New York (1978)

    Book  MATH  Google Scholar 

  25. Wilke, T.: Automaten und Logiken zur Beschreibung zeitabhängiger Systeme. PhD thesis, Christian-Albrecht-Universität Kiel (1994)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Universität Leipzig, 04009, Leipzig, Germany

    Karin Quaas

Authors
  1. Karin Quaas
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computing Laboratory, Oxford University, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK

    Joël Ouaknine

  2. Institute for Computing and Information Sciences , Radboud University Nijmegen , P.O. Box 9010, 6500, Nijmegen, GL, The Netherlands

    Frits W. Vaandrager

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Quaas, K. (2009). On the Supports of Recognizable Timed Series. In: Ouaknine, J., Vaandrager, F.W. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2009. Lecture Notes in Computer Science, vol 5813. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04368-0_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-04368-0_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-04367-3

  • Online ISBN: 978-3-642-04368-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation