On the containment problem for deterministic multicounter machine models

Óscar H. Ibarra

doi:10.1016/j.ic.2025.105383

Return

On the containment problem for deterministic multicounter machine models

2025-11-01

Óscar H. Ibarra

Ian McQuillan *

DOI：10.1016/j.ic.2025.105383

Original

Save

View PDF

Abstract

En 中文

A new model of multicounter machines is introduced where testing the counter status of a counter is optional, rather than existing models where they are always either required (traditional multicounter machines) or no status can be checked (partially-blind multicounter machines). If, in every accepting computation, each counter has a bounded number of occurrences where its status is tested and verified to be zero, then the machine is called finite-testable. One-way nondeterministic finite-testable multicounter machines are shown to be equivalent to partially-blind multicounter machines. However, oneway deterministic finite-testable multicounter machines are strictly more powerful than deterministic partially-blind machines. Interestingly, one-way deterministic finite-testable multicounter machines are shown to have a decidable containment problem. This makes it the most general known model where this problem is decidable, making the class important in the areas of model checking and formal verification. We also study properties of their reachability sets. (c) 2025 The Authors. Published by Elsevier Inc. This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/4.0/).

Keywords:

Multicounter machines

Determinism

Containment

Vector addition systems

Petri nets

AI Summary

Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.