2014/04/21 by Piotr Hofman, Hofman, Piotr, Patrick Totzke +1 · 1 citation
Computer Science · Social Sciences · #Access Control and Trust #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Petri Nets in System Modeling #cs.LO
paper · pdf · doi:10.48550/arxiv.1404.5157
openalex publication_date 2014/04/21 · arxiv created 2015/04/19 · arxiv updated 2015/04/21 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.