Skip to main content
SpringerLink
Log in

Weighted Timed MSO Logics

  • Conference paper
Developments in Language Theory (DLT 2009)

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

Included in the following conference series:

Abstract

We aim to generalize Büchi’s fundamental theorem on the coincidence of recognizable and MSO-definable languages to a weighted timed setting. For this, we investigate subclasses of weighted timed automata and show how we can extend existing timed MSO logics with weights. Here, we focus on the class of weighted event-recording automata and define a weighted extension of the full logic MSO\(_{\rm er}{(\it \Sigma)}\) introduced by D’Souza. We show that every weighted event-recording automaton can effectively be transformed into a corresponding sentence of our logic and vice versa. The methods presented in the paper can be adopted to weighted versions of timed automata and Wilke’s logic of relative distance. The results indicate the robustness of weighted timed automata models and may be used for specification purposes.

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. Alur, R., Fix, L., Henzinger, T.A.: Event-clock automata: A determinizable class of timed automata. Theor. Comput. Sci. 211(1-2), 253–273 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  2. Alur, R., La Torre, S., Pappas, G.J.: Optimal paths in weighted timed automata. Theoretical Computer Science 318, 297–322 (2004)

    Article  MathSciNet  MATH  Google Scholar 

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

  4. 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 

  5. 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 

  6. Büchi, J.R.: On a decision method in restricted second order arithmetics. In: Nagel, E., et al. (eds.) Proc. Intern. Congress on Logic, Methodology and Philosophy of Sciences, pp. 1–11. Stanford University Press, Stanford (1960)

    Google Scholar 

  7. Dima, C.: Kleene theorems for event-clock automata. In: Ciobanu, G., Păun, G. (eds.) FCT 1999. LNCS, vol. 1684, pp. 215–225. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  8. Droste, M., Gastin, P.: Weighted automata and weighted logics. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 513–525. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  9. Droste, M., Gastin, P.: Weighted automata and weighted logics. Theor. Comput. Sci. 380(1-2), 69–86 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  10. Droste, M., Gastin, P.: Weighted automata and weighted logics. In: Droste, M., Kuich, W., Vogler, H. (eds.) Handbook of Weighted Automata, pp. 173–206. Springer, Heidelberg (to appear, 2009)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  12. Droste, M., Rahonis, G.: Weighted automata and weighted logics on infinite words. In: H. Ibarra, O., Dang, Z. (eds.) DLT 2006. LNCS, vol. 4036, pp. 49–58. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  13. Droste, M., Vogler, H.: Weighted tree automata and weighted logics. Theor. Comput. Sci. 366(3), 228–247 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  14. D’Souza, D.: A logical characterisation of event recording automata. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, pp. 240–251. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  15. Elgot, C.C.: Decision problems of finite automata design and related arithmetics. Trans. Am. Math. Soc. 98, 21–51 (1961)

    Article  MathSciNet  MATH  Google Scholar 

  16. Grinchtein, O., Jonsson, B., Pettersson, P.: Inference of event-recording automata using timed decision trees. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 435–449. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  17. Henzinger, T.A., Raskin, J.-F., Schobbens, P.-Y.: The regular real-time languages. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 580–591. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  18. Mathissen, C.: Definable transductions and weighted logics for texts. In: Harju, T., Karhumäki, J., Lepistö, A. (eds.) DLT 2007. LNCS, vol. 4588, pp. 324–336. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  19. Mathissen, C.: Weighted logics for nested words and algebraic formal power series. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 221–232. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  20. Mäurer, I.: Weighted picture automata and weighted logics. In: Durand, B., Thomas, W. (eds.) STACS 2006. LNCS, vol. 3884, pp. 313–324. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  21. Meinecke, I.: Weighted logics for traces. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol. 3967, pp. 235–246. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  22. Quaas, K.: A Kleene-Schützenberger-Theorem for Weighted Event-Clock-Automata (2008), http://www.informatik.uni-leipzig.de/~quaas/weca_ks.pdf

  23. Quaas, K.: A logical characterization for weighted event-recording automata (2009), http://www.informatik.uni-leipzig.de/~quaas/wera_logic.pdf

  24. Quaas, K.: A logical characterization for weighted timed automata (2009), http://www.informatik.uni-leipzig.de/~quaas/wta_logic.pdf

  25. Raskin, J.-F., Schobbens, P.-Y.: State clock logic: A decidable real-time logic. In: Maler, O. (ed.) HART 1997. LNCS, vol. 1201, pp. 33–47. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  26. Thomas, W.: Languages, automata and logic. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, pp. 389–485. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  27. Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Formal Models and Sematics (B), vol. B, pp. 133–192. Elsevier, Amsterdam (1990)

    Google Scholar 

  28. Wilke, T.: Specifying Timed State Sequences in Powerful Decidable Logics and Timed Automata. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 694–715. Springer, Heidelberg (1994)

    Chapter  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. Institut für Formale Methoden der Informatik, FMI, Universität Stuttgart, Universitätsstrasse 38, 70569, Stuttgart, Germany

    Volker Diekert  & Dirk Nowotka  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Quaas, K. (2009). Weighted Timed MSO Logics. In: Diekert, V., Nowotka, D. (eds) Developments in Language Theory. DLT 2009. Lecture Notes in Computer Science, vol 5583. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02737-6_34

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02737-6_34

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation