2026-07-25T11:48:35Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13285 2024-03-12T11:59:40Z ddc:004 open_access

Nivat-Theorem and Logic for Weighted Pushdown Automata on Infinite Words Droste, Manfred Dziadek, Sven Kuich, Werner Weighted automata Pushdown automata Infinite words Weighted logic Recently, weighted ω-pushdown automata have been introduced by Droste, Ésik, Kuich. This new type of automaton has access to a stack and models quantitative aspects of infinite words. Here, we consider a simple version of those automata. The simple ω-pushdown automata do not use ε-transitions and have a very restricted stack access. In previous work, we could show this automaton model to be expressively equivalent to context-free ω-languages in the unweighted case. Furthermore, semiring-weighted simple ω-pushdown automata recognize all ω-algebraic series. Here, we consider ω-valuation monoids as weight structures. As a first result, we prove that for this weight structure and for simple ω-pushdown automata, Büchi-acceptance and Muller-acceptance are expressively equivalent. In our second result, we derive a Nivat theorem for these automata stating that the behaviors of weighted ω-pushdown automata are precisely the projections of very simple ω-series restricted to ω-context-free languages. The third result is a weighted logic with the same expressive power as the new automaton model. To prove the equivalence, we use a similar result for weighted nested ω-word automata and apply our present result of expressive equivalence of Muller and Büchi acceptance. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Manfred Droste and Sven Dziadek and Werner Kuich 2020 Is Part Of LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2020.44 urn:nbn:de:0030-drops-132850 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.44 eng https://creativecommons.org/licenses/by/3.0/legalcode