zinoex/intervalmdp.jl

GPU-accelerated value iteration for Interval Markov Decision Processes

intervalmdp.jl's Issues

Test Interval Value Iteration

• Sparse
• CUDA

Automatically adapt CUDA kernel launch configuration

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

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

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.

Control synthesis

Apply policy to IMDP to obtain IMC

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!

SparseOrdering to CuSparseOrdering adaptor

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.

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.

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.

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

IMDP

Extend IVI to IMDPs.

• Verification
• Control synthesis

Reward optimization

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

Translate LTLf to reachability

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

Rational number support

Update symbols for parametric types

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

Use view and reshape to avoid allocating memory

• Dense
• Sparse
• CUDA

Analyze CUDA performance trace for small arrays