@inproceedings{DartoisFiliotTalbot:FOSSACS:2019,
    Abstract = {In this paper, we investigate the complexity of the emptiness problem for Parikh automata equipped with a pushdown stack. Pushdown Parikh automata extend pushdown automata with counters which can only be incremented and an acceptance condition given as a semi-linear set, which we represent as an existential Presburger formula over the final values of the counters. We show that the non-emptiness problem both in the deterministic and non-deterministic cases is NP-c. If the input head can move in a two-way fashion, emptiness gets undecidable, even if the pushdown stack is visibly and the automaton deterministic. We define a restriction, called the single-use restriction, to recover decidability in the presence of two-wayness, when the stack is visibly. This syntactic restriction enforces that any transition which increments at least one dimension is triggered only a bounded number of times per input position. Our main contribution is to show that non-emptiness of two-way visibly Parikh automata which are single-use is NExpTime-c. We finally give applications to decision problems for expressive transducer models from nested words to words, including the equivalence problem.},
    Address = {Cham},
    Author = {Dartois, Luc and Filiot, Emmanuel and Talbot, Jean-Marc},
    BookTitle = {Proc.~of FOSSACS'19},
    Editor = {Boja{\'{n}}czyk, Miko{{\l}}aj and Simpson, Alex},
    File = {Dartois2019\_Chapter\_Two-WayParikhAutomataWithAVisi (0) (0) - a - a - p.pdf},
    ISBN = {978-3-030-17127-8},
    Pages = {189--206},
    Publisher = {Springer International Publishing},
    Title = {Two-Way {Parikh} Automata with a Visibly Pushdown Stack},
    Year = {2019},
    date-added = {2019-06-20 11:09:23 +0200},
    date-modified = {2020-05-07 07:20:46 +0200},
    doi = {10.1007/978-3-030-17127-8_11}
}

@inproceedings{DartoisFiliotTalbot:FOSSACS:2019, Abstract = {In this paper, we investigate the complexity of the emptiness problem for Parikh automata equipped with a pushdown stack. Pushdown Parikh automata extend pushdown automata with counters which can only be incremented and an acceptance condition given as a semi-linear set, which we represent as an existential Presburger formula over the final values of the counters. We show that the non-emptiness problem both in the deterministic and non-deterministic cases is NP-c. If the input head can move in a two-way fashion, emptiness gets undecidable, even if the pushdown stack is visibly and the automaton deterministic. We define a restriction, called the single-use restriction, to recover decidability in the presence of two-wayness, when the stack is visibly. This syntactic restriction enforces that any transition which increments at least one dimension is triggered only a bounded number of times per input position. Our main contribution is to show that non-emptiness of two-way visibly Parikh automata which are single-use is NExpTime-c. We finally give applications to decision problems for expressive transducer models from nested words to words, including the equivalence problem.}, Address = {Cham}, Author = {Dartois, Luc and Filiot, Emmanuel and Talbot, Jean-Marc}, BookTitle = {Proc.~of FOSSACS'19}, Editor = {Boja{\'{n}}czyk, Miko{{\l}}aj and Simpson, Alex}, File = {Dartois2019_Chapter_Two-WayParikhAutomataWithAVisi (0) (0) - a - a - p.pdf}, ISBN = {978-3-030-17127-8}, Pages = {189--206}, Publisher = {Springer International Publishing}, Title = {Two-Way {Parikh} Automata with a Visibly Pushdown Stack}, Year = {2019}, date-added = {2019-06-20 11:09:23 +0200}, date-modified = {2020-05-07 07:20:46 +0200}, doi = {10.1007/978-3-030-17127-8_11} }