Trace Inclusion for One-Counter Nets Revisited

Piotr Hofman; Patrick Totzke

doi:10.1007/978-3-319-11439-2_12

Trace Inclusion for One-Counter Nets Revisited

Piotr Hofman, Patrick Totzke

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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.
We show that trace inclusion between a OCN and a deterministic OCN is NL-complete, even with arbitrary binary-encoded initial countervalues as part of the input. Secondly, we show that the the trace universality problem of nondeterministic OCN, which is equivalent to checking trace inclusion between a finite and a OCN-process, is Ackermann-complete.

Original language	English
Title of host publication	Reachability Problems
Subtitle of host publication	8th International Workshop, RP 2014, Oxford, UK, September 22-24, 2014. Proceedings
Editors	Joël Ouaknine, Igor Potapov, James Worrell
Place of Publication	Cham
Publisher	Springer
Pages	151-162
Number of pages	12
ISBN (Electronic)	978-3-319-11439-2
ISBN (Print)	978-3-319-11438-5
DOIs	https://doi.org/10.1007/978-3-319-11439-2_12
Publication status	Published - 2014

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer International Publishing
Volume	8762
ISSN (Print)	0302-9743

Access to Document

10.1007/978-3-319-11439-2_12

HT2014Accepted author manuscript, 347 KB

http://link.springer.com/chapter/10.1007%2F978-3-319-11439-2_12

Cite this

@inproceedings{172dbc6cd3ec49f8bd3c4f44bebadf12,

title = "Trace Inclusion for One-Counter Nets Revisited",

abstract = "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. We show that trace inclusion between a OCN and a deterministic OCN is NL-complete, even with arbitrary binary-encoded initial countervalues as part of the input. Secondly, we show that the the trace universality problem of nondeterministic OCN, which is equivalent to checking trace inclusion between a finite and a OCN-process, is Ackermann-complete.",

author = "Piotr Hofman and Patrick Totzke",

year = "2014",

doi = "10.1007/978-3-319-11439-2\_12",

language = "English",

isbn = "978-3-319-11438-5",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "151--162",

editor = "Jo{\"e}l Ouaknine and Igor Potapov and James Worrell",

booktitle = "Reachability Problems",

address = "United Kingdom",

}

Trace Inclusion for One-Counter Nets Revisited. / Hofman, Piotr; Totzke, Patrick.
Reachability Problems: 8th International Workshop, RP 2014, Oxford, UK, September 22-24, 2014. Proceedings. ed. / Joël Ouaknine; Igor Potapov; James Worrell. Cham: Springer, 2014. p. 151-162 (Lecture Notes in Computer Science; Vol. 8762).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Trace Inclusion for One-Counter Nets Revisited

AU - Hofman, Piotr

AU - Totzke, Patrick

PY - 2014

Y1 - 2014

N2 - 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. We show that trace inclusion between a OCN and a deterministic OCN is NL-complete, even with arbitrary binary-encoded initial countervalues as part of the input. Secondly, we show that the the trace universality problem of nondeterministic OCN, which is equivalent to checking trace inclusion between a finite and a OCN-process, is Ackermann-complete.

AB - 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. We show that trace inclusion between a OCN and a deterministic OCN is NL-complete, even with arbitrary binary-encoded initial countervalues as part of the input. Secondly, we show that the the trace universality problem of nondeterministic OCN, which is equivalent to checking trace inclusion between a finite and a OCN-process, is Ackermann-complete.

U2 - 10.1007/978-3-319-11439-2_12

DO - 10.1007/978-3-319-11439-2_12

M3 - Conference contribution

SN - 978-3-319-11438-5

T3 - Lecture Notes in Computer Science

SP - 151

EP - 162

BT - Reachability Problems

A2 - Ouaknine, Joël

A2 - Potapov, Igor

A2 - Worrell, James

PB - Springer

CY - Cham

ER -

Trace Inclusion for One-Counter Nets Revisited

Abstract

Publication series

Access to Document

Fingerprint

Cite this