2026-09-27T09:07:12Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9658 2026-09-23T05:18:20Z ddc:004 open_access

A Feferman-Vaught Decomposition Theorem for Weighted MSO Logic Droste, Manfred Paul, Erik Quantitative Logic Quantitative Model Theory Feferman-Vaught Theorem Translation Scheme Transduction 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Manfred Droste and Erik Paul 2018 Is Part Of LIPIcs, Volume 117, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2018.76 urn:nbn:de:0030-drops-96581 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2018.76 eng https://creativecommons.org/licenses/by/3.0/legalcode