refine_plan.algorithms.semi_mdp_solver

Functions which solve a semi-MDP into storm and retrieve the policy.

Author: Charlie Street Owner: Charlie Street

Module Contents

Functions

synthesise_policy(semi_mdp[, prism_prop])

Solve a semi-MDP and return the policy.
refine_plan.algorithms.semi_mdp_solver.synthesise_policy(semi_mdp, prism_prop='Rmax=?[F "goal"]')

Solve a semi-MDP and return the policy.

Note that stormpy can only handle reachability properties.

Parameters:

  • semi_mdp – The semiMDP

  • prism_prop – The property to solve for (must be reachability-based)

Returns:

A policy with the value function included

Raises:

solution_exception – Raised if issue arises with model checking result