Trace Inclusion for One-Counter Nets Revisited

Piotr Hofman, Patrick Totzke

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish
Title of host publicationReachability Problems
Subtitle of host publication8th International Workshop, RP 2014, Oxford, UK, September 22-24, 2014. Proceedings
EditorsJoël Ouaknine, Igor Potapov, James Worrell
Place of PublicationCham
PublisherSpringer International Publishing
Pages151-162
Number of pages12
ISBN (Electronic)978-3-319-11439-2
ISBN (Print)978-3-319-11438-5
DOIs
Publication statusPublished - 2014

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing
Volume8762
ISSN (Print)0302-9743

Fingerprint

Dive into the research topics of 'Trace Inclusion for One-Counter Nets Revisited'. Together they form a unique fingerprint.

Cite this