The complexity of regular abstractions of one-counter languages

DOI10.1145/2933575.2934561zbMATH Open1401.68142arXiv1602.03419OpenAlexW2258615751MaRDI QIDQ4635876FDOQ4635876

Authors: Mohamed Faouzi Atig, Piotr Hofman, K. Narayan Kumar, Prakash Saivasan, Georg Zetzsche, Dmitry Chistikov 

Publication date: 23 April 2018

Published in: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Abstract: We study the computational and descriptional complexity of the following transformation: Given a one-counter automaton (OCA) A, construct a nondeterministic finite automaton (NFA) B that recognizes an abstraction of the language L(A): its (1) downward closure, (2) upward closure, or (3) Parikh image. For the Parikh image over a fixed alphabet and for the upward and downward closures, we find polynomial-time algorithms that compute such an NFA. For the Parikh image with the alphabet as part of the input, we find a quasi-polynomial time algorithm and prove a completeness result: we construct a sequence of OCA that admits a polynomial-time algorithm iff there is one for all OCA. For all three abstractions, it was previously unknown if appropriate NFA of sub-exponential size exist.

Full work available at URL: https://arxiv.org/abs/1602.03419

Recommendations

• The complexity of downward closure comparisons
• Computing downward closures for stacked counter automata
• One-counter automata with counter observability
• Bisimulation equivalence and regularity for real-time one-counter automata

zbMATH Keywords

Parikh imageone-counter automatadownward closureupward closure

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Cited In (9)

• Verifying quantitative temporal properties of procedural programs
• Title not available (Why is that?)
• One-counter automata with counter observability
• Existential Definability over the Subword Ordering
• New pumping technique for 2-dimensional VASS
• Regular separability of one counter automata
• Computing linear arithmetic representation of reachability relation of one-counter automata
• Computing downward closures for stacked counter automata
• One-counter automata for parsing and language approximation

This page was built for publication: The complexity of regular abstractions of one-counter languages

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635876)