3 results
Michael Blondin ; Alain Finkel ; Pierre McKenzie.
The well-quasi-ordering (i.e., a well-founded quasi-ordering such that all antichains are finite) that defines well-structured transition systems (WSTS) is shown not to be the weakest hypothesis that implies decidability of the coverability problem. We show coverability decidable for monotone […]
Published on September 13, 2017
Michael Blondin ; Christoph Haase ; Filip Mazowiecki ; Mikhail Raskin.
We study the reachability problem for affine $\mathbb{Z}$-VASS, which are integer vector addition systems with states in which transitions perform affine transformations on the counters. This problem is easily seen to be undecidable in general, and we therefore restrict ourselves to affine […]
Published on July 20, 2021
Michael Blondin ; Mikhail Raskin.
Vector addition systems with states (VASS) are widely used for the formal verification of concurrent systems. Given their tremendous computational complexity, practical approaches have relied on techniques such as reachability relaxations, e.g., allowing for negative intermediate counter values. It […]
Published on July 20, 2021