Model Checking Coverability Graphs of Vector Addition Systems
Sylvain Schmitz (LSV, Cachan)
Info
|
Date |
18th April 2012 (week 0, Trinity Term 2012) |
|
Time |
11:30 |
|
Place |
147 |
Abstract
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.)
Further info
|
Related series |
|
