STV+Reductions

This is the second alpha version of the STV model checker demonstration tool.

This version includes the following functionalities:

• verification of strategic abilities under imperfect information using approximation methods
• strategy synthesis using DominoDFS algorithm
• model reduction based on the partial order reductions algorithm
• bisimulation checking
• model generation based on a simplified input language specification

Requirements:

• Python 3.7 or newer, installed and available in the PATH

Usage

Windows

• Download the zipped package stv-v0.2-alpha-win32-x64.zip
• Unzip the downloaded package into stv-v0.2-alpha-win32-x64
• Open stv-v0.2-alpha-win32-x64/app
• Launch stv.exe
• Example input models are located in stv-v0.2-alpha-win32-x64/examples

Linux

• Download the zipped package stv-v0.2-alpha-linux-x64.zip
• Unzip the downloaded package into stv-v0.2-alpha-linux-x64
• Open terminal and go to stv-v0.2-alpha-linux-x64.zip/app
• Run ./stv
• Example input models are located in stv-v0.2-alpha-linux-x64/examples