PV2 ⊧ AMYTISSsynthesises a spec-conforming controller from a Markov decision process

Application domain/field

• Stochastic systems
• Discrete-time stochastic systems

Type of tool

Synthesis tool

Expected input

Configuration file that describes a stochastic system (Markov Decision Process) with difference equations.

Format:

Plaintext file (the configuration options are described on Github)

Expected output

Controller that adheres to safety, reachability or reach-avoid specifications.

Internals

Uses pFaces

Comments

Tool for designing correct-by-construction controllers for large-scale discrete-time stochastic systems