@article{HOFMAN201850,
    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 counter-values as part of the input. Secondly, we show that the trace universality problem of nondeterministic OCN, which is equivalent to checking trace inclusion between a finite system and a OCN-process, is Ackermann-complete.},
    Author = {Hofman, Piotr and Totzke, Patrick},
    File = {Trace inclusion for one-counter nets revisited - 1-s2.0-S0304397517303961-main - a - a - g.pdf},
    ISSN = {0304-3975},
    Journal = {Theoretical Computer Science},
    Keywords = {Counter-automata, Vector addition systems, Equivalence checking},
    Note = {Reachability Problems 2014: Special Issue},
    Pages = {50 - 63},
    Title = {Trace inclusion for one-counter nets revisited},
    URL = {http://www.sciencedirect.com/science/article/pii/S0304397517303961},
    Volume = {735},
    Year = {2018},
    bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/S0304397517303961},
    bdsk-url-2 = {https://doi.org/10.1016/j.tcs.2017.05.009},
    date-added = {2020-03-03 17:30:45 +0100},
    date-modified = {2020-03-03 17:30:45 +0100},
    doi = {10.1016/j.tcs.2017.05.009}
}

@article{HOFMAN201850, 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 counter-values as part of the input. Secondly, we show that the trace universality problem of nondeterministic OCN, which is equivalent to checking trace inclusion between a finite system and a OCN-process, is Ackermann-complete.}, Author = {Hofman, Piotr and Totzke, Patrick}, File = {Trace inclusion for one-counter nets revisited - 1-s2.0-S0304397517303961-main - a - a - g.pdf}, ISSN = {0304-3975}, Journal = {Theoretical Computer Science}, Keywords = {Counter-automata, Vector addition systems, Equivalence checking}, Note = {Reachability Problems 2014: Special Issue}, Pages = {50 - 63}, Title = {Trace inclusion for one-counter nets revisited}, URL = {http://www.sciencedirect.com/science/article/pii/S0304397517303961}, Volume = {735}, Year = {2018}, bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/S0304397517303961}, bdsk-url-2 = {https://doi.org/10.1016/j.tcs.2017.05.009}, date-added = {2020-03-03 17:30:45 +0100}, date-modified = {2020-03-03 17:30:45 +0100}, doi = {10.1016/j.tcs.2017.05.009} }