Document Open Access Logo

Weighted One-Deterministic-Counter Automata

Authors Prince Mathew , Vincent Penelle, Prakash Saivasan, A.V. Sreejith

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2023.39.pdf
  • Filesize: 0.99 MB
  • 23 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata extensions
Keywords
  • One-counter automata
  • Equivalence
  • Weighted automata
  • Reachability

Metrics

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

Abstract

We introduce weighted one-deterministic-counter automata (odca). These are weighted one-counter automata (oca) with the property of counter-determinacy, meaning that all paths labelled by a given word starting from the initial configuration have the same counter-effect. Weighted odcas are a strict extension of weighted visibly ocas, which are weighted ocas where the input alphabet determines the actions on the counter. 
We present a novel problem called the co-VS (complement to a vector space) reachability problem for weighted odcas over fields, which seeks to determine if there exists a run from a given configuration of a weighted odca to another configuration whose weight vector lies outside a given vector space. We establish two significant properties of witnesses for co-VS reachability: they satisfy a pseudo-pumping lemma, and the lexicographically minimal witness has a special form. It follows that the co-VS reachability problem is in 𝖯.
These reachability problems help us to show that the equivalence problem of weighted odcas over fields is in 𝖯 by adapting the equivalence proof of deterministic real-time ocas [Stanislav Böhm and Stefan Göller, 2011] by Böhm et al. This is a step towards resolving the open question of the equivalence problem of weighted ocas. Finally, we demonstrate that the regularity problem, the problem of checking whether an input weighted odca over a field is equivalent to some weighted automaton, is in 𝖯. We also consider boolean odcas and show that the equivalence problem for (non-deterministic) boolean odcas is in PSPACE, whereas it is undecidable for (non-deterministic) boolean ocas.

Cite As Get BibTex

Prince Mathew, Vincent Penelle, Prakash Saivasan, and A.V. Sreejith. Weighted One-Deterministic-Counter Automata. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 39:1-39:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.FSTTCS.2023.39

Author Details

Prince Mathew
  • Indian Institute of Technology Goa, India
Vincent Penelle
  • Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, F-33400, Talence, France
Prakash Saivasan
  • The Institute of Mathematical Sciences, HBNI, India
  • CNRS UMI ReLaX, India
A.V. Sreejith
  • Indian Institute of Technology Goa, India

Funding

  • Sreejith, A.V.: supported by SERB for the project "Probabilistic Pushdown Automata" [MTR/2021/000788].

Acknowledgements

The authors would like to thank Rahul C S for his intuitive suggestions that helped in proving Lemma 14.

References

  1. Steven P. Abney, David A. McAllester, and Fernando Pereira. Relating probabilistic grammars and automata. In Robert Dale and Kenneth Ward Church, editors, 27th Annual Meeting of the Association for Computational Linguistics, University of Maryland, College Park, Maryland, USA, 20-26 June 1999, pages 542-549. ACL, 1999. URL: https://doi.org/10.3115/1034678.1034759.
  2. Rajeev Alur and P. Madhusudan. Visibly pushdown languages. In László Babai, editor, Proceedings of the 36th Annual ACM Symposium on Theory of Computing, Chicago, IL, USA, June 13-16, 2004, pages 202-211. ACM, 2004. URL: https://doi.org/10.1145/1007352.1007390.
  3. Stanislav Böhm and Stefan Göller. Language equivalence of deterministic real-time one-counter automata is NL-Complete. In Filip Murlak and Piotr Sankowski, editors, MFCS, volume 6907 of Lecture Notes in Computer Science, pages 194-205. Springer, 2011. Google Scholar
  4. Stanislav Böhm, Stefan Göller, and Petr Jancar. Bisimilarity of one-counter processes is PSPACE-Complete. In Paul Gastin and François Laroussinie, editors, CONCUR, volume 6269 of Lecture Notes in Computer Science, pages 177-191. Springer, 2010. Google Scholar
  5. Stanislav Böhm, Stefan Göller, and Petr Jancar. Equivalence of deterministic one-counter automata is NL-Complete. In Dan Boneh, Tim Roughgarden, and Joan Feigenbaum, editors, Symposium on Theory of Computing Conference, STOC'13, Palo Alto, CA, USA, June 1-4, 2013, pages 131-140. ACM, 2013. URL: https://doi.org/10.1145/2488608.2488626.
  6. Stanislav Böhm, Stefan Göller, and Petr Jancar. Bisimulation equivalence and regularity for real-time one-counter automata. J. Comput. Syst. Sci, 80(4):720-743, 2014. Google Scholar
  7. Tomás Brázdil, Javier Esparza, Stefan Kiefer, and Antonín Kucera. Analyzing probabilistic pushdown automata. Formal Methods Syst. Des, 43(2):124-163, 2013. Google Scholar
  8. Tomáš Brázdil, Antonín Kučera, and Oldřich Stražovský. On the decidability of temporal properties of probabilistic pushdown automata. In Volker Diekert and Bruno Durand, editors, STACS 2005, pages 145-157, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  9. Vojtech Forejt, Petr Jancar, Stefan Kiefer, and James Worrell. Bisimilarity of probabilistic pushdown automata. In Deepak D'Souza, Telikepalli Kavitha, and Jaikumar Radhakrishnan, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012, December 15-17, 2012, Hyderabad, India, volume 18 of LIPIcs, pages 448-460. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2012.448.
  10. Vojtech Forejt, Petr Jancar, Stefan Kiefer, and James Worrell. Language equivalence of probabilistic pushdown automata. Inf. Comput, 237:1-11, 2014. Google Scholar
  11. Juraj Hromkovič and Georg Schnitger. On probabilistic pushdown automata. Information and Computation, 208(8):982-995, 2010. URL: https://doi.org/10.1016/j.ic.2009.11.001.
  12. Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, and James Worrell. On the complexity of equivalence and minimisation for q-weighted automata. Log. Methods Comput. Sci., 9(1), 2013. URL: https://doi.org/10.2168/LMCS-9(1:8)2013.
  13. Daniel Krob. The equality problem for rational series with multiplicities in the tropical semiring is undecidable. In Proceedings of the 19th International Colloquium on Automata, Languages and Programming, ICALP '92, pages 101-112, Berlin, Heidelberg, 1992. Springer-Verlag. Google Scholar
  14. Antonín Kucera, Javier Esparza, and Richard Mayr. Model checking probabilistic pushdown automata. Log. Methods Comput. Sci., 2(1), 2006. URL: https://doi.org/10.2168/LMCS-2(1:2)2006.
  15. Antonín Kučera. Methods for quantitative analysis of probabilistic pushdown automata. Electronic Notes in Theoretical Computer Science, 149(1):3-15, 2006. Proceedings of the 7th International Workshop on Verification of Infinite-State Systems (INFINITY 2005). URL: https://doi.org/10.1016/j.entcs.2005.11.013.
  16. Meyer and Stockmeyer. Word problems requiring exponential time. In STOC: ACM Symposium on Theory of Computing (STOC), 1973. Google Scholar
  17. Dirk Nowotka and Jirí Srba. Height-deterministic pushdown automata. In Ludek Kucera and Antonín Kucera, editors, MFCS, volume 4708 of Lecture Notes in Computer Science, pages 125-134. Springer, 2007. Google Scholar
  18. William Ogden. A helpful result for proving inherent ambiguity. Mathematical Systems Theory, 2(3):191-194, 1968. Google Scholar
  19. Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. Reasoning about recursive probabilistic programs. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 672-681, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2933575.2935317.
  20. M. P. Schützenberger. On the definition of a family of automata. Information and Control, 4(2-3):245-270, September 1961. Google Scholar
  21. Géraud Sénizergues. The equivalence problem for deterministic pushdown automata is decidable. In Pierpaolo Degano, Roberto Gorrieri, and Alberto Marchetti-Spaccamela, editors, Automata, Languages and Programming, pages 671-681, Berlin, Heidelberg, 1997. Springer Berlin Heidelberg. Google Scholar
  22. Stirling. Deciding DPDA equivalence is primitive recursive. In ICALP: Annual International Colloquium on Automata, Languages and Programming, 2002. Google Scholar
  23. Wen-Guey Tzeng. A polynomial-time algorithm for the equivalence of probabilistic automata. SIAM J. Comput, 21(2):216-227, 1992. Google Scholar
  24. Valiant and Paterson. Deterministic one-counter automata. JCSS: Journal of Computer and System Sciences, 10, 1975. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact