System representation

num_states(mp::IntervalMarkovProcess)

Return the number of states.

num_actions(mp::IntervalMarkovProcess)

Return the number of actions.

initial_states(mp::IntervalMarkovProcess)

Return the initial states. If the initial states are not specified, return nothing.

AllStates

A type to represent all states in a Markov process. This type is used to specify all states as the initial states.

FactoredRobustMarkovDecisionProcess{N, M, P <: NTuple{N, Marginal}, VI <: InitialStates} <: IntervalMarkovProcess

Factored Robust Markov Decision Processes (fRMDPs) [1, 2] are an extension of Robust Markov Decision Processes (RMDPs) [3–5] that incorporate a factored representation of the state and action spaces, i.e. with state and action variables.

Formally, a fRMDP $M$ is a tuple $M = (S, S_0, A, \mathcal{G}, \Gamma)$, where

• $S = S_1 \times \cdots \times S_n$ is a finite set of joint states with $S_i$ being a finite set of states for the $i$-th state variable,
• $S_0 \subseteq S$ is a set of initial states,
• $A = A_1 \times \cdots \times A_m$ is a finite set of joint actions with $A_j$ being a finite set of actions for the $j$-th action variable,
• $\mathcal{G} = (\mathcal{V}, \mathcal{E})$ is a directed bipartite graph with nodes $\mathcal{V} = \mathcal{V}_{ind} \cup \mathcal{V}_{cond} = \{S_1, \ldots, S_n, A_1, \ldots, A_m\} \cup \{S'_1, \ldots, S'_n\}$ representing the state and action variables and their next-state counterparts, and edges $\mathcal{E} \subseteq \mathcal{V}_{ind} \times \mathcal{V}_{cond}$ representing dependencies of $S'_i$ on $S_j$ and $A_k$,
• $\Gamma = \{\Gamma_{s, a}\}_{s \in S, a \in A}$ is a set of ambiguity sets for source-action pair $(s, a)$, where each $\Gamma_{s, a} = \bigotimes_{i=1}^n \Gamma^i_{\text{Pa}_\mathcal{G}(S'_i) \cap (s, a)}$ is a product of ambiguity sets $\Gamma^i_{\text{Pa}_\mathcal{G}(S'_i) \cap (s, a)}$ along each marginal $i$ conditional on the values in $(s, a)$ of the parent variables $\text{Pa}_\mathcal{G}(S'_i)$ of $S'_i$ in $\mathcal{G}$, i.e.

\[ \Gamma_{s, a} = \left\{ \gamma \in \mathcal{D}(S) \,:\, \gamma(t) = \prod_{i=1}^n \gamma^i(t_i | s_{\text{Pa}_{\mathcal{G}_S}(S'_i)}, a_{\text{Pa}_{\mathcal{G}_A}(S'_i)}), \, \gamma^i(\cdot | s_{\text{Pa}_{\mathcal{G}_S}(S'_i)}, a_{\text{Pa}_{\mathcal{G}_A}(S'_i)}) \in \Gamma^i_{\text{Pa}_\mathcal{G}(S'_i)} \right\}.\]

For a given source-action pair $(s, a) \in S \times A$, any distribution $\gamma_{s, a} \in \Gamma_{s, a}$ is called a feasible distribution, and feasible transitions are triplets $(s, a, t) \in S \times A \times S$ where $t \in \mathop{supp}(\gamma_{s, a})$ for any feasible distribution $\gamma_{s, a} \in \Gamma_{s, a}$.

Type parameters

• N is the number of state variables.
• M is the number of action variables.
• P <: NTuple{N, Marginal} is a tuple type with a (potentially different) type for each marginal.
• VI <: InitialStates is the type of initial states.

Fields

• state_vars::NTuple{N, Int32}: the number of values $|S_i|$ for each state variable $S_i$ as a tuple.
• action_vars::NTuple{M, Int32}: the number of values $|A_k|$ for each action variable $A_k$ as a tuple.
• source_dims::NTuple{N, Int32}: for systems with terminal states along certain slices, it is possible to avoid specifying them by using source_dims less than state_vars; this is useful e.g. in building abstractions. The terminal states must be the last value for the slice dimension. If not supplied, it is assumed source_dims == state_vars.
• transition::P is the marginal ambiguity sets. For a given source-action pair $(s, a) \in S \times A$, any Marginal element of transition subselects s and a corresponding to its state_variables and action_variables, i.e. it encodes the operation \text{Pa}_\mathcal{G}(S'_i) \cap (s, a). The underlying ambiguity_sets object on Marginal encodes $\Gamma^i_{\text{Pa}_\mathcal{G}(S'_i) \cap (s, a)}$ for all values of $\text{Pa}_\mathcal{G}(S'_i)$. See Marginal for details about the layout of the underlying AbstractAmbiguitySets object.
• initial_states::VI: stores a representation of S_0. If no set of initial_states are given, then it is simply assigned the zero-byte object AllStates(), which represents that all states are potential initial states. It is not used within the value iteration.

Example

using IntervalMDP

state_vars = (2, 3)
action_vars = (1, 2)

state_indices = (1, 2)
action_indices = (1,)
state_dims = (2, 3)
action_dims = (1,)
marginal1 = Marginal(IntervalAmbiguitySets(;
    # 6 ambiguity sets = 2 * 3 source states, 1 action
    # Column layout: (a¹₁, s¹₁, s²₁), (a¹₁, s¹₂, s²₁), (a¹₁, s¹₁, s²₂), (a¹₁, s¹₂, s²₂), (a¹₁, s¹₁, s²₃), (a¹₁, s¹₂, s²₃)
    # Equivalent to CartesianIndices(actions_dims..., state_dims...), i.e. actions first, then states in lexicographic order
    lower = [
        1/15  7/30  1/15  13/30  4/15  1/6
        2/5   7/30  1/30  11/30  2/15  1/10
    ],
    upper = [
        17/30  7/10   2/3   4/5  7/10  2/3
        9/10   13/15  9/10  5/6  4/5   14/15
    ]
), state_indices, action_indices, state_dims, action_dims)

state_indices = (2,)
action_indices = (2,)
state_dims = (3,)
action_dims = (2,)
marginal2 = Marginal(IntervalAmbiguitySets(;
    # 6 ambiguity sets = 3 source states, 2 actions
    # Column layout: (a²₁, s²₁), (a²₂, s²₁), (a²₁, s²₂), (a²₂, s²₂), (a²₁, s²₃), (a²₂, s²₃)
    # Equivalent to CartesianIndices(actions_dims..., state_dims...), i.e. actions first, then states in lexicographic order
    lower = [
        1/30  1/3   1/6   1/15  2/5   2/15
        4/15  1/4   1/6   1/30  2/15  1/30
        2/15  7/30  1/10  7/30  7/15  1/5
    ],
    upper = [
        2/3    7/15  4/5    11/30  19/30  1/2
        23/30  4/5   23/30  3/5    7/10   8/15
        7/15   4/5   23/30  7/10   7/15   23/30
    ]
), state_indices, action_indices, state_dims, action_dims)

initial_states = [(1, 1)]  # Initial states are optional
mdp = FactoredRobustMarkovDecisionProcess(state_vars, action_vars, (marginal1, marginal2), initial_states)

# output

FactoredRobustMarkovDecisionProcess
├─ 2 state variables with cardinality: (2, 3)
├─ 2 action variables with cardinality: (1, 2)
├─ Initial states: [(1, 1)]
├─ Transition marginals:
│  ├─ Marginal 1:
│  │  ├─ Conditional variables: states = (1, 2), actions = (1,)
│  │  └─ Ambiguity set type: Interval (dense, Matrix{Float64})
│  └─ Marginal 2:
│     ├─ Conditional variables: states = (2,), actions = (2,)
│     └─ Ambiguity set type: Interval (dense, Matrix{Float64})
└─Inferred properties
   ├─Model type: Factored Interval MDP
   ├─Number of states: 6
   ├─Number of actions: 2
   ├─Default model checking algorithm: Robust Value Iteration
   └─Default Bellman operator algorithm: Binary tree LP McCormick Relaxation

state_values(mdp::FactoredRMDP)

Return a tuple with the number of states for each state variable in the fRMDP.

action_values(mdp::FactoredRMDP)

Return a tuple with the number of actions for each action variable in the fRMDP.

marginals(mdp::FactoredRMDP)

Return the marginals of the fRMDP.

IntervalMarkovChain(ambiguity_set::IntervalAmbiguitySets, initial_states=AllStates())

A convenience constructor for a FactoredRobustMarkovDecisionProcess representing an interval Markov chain, as IMCs are a subclass of fRMDPs, from a single IntervalAmbiguitySets object.

Formally, an IMC $M$ is a tuple $M = (S, S_0, \Gamma)$, where

• $S$ is a finite set of states,
• $S_0 \subseteq S$ is a set of initial states,
• $\Gamma = \{\Gamma_{s}\}_{s \in S}$ is a set of ambiguity sets for source state $s$, where each $\Gamma_{s}$ is an interval ambiguity set over $S$.

Notice also that an IMC is an IntervalMarkovDecisionProcess with a single action.

Example

using IntervalMDP

prob = IntervalAmbiguitySets(;
    lower = [
        0     1/2   0
        1/10  3/10  0
        1/5   1/10  1
    ],
    upper = [
        1/2   7/10  0
        3/5   1/2   0
        7/10  3/10  1
    ],
)

initial_states = [1]
mc = IntervalMarkovChain(prob, initial_states)

# output

FactoredRobustMarkovDecisionProcess
├─ 1 state variables with cardinality: (3,)
├─ 1 action variables with cardinality: (1,)
├─ Initial states: [1]
├─ Transition marginals:
│  └─ Marginal 1:
│     ├─ Conditional variables: states = (1,), actions = (1,)
│     └─ Ambiguity set type: Interval (dense, Matrix{Float64})
└─Inferred properties
   ├─Model type: Interval MDP
   ├─Number of states: 3
   ├─Number of actions: 1
   ├─Default model checking algorithm: Robust Value Iteration
   └─Default Bellman operator algorithm: O-Maximization

IntervalMarkovDecisionProcess(ambiguity_set::IntervalAmbiguitySets, num_actions::Integer, initial_states::InitialStates = AllStates())

A convenience constructor for a FactoredRobustMarkovDecisionProcess representing an interval Markov decision process, as IMDPs are a subclass of fRMDPs, from a single IntervalAmbiguitySets object and a specified number of actions.

Formally, an IMDP $M$ is a tuple $M = (S, S_0, A, \Gamma)$, where

• $S$ is a finite set of states,
• $S_0 \subseteq S$ is a set of initial states,
• $A$ is a finite set of actions,
• `$\Gamma = \{\Gamma_{s,a}\}_{s \in S,a \in A}$ is a set of ambiguity sets for source-action pair $(s, a)$, where each $\Gamma_{s,a}$ is an interval ambiguity set over $S$.

Example

using IntervalMDP

prob1 = IntervalAmbiguitySets(;
    lower = [
        0    1/2
        1/10 3/10
        1/5  1/10
    ],
    upper = [
        1/2  7/10
        3/5  1/2
        7/10 3/10
    ],
)

prob2 = IntervalAmbiguitySets(;
    lower = [
        1/10 1/5
        1/5  3/10
        3/10 2/5
    ],
    upper = [
        3/5 3/5
        1/2 1/2
        2/5 2/5
    ],
)

prob3 = IntervalAmbiguitySets(;
    lower = Float64[
        0 0
        0 0
        1 1
    ],
    upper = Float64[
        0 0
        0 0
        1 1
    ]
)

initial_states = [1]
mdp = IntervalMarkovDecisionProcess([prob1, prob2, prob3], initial_states)

# output

FactoredRobustMarkovDecisionProcess
├─ 1 state variables with cardinality: (3,)
├─ 1 action variables with cardinality: (2,)
├─ Initial states: [1]
├─ Transition marginals:
│  └─ Marginal 1:
│     ├─ Conditional variables: states = (1,), actions = (1,)
│     └─ Ambiguity set type: Interval (dense, Matrix{Float64})
└─Inferred properties
   ├─Model type: Interval MDP
   ├─Number of states: 3
   ├─Number of actions: 2
   ├─Default model checking algorithm: Robust Value Iteration
   └─Default Bellman operator algorithm: O-Maximization

IntervalMarkovDecisionProcess(ps::Vector{<:IntervalAmbiguitySets}, initial_states::InitialStates = AllStates())

A convenience constructor for a FactoredRobustMarkovDecisionProcess representing an interval Markov decision process from a vector of IntervalAmbiguitySets objects, one for each state and with the same number of actions in each.

Example

using IntervalMDP

prob = IntervalAmbiguitySets(;
    lower = [
        0    1/2  1/10 1/5  0 0
        1/10 3/10 1/5  3/10 0 0
        1/5  1/10 3/10 2/5  1 1
    ],
    upper = [
        1/2  7/10 3/5 2/5 0 0
        3/5  1/2  1/2 2/5 0 0
        7/10 3/10 2/5 2/5 1 1
    ],
)

num_actions = 2
initial_states = [1]
mdp = IntervalMarkovDecisionProcess(prob, num_actions, initial_states)

# output

FactoredRobustMarkovDecisionProcess
├─ 1 state variables with cardinality: (3,)
├─ 1 action variables with cardinality: (2,)
├─ Initial states: [1]
├─ Transition marginals:
│  └─ Marginal 1:
│     ├─ Conditional variables: states = (1,), actions = (1,)
│     └─ Ambiguity set type: Interval (dense, Matrix{Float64})
└─Inferred properties
   ├─Model type: Interval MDP
   ├─Number of states: 3
   ├─Number of actions: 2
   ├─Default model checking algorithm: Robust Value Iteration
   └─Default Bellman operator algorithm: O-Maximization

Marginal{A <: AbstractAmbiguitySets, N, M, I <: LinearIndices}

A struct to represent the dependency graph of an fRMDP, namely by subselecting (in getindex) the (decomposed) state and action. Furthermore, the struct is responsible for converting the Cartesian index to a linear index for the underlying ambiguity sets.

ambiguity_sets(p::Marginal)

Return the underlying ambiguity sets of the marginal.

state_variables(p::Marginal)

Return the state variable indices of the marginal.

action_variables(p::Marginal)

Return the action variable indices of the marginal.

source_shape(p::Marginal)

Return the shape of the source (state) variables of the marginal. The FactoredRobustMarkovDecisionProcess checks if this is less than or equal to the corresponding state values.

action_shape(p::Marginal)

Return the shape of the action variables of the marginal. The FactoredRobustMarkovDecisionProcess checks if this is equal to the corresponding action values.

getindex(p::Marginal, action, source)

Get the ambiguity set corresponding to the given source (state) and action, where the relevant indices of source and action are selected by p.action_indices and p.state_indices respectively. The selected index is then converted to a linear index for the underlying ambiguity sets.

num_sets(ambiguity_sets::AbstractAmbiguitySets)

Return the number of ambiguity sets in the AbstractAmbiguitySets object.

num_target(p::Marginal)

Return the number of target states of the marginal.

support(ambiguity_set::AbstractAmbiguitySet)

Return the support (set of indices with non-zero probability) of the ambiguity set.

IntervalAmbiguitySets{R, MR <: AbstractMatrix{R}}

A matrix pair to represent the lower and upper bound of num_sets(ambiguity_sets) interval ambiguity sets (on the columns) to num_target(ambiguity_sets) destinations (on the rows). Marginal adds interpretation to the column indices. The matrices can be Matrix{R} or SparseMatrixCSC{R}, or their CUDA equivalents. Due to the space complexity, if modelling IntervalMarkovChains or IntervalMarkovDecisionProcesses, it is recommended to use sparse matrices.

The columns represent the different ambiguity sets and the rows represent the targets. Due to the column-major format of Julia, this is a more efficient representation in terms of cache locality.

The lower bound is explicitly stored, while the upper bound is computed from the lower bound and the gap. This choice is because it simplifies repeated probability assignment using O-maximization [7, 8].

Fields

• lower::MR: The lower bound probabilities for num_sets(ambiguity_sets) ambiguity sets to num_target(ambiguity_sets) target states.
• gap::MR: The gap between upper and lower bound transition probabilities for num_sets(ambiguity_sets) ambiguity sets to num_target(ambiguity_sets) target states.

Examples

using IntervalMDP

dense_prob = IntervalAmbiguitySets(;
    lower = [0.0 0.5; 0.1 0.3; 0.2 0.1],
    upper = [0.5 0.7; 0.6 0.5; 0.7 0.3],
)

# output

IntervalAmbiguitySets
├─ Storage type: Matrix{Float64}
├─ Number of target states: 3
└─ Number of ambiguity sets: 2

using IntervalMDP, SparseArrays
sparse_prob = IntervalAmbiguitySets(;
    lower = sparse_hcat(
        SparseVector(15, [4, 10], [0.1, 0.2]),
        SparseVector(15, [5, 6, 7], [0.5, 0.3, 0.1]),
    ),
    upper = sparse_hcat(
        SparseVector(15, [1, 4, 10], [0.5, 0.6, 0.7]),
        SparseVector(15, [5, 6, 7], [0.7, 0.5, 0.3]),
    ),
)

# output

IntervalAmbiguitySets
├─ Storage type: SparseArrays.FixedSparseCSC{Float64, Int64}
├─ Number of target states: 15
├─ Number of ambiguity sets: 2
├─ Maximum support size: 3
└─ Number of non-zeros: 6

lower(p::IntervalAmbiguitySet)

Return the lower bound transition probabilities of the ambiguity set to all target states.

upper(p::IntervalAmbiguitySet)

Return the upper bound transition probabilities of the ambiguity set to all target states.

gap(p::IntervalAmbiguitySet)

Return the gap between upper and lower bound transition probabilities of the ambiguity set to all target states.

DFA{
    T <: TransitionFunction,  
    VT <: AbstractVector{Int32},
    DA <: AbstractDict{String, Int32}
}

A type representing Deterministic Finite Automaton (DFA) which are finite automata with deterministic transitions.

Formally, let $(Q, 2^{AP}, \delta, q_0, Q_{ac})$ be an DFA, where

• $Q$ is the set of states,
• $Q_{ac} \subseteq Q$ is the set of accepting states,
• $Q_0$ is the initial state,
• $2^{AP}$ is the power set of automic propositions, and
• $\delta : |Q| \times |2^{AP}| => |Q|$ is the deterministic transition function, for each state-input pair.

Then the DFA type is defined as follows: indices 1:num_states are the states in $Q$, transition represents $\delta$, the set $2^{AP}$ is , and initial_state is the initial state $q_0$. See TransitionFunction for more information on the structure of the transition function.

Fields

• transition::T: transition function.
• initial_state::Int32: initial states.
• accepting_states::VT: vector of accepting states
• labelmap::DA: mapping from label to index.

num_states(dfa::DFA)

Return the number of states $|Q|$ of the Deterministic Finite Automaton.

num_labels(dfa::DFA)

Return the number of labels (DFA inputs) in the Deterministic Finite Automaton.

transition(dfa::DFA)

Return the transition object of the Deterministic Finite Automaton.

labelmap(dfa::DFA)

Return the label index mapping $2^{AP} \to \mathbb{N}$ of the Deterministic Finite Automaton.

initial_state(dfa::DFA)

Return the initial state of the Deterministic Finite Automaton.

struct ProductProcess{
    M <: IntervalMarkovProcess,
    D <: DeterministicAutomaton,
    L <: AbstractLabelling,
}

A type representing the product between interval Markov processes (e.g. FactoredRobustMarkovDecisionProcess) and an automaton (typically a deterministic finite automaton DFA).

Formally, given an interval Markov process $M = (S, A, \Gamma, S_{0})$, a labelling function $L : S \to 2^{AP}$, and a DFA $D = (Q, 2^{AP}, \delta, q_{0}, Q_{ac})$, then a product process is a tuple $M_{prod} = (Z, A, \Gamma^{prod}, Z_{ac}, Z_{0})$ where

• $Z = S \times Q$ is the set of product states q = (s, z)``,
• $Q_{0} = S_0 \times \{q_0\} \subset Z$ is the set of initial product states $z_0 = (s_0, q_0)$,
• $Z_{ac} = S \times Q_{ac} \subseteq Z$ is the set of accepting product states,
• $A$ is the set of actions, and
• $\Gamma^{prod} = \{\Gamma^{prod}_{z,a}\}_{z \in Z, a \in A}$ where $\Gamma^{prod}_{z,a} = \{ \gamma_{z,a} : \gamma_{z,a}((t, z')) = \gamma_{s,a}(t)\delta_{q,L(s)}(z') \}$

is a set of ambiguity sets on the product transition probabilities, for each product source-action pair.

See FactoredRobustMarkovDecisionProcess and DFA for more information on the structure, definition, and usage of the DFA and IMDP.

Fields

• mdp::M: contains details for the interval Markov process.
• dfa::D: contains details for the DFA
• labelling_func::L: the labelling function from IMDP states to DFA actions

markov_process(proc::ProductIntervalMarkovDecisionProcessDFA)

Return the interval markov decision process of the product

automaton(proc::ProductIntervalMarkovDecisionProcessDFA)

Return the deterministic finite automaton of the product

labelling_function(proc::ProductProcess)

Return the labelling function of the product

struct TransitionFunction{
    T <: Integer, 
    MT <: AbstractMatrix{T}
}

A type representing the determininistic transition function of a DFA.

Formally, let $T : |Q| \times |2^{AP}| => |Q|$ be a transition function, where

• $Q$ is the set of DFA states, and
• $2^{AP}$ is the power set of atomic propositions

Then the TransitionFunction type is defined as matrix which stores the mapping. The row indices are the alphabet indices and the column indices represent the states.

Fields

• transition::MT: transition functions encoded as matrix with labels on the rows, source states on the columns, and integer values for the destination.

The choice to have labels on the rows is due to the column-major storage of matrices in Julia and the fact that we want the outer loop over DFA source states in the Bellman operator bellman!.

We check that the transition matrix is valid, i.e. that all indices are positive and do not exceed the number of states.

transition(transition_func::TransitionFunction)

Return the transition matrix of the transition function.

num_states(tf::TransitionFunction)

Return the number of states $|Q|$ of the transition function.

num_labels(tf::TransitionFunction)

Return the number of labels (DFA inputs) in the transition function.

struct DeterministicLabelling{
    T  <: Integer, 
    AT <: AbstractArray{T}
}

A type representing the labelling of IMDP states into DFA inputs.

Formally, let $L : S \to 2^{AP}$ be a labelling function, where

• $S$ is the set of IMDP states, and
• $2^{AP}$ is the power set of atomic propositions

Then the DeterministicLabelling type is defined as vector which stores the mapping.

Fields

• map::AT: mapping function where indices are (factored) IMDP states and stored values are DFA inputs.
• num_outputs::Int32: number of labels accounted for in mapping.

mapping(dl::DeterministicLabelling)

Return the mapping array of the labelling function.

num_labels(dl::DeterministicLabelling)

Return the number of labels (DFA inputs) in the labelling function.

state_values(dl::DeterministicLabelling)

Return a tuple with the number of states for each state variable of the labeling function $L : S \to 2^{AP}$, which can be multiple dimensions in case of factored IMDPs.

struct ProbabilisticLabelling{
    R <: Real, 
    MR <: AbstractMatrix{R}
}

A type representing the Probabilistic labelling of IMDP states into DFA inputs. Each labelling is assigned a probability.

Formally, let $L : S \times 2^{AP} \to [0, 1]$ be a labelling function, where

• $S$ is the set of IMDP states, and
• $2^{AP}$ is the power set of atomic propositions

Then the ProbabilisticLabelling type is defined as matrix which stores the mapping.

Fields

• map::MT: mapping function encoded as matrix with labels on the rows, IMDP states on the columns, and valid probability values for the destination.

The choice to have labels on the rows is due to the column-major storage of matrices in Julia and the fact that we want the inner loop over DFA target states in the Bellman operator bellman!.

mapping(pl::ProbabilisticLabelling)

Return the mapping matrix of the probabilistic labelling function.

num_labels(pl::ProbabilisticLabelling)

Return the number of labels (DFA inputs) in the probabilistic labelling function.

state_values(pl::ProbabilisticLabelling)

Return a tuple with the number of states for each state variable of the labeling function $L : S \to 2^{AP}$, which can be multiple dimensions in case of factored IMDPs.