Inclusion Problems for One-Counter Systems
We study the decidability and complexity of verification problems for infinite-state systems.
A fundamental question in formal verification is if the behaviour of one process is reproducible by another. This inclusion problem can be studied for various models of computation and behavioural preorders. It is generally intractable or even undecidable already for very limited computational models.
The aim of this work is to clarify the status of the decidability and complexity of some well-known inclusion problems for suitably restricted computational models. In particular, we address the problems of checking strong and weak simulation and trace inclusion for processes definable by one-counter automata (OCA), that consist of a finite control and a single counter ranging over the non-negative integers. We take special interest of the subclass of one-counter nets (OCNs), that cannot fully test the counter for zero and which is subsumed both by pushdown automata and Petri nets / vector addition systems.
Our new results include the PSPACE-completeness of strong and weak simulation, and the undecidability of trace inclusion for OCNs. Moreover, we consider semantic preorders between OCA/OCN and finite systems and close some gaps regarding their complexity. Finally, we study deterministic processes, for which simulation and trace inclusion coincide.
Errata
- p43, Theorem 4.12: The value of \(C\) should actually be the maximal length of an acyclic path in the product graph of \(N\) and \(N'\) plus \(1\), ie., the length of the shortest simple cycle in the product.
- p47, par4,l-1: There are no more than \(2^{K W 3}\) pairwise different cross-sections.
- p114, Figure 7.3: The transitions in the \(c\)-cycle on the left automaton should all have effect \(1\).