Document Open Access Logo

A Feferman-Vaught Decomposition Theorem for Weighted MSO Logic

Authors Manfred Droste, Erik Paul

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2018.76.pdf
  • Filesize: 463 kB
  • 15 pages

Document Identifiers

Author Details

Manfred Droste
  • Institute of Computer Science, Leipzig University, 04109 Leipzig, Germany
Erik Paul
  • Institute of Computer Science, Leipzig University, 04109 Leipzig, Germany

Funding

This work was supported by Deutsche Forschungsgemeinschaft (DFG), Graduiertenkolleg 1763 (QuantLA).

Cite AsGet BibTex

Manfred Droste and Erik Paul. A Feferman-Vaught Decomposition Theorem for Weighted MSO Logic. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 76:1-76:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.MFCS.2018.76

Abstract

We prove a weighted Feferman-Vaught decomposition theorem for disjoint unions and products of finite structures. The classical Feferman-Vaught Theorem describes how the evaluation of a first order sentence in a generalized product of relational structures can be reduced to the evaluation of sentences in the contributing structures and the index structure. The logic we employ for our weighted extension is based on the weighted MSO logic introduced by Droste and Gastin to obtain a Büchi-type result for weighted automata. We show that for disjoint unions and products of structures, the evaluation of formulas from two respective fragments of the logic can be reduced to the evaluation of formulas in the contributing structures. We also prove that the respective restrictions are necessary. Surprisingly, for the case of disjoint unions, the fragment is the same as the one used in the Büchi-type result of weighted automata. In fact, even the formulas used to show that the respective restrictions are necessary are the same in both cases. However, here proving that they do not allow for a Feferman-Vaught-like decomposition is more complex and employs Ramsey's Theorem. We also show how translation schemes can be applied to go beyond disjoint unions and products.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • Quantitative Logic
  • Quantitative Model Theory
  • Feferman-Vaught Theorem
  • Translation Scheme
  • Transduction

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Benedikt Bollig, Paul Gastin, and Benjamin Monmege. Weighted specifications over nested words. In Frank Pfenning, editor, Proc. FoSSaCS, volume 7794 of LNCS, pages 385-400. Springer, 2013. Google Scholar
  2. Bruno Courcelle. Monadic second-order definable graph transductions: a survey. Theor. Comput. Sci., 126(1):53-75, 1994. Google Scholar
  3. Manfred Droste and Paul Gastin. Weighted automata and weighted logics. Theor. Comput. Sci., 380(1-2):69-86, 2007. Google Scholar
  4. Manfred Droste and George Rahonis. Weighted automata and weighted logics with discounting. Theor. Comput. Sci., 410(37):3481-3494, 2009. URL: http://dx.doi.org/10.1016/j.tcs.2009.03.029.
  5. Andrzej Ehrenfeucht. An application of games to the completeness problem for formalized theories. Fund. Math., 49(2):129-141, 1961. Google Scholar
  6. Solomon Feferman and Robert L. Vaught. The first order properties of products of algebraic systems. Fund. Math., 47:57-103, 1959. Google Scholar
  7. Siegfried Gottwald. A Treatise on Many-Valued Logics, volume 9 of Studies in Logic and Computation. Research Studies Press, 2001. Google Scholar
  8. Yuri Gurevich. Modest theory of short chains. I. J. Symbolic Logic, 44(4):481-490, 12 1979. Google Scholar
  9. Yuri Gurevich. Chapter XIII: Monadic second-order theories. In Jon Barwise and Solomon Feferman, editors, Model-Theoretic Logics, volume 8 of Perspect. Math. Logic, pages 479-506. Springer, 1985. Google Scholar
  10. Petr Hájek. Metamathematics of Fuzzy Logic, volume 4 of Trends in Logic. Kluwer, 1998. Google Scholar
  11. Hendrik Jan Hoogeboom and Paulien ten Pas. Monadic second-order definable text languages. Theory Comput. Syst., 30(4):335-354, 1997. URL: http://dx.doi.org/10.1007/s002240000055.
  12. Hans Läuchli and John Leonard. On the elementary theory of linear order. Fund. Math., 59(1):109-116, 1966. Google Scholar
  13. Johann A. Makowsky. Algorithmic uses of the Feferman–Vaught theorem. Ann. Pure Appl. Logic, 126(1):159-213, 2004. Google Scholar
  14. Christian Mathissen. Definable transductions and weighted logics for texts. In Tero Harju, Juhani Karhumäki, and Arto Lepistö, editors, Proc. DLT, pages 324-336. Springer, 2007. Google Scholar
  15. Christian Mathissen. Weighted logics for nested words and algebraic formal power series. In Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz, editors, Proc. ICALP, volume 5126 of LNCS, pages 221-232. Springer, 2008. Google Scholar
  16. Christian Mathissen. Weighted Automata and Weighted Logics over Tree-like Structures. PhD thesis, Leipzig University, Germany, 2009. URL: http://www.dr.hut-verlag.de/978-3-86853-180-0.html.
  17. Andrzej Mostowski. On direct products of theories. J. Symbolic Logic, 17(1):1-31, 1952. Google Scholar
  18. Frank P. Ramsey. On a problem of formal logic. Proc. London Math. Soc., 30(1):264-286, 1930. Google Scholar
  19. Elena V. Ravve, Zeev Volkovich, and Gerhard-Wilhelm Weber. Effective optimization with weighted automata on decomposable trees. Optimization, 63(1):109-127, 2014. Google Scholar
  20. Marcel-Paul Schützenberger. On the definition of a family of automata. Inform. Control, 4(2–3):245-270, 1961. Google Scholar
  21. Saharon Shelah. The monadic theory of order. Ann. Math., 102(3):379-419, 1975. Google Scholar
  22. Alan S. Stern, Jan Mycielski, and Pavel Pudlák. A Lattice of Chapters of Mathematics: Interpretations between Theorems, volume 426 of Mem. Amer. Math. Soc. American Math. Soc., 1990. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact