SU\G(𝔸)/K·U
Sign Up for free Log In

On History-Deterministic One-Counter Nets

Authors

Aditya Prakash, K. S. Thejaswini
Type: Preprint
Publication Date: 2022-01-01
Citations: 1
DOI: https://doi.org/10.48550/arxiv.2210.10084

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 one-counter automaton. We also show the decidability of comparing languages of history-deterministic OCNs, such as language inclusion and language universality.

Topics

Locations

  • arXiv (Cornell University)
    View
  • Warwick Research Archive Portal (University of Warwick)
    View PDF
  • DataCite API
    View

Ask a Question About This Paper

Summary

Login to see paper summary

Determinization of One-Counter Nets

2021-01-01
Shaull Almagor , Asaf Yeshurun
One-Counter Nets (OCNs) are finite-state automata equipped with a counter that is not allowed to become negative, but does not have zero tests. Their simplicity and close connection to various … One-Counter Nets (OCNs) are finite-state automata equipped with a counter that is not allowed to become negative, but does not have zero tests. Their simplicity and close connection to various other models (e.g., VASS, Counter Machines and Pushdown Automata) make them an attractive model for studying the border of decidability for the classical decision problems. The deterministic fragment of OCNs (DOCNs) typically admits more tractable decision problems, and while these problems and the expressive power of DOCNs have been studied, the determinization problem, namely deciding whether an OCN admits an equivalent DOCN, has not received attention. We introduce four notions of OCN determinizability, which arise naturally due to intricacies in the model, and specifically, the interpretation of the initial counter value. We show that in general, determinizability is undecidable under most notions, but over a singleton alphabet (i.e., 1 dimensional VASS) one definition becomes decidable, and the rest become trivial, in that there is always an equivalent DOCN.
View PDF Chat

History-deterministic Timed Automata

2023-01-01
Sougata Bose , Thomas A. Henzinger , Karoliina Lehtinen +2 more
We explore the notion of history-determinism in the context of timed automata (TA) over infinite timed words. History-deterministic (HD) automata are those in which nondeterminism can be resolved on the … We explore the notion of history-determinism in the context of timed automata (TA) over infinite timed words. History-deterministic (HD) automata are those in which nondeterminism can be resolved on the fly, based on the run constructed thus far. History-determinism is a robust property that admits different game-based characterisations, and HD specifications allow for game-based verification without an expensive determinization step. We show that the class of timed $\omega$-languages recognised by HD timed automata strictly extends that of deterministic ones, and is strictly included in those recognised by fully non-deterministic TA. For non-deterministic timed automata it is known that universality is already undecidable for safety/reachability TA. For history-deterministic TA with arbitrary parity acceptance, we show that timed universality, inclusion, and synthesis all remain decidable and are EXPTIME-complete. For the subclass of TA with safety or reachability acceptance, one can decide (in EXPTIME) whether such an automaton is history-deterministic. If so, it can effectively determinized without introducing new automata states.
View PDF Chat

History-deterministic Timed Automata

2024-10-02
Sougata Bose , Thomas A. Henzinger , Karoliina Lehtinen +2 more
We explore the notion of history-determinism in the context of timed automata (TA) over infinite timed words. History-deterministic (HD) automata are those in which nondeterminism can be resolved on the … We explore the notion of history-determinism in the context of timed automata (TA) over infinite timed words. History-deterministic (HD) automata are those in which nondeterminism can be resolved on the fly, based on the run constructed thus far. History-determinism is a robust property that admits different game-based characterisations, and HD specifications allow for game-based verification without an expensive determinization step. We show that the class of timed $\omega$-languages recognized by HD timed automata strictly extends that of deterministic ones, and is strictly included in those recognised by fully non-deterministic TA. For non-deterministic timed automata it is known that universality is already undecidable for safety/reachability TA. For history-deterministic TA with arbitrary parity acceptance, we show that timed universality, inclusion, and synthesis all remain decidable and are EXPTIME-complete. For the subclass of TA with safety or reachability acceptance, one can decide (in EXPTIME) whether such an automaton is history-deterministic. If so, it can effectively determinized without introducing new automaton states.
View PDF Chat

History-Deterministic Parity Automata: Games, Complexity, and the 2-Token Theorem

2025-01-21
Aditya Prakash
History-deterministic automata are a restricted class of nondeterministic automata where the nondeterminism while reading an input can be resolved successfully based on the prefix read so far. History-deterministic automata are … History-deterministic automata are a restricted class of nondeterministic automata where the nondeterminism while reading an input can be resolved successfully based on the prefix read so far. History-deterministic automata are exponentially more succinct than deterministic automata, while still retaining some of the algorithmic properties of deterministic automata, especially in the context of reactive synthesis. This thesis focuses on the problem of checking history-determinism for parity automata. Our main result is the 2-token theorem, due to which we obtain that checking history-determinism for parity automata with a fixed parity index can be checked in PTIME. This improves the naive EXPTIME upper bound of Henzinger and Piterman that has stood since 2006. More precisely, we show that the so-called 2-token game, which can be solved in PTIME for parity automata with a fixed parity index, characterises history-determinism for parity automata. This game was introduced by Bagnol and Kuperberg in 2018, who showed that to decide if a B\"uchi automaton is history-deterministic, it suffices to find the winner of the 2-token game on it. They conjectured that this 2-token game based characterisation of history-determinism extends to parity automata. We prove Bagnol and Kuperberg's conjecture that the winner of the 2-token game characterises history-determinism on parity automata. We also give a polynomial time determinisation procedure for history-deterministic B\"uchi automata, thus solving an open problem of Kuperberg and Skrzypczak from 2015. This result is a consequence of our proof of the 2-token theorem. Finally, we also show NP-hardness for the problem of checking history-determinism for parity automata when the parity index is not fixed. This is an improvement from the lower bound of solving parity games shown by Kuperberg and Skrzypczak in 2015.
View PDF Chat

Token Games and History-Deterministic Quantitative-Automata

2023-11-03
Udi Boker , Karoliina Lehtinen
A nondeterministic automaton is history-deterministic if its nondeterminism can be resolved by only considering the prefix of the word read so far. Due to their good compositional properties, history-deterministic automata … A nondeterministic automaton is history-deterministic if its nondeterminism can be resolved by only considering the prefix of the word read so far. Due to their good compositional properties, history-deterministic automata are useful in solving games and synthesis problems. Deciding whether a given nondeterministic automaton is history-deterministic (the HDness problem) is generally a difficult task, which can involve an exponential procedure, or even be undecidable, as is the case for example with pushdown automata. Token games provide a PTime solution to the HDness problem of B\"uchi and coB\"uchi automata, and it is conjectured that 2-token games characterise HDness for all $\omega$-regular automata. We extend token games to the quantitative setting and analyse their potential to help deciding HDness of quantitative automata. In particular, we show that 1-token games characterise HDness for all quantitative (and Boolean) automata on finite words, as well as discounted-sum (DSum), Inf and Reachability automata on infinite words, and that 2-token games characterise HDness of LimInf and LimSup automata, as well as Sup automata on infinite words. Using these characterisations, we provide solutions to the HDness problem of Safety, Reachability, Inf and Sup automata on finite and infinite words in PTime, of DSum automata on finite and infinite words in NP$\cap$co-NP, of LimSup automata in quasipolynomial time, and of LimInf automata in exponential time, where the latter two are only polynomial for automata with a logarithmic number of weights.
View PDF Chat

Token Games and History-Deterministic Quantitative-Automata

2021-01-01
Udi Boker , Karoliina Lehtinen
A nondeterministic automaton is history-deterministic if its nondeterminism can be resolved by only considering the prefix of the word read so far. Due to their good compositional properties, history-deterministic automata … A nondeterministic automaton is history-deterministic if its nondeterminism can be resolved by only considering the prefix of the word read so far. Due to their good compositional properties, history-deterministic automata are useful in solving games and synthesis problems. Deciding whether a given nondeterministic automaton is history-deterministic (the HDness problem) is generally a difficult task, which can involve an exponential procedure, or even be undecidable, as is the case for example with pushdown automata. Token games provide a PTime solution to the HDness problem of B\"uchi and coB\"uchi automata, and it is conjectured that 2-token games characterise HDness for all $\omega$-regular automata. We extend token games to the quantitative setting and analyse their potential to help deciding HDness of quantitative automata. In particular, we show that 1-token games characterise HDness for all quantitative (and Boolean) automata on finite words, as well as discounted-sum (DSum), Inf and Reachability automata on infinite words, and that 2-token games characterise HDness of LimInf and LimSup automata, as well as Sup automata on infinite words. Using these characterisations, we provide solutions to the HDness problem of Safety, Reachability, Inf and Sup automata on finite and infinite words in PTime, of DSum automata on finite and infinite words in NP$\cap$co-NP, of LimSup automata in quasipolynomial time, and of LimInf automata in exponential time, where the latter two are only polynomial for automata with a logarithmic number of weights.
View PDF Chat

History-Deterministic Timed Automata

2022-01-01
Thomas A. Henzinger , Karoliina Lehtinen , Patrick Totzke
View PDF Chat

Token Games and History-Deterministic Quantitative Automata

2022-01-01
Udi Boker , Karoliina Lehtinen
Abstract A nondeterministic automaton is history-deterministic if its nondeterminism can be resolved by only considering the prefix of the word read so far. Due to their good compositional properties, history-deterministic … Abstract A nondeterministic automaton is history-deterministic if its nondeterminism can be resolved by only considering the prefix of the word read so far. Due to their good compositional properties, history-deterministic automata are useful in solving games and synthesis problems. Deciding whether a given nondeterministic automaton is history-deterministic (the problem) is generally a difficult task, which might involve an exponential procedure, or even be undecidable, for example for pushdown automata. Token games provide a PTime solution to the problem of Büchi and coBüchi automata, and it is conjectured that 2-token games characterise for all $$\omega $$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>ω</mml:mi> </mml:math> -regular automata. We extend token games to the quantitative setting and analyze their potential to help deciding for quantitative automata. In particular, we show that 1-token games characterise for all quantitative (and Boolean) automata on finite words, as well as discounted-sum ( $${\mathsf {DSum}}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>DSum</mml:mi> </mml:math> ) automata on infinite words, and that 2-token games characterise of $${\mathsf {LimInf}}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>LimInf</mml:mi> </mml:math> and $${\mathsf {LimSup}}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>LimSup</mml:mi> </mml:math> automata. Using these characterisations, we provide solutions to the problem of $${\mathsf {Inf}}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>Inf</mml:mi> </mml:math> and $${\mathsf {Sup}}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>Sup</mml:mi> </mml:math> automata on finite words in PTime , for $${\mathsf {DSum}}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>DSum</mml:mi> </mml:math> automata on finite and infinite words in NP $$\cap $$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mo>∩</mml:mo> </mml:math> co-NP , for $${\mathsf {LimSup}}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>LimSup</mml:mi> </mml:math> automata in quasipolynomial time, and for $${\mathsf {LimInf}}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>LimInf</mml:mi> </mml:math> automata in exponential time, where the latter two are only polynomial for automata with a logarithmic number of weights.
View PDF Chat

Lookahead Games and Efficient Determinisation of History-Deterministic B\"uchi Automata

2024-04-26
Rohan K Acharya , Marcin Jurdziński , Aditya Prakash
Our main technical contribution is a polynomial-time determinisation procedure for history-deterministic B\"uchi automata, which settles an open question of Kuperberg and Skrzypczak, 2015. A key conceptual contribution is the lookahead … Our main technical contribution is a polynomial-time determinisation procedure for history-deterministic B\"uchi automata, which settles an open question of Kuperberg and Skrzypczak, 2015. A key conceptual contribution is the lookahead game, which is a variant of Bagnol and Kuperberg's token game, in which Adam is given a fixed lookahead. We prove that the lookahead game is equivalent to the 1-token game. This allows us to show that the 1-token game characterises history-determinism for semantically-deterministic B\"uchi automata, which paves the way to our polynomial-time determinisation procedure.
View PDF Chat

One-Counter Stochastic Games

2010-01-01
Tomǎš Brázdil , Václav Brožek , Kousha Etessami
We study the computational complexity of basic decision problems for one-counter simple stochastic games (OC-SSGs), under various objectives. OC-SSGs are 2-player turn-based stochastic games played on the transition graph of … We study the computational complexity of basic decision problems for one-counter simple stochastic games (OC-SSGs), under various objectives. OC-SSGs are 2-player turn-based stochastic games played on the transition graph of classic one-counter automata. We study primarily the termination objective, where the goal of one player is to maximize the probability of reaching counter value 0, while the other player wishes to avoid this. Partly motivated by the goal of understanding termination objectives, we also study certain "limit" and "long run average" reward objectives that are closely related to some well-studied objectives for stochastic games with rewards. Examples of problems we address include: does player 1 have a strategy to ensure that the counter eventually hits 0, i.e., terminates, almost surely, regardless of what player 2 does? Or that the liminf (or limsup) counter value equals infinity with a desired probability? Or that the long run average reward is &gt;0 with desired probability? We show that the qualitative termination problem for OC-SSGs is in NP intersection coNP, and is in P-time for 1-player OC-SSGs, or equivalently for one-counter Markov Decision Processes (OC-MDPs). Moreover, we show that quantitative limit problems for OC-SSGs are in NP intersection coNP, and are in P-time for 1-player OC-MDPs. Both qualitative limit problems and qualitative termination problems for OC-SSGs are already at least as hard as Condon's quantitative decision problem for finite-state SSGs.

Simulation Over One-counter Nets is PSPACE-Complete

2013-01-01
Piotr Hofman , Sławomir Lasota , Richard Mayr +1 more
One-counter nets (OCN) are Petri nets with exactly one unbounded place. They are equivalent to a subclass of one-counter automata with just a weak test for zero. Unlike many other … One-counter nets (OCN) are Petri nets with exactly one unbounded place. They are equivalent to a subclass of one-counter automata with just a weak test for zero. Unlike many other semantic equivalences, strong and weak simulation preorder are decidable for OCN, but the computational complexity was an open problem. We show that both strong and weak simulation preorder on OCN are PSPACE-complete.

One-Counter Automata with Counter Observability

2016-01-01
Benedikt Bollig
In a one-counter automaton (OCA), one can produce a letter from some finite alphabet, increment and decrement the counter by one, or compare it with constants up to some threshold. … In a one-counter automaton (OCA), one can produce a letter from some finite alphabet, increment and decrement the counter by one, or compare it with constants up to some threshold. It is well-known that universality and language inclusion for OCAs are undecidable. In this paper, we consider OCAs with counter observability: Whenever the automaton produces a letter, it outputs the current counter value along with it. Hence, its language is now a set of words over an infinite alphabet. We show that universality and inclusion for that model are PSPACE-complete, thus no harder than the corresponding problems for finite automata. In fact, by establishing a link with visibly one-counter automata, we show that OCAs with counter observability are effectively determinizable and closed under all boolean operations.
View PDF Chat

History-Determinism vs Fair Simulation

2024-07-11
Udi Boker , Thomas A. Henzinger , Karoliina Lehtinen +1 more
An automaton is history-deterministic if its nondeterminism can be resolved on the fly, only using the prefix of the word read so far. This mild form of nondeterminism has attracted … An automaton is history-deterministic if its nondeterminism can be resolved on the fly, only using the prefix of the word read so far. This mild form of nondeterminism has attracted particular attention for its applications in synthesis problems. An automaton $A$ is guidable with respect to a class $C$ of automata if it can fairly simulate every automaton in $C$ whose language is contained in that of $A$. In other words, guidable automata are those for which inclusion and simulation coincide, making them particularly interesting for model-checking. We study the connection between these two notions, and specifically the question of when they coincide. For classes of automata on which they do, deciding guidability, an otherwise challenging decision problem, reduces to deciding history-determinism, a problem that is starting to be well-understood for many classes. We provide a selection of sufficient criteria for a class of automata to guarantee the coincidence of the notions, and use them to show that the notions coincide for the most common automata classes, among which are $\omega$-regular automata and many infinite-state automata with safety and reachability acceptance conditions, including vector addition systems with states, one-counter nets, pushdown-, Parikh-, and timed-automata. We also demonstrate that history-determinism and guidability do not always coincide, for example, for the classes of timed automata with a fixed number of clocks.
View PDF Chat

History-deterministic Vector Addition Systems

2023-01-01
Sougata Bose , David Purser , Patrick Totzke
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. History-determinism requires that the non-deterministic … 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. 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, and with and without $\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 a VASS is history-deterministic, or if a language equivalent history-deterministic VASS exists. Checking language inclusion between history-deterministic 2-VASS is also undecidable.
View PDF Chat

Checking History-Determinism is NP-hard for Parity Automata

2023-01-01
Aditya Prakash
We show that the problem of checking if a given nondeterministic parity automaton simulates another given nondeterministic parity automaton is NP-hard. We then adapt the techniques used for this result … We show that the problem of checking if a given nondeterministic parity automaton simulates another given nondeterministic parity automaton is NP-hard. We then adapt the techniques used for this result to show that the problem of checking history-determinism for a given parity automaton is NP-hard. This is an improvement from Kuperberg and Skrzypczak's previous lower bound of parity games from 2015. We also show that deciding if Eve wins the one-token game or the two-token game of a given parity automaton is NP-hard. Finally, we show that the problem of deciding if the language of a nondeterministic parity automaton is contained in the language of a history-deterministic parity automaton can be solved in quasi-polynomial time.
View PDF Chat

Decidability of Weak Simulation on One-counter Nets

2013-04-15
Piotr Hofman , Richard Mayr , Patrick Totzke
One-counter nets (OCN) are Petri nets with exactly one unbounded place. They are equivalent to a subclass of one-counter automata with only a weak test for zero. We show that … One-counter nets (OCN) are Petri nets with exactly one unbounded place. They are equivalent to a subclass of one-counter automata with only a weak test for zero. We show that weak simulation preorder is decidable for OCN and that weak simulation approximants do not converge at level omega, but only at omega^2. In contrast, other semantic relations like weak bisimulation are undecidable for OCN, and so are weak (and strong) trace inclusion.

Decidability of Weak Simulation on One-counter Nets

2013-01-01
Piotr Hofman , Richard Mayr , Patrick Totzke
One-counter nets (OCN) are Petri nets with exactly one unbounded place. They are equivalent to a subclass of one-counter automata with only a weak test for zero. We show that … One-counter nets (OCN) are Petri nets with exactly one unbounded place. They are equivalent to a subclass of one-counter automata with only a weak test for zero. We show that weak simulation preorder is decidable for OCN and that weak simulation approximants do not converge at level omega, but only at omega^2. In contrast, other semantic relations like weak bisimulation are undecidable for OCN, and so are weak (and strong) trace inclusion.
View PDF Chat

Continuous One-counter Automata

2022-08-23
Michael Blondin , Tim Leys , Filip Mazowiecki +2 more
We study the reachability problem for continuous one-counter automata, COCA for short. In such automata, transitions are guarded by upper- and lower-bound tests against the counter value. Additionally, the counter … We study the reachability problem for continuous one-counter automata, COCA for short. In such automata, transitions are guarded by upper- and lower-bound tests against the counter value. Additionally, the counter updates associated with taking transitions can be (non-deterministically) scaled down by a nonzero factor between zero and one. Our three main results are as follows: we prove (1) that the reachability problem for COCA with global upper- and lower-bound tests is in NC 2 ; (2) that, in general, the problem is decidable in polynomial time; and (3) that it is NP-complete for COCA with parametric counter updates and bound tests.
View PDF Chat

Trace Inclusion for One-Counter Nets Revisited

2014-01-01
Piotr Hofman , Patrick Totzke
One-Counter nets (OCN) consist of a nondeterministic finite control and a single integer counter that cannot be fully tested for zero. They form a natural subclass of both One-Counter Automata, … One-Counter nets (OCN) consist of a nondeterministic finite control and a single integer counter that cannot be fully tested for zero. They form a natural subclass of both One-Counter Automata, which allow zero-tests and Petri Nets/VASS, which allow multiple such weak counters. The trace inclusion problem has recently been shown to be undecidable for OCN. In this paper, we contrast the complexity of two natural restrictions which imply decidability. First, we show that trace inclusion between an OCN and a deterministic OCN is NL-complete, even with arbitrary binary-encoded initial counter-values as part of the input. Secondly, we show Ackermannian completeness of for the trace universality problem of nondeterministic OCN. This problem is equivalent to checking trace inclusion between a finite and a OCN-process.
View PDF Chat

Trace Inclusion for One-Counter Nets Revisited

2014-04-21
Piotr Hofman , Patrick Totzke
One-Counter nets (OCN) consist of a nondeterministic finite control and a single integer counter that cannot be fully tested for zero. They form a natural subclass of both One-Counter Automata, … One-Counter nets (OCN) consist of a nondeterministic finite control and a single integer counter that cannot be fully tested for zero. They form a natural subclass of both One-Counter Automata, which allow zero-tests and Petri Nets/VASS, which allow multiple such weak counters. The trace inclusion problem has recently been shown to be undecidable for OCN. In this paper, we contrast the complexity of two natural restrictions which imply decidability. First, we show that trace inclusion between an OCN and a deterministic OCN is NL-complete, even with arbitrary binary-encoded initial counter-values as part of the input. Secondly, we show Ackermannian completeness of for the trace universality problem of nondeterministic OCN. This problem is equivalent to checking trace inclusion between a finite and a OCN-process.