On History-Deterministic One-Counter Nets
Aditya Prakash, K. S. Thejaswini

TL;DR
This paper investigates history-determinism in one-counter nets, establishing decidability and complexity results, and analyzing language properties, including the construction of equivalent deterministic automata and decidability of language comparisons.
Contribution
It introduces the concept of history-determinism for OCNs, proves its decidability and complexity bounds, and explores language properties and equivalences.
Findings
Deciding history-determinism in OCNs is PSPACE-complete with unary encoding.
Deciding history-determinism in OCNs is EXPSPACE-complete with binary encoding.
History-deterministic OCNs have eventually periodic resolvers and equivalent deterministic automata.
Abstract
We consider the model of history-deterministic one-counter nets (OCNs). History-determinism is a property of transition systems that allows for a limited kind of non-determinism which can be resolved 'on-the-fly'. Token games, which have been used to characterise history-determinism over various models, also characterise history-determinism over OCNs. By reducing 1-token games to simulation games, we are able to show that checking for history-determinism of OCNs is decidable. Moreover, we prove that this problem is PSPACE-complete for a unary encoding of transitions, and EXPSPACE-complete for a binary encoding. We then study the language properties of history-deterministic OCNs. We show that the resolvers of non-determinism for history-deterministic OCNs are eventually periodic. As a consequence, for a given history-deterministic OCN, we construct a language equivalent deterministic…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Model-Driven Software Engineering Techniques
