On History-Deterministic One-Counter Nets Aditya Prakash1and K. S. Thejaswini1 Department of Computer Science University of Warwick

2025-05-02 0 0 838.88KB 44 页 10玖币

侵权投诉

On History-Deterministic One-Counter Nets

Aditya Prakash1and K. S. Thejaswini1

Department of Computer Science, University of Warwick

{aditya.prakash,thejaswini.raghavan.1}@warwick.ac.uk

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-ﬂy’. 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 decid-

able. 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 lan-

guages of history-deterministic OCNs, such as language inclusion and

language universality.

Keywords: History-determinism ·Token games ·One-counter nets ·

One-counter automaton.

1 Introduction

While deterministic automata are algorithmically eﬃcient for problems such as

synthesis or for solving games, they are often much less succinct, or less expressive

than their non-deterministic counterparts. The notion of history-determinism

was introduced by Henzinger and Piterman [15] for automata over inﬁnite words

with parity acceptance conditions, as a tool to solve synthesis games eﬃciently.

Such automata are known to compose well with games, and hence are also called

good-for-games (GFG) automata [15,11]. History-deterministic automata form a

robust class of models that is both algorithmically and conceptually interesting,

and has been extensively studied over the recent years [15,11,4,25,6,1,5,9,28].

The notion of history-determinism emerged independently in the setting of

cost automata, that can capture all regular cost functions as opposed to their de-

terministic version [10]. Recently, history-determinism has been studied in other

quantitative settings [7,8], as well as inﬁnite-state systems such as pushdown

automata [13,26], Parikh automata [12], and timed automata [14].

arXiv:2210.10084v3 [cs.FL] 22 Nov 2022

2 A. Prakash, K. S. Thejaswini

One-counter nets are ﬁnite-state systems along with a counter that stores

a non-negative integer value that can never be explicitly tested for zero. They

correspond to 1-dimensional VASS, Petri nets with exactly one unbounded place,

and are a subclass of one-counter automata which do not have zero tests, and

hence are also a subclass of pushdown automata. They are one of the simplest

inﬁnite-state systems, and hence many problems pertaining to one-counter nets

are easier than their counterparts that subsume them.

The structure of the resolvers that resolve non-determinism on-the-ﬂy are cru-

cial to understand history-determinism in various models. While for automata

over inﬁnite words with parity conditions, these resolvers take the shape of deter-

ministic parity automata [15], the situation for resolvers in history-deterministic

inﬁnite-state systems is not as well understood. Indeed, the computability of

such a resolver for a given history-deterministic pushdown automaton is left as

an open problem in the works of Guha, Jecker, Lehtinen and Zimmermann [13].

For history-deterministic Parikh automata, it is still an open problem if the re-

solver can be given by a deterministic Parikh transducer [12]. Moreover, many

other problems such as deciding history-determinism or even language inclusion

among history-deterministic automata are undecidable for pushdown automata

and Parikh automata [13,26,12]. We consider history-determinism over a well-

studied class of inﬁnite-state systems of one-counter nets, where we are able to

answer positively to all of the above questions.

The techniques we use to answer several of these questions use results and

techniques from the simulation problem over one-counter nets [17,16]. This is

not surprising, since simulation of various models has close ties with history-

determinism [15,14].

Our Contribution We study history-deterministic OCNs and establish them as

a class of inﬁnite-state systems where many problems pertaining to history-

determinism are decidable. This is unlike other classes of history-deterministic

inﬁnite-state systems that subsume them.

Firstly, we show that checking for history-determinism for a given one-counter

net is PSPACE-complete when the transitions are encoded in unary, and is

EXPSPACE-complete for a succinct encoding (Theorem 4, Theorem 27). We

achieve the upper bound by giving a novel reduction from the 1-token game

G1to the simulation problem over OCNs. 1-token games characterise history-

determinism over OCNs, and thus our reduction further extends the link between

history-determinism and simulation. This decidability result is in contrast to

one-counter automata (OCA), where checking for history-determinism becomes

undecidable by just adding zero-tests to OCNs (Theorem 28).

Secondly, we show that resolvers for non-determinism in history-deterministic

OCNs can be expressed as an eventually periodic set. Using this, we are able to

determinise history-deterministic OCNs to give a language equivalent determin-

istic OCA.

Finally, we show the decidability of the problems of language inclusion and

language universality for history-deterministic OCNs to be in PSPACE and

Prespectively. This is in unlike non-deterministic OCNs, where these problems

On History-Deterministic One-Counter Nets 3

are known to be undecidable and Ackermann-complete respectively. Even for the

class of deterministic OCA, which we show history-deterministic OCNs can be

converted to, the inclusion problem is known to be undecidable.

Organisation of the paper Section 2 contains preliminaries where we introduce

notation and deﬁne the concepts mentioned above rigorously. In Section 3, we

show PSPACE-completeness of checking if an input OCN is history-deterministic.

In Section 4, we show that the language expressed by history-deterministic one-

counter nets are contained in the language accepted by deterministic one-counter

automata. Moreover, we discuss the complexity of checking language-inclusion,

language-equivalence and universality of history-deterministic nets. Finally, in

the Section 5, we analyse the changes in complexity when the counters are rep-

resented succinctly, or if zero tests are added. Due to space constraints, missing

proofs can be found in the appendix.

2 Preliminaries

We use Σthroughout to denote a ﬁnite set of alphabet, and Σ∗to denote the

set of all ﬁnite words consisting of letters from Σ. The empty word over Σshall

be denoted by . We use Σto denote the set Σ∪ {}. A language Lover Σis

a subset of Σ∗.

Labelled Transition System Alabelled transition system (LTS) is a tuple Scon-

sisting of S= (Q, Σ,!, q0, F ). In this paper, we assume that Qis a (countable)

set of states, q0∈Qis the initial state, F⊆Qis the set of ﬁnal states, Σis a

ﬁnite alphabet, !⊆Q×Σ×Qis the set of transitions.

If a a transition (q1, a, q2)belongs to !, we instead represent it as q1

−! q2

as well. On a (ﬁnite) word w, a ρis said to be a (ﬁnite) run of the labelled

transition system Aif it is an (ﬁnite) alternating sequence of states and letters

of Σ:ρ=q0

−! q1

−! . . . qk−1

−! qk, where each qi

−! qi+1 ∈!and

a0·a1. . . ak=wand ai∈Σ. A run ρdescribed above is accepting if the state

qk∈F.

An LTS that has no -transitions is said to be a realtime LTS. For an LTS

S= (Q, Σ, !, q0, F )being realtime, we have !⊆Q×Σ×Q. Unless men-

tioned otherwise, we mostly deal with realtime LTS for the sake of a simpler

presentation.

An LTS S= (Q, Σ, !, q0, F )is deterministic if !is a function from Q×Σ

to Q, and not just a relation.

Two player games Throughout the paper, we will be using two player games on

countably sized arenas, between the players Adam and Eve, denoted by ∀

∀

∀and

∃

∃respectively. The winning condition will be a reachability condition for one of

the players, often ∀

∀

∀. By the work of Martin [27], we know that such games are

determined, that is they have a winner, which is either ∀

∀

∀or ∃

∃

∃. Moreover, each of

the players have a positional strategy, where their current strategy depends on

4 A. Prakash, K. S. Thejaswini

their positions in the current arena. We shall say that two games are equivalent,

if they have the same winner.

One-Counter Automata Aone-counter automaton (OCA) Ais given by a tuple

A= (Q, Σ, ∆, q0, F ), where Qis a ﬁnite set of states, q0∈Qis the initial state,

F⊆Qis the set of ﬁnal states, Σis a ﬁnite alphabet, and ﬁnally, ∆is the set

of transitions, given as a relation ∆⊆Q× {zero,¬zero} × Σ× {−1,0,1} × Q.

Here, the symbols zero and ¬zero are used to distinguish between transitions

that can happen when the counter value is 0, and when the counter value is

positive respectively. One can think of the counter as a ‘stack’, where the stack

has a distinguished bottom-of-the-stack symbol, which cannot be popped. The

conﬁgurations in the automaton are given by pairs (q, m), where qdenotes the

current state, and m∈N0denotes the counter value. We use C(A)to denote the

set of conﬁgurations of A.

A one-counter automaton can be viewed as a succinct description of an

inﬁnite-state LTS over the set of conﬁgurations, such that the conﬁgurations

are as deﬁned below. For each conﬁguration (q, m), upon reading a∈Σ,

–if m > 0, takes a transition of the form (q, ¬zero, a, d, q0), where d∈ {−1,0,1}

to (q0, m +d);

–if m= 0, takes a transition of the form (q, zero, a, d, q0), where d∈ {0,1}to

(q0, m +d).

For two conﬁgurations c, c0∈ C(A) = Q×N0, we use the notation ca,d

−−! c0

to denote the fact that c0can be reached from cupon taking some transition

δ∈∆upon reading a, with a change of counter value d. We shall also say that

ca,d

−−! c0is a transition in A, as ca,d

−−! c0is a transition in the inﬁnite LTS of

A. We thus view Aas both an automaton and a LTS, and switch between these

two notions interchangeably. A run of Aover a word wis a ﬁnite sequence of

alternating conﬁgurations and transitions : ρ=c0

a0,d0

−−−! c1· · · cn

an,dn

−−−−! cn+1

such that a0a1· · · an=w, and c0= (q0,0). The run ρis an accepting run if its

last conﬁguration cn+1 = (qn+1, kn+1)is accepting, i.e. qn+1 ∈F. We say a word

wis an accepting word in Aif it has an accepting run in A. Finally, we deﬁne the

language of A, denoted by L(A)to be the set of all accepting words in A. We

say that a one-counter automaton Ais a deterministic one-counter automaton,

if ∆is a (partial) function from Q× {zero,¬zero} × Σto {−1,0,1} × Q.

One-counter nets The model of one-counter nets (OCNs) can be interpreted as

a restriction added to one-counter automaton that do not have the ability to

test for zero. Alternatively, one can view this as a ﬁnite-state automaton that

has access to a stack which can store only one symbol and no bottom-of-the-

stack element. Any feasible run cannot pop an empty stack. More formally, a

one-counter net Nis a tuple (Q, Σ, ∆, q0, F )where Qis the set of ﬁnite states,

Σis a ﬁnite alphabet, q0∈Qis the initial state and F⊆Qis the set of ﬁnal or

accepting states. The set ∆⊆Q×Σ× {−1,0,1} × Qare the transitions in the

net N.

On History-Deterministic One-Counter Nets 5

The conﬁgurations of an OCN are similar to that of an OCA. It consists of

a pair (q, n)∈Q×N. We shall use the notation C(N) = Q×Nto denote the

set of conﬁgurations of N. From a conﬁguration (q, n), we reach a conﬁguration

(p, n +d)in one step, if there is a transition δ= (q, a, d, p), for some a∈Σand

d∈ {−1,0,+1}and n+d≥0. We can deﬁne a run on an OCN, an accepting run

and an accepting word similar to an OCA. We shall say an OCN Nis complete, if

for every conﬁguration c∈ C(N)and every letter a∈Σ, there exists a transition

ca,d

−−! c0.

Remark 1. For the most of the paper we talk about one-counter nets (automata)

with unary transitions, i.e. transitions that increment or decrement the counter

by at most 1. However, they are as expressive as succinct models where the

transitions are given in binary. This can be observed, for instance, by giving a

construction similar to that of Valiant’s for deterministic pushdown automata

(Section 1.7, [30]).

History-Deterministic One-Counter Nets We deﬁne history-determinism in the

setting of one-counter net. We say an OCN Nis history-deterministic, if the

non-deterministic choices required to accept a word wwhich is in L(N)can be

made on-the-ﬂy. These choices depend only on the word read so far, and do not

require the knowledge of the future of the word to construct an accepting run

for a word in L(N)(hence the term history-determinism). Formally, we say an

OCN Nis history-deterministic, if ∃

∃

∃wins the letter game on Ndeﬁned below.

Deﬁnition 2 (Letter game for OCN). Given an OCN N= (Q, Σ, ∆, q0, F ),

the letter game on Nis deﬁned between the players ∀

∀

∀and ∃

∃

∃as follows: the

positions of the game are C(N)×Σ∗, with the initial position ((q0,0), ). At

round iof the play, where the position is (ci, wi):

–∀

∀

∀selects ai∈Σ

–∃

∃

∃selects a transition δwhich can be taken at the conﬁguration cion reading

ai, i.e. ci

ai,di

−−−! ci+1

If ∃

∃

∃is unable to choose a transition (i.e. there is no aitransition at the conﬁg-

uration ciin the LTS generated by the net N), and wi+1 =wiaiis the preﬁx

of an accepting word, ∃

∃

∃loses immediately. The player ∀

∀

∀wins immediately when

the word wi+1is accepting but the conﬁguration ci+1 is not at an accepting state,

and the game terminates. The game continues from (ci+1, wi+1)otherwise. The

player ∃

∃

∃wins any inﬁnite play.

We say a strategy for ∃

∃

∃in the letter game of Nis a resolver for N, if it is a

winning strategy for ∃

∃

∃in the letter game.

Our characterization of history-deterministic one-counter nets by the above

letter game is slightly diﬀerent from the one presented in the work of Guha,

Jecker, Lehtinen and Zimmermann [13] for pushdown automata. In their work,

they deﬁne history-determinism as having a consistent strategy based on the

transitions taken so far. It is easy to argue that these two deﬁnitions are equiv-

alent.

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

OnHistory-DeterministicOne-CounterNetsAdityaPrakash1andK.S.Thejaswini1DepartmentofComputerScience,UniversityofWarwick{aditya.prakash,thejaswini.raghavan.1}@warwick.ac.ukAbstract.Weconsiderthemodelofhistory-deterministicone-counternets(OCNs).History-determinismisapropertyoftransitionsystemsthatallows...

展开>> 收起<<

On History-Deterministic One-Counter Nets Aditya Prakash1and K. S. Thejaswini1 Department of Computer Science University of Warwick.pdf

共44页,预览5页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

On History-Deterministic One-Counter Nets Aditya Prakash1and K. S. Thejaswini1 Department of Computer Science University of Warwick

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: