About VaChe

VaChe is a prototype toolbox for VASS under the process semantics which is built on TINA for reachability properties and Mona for MSO model-checking.

This toolbox includes :

• A tool for the edition and reachability analysis of VASS under the process semantics.
• A tool for the model-checking of bounded Petri nets against MSO formulae over processes.