Mohamed Faouzi Atig
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 whether appropriate NFA of sub-exponential size exist.
- P. A. Abdulla, M. F. Atig, and J. Cederberg. Analysis of message passing programs using SMT-solvers. In ATVA, 2013.Google Scholar
Cross Ref
- P. A. Abdulla, M. F. Atig, R. Meyer, and M. S. Salehi. What's decidable about availability languages? In FSTTCS, 2015.Google Scholar
- R. Alur and P. Černý. Streaming transducers for algorithmic verification of single-pass list-processing programs. In POPL, 2011. Google ScholarDigital Library
- M. F. Atig, A. Bouajjani, and T. Touili. On the reachability analysis of acyclic networks of pushdown systems. In CONCUR, 2008. Google ScholarDigital Library
- M. F. Atig, A. Bouajjani, and T. Touili. Analyzing asynchronous programs with preemption. In FSTTCS, 2008.Google Scholar
- M. F. Atig, A. Bouajjani, and S. Qadeer. Context-bounded analysis for concurrent programs with dynamic creation of threads. Logical Methods in Computer Science, 7(4), 2011.Google Scholar
- M. F. Atig, A. Bouajjani, K. N. Kumar, and P. Saivasan. On bounded reachability analysis of shared memory systems. In FSTTCS, 2014.Google Scholar
- G. Bachmeier, M. Luttenberger, and M. Schlund. Finite automata for the sub- and superword closure of CFLs: Descriptional and computational complexity. In LATA, 2015.Google ScholarCross Ref
- S. Böhm, S. Göller, and P. Jancar. Equivalence of deterministic one-counter automata is NL-complete. In STOC, 2013. Google ScholarDigital Library
- C. Chitic and D. Rosu. On validation of XML streams using finite state machines. In WebDB, 2004. Google ScholarDigital Library
- B. Courcelle. On constructing obstruction sets of words. Bulletin of the EATCS, 44:178--186, 1991.Google Scholar
- J. Duske and R. Parchmann. Linear indexed languages. Theor. Comput. Sci., 32:47--60, 1984. Google ScholarDigital Library
- J. Esparza and P. Ganty. Complexity of pattern-based verification for multithreaded programs. In POPL, 2011. Google ScholarDigital Library
- J. Esparza, P. Ganty, S. Kiefer, and M. Luttenberger. Parikh's theorem: A simple and direct automaton construction. Inf. Process. Lett., 111(12):614--619, 2011. Google ScholarDigital Library
- J. Esparza, P. Ganty, and T. Poch. Pattern-based verification for multithreaded programs. ACM Trans. Program. Lang. Syst., 36(3):9:1--9:29, 2014. Google ScholarDigital Library
- J. Esparza, M. Luttenberger, and M. Schlund. A brief history of Strahler numbers. In LATA, 2014.Google ScholarDigital Library
- P. Ganty and R. Majumdar. Algorithmic verification of asynchronous programs. ACM Trans. Program. Lang. Syst., 34(1):6:1--6:48, May 2012. ISSN 0164-0925. Google ScholarDigital Library
- H. Gruber, M. Holzer, and M. Kutrib. More on the size of Higman-Haines sets: effective constructions. Fundamenta Informaticae, 91(1):105--121, 2009. Google ScholarDigital Library
- P. Habermehl, R. Meyer, and H. Wimmel. The downward-closure of Petri net languages. In ICALP, 2010. Google ScholarDigital Library
- M. Hague and A. W. Lin. Synchronisation- and reversal-bounded analysis of multithreaded programs with counters. In CAV, 2012. Google ScholarDigital Library
- M. Hague, J. Kochems, and C. L. Ong. Unboundedness and downward closures of higher-order pushdown automata. In POPL, 2016. Google ScholarDigital Library
- G. Higman. Ordering by divisibility in abstract algebras. Proc. London Math. Soc. (3), 2(7):326--336, 1952.Google ScholarCross Ref
- J. Hoenicke, R. Meyer, and E. Olderog. Kleene, Rabin, and Scott are available. In CONCUR, 2010. Google ScholarDigital Library
- E. Kopczynski and A. W. To. Parikh images of grammars: Complexity and applications. In LICS, 2010. Google ScholarDigital Library
- S. La Torre, P. Madhusudan, and G. Parlato. A robust class of context-sensitive languages. In LICS, 2007. Google ScholarDigital Library
- S. La Torre, M. Napoli, and G. Parlato. Scope-bounded pushdown languages. In DLT, 2014.Google ScholarCross Ref
- S. La Torre, A. Muscholl, and I. Walukiewicz. Safety of parametrized asynchronous shared-memory systems is almost always decidable. In CONCUR, 2015.Google Scholar
- P. Lafourcade, D. Lugiez, and R. Treinen. Intruder deduction for AC-like equational theories with homomorphisms. In RTA, 2005. Google ScholarDigital Library
- M. Latteux. Langages à un compteur. J. Comput. Syst. Sci., 26(1):14--33, 1983.Google ScholarCross Ref
- Z. Long, G. Calin, R. Majumdar, and R. Meyer. Language-theoretic abstraction refinement. In FASE, 2012. Google ScholarDigital Library
- R. Mayr. Undecidable problems in unreliable computations. Theor. Comput. Sci., 297(1-3):337--354, 2003. Google ScholarDigital Library
- R. J. Parikh. On context-free languages. J. ACM, 13(4): 570--581, Oct. 1966. Google ScholarDigital Library
- K. Sen and M. Viswanathan. Model checking multithreaded programs with asynchronous atomic methods. In CAV, 2006. Google ScholarDigital Library
- L. G. Valiant and M. Paterson. Deterministic one-counter automata. J. Comput. Syst. Sci., 10(3):340--350, 1975. Google ScholarDigital Library
- J. van Leeuwen. Effective constructions in well-partially-ordered free monoids. Discrete Math., 21(3):237--252, 1978. Google ScholarDigital Library
- K. N. Verma, H. Seidl, and T. Schwentick. On the complexity of equational Horn clauses. In CADE-20, 2005. Google ScholarDigital Library
- G. Zetzsche. An approach to computing downward closures. In ICALP, 2015. Google ScholarDigital Library
- G. Zetzsche. Computing downward closures for stacked counter automata. In STACS, 2015.Google Scholar
Index Terms
- The complexity of regular abstractions of one-counter languages
Recommendations
The complexity of bisimilarity-checking for one-counter processes
We study the problem of bisimilarity-checking between processes of one-counter automata and finite-state processes. We show that deciding weak bisimilarity between processes of one-counter nets (which are `restricted one-counter automata where the ...
Pushdown and One-Counter Automata: Constant and Non-constant Memory Usage
Descriptional Complexity of Formal SystemsAbstractIt cannot be decided whether a one-counter automaton accepts each string in its language using a counter whose value is bounded by a constant. Furthermore, when the counter is bounded by a constant, its value cannot be limited by any recursive ...
Automata Classes Accepting Languages Whose Commutative Closure is Regular
SOFSEM 2024: Theory and Practice of Computer ScienceAbstractThe commutative closure operation, which corresponds to the Parikh image, is a natural operation on formal languages occurring in verification and model-checking. Commutative closures of regular languages correspond to semilinear sets and, by ...
Comments