MSL Toolbox

MSL Toolbox

Description: The MSL (Maximal Satisfiability LTL) toolbox automatically generates an optimal control policy for a Markov Decision Process (MDP) that maximizes the probability of satisfying a Linear Temporal Logic (LTL) formula. For more detail of the algorithm that produces the policy, please see [1]. Note in [1] we model the system with probabilistic observations and convert the system model to an MDP, we then use this software to generate the policy. This software calls open source software [2] and [3].

Requirements:

- Mac OS X 10.6, Linux and Windows (Linux and Windows should work, but let me know if there is any issue)
- MATLAB 2010b or later with Bioinformatics toolbox (for SCC computation)

VO Integration: No

Active: N/A

Available Benchmarks: No

Website: http://sites.bu.edu/hyness/maximal_sat-ltl/

Download: MSL package

Documentation: See "How to Use" section of webpage.

Contact: HyNeSs Lab: Xu Chu (Dennis) Ding, Stephen L. Smith, Calin Belta, and Daniela Rus

Excerpt from: http://sites.bu.edu/hyness/maximal_sat-ltl/