Model Checking Vector Addition Systems with one zero-test

DOI10.2168/LMCS-8(2:11)2012zbMath1242.68196arXiv1205.4458MaRDI QIDQ2895472

Rémi Bonnet, Jérôme Leroux, Marc Zeitoun, Alain Finkel

Publication date: 3 July 2012

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1205.4458

zbMATH Keywords

boundednessreachabilitycoverzero-testvector addition systemKarp-Miller algorithmLTL model-checkingplace boundedness

Mathematics Subject Classification ID

Computability and recursion theory (03D99) Discrete mathematics in relation to computer science (68R99)

Related Items

An Approach to Computing Downward Closures ⋮ A Note on Decidable Separability by Piecewise Testable Languages ⋮ Coverability and Termination in Recursive Petri Nets ⋮ On Petri Nets with Hierarchical Special Arcs ⋮ Coverability, Termination, and Finiteness in Recursive Petri Nets

This page was built for publication: Model Checking Vector Addition Systems with one zero-test