We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

cs

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo

Computer Science > Logic in Computer Science

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.
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.
Subjects: Logic in Computer Science (cs.LO)
Cite as: arXiv:1404.5157 [cs.LO]
  (or arXiv:1404.5157v2 [cs.LO] for this version)

Submission history

From: Piotr Hofman [view email]
[v1] Mon, 21 Apr 2014 10:14:13 GMT (539kb,D)
[v2] Sun, 19 Apr 2015 14:57:45 GMT (182kb,D)

Link back to: arXiv, form interface, contact.