Arrow Research search

Author name cluster

Piotr Hofman

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers
1 author row

Possible papers

4

Highlights Conference 2022 Conference Abstract

Language Inclusion for Boundedly-Ambiguous Vector Addition Systems is Decidable

  • Piotr Hofman

We consider the problems of language inclusion and language equivalence for Vector Addition Systems with States (VASSes) with the acceptance condition defined by the set of accepting states (and more generally by some upward-closed conditions). In general, the problem of language equivalence is undecidable even for one-dimensional VASSes, thus to get decidability we investigate restricted subclasses. On one hand, we show that the problem of language inclusion of a VASS in k-ambiguous VASS (for any natural k) is decidable and even in Ackermann. On the other hand, we prove that the language equivalence problem is Ackermann-hard already for deterministic VASSes. These two results imply Ackermann-completeness for language inclusion and equivalence in several possible restrictions. Some of our techniques can be also applied in much broader generality in infinite-state systems, namely for some subclass of well-structured transition systems. The whole paper is here: https: //arxiv. org/abs/2202. 08033 and it is currently submitted to LICS.

Details

TCS Journal 2018 Journal Article

Trace inclusion for one-counter nets revisited

  • Piotr Hofman
  • Patrick Totzke

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.

Details DOI

Highlights Conference 2013 Conference Abstract

Decidability of weak simulation on one-counter nets

  • Piotr Hofman
  • Richard Mayr
  • Patrick Totzke

One-counter nets (OCN) are Petri nets with exactly one unbounded place. They are equivalent to a subclass of one-counter automata with only a weak test for zero. We show that weak simulation preorder is decidable for OCN. In contrast, other semantic relations like weak bisimulation are undecidable for OCN, and so are weak (and strong) trace inclusion.

PDF Details
v2026.09.13