Skip to main content

A Weighted MSO Logic with Storage Behaviour and Its Büchi-Elgot-Trakhtenbrot Theorem

  • Conference paper
  • First Online:

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

Abstract

We introduce a weighted MSO-logic in which one outermost existential quantification over behaviours of a storage type is allowed. As weight structures we take unital valuation monoids which include all semirings, bounded lattices, and computations of average or discounted costs. Each formula is interpreted over finite words yielding elements in the weight structure. We prove that this logic is expressively equivalent to weighted automata with storage. In particular, this implies a Büchi-Elgot-Trakhtenbrot Theorem for weighted iterated pushdown languages. For this choice of storage type, the satisfiability problem of the logic is decidable for each bounded lattice provided that its infimum is computable.

L. Herrmann—Supported by DFG Graduiertenkolleg 1763 (QuantLA).

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

Buying options

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

Learn about institutional subscriptions

References

  1. Büchi, J.: Weak second-order arithmetic and finite automata. Zeitschr. für math. Logik und Grundl. der Mathem. 6, 66–92 (1960)

    Article  MATH  Google Scholar 

  2. Büchi, J.: On a decision method in restricted second-order arithmetic. In: Proceedings of 1960 International Congress for Logic, Methodology and Philosophy of Science, pp. 1–11. Stanford University Press, Stanford (1962)

    Google Scholar 

  3. Damm, W., Goerdt, A.: An automata-theoretical characterization of the OI-hierarchy. Inf. Control 71, 1–32 (1986)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  5. Droste, M., Gastin, P.: Weighted automata and weighted logics. In: Droste, M., Kuich, W., Vogler, H. (eds.) Handbook of Weighted Automata, Chap. 5. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  6. Droste, M., Meinecke, I.: Weighted automata and weighted MSO logics for average and long-time behaviors. Inf. Comput. 220–221, 44–59 (2012)

    Article  MathSciNet  Google Scholar 

  7. Droste, M., Stüber, T., Vogler, H.: Weighted finite automata over strong bimonoids. Inf. Sci. 180, 156–166 (2010)

    Article  MATH  Google Scholar 

  8. Droste, M., Vogler, H.: Weighted automata and multi-valued logics over arbitrary bounded lattices. Theoret. Comput. Sci. 418, 14–36 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  9. Droste, M., Vogler, H.: The Chomsky-Schützenberger theorem for quantitative context-free languages. Int. J. Found. Comput. Sci. 25(8), 955–969 (2014)

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  11. Engelfriet, J.: Iterated pushdown automata and complexity classes. In: Proceedings of 15th Annual ACM Symposium on Theory of Computing (STOCS), pp. 365–373 (1983)

    Google Scholar 

  12. Engelfriet, J.: Context-free grammars with storage. Technical Report 86–11, University of Leiden (1986). arxiv:1408.0683 [cs.FL] (2014)

  13. Engelfriet, J., Vogler, H.: Pushdown machines for the macro tree transducer. Theoret. Comput. Sci. 42(3), 251–368 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  14. Fratani, S., Voundy, E.: Context-free characterization of indexed languages. CoRR - Computing Research Repository arXiv:1409.6112 (2014)

  15. Fülöp, Z., Stüber, T., Vogler, H.: A Büchi-like theorem for weighted tree automata over multioperator monoids. Theory Comput. Syst. 50(2), 241–278 (2012). doi:10.1007/s00224-010-9296-1. Published online 28.10.2010

    Article  MathSciNet  MATH  Google Scholar 

  16. Fülöp, Z., Vogler, H.: Characterizations of recognizable weighted tree languages by logic and bimorphisms. Soft Comput. (2015). doi:10.1007/s00500-015-1717-2

    Google Scholar 

  17. Ginsburg, S.: Algebraic and Automata-theoretic Properties of Formal Languages. North-Holland Publishing, Amsterdam (1975)

    MATH  Google Scholar 

  18. Herrmann, L., Vogler, H.: A Chomsky-Schützenberger theorem for weighted automata with storage. In: Maletti, A. (ed.) CAI 2015. LNCS, vol. 9270, pp. 115–127. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  19. Kirsten, D.: The support of a recognizable series over a zero-sum free, commutative semiring is recognizable. Acta Cybern. 20(2), 211–221 (2011)

    MathSciNet  MATH  Google Scholar 

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

    Chapter  Google Scholar 

  21. Maslov, A.N.: Multilevel stack automata. Probl. Inf. Transm. 12, 38–43 (1976)

    Google Scholar 

  22. Mathissen, C.: Weighted logics for nested words and algebraic formal power series. Log. Meth. Comput. Sci. 5, 1–34 (2010)

    MathSciNet  Google Scholar 

  23. Scott, D.: Some definitional suggestions for automata theory. J. Comput. Syst. Sci. 1, 187–212 (1967)

    Article  MATH  Google Scholar 

  24. Trakhtenbrot, B.: Finite automata and logic of monadic predicates. Doklady Akademii Nauk SSSR 149, 326–329 (1961). in Russian

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Luisa Herrmann .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Vogler, H., Droste, M., Herrmann, L. (2016). A Weighted MSO Logic with Storage Behaviour and Its Büchi-Elgot-Trakhtenbrot Theorem. In: Dediu, AH., Janoušek, J., Martín-Vide, C., Truthe, B. (eds) Language and Automata Theory and Applications. LATA 2016. Lecture Notes in Computer Science(), vol 9618. Springer, Cham. https://doi.org/10.1007/978-3-319-30000-9_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-30000-9_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-29999-0

  • Online ISBN: 978-3-319-30000-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics