Future Algorithm Changes and Work

This page is a work in progress

Dynamic Programming Improvements

This version of the algorithm will produce the exact same output as STAMINA 2.0, but will prevent re-exploration of states.

Priority Queue on Estimated Reachability

This idea is extremely simple and would be easy to implement, except for one small thing: the SparseMatrixBuilder class in STORM seems to only want to insert at indecies higher than what have already been inserted! This means I cannot insert state index 6 followed by 4, but must insert 4, then 5, then 6.

Heuristic BFS

Either a naive BFS or a priority queue on estimated reachability which assumes that probability window falls off exponentially with some parameter λ. Checks a number of times with extremely small models to estimate that λ, then attempts to explore to n states (where the regression predicted Pmax - Pmin < w), and repeats until it does.