Skip to main content
SpringerLink
Log in

A Logical Characterization of Timed Pushdown Languages

  • Conference paper
  • First Online:
Book cover Computer Science -- Theory and Applications (CSR 2015)

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

Included in the following conference series:

Abstract

Dense-timed pushdown automata with a timed stack were introduced by Abdulla et al. in LICS 2012 to model the behavior of real-time recursive systems. In this paper, we introduce a quantitative logic on timed words which is expressively equivalent to timed pushdown automata. This logic is an extension of Wilke’s relative distance logic by quantitative matchings. To show the expressive equivalence result, we prove a decomposition theorem which establishes a connection between timed pushdown languages and visibly pushdown languages of Alur and Mudhusudan; then we apply their result about the logical characterization of visibly pushdown languages. As a consequence, we obtain the decidability of the satisfiability problem for our new logic.

M. Droste— Part of this work was done while the author was visiting Immanuel Kant Baltic Federal University, Kaliningrad, Russia.

V. Perevoshchikov— Supported by DFG Graduiertenkolleg 1763 (QuantLA).

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 EPUB and 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

References

  1. Abdulla, P.A., Atig, M.F., Stenman, J.: Dense-timed pushdown automata. In: LICS 2012, pp. 35–44. IEEE Computer Society (2012)

    Google Scholar 

  2. Abdulla, P.A., Atig, M.F., Stenman, J.: Computing optimal reachability costs in priced dense-timed pushdown automata. In: Dediu, A.-H., Martín-Vide, C., Sierra-Rodríguez, J.-L., Truthe, B. (eds.) LATA 2014. LNCS, vol. 8370, pp. 62–75. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  3. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  4. Alur, R., Madhusudan, P.: Visibly pushdown languages. In: STOC 2004, pp. 202–211. ACM (2004)

    Google Scholar 

  5. Berstel, J.: Transductions and Context-Free Languages. Teubner Studienbücher Informatik. Teubner, Stuttgart (1979)

    Book  MATH  Google Scholar 

  6. Bouajjani, A., Echahed, R., Robbana, R.: On the automatic verification of systems with continuous variables and unbounded discrete data structures. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol. 999. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  7. Büchi, J.R.: Weak second order arithmetic and finite automata. Zeitschrift für Mathematische Logik und Grundlagen der Informatik 6, 66–92 (1960)

    Article  MATH  Google Scholar 

  8. Dang, Z.: Pushdown timed automata: a binary reachability characterization and safety verification. Theor. Comput. Sci. 302, 93–121 (2003)

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  10. Droste, M., Perevoshchikov, V.: A Nivat theorem for weighted timed automata and weighted relative distance logic. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014, Part II. LNCS, vol. 8573, pp. 171–182. Springer, Heidelberg (2014)

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  12. Emmi, M., Majumdar, R.: Decision problems for the verification of real-time software. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 200–211. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  13. Lautemann, C., Schwentick, T., Therien, D.: Logics for context-free languages. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

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

  15. Nivat, M.: Transductions des langages de Chomsky. Ann. de l’Inst. Fourier 18, 339–456 (1968)

    Article  MATH  MathSciNet  Google Scholar 

  16. Quaas, K.: MSO logics for weighted timed automata. Formal Methods Syst. Des. 38(3), 193–222 (2011)

    Article  MATH  MathSciNet  Google Scholar 

  17. Thatcher, J.W., Wright, J.B.: Generalized finite automata theory with an application to a decision problem of second-order logic. Math. Syst. Theory 2, 57–81 (1968)

    Article  MathSciNet  Google Scholar 

  18. 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. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Manfred Droste & Vitaly Perevoshchikov

Authors
  1. Manfred Droste
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Vitaly Perevoshchikov
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Vitaly Perevoshchikov .

Editor information

Editors and Affiliations

  1. Steklov Mathematical Institute of Russian Academy of Sciences, Lomonosov Moscow State University and National Research University Higher School of Economics, Moscow, Russia

    Lev D. Beklemishev

  2. Moscow Institute of Physics and Technology, Moscow, Russia and Kazan (Volga Region) Federal University, Kazan, Kabardino-Balkar.Rep, Russia

    Daniil V. Musatov

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Droste, M., Perevoshchikov, V. (2015). A Logical Characterization of Timed Pushdown Languages. In: Beklemishev, L., Musatov, D. (eds) Computer Science -- Theory and Applications. CSR 2015. Lecture Notes in Computer Science(), vol 9139. Springer, Cham. https://doi.org/10.1007/978-3-319-20297-6_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-20297-6_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-20296-9

  • Online ISBN: 978-3-319-20297-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation