Skip to content

Latest commit

 

History

History
30 lines (18 loc) · 1.87 KB

README.md

File metadata and controls

30 lines (18 loc) · 1.87 KB

POMDPModelChecking.jl

Build Status CodeCov

This package provides support for performing verification and policy synthesis in POMDPs from LTL formulas. It relies on POMDPs.jl for expressing the model and Spot.jl for manipulating LTL formulas.

If this package is useful to you, consider citing: M. Bouton, J. Tumova, and M. J. Kochenderfer, "Point-Based Methods for Model Checking in Partially Observable Markov Decision Processes," in AAAI Conference on Artificial Intelligence (AAAI), 2020.

Installation

using Pkg
Pkg.add("POMDPModelChecking")

Notes

This package exports two solvers: ReachabilitySolver and ModelCheckingSolver. Those solvers are intended to be used on models implemented with POMDPs.jl, please refer to the POMDPs.jl documentation to learn how to implement a POMDP or MDP model using the correct interface.

Interface with Storm :

A writer is already written to convert MDP to the good format, a solver interface has been prototyped, relying on the python library stormpy. The files are in the legacy/ folder but are only experimental for now.

Disclaimer

This is still work in progress and could be improved a lot, please submit issues if you encounter. Contributions and PR welcome!