Zinoex · Zinoex · Aug 29, 2025 · Aug 31, 2025 · Aug 31, 2025 · Sep 1, 2025
diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
@@ -26,7 +26,7 @@ jobs:
       fail-fast: false
       matrix:
         version:
-          - '1.10'
+          - '1.11'
           - 'nightly'
         os:
           - ubuntu-latest

diff --git a/.github/workflows/FormatCheck.yml b/.github/workflows/FormatCheck.yml
@@ -13,7 +13,7 @@ jobs:
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
-        julia-version: [1.10.0]
+        julia-version: [1.11.0]
         julia-arch: [x86]
         os: [ubuntu-latest]
     steps:
@@ -23,11 +23,8 @@ jobs:
 
       - uses: actions/checkout@v4
       - name: Install JuliaFormatter and format
-        # This will use the latest version by default but you can set the version like so:
-        #
-        # julia  -e 'using Pkg; Pkg.add(PackageSpec(name="JuliaFormatter", version="0.13.0"))'
         run: |
-          julia  -e 'using Pkg; Pkg.add(PackageSpec(name="JuliaFormatter", version="1.0.62"))'
+          julia  -e 'using Pkg; Pkg.add(PackageSpec(name="JuliaFormatter", version="2.1.6"))'
           julia  -e 'using JuliaFormatter; format(".", verbose=true)'
       - name: Format check
         run: |

diff --git a/.github/workflows/documentation.yml b/.github/workflows/documentation.yml
@@ -19,7 +19,7 @@ jobs:
       - uses: actions/checkout@v4
       - uses: julia-actions/setup-julia@v2
         with:
-          version: '1.10'
+          version: '1.11'
       - uses: julia-actions/cache@v2
       - name: Install dependencies
         run: julia --project=docs/ -e 'using Pkg; Pkg.develop(PackageSpec(path=pwd())); Pkg.instantiate()'

diff --git a/Project.toml b/Project.toml
@@ -5,10 +5,13 @@ version = "0.6.0"
 
 [deps]
 CommonSolve = "38540f10-b2f7-11e9-35d8-d573e4eb0ff2"
+HiGHS = "87dc4568-4c63-4d18-b0c0-bb2238e4078b"
 JSON = "682c06a0-de6a-54ab-a142-c8b1cf79cde6"
+JuMP = "4076af6c-e467-56ae-b986-b466b2749572"
 LinearAlgebra = "37e2e46d-f89d-539d-b4ee-838fcccc9c8e"
 NCDatasets = "85f8d34a-cbdd-5861-8df4-14fed0d494ab"
 SparseArrays = "2f01184e-e22b-5df5-ae63-d93ebab69eaf"
+StyledStrings = "f489334b-da3d-4c2e-b8f0-e476e12c162b"
 
 [weakdeps]
 Adapt = "79e6a3ab-5dfb-504d-930d-738a2a938a0e"
@@ -21,13 +24,16 @@ IntervalMDPCudaExt = ["Adapt", "CUDA", "GPUArrays", "LLVM"]
 
 [compat]
 Adapt = "4"
-CUDA = "5.1"
+CUDA = "5.9.1"
 CommonSolve = "0.2.4"
 GPUArrays = "10, 11"
+HiGHS = "1.19.0"
 JSON = "0.21.4"
+JuMP = "1.29.0"
 LLVM = "7, 8, 9"
 NCDatasets = "0.13, 0.14"
-julia = "1.9"
+StyledStrings = "1.0.3"
+julia = "1.11"
 
 [extras]
 Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"

diff --git a/README.md b/README.md
@@ -4,23 +4,28 @@
 [![Build Status](https://github.com/zinoex/IntervalMDP.jl/actions/workflows/CI.yml/badge.svg?branch=main)](https://github.com/zinoex/IntervalMDP.jl/actions/workflows/CI.yml?query=branch%3Amain)
 [![Codecov](https://codecov.io/gh/Zinoex/IntervalMDP.jl/graph/badge.svg?token=K62S0148BK)](https://codecov.io/gh/Zinoex/IntervalMDP.jl)
 
-IntervalMDP.jl is a Julia package for modeling and certifying Interval Markov Decision Processes (IMDPs) via Value Iteration.
+for modeling
+and verifying properties of various subclasses of factored Robust Markov Decision Processes (fRMDPs), in particular
+Interval Markov Decision Processes (IMDPs) and factored IMDPs (fIMDPs) 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.
+RMDPs are an extension of Markov Decision Processes (MDPs) that account for uncertainty in the transition
+probabilities, and the factored variant introduces state and action variables such that the transition model
+is a product of the transition models of the individual variables, allowing for more compact representations
+and efficient algorithms. This package focuses on different subclasses of fRMDPs for which value iteration
+can be performed efficiently including Interval Markov Chains (IMCs), IMDPs, orthogonally-decoupled IMDPs
+(odIMDPs), and fIMDPs. 
 
-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. 
+The aim of this package is to provide a user-friendly interface to solve verification and control synthesis
+problems for fRMDPs with great efficiency, which includes methods for accelerating the computation using
+CUDA hardware, pre-allocation, and other optimization techniques.
 
 ## Features
-- Value iteration (Bellman operator via O-maximization)
-- Dense and sparse matrix support
-- Parametric probability and value types for customizable precision including rationals and floating-point numbers
-- Multithreaded CPU and CUDA-accelerated value iteration
-- Data loading and writing in formats by various tools (PRISM, bmdp-tool, IMDP.jl)
+- Value iteration over IMCs, IMDPs, odIMDPs, and fIMDPs.
+- Multithreaded CPU and CUDA-accelerated value iteration.
+- Dense and sparse matrix support.
+- Parametric probability types (`Float64`, `Float32`, `Rational{BigInt}`) for customizable precision. Note that
+  `Rational{BigInt}` is not supported for CUDA acceleration.
+- Data loading and writing in formats by various tools (PRISM, bmdp-tool, IntervalMDP.jl)
 
 ## Installation
 
@@ -44,7 +49,7 @@ The goal is to compute the maximum pessimistic probability of reaching state 3 w
 using IntervalMDP
 
 # IMC
-prob = IntervalProbabilities(;
+prob = IntervalAmbiguitySets(;
     lower = [
         0.0 0.5 0.0
         0.1 0.3 0.0

diff --git a/benchmark/imdp/execute.jl b/benchmark/imdp/execute.jl
@@ -1,5 +1,11 @@
 using Revise, BenchmarkTools
 using IntervalMDP, CUDA
 
-V_conv, _, u = value_iteration(prob)
-display(@benchmark value_iteration(prob))
+cu_prob = IntervalMDP.cu(prob)
+
+function test()
+    CUDA.@sync solve(cu_prob)
+end
+
+test()  # Warm-up
+display(@benchmark test())
diff --git a/benchmark/imdp/problem.jl b/benchmark/imdp/problem.jl
@@ -4,6 +4,14 @@ using IntervalMDP, IntervalMDP.Data, SparseArrays, CUDA, Adapt
 
 path = joinpath(@__DIR__, "multiObj_robotIMDP.txt")
 mdp, terminal_states = read_bmdp_tool_file(path)
-prop = InfiniteTimeReachability(terminal_states, 1e-6)
+
+marginal = marginals(mdp)[1]
+amb = IntervalAmbiguitySets(
+    Array(ambiguity_sets(marginal).lower),
+    Array(ambiguity_sets(marginal).gap),
+)
+
+mdp = IntervalMarkovDecisionProcess(amb, num_actions(mdp), initial_states(mdp))
+prop = FiniteTimeReachability(terminal_states, 100)
 spec = Specification(prop, Pessimistic, Maximize)
-prob = Problem(mdp, spec)
+prob = VerificationProblem(mdp, spec)
diff --git a/docs/Project.toml b/docs/Project.toml
@@ -1,5 +1,8 @@
 [deps]
+Clarabel = "61c947e1-3e6d-4ee4-985a-eec8c727bd6e"
 Documenter = "e30172f5-a6a5-5a46-863b-614d45cd2de4"
+DocumenterCitations = "daee34ce-89f3-4625-b898-19384cb65244"
+HiGHS = "87dc4568-4c63-4d18-b0c0-bb2238e4078b"
 IntervalMDP = "051c988a-e73c-45a4-90ec-875cac0402c7"
 Revise = "295af30f-e4ad-537b-8983-00126c2a3abe"
 SparseArrays = "2f01184e-e22b-5df5-ae63-d93ebab69eaf"
diff --git a/docs/make.jl b/docs/make.jl
@@ -1,9 +1,11 @@
 using IntervalMDP, IntervalMDP.Data
-using Documenter
+using Documenter, DocumenterCitations
 
 push!(LOAD_PATH, "../src/")
 DocMeta.setdocmeta!(IntervalMDP, :DocTestSetup, :(using IntervalMDP); recursive = true)
 
+bib = CitationBibliography(joinpath(@__DIR__, "src", "refs.bib"); style = :numeric)
+
 makedocs(;
     modules = [IntervalMDP, IntervalMDP.Data],
     authors = "Frederik Baymler Mathiesen <frederik@baymler.com> and contributors",
@@ -12,24 +14,28 @@ makedocs(;
         prettyurls = get(ENV, "CI", "false") == "true",
         canonical = "https://www.baymler.com/IntervalMDP.jl",
         edit_link = "main",
-        assets = String[],
+        assets = String["assets/citations.css"],
     ),
     pages = [
         "Home" => "index.md",
         "Usage" => "usage.md",
-        "Data formats" => "data.md",
-        "Theory" => "theory.md",
+        "Models" => "models.md",
+        "Specifications" => "specifications.md",
         "Algorithms" => "algorithms.md",
-        "Reference" => Any[
+        "API reference" => Any[
             "Systems" => "reference/systems.md",
             "Specifications" => "reference/specifications.md",
             "Solve Interface" => "reference/solve.md",
             "Data Storage" => "reference/data.md",
+            "Index" => "api.md",
         ],
-        "Index" => "api.md",
+        "Data formats" => "data.md",
+        "Developer docs" => "developer.md",
+        "References" => "references.md",
     ],
-    doctest = false,
+    doctest = true,
     checkdocs = :exports,
+    plugins = [bib],
 )
 
 deploydocs(; repo = "github.com/Zinoex/IntervalMDP.jl", devbranch = "main")