History-Deterministic Vector Addition Systems

*In International Conference on Concurrency Theory (CONCUR)*, 2023

We consider history-determinism, a restricted form of
non-determinism, for Vector Addition Systems with States
(VASS) when used as acceptors to recognise languages of
finite words, both with coverability and reachability
acceptance. History-determinism requires that the
non-deterministic choices can be resolved on-the-fly; based
on the past and without jeopardising acceptance of any
possible continuation of the input word.

Our
results show that the history-deterministic (HD) VASS sit
strictly between deterministic and non-deterministic VASS
regardless of the number of counters. We compare the
relative expressiveness of HD systems, and
closure-properties of the induced language classes, with
coverability and reachability semantics, with and without
silent (\(\varepsilon\)-labelled) transitions.

Whereas in dimension 1, inclusion and regularity remain
decidable, from dimension two onwards, HD-VASS with
suitable resolver strategies, are essentially able to
simulate 2-counter Minsky machines, leading to several
undecidability results: It is undecidable whether an VASS
is history-deterministic, or if a language equivalent
history-deterministic VASS exists. Checking language
inclusion between history-deterministic 2-VASS is also
undecidable.

```
@inproceedings{BPT2023,
title = {{History-Deterministic Vector Addition Systems}},
author = {Bose, Sougata and Purser, David and Totzke, Patrick},
booktitle = {International Conference on Concurrency Theory (CONCUR)},
year = {2023},
pages = {18:1--18:17},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-95977-299-0},
issn = {1868-8969},
volume = {279},
editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/opus/volltexte/2023/19012},
urn = {urn:nbn:de:0030-drops-190120},
doi = {10.4230/LIPIcs.CONCUR.2023.18}
}
```