zinoex / intervalmdp.jl

GPU-accelerated value iteration for Interval Markov Decision Processes

IntervalMDP.jl - Interval Markov Decision Processes

IntervalMDP.jl is a Julia package for modeling and certifying Interval Markov Decision Processes (IMDPs) via Value Iteration.

IMDPs are a generalization of Markov Decision Processes (MDPs) where the transition probabilities are represented by intervals instead of point values, to model uncertainty. IMDPs are also frequently chosen as the model for abstracting the dynamics of a stochastic system, as one may compute upper and lower bounds on transitioning from one region to another.

The aim of this package is to provide a user-friendly interface to solve value iteration for IMDPs with great efficiency. Furthermore, it provides methods for accelerating the computation of the certificate using CUDA hardware.

Features

• O-maximization and value iteration
• Dense and sparse matrix support
• Parametric probability types for customizable precision
• Multithreaded CPU and CUDA-accelerated value iteration
• Data loading and writing in formats by various tools (PRISM, bmdp-tool, IMDP.jl)

Installation

This package requires Julia v1.9 or later. Refer to the official documentation on how to install it for your system.

To install IntervalMDP.jl, use the following command inside Julia's REPL:

julia> import Pkg; Pkg.add("IntervalMDP")

If you want to use the CUDA extension, you also need to install CUDA.jl:

julia> import Pkg; Pkg.add("CUDA")

Usage

Here is an example of how to use the package to solve a finite horizon reachability problem for an Interval Markov Chain (IMC) with 3 states and 1 initial state. The goal is to compute the maximum pessimistic probability of reaching state 3 within 10 time steps.

using IntervalMDP

# IMC
prob = IntervalProbabilities(;
    lower = [
        0.0 0.5 0.0
        0.1 0.3 0.0
        0.2 0.1 1.0
    ],
    upper = [
        0.5 0.7 0.0
        0.6 0.5 0.0
        0.7 0.3 1.0
    ],
)

initial_states = [1]  # Initial states are optional
imc = IntervalMarkovChain(prob, initial_states)

target_set = [3]
prop = FiniteTimeReachability(target_set, 10)  # Time steps
spec = Specification(prop, Pessimistic, Maximize)
problem = Problem(imc, spec)

# Solve
V, k, residual = value_iteration(problem)

See Usage for more information about different specifications, using sparse matrices, and CUDA.

Copyright notice

Technische Universiteit Delft hereby disclaims all copyright interest in the program “IntervalMDP.jl” (GPU-accelerated value iteration for Interval Markov Decision Processes) written by the Frederik Baymler Mathiesen. Fred van Keulen, Dean of Mechanical Engineering.

© 2024, Frederik Baymler Mathiesen, HERALD Lab, TU Delft

intervalmdp.jl's Issues

CUDA parallel sorting

Instead of the "populate subsets" approach, try to see if the following yields more performance:

1. For each state
   1. Select subsets of the value function corresponding the non-zero
   2. Sort local permutation according subset
   3. Assign probabilities

Each of these can possibly be a different kernel.

Improve device error messages

The CUDA error messages when only the system or the spec is on a the GPU are barely understandable. Add an short circuit check that gives the user a more meaningful message. This can be done at problem construction similar to other spec checks.

IMDP

Extend IVI to IMDPs.

• Verification
• Control synthesis

Automatically adapt CUDA kernel launch configuration

Use the CUDA.jl launch_configuration for optimal configuration of threads and blocks.

Rational number support

Composition of IntervalMarkovProcesses

• Parallel
• Serial

Incremental contruction of IMDP/IMC

When constructing an IMDP for anything but simple models, you want to avoid dense matrices and sparsify them after. Instead, you would want to construct it sparsely directly. However, this can be very inefficient, depending on sparse formats and the order in which indices are added. For this reason, make a specialized, fast procedure to construct a sparse IMDP incrementally.

TagBot trigger issue

This issue is used to trigger TagBot; feel free to unsubscribe.

If you haven't already, you should update your TagBot.yml to include issue comment triggers.
Please see this post on Discourse for instructions and more details.

If you'd like for me to do this for you, comment TagBot fix on this issue.
I'll open a PR within a few hours, please be patient!

Test asserts

The library contains many asserts, but they remain largely untested. Add unit tests triggering asserts to ensure they assert the correct conditions. Additionally, some of the asserts should possibly be DomainErrors instead.

Analyze CUDA performance trace for small arrays

Use view and reshape to avoid allocating memory

• Dense
• Sparse
• CUDA

Remove Vector of StateIntervalProbabilities

StateIntervalProbabilities is massively complicates the code with specializations, and is inefficient. Therefore, I think we should remove it as an option.

Control synthesis

Test device check

Update symbols for parametric types

Switch from R and T to Tv and Ti for types that have a value and index type.

Apply policy to IMDP to obtain IMC

Analyze if more threads for probability assignment on CUDA is more efficient

Reward optimization

Translate LTLf to reachability

Construct product IMC of the LTLf automaton and the input IMC to certify LTLf using reachability.

Test Interval Value Iteration

• Sparse
• CUDA

O-maximization for dense CUDA matrices

Implementation of:

• CuDenseOrdering
• sort_states
• probability_assignment
• interval_value_iteration

Testing:

• O-maximization
• Partial O-maximization
• O-minimization
• interval_value_iteration
• Large matrices

Read bmdp-tool into an IntervalMarkovChain if num_actions == 1

SparseOrdering to CuSparseOrdering adaptor