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 to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Büchi, J.: Weak second-order arithmetic and finite automata. Zeitschr. für math. Logik und Grundl. der Mathem. 6, 66–92 (1960)
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)
Damm, W., Goerdt, A.: An automata-theoretical characterization of the OI-hierarchy. Inf. Control 71, 1–32 (1986)
Droste, M., Gastin, P.: Weighted automata and weighted logics. Theoret. Comput. Sci. 380(1–2), 69–86 (2007)
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)
Droste, M., Meinecke, I.: Weighted automata and weighted MSO logics for average and long-time behaviors. Inf. Comput. 220–221, 44–59 (2012)
Droste, M., Stüber, T., Vogler, H.: Weighted finite automata over strong bimonoids. Inf. Sci. 180, 156–166 (2010)
Droste, M., Vogler, H.: Weighted automata and multi-valued logics over arbitrary bounded lattices. Theoret. Comput. Sci. 418, 14–36 (2012)
Droste, M., Vogler, H.: The Chomsky-Schützenberger theorem for quantitative context-free languages. Int. J. Found. Comput. Sci. 25(8), 955–969 (2014)
Elgot, C.: Decision problems of finite automata design and related arithmetics. Trans. Am. Math. Soc. 98, 21–52 (1961)
Engelfriet, J.: Iterated pushdown automata and complexity classes. In: Proceedings of 15th Annual ACM Symposium on Theory of Computing (STOCS), pp. 365–373 (1983)
Engelfriet, J.: Context-free grammars with storage. Technical Report 86–11, University of Leiden (1986). arxiv:1408.0683 [cs.FL] (2014)
Engelfriet, J., Vogler, H.: Pushdown machines for the macro tree transducer. Theoret. Comput. Sci. 42(3), 251–368 (1986)
Fratani, S., Voundy, E.: Context-free characterization of indexed languages. CoRR - Computing Research Repository arXiv:1409.6112 (2014)
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
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
Ginsburg, S.: Algebraic and Automata-theoretic Properties of Formal Languages. North-Holland Publishing, Amsterdam (1975)
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)
Kirsten, D.: The support of a recognizable series over a zero-sum free, commutative semiring is recognizable. Acta Cybern. 20(2), 211–221 (2011)
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)
Maslov, A.N.: Multilevel stack automata. Probl. Inf. Transm. 12, 38–43 (1976)
Mathissen, C.: Weighted logics for nested words and algebraic formal power series. Log. Meth. Comput. Sci. 5, 1–34 (2010)
Scott, D.: Some definitional suggestions for automata theory. J. Comput. Syst. Sci. 1, 187–212 (1967)
Trakhtenbrot, B.: Finite automata and logic of monadic predicates. Doklady Akademii Nauk SSSR 149, 326–329 (1961). in Russian
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights 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)