History-deterministic Parikh Automata

TL;DR

This work introduces history-deterministic Parikh automata (HDPA), models in which nondeterminism is resolved on the fly by a resolver based on the run so far. It establishes that HDPA are strictly more expressive than deterministic PA and incomparable to unambiguous variants, while being equivalent to history-deterministic reversal-bounded counter machines, thus positioning them as a natural middle ground for quantitative automata. HDPA share most closure properties with deterministic PA (except closure under complement) and support decidable safety model checking, though several classic decision problems (universality, inclusion, equivalence, regularity) remain undecidable. The paper also analyzes resolvers, showing some HDPA admit $DPA$-implementable resolvers and revealing a tight connection between HDPA and one-way history-deterministic RBCMs, with further discussion on the complexity of nondeterminism resolution. Overall, HDPA emerge as a robust, composition-friendly model for quantitative specifications, with clear avenues for exploration in resolver complexity and games.

Abstract

Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run. Thereby, they preserve many of the desirable properties of finite automata. Deterministic Parikh automata are strictly weaker than nondeterministic ones, but enjoy better closure and algorithmic properties. This state of affairs motivates the study of intermediate forms of nondeterminism. Here, we investigate history-deterministic Parikh automata, i.e., automata whose nondeterminism can be resolved on the fly. This restricted form of nondeterminism is well-suited for applications which classically call for determinism, e.g., solving games and composition. We show that history-deterministic Parikh automata are strictly more expressive than deterministic ones, incomparable to unambiguous ones, and enjoy almost all of the closure properties of deterministic automata. Finally, we investigate the complexity of resolving nondeterminism in history-deterministic Parikh automata.

Figures (6)

• Figure 1: The automaton for Example \ref{['example_intro']}.
• Figure 2: The automaton for Example \ref{['example_nondyck']}.
• Figure 3: The classes of languages accepted by different models of Parikh automata.
• Figure 4: The automaton for the language $T$.
• Figure 5: The automaton for the language $E'$.

Theorems & Definitions (39)

• proposition 1
• proposition 2: GSalgol
• definition 1
• remark 1
• lemma 1
• proof
• theorem 1
• proof
• theorem 2
• proof