2022/10/18 by Aditya Prakash, Prakash, Aditya, K. S. Thejaswini +1 · 2 citations
Computer Science · #F.4.3 #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic, programming, and type systems #Model-Driven Software Engineering Techniques
paper · pdf · doi:10.48550/arxiv.2210.10084
openalex publication_date 2022/10/18 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 one-counter automaton. We also show the decidability of comparing languages of history-deterministic OCNs, such as language inclusion and language universality.