Document Open Access Logo

Nivat-Theorem and Logic for Weighted Pushdown Automata on Infinite Words

Authors Manfred Droste , Sven Dziadek , Werner Kuich

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2020.44.pdf
  • Filesize: 0.53 MB
  • 14 pages

Document Identifiers

Author Details

Manfred Droste
  • Institut für Informatik, Universität Leipzig, Germany
Sven Dziadek
  • Institut für Informatik, Universität Leipzig, Germany
Werner Kuich
  • Institut für Diskrete Mathematik und Geometrie, Technische Unversität Wien, Austria

Funding

  • Dziadek, Sven: supported by DFG Research Training Group 1763 (QuantLA).
  • Kuich, Werner: partially supported by Austrian Science Fund (FWF): grant no. I1661 N25.

Cite As Get BibTex

Manfred Droste, Sven Dziadek, and Werner 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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 44:1-44:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.FSTTCS.2020.44

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Quantitative automata
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Grammars and context-free languages
Keywords
  • Weighted automata
  • Pushdown automata
  • Infinite words
  • Weighted logic

Metrics

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

References

  1. R. Alur and P. Madhusudan. Visibly pushdown languages. In ACM Symposium on Theory of Computing (STOC 2004), pages 202-211, 2004. URL: https://doi.org/10.1145/1007352.1007390.
  2. P. Babari and M. Droste. A Nivat theorem for weighted picture automata and weighted MSO logics. J. Comput. Syst. Sci., 104:41-57, 2019. URL: https://doi.org/10.1016/j.jcss.2017.02.009.
  3. C. Baier and J.-P. Katoen. Principles of Model Checking. The MIT Press, 2008. Google Scholar
  4. A. Blass and Y. Gurevich. A note on nested words. Microsoft Research, 2006. URL: https://www.microsoft.com/en-us/research/publication/180-a-note-on-nested-words/.
  5. J. R. Büchi. Weak second-order arithmetic and finite automata. Mathematical Logic Quarterly, 6:66-92, 1960. URL: https://doi.org/10.1002/malq.19600060105.
  6. J. R. Büchi. Symposium on decision problems: On a decision method in restricted second order arithmetic. In Logic, Methodology and Philosophy of Science, volume 44 of Studies in Logic and the Foundations of Mathematics, pages 1-11. Elsevier, 1966. URL: https://doi.org/10.1016/S0049-237X(09)70564-6.
  7. K. Chatterjee, L. Doyen, and T. A. Henzinger. Quantitative languages. In Computer Science Logic (CSL 2008), pages 385-400. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-87531-4_28.
  8. N. Chomsky and M. P. Schützenberger. The algebraic theory of context-free languages. In Studies in Logic and the Foundations of Mathematics, volume 35: Computer Programming and Formal Systems, pages 118-161. Elsevier, 1963. URL: https://doi.org/10.1016/S0049-237X(08)72023-8.
  9. E. M Clarke, T. A Henzinger, H. Veith, and R. P. Bloem. Handbook of Model Checking. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-10575-8.
  10. R. S. Cohen and A. Y. Gold. Theory of ω-languages I: Characterizations of ω-context-free languages. Journal of Computer and System Sciences, 15(2):169-184, 1977. URL: https://doi.org/10.1016/S0022-0000(77)80004-4.
  11. M. Droste and S. Dück. Weighted automata and logics for infinite nested words. Information and Computation, 253:448-466, 2017. URL: https://doi.org/10.1016/j.ic.2016.06.010.
  12. M. Droste, S. Dziadek, and W. Kuich. Greibach normal form for ω-algebraic systems and weighted simple ω-pushdown automata. In Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019), volume 150 of LIPIcs, pages 38:1-38:14, 2019. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2019.38.
  13. M. Droste, S. Dziadek, and W. Kuich. Weighted simple reset pushdown automata. Theoretical Computer Science, 777:252-259, 2019. URL: https://doi.org/10.1016/j.tcs.2019.01.016.
  14. M. Droste, S. Dziadek, and W. Kuich. Greibach normal form for ω-algebraic systems and weighted simple ω-pushdown automata, 2020. Submitted. URL: http://arxiv.org/abs/2007.08866.
  15. M. Droste, S. Dziadek, and W. Kuich. Logic for ω-pushdown automata. Information and Computation, 2020. Special issue on "Weighted Automata", Accepted for publication. Google Scholar
  16. M. Droste, Z. Ésik, and W. Kuich. The triple-pair construction for weighted ω-pushdown automata. In Conference on Automata and Formal Languages (AFL 2017), volume 252 of Electronic Proceedings in Theoretical Computer Science, pages 101-113, 2017. URL: https://doi.org/10.4204/EPTCS.252.12.
  17. M. Droste and P. Gastin. Weighted automata and weighted logics. Theoretical Computer Science, 380(1-2):69-86, 2007. URL: https://doi.org/10.1016/j.tcs.2007.02.055.
  18. M. Droste and P. Gastin. Weighted automata and weighted logics. In M. Droste, W. Kuich, and H. Vogler, editors, Handbook of Weighted Automata, EATCS Monographs in Theoretical Computer Science, chapter 5, pages 175-211. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-01492-5_5.
  19. M. Droste and W. Kuich. A Kleene theorem for weighted ω-pushdown automata. Acta Cybernetica, 23:43-59, 2017. URL: https://doi.org/10.14232/actacyb.23.1.2017.4.
  20. M. Droste, W. Kuich, and H. Vogler, editors. Handbook of Weighted Automata. EATCS Monographs in Theoretical Computer Science. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-01492-5.
  21. M. Droste and D. Kuske. Weighted automata. In J.-E. Pin, editor, Handbook of Automata Theory, chapter 4. European Mathematical Society, to appear. Google Scholar
  22. M. Droste and I. Meinecke. Weighted automata and weighted MSO logics for average and long-time behaviors. Information and Computation, 220:44-59, 2012. URL: https://doi.org/10.1016/j.ic.2012.10.001.
  23. M. Droste and V. Perevoshchikov. A logical characterization of timed pushdown languages. In Computer Science Symposium in Russia (CSR 2015), volume 9139 of LNCS, pages 189-203. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-20297-6_13.
  24. M. Droste and V. Perevoshchikov. Logics for weighted timed pushdown automata. In Fields of Logic and Computation II, pages 153-173. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-23534-9_9.
  25. M. Droste and G. Rahonis. Weighted automata and weighted logics on infinite words. In Developments in Language Theory (DLT 2006), volume 54, pages 49-58. Springer, 2006. URL: https://doi.org/10.1007/11779148_6.
  26. C. C. Elgot. Decision problems of finite automata design and related arithmetics. Transactions of the American Mathematical Society, 98:21-51, 1961. URL: https://doi.org/10.2307/2270940.
  27. Z. Ésik and W. Kuich. A semiring-semimodule generalization of ω-context-free languages. In Theory Is Forever, volume 3113 of LNCS, pages 68-80. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-27812-2_7.
  28. D. Krob. Monoides et semi-anneaux complets. Semigroup Forum, 36:323-339, 1987. URL: https://doi.org/10.1007/BF02575025.
  29. C. Lautemann, T. Schwentick, and D. Thérien. Logics for context-free languages. In Computer Science Logic (CSL 1994), volume 933 of LNCS, pages 205-216. Springer, 1994. URL: https://doi.org/10.1007/BFb0022257.
  30. K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993. URL: https://doi.org/10.1007/978-1-4615-3190-6.
  31. M. Nivat. Transductions des langages de Chomsky. Annales de l'Institut Fourier, 18(1):339-455, 1968. URL: https://doi.org/10.5802/aif.287.
  32. W. Thomas. Automata on infinite objects. In Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 4, pages 133-191. Elsevier, 1990. URL: https://doi.org/10.1016/B978-0-444-88074-1.50009-3.
  33. B. A. Trakhtenbrot. Finite automata and the logic of single-place predicates. Doklady Akademii Nauk, 140(2):326-329, 1961. In Russian. URL: http://mi.mathnet.ru/dan25511.
  34. H. Vogler, M. Droste, and L. Herrmann. A weighted MSO logic with storage behaviour and its Büchi-Elgot-Trakhtenbrot theorem. In Language and Automata Theory and Applications (LATA 2016), volume 9618 of LNCS, pages 127-139. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-30000-9_10.
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 About DROPS Imprint Privacy Contact