[Zurück]

M. Droste, S. Dziadek, W. Kuich:
"Nivat-Theorem and Logic for Weighted Pushdown Automata on Infinite Words";
in: "40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)", 182; herausgegeben von: Schloss Dagstuhl - Leibniz Zentrum für Informatik; Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Deutschland, 2020, ISBN: 978-3-95977-174-0, S. 44:1 - 44:14.

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.

Weighted automata, Pushdown automata, Infinite words, Weighted Automata

http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2020.44