Skip to main content

Model Checking Coverability Graphs of Vector Addition Systems

Sylvain Schmitz ( LSV, Cachan )

We propose a different unifying framework for expressing properties on VAS using their coverability graph. We introduce for this an extension of CTL allowing to express such properties, and show decidability and even ExpSpace-completeness for the VAS model-checking problem of some fragments. (Joint work with Michel Blockelet.)

Share this: