Problem
IntervalMDP.VerificationProblem — TypeVerificationProblem{S <: StochasticProcess, F <: Specification, C <: AbstractStrategy}A verification problem is a tuple of an interval Markov process and a specification.
Fields
system::S: interval Markov process.spec::F: specification (either temporal logic or reachability-like).strategy::C: strategy to be used for verification, which can be a given strategy or a no strategy, i.e. select (but do not store! see [ControlSynthesisProblem]) optimal action for every state at every timestep.
IntervalMDP.ControlSynthesisProblem — TypeControlSynthesisProblem{S <: StochasticProcess, F <: Specification}A verification problem is a tuple of an interval Markov process and a specification.
Fields
system::S: interval Markov process.spec::F: specification (either temporal logic or reachability-like).
IntervalMDP.system — Functionsystem(prob::VerificationProblem)Return the system of a problem.
system(prob::ControlSynthesisProblem)Return the system of a problem.
IntervalMDP.specification — Functionspecification(prob::VerificationProblem)Return the specification of a problem.
specification(prob::ControlSynthesisProblem)Return the specification of a problem.
IntervalMDP.strategy — Functionstrategy(prob::VerificationProblem)Return the strategy of a problem, if provided.
strategy(s::ControlSynthesisSolution)Return the strategy of a control synthesis solution.
IntervalMDP.Specification — TypeSpecification{F <: Property}A specfication is a property together with a satisfaction mode and a strategy mode. The satisfaction mode is either Optimistic or Pessimistic. See SatisfactionMode for more details. The strategy mode is either Maxmize or Minimize. See StrategyMode for more details.
Fields
prop::F: verification property (either temporal logic or reachability-like).satisfaction::SatisfactionMode: satisfaction mode (either optimistic or pessimistic). Default is pessimistic.strategy::StrategyMode: strategy mode (either maximize or minimize). Default is maximize.
IntervalMDP.system_property — Functionsystem_property(spec::Specification)IntervalMDP.Property — TypePropertySuper type for all system Property
IntervalMDP.BasicProperty — TypeBasicPropertyA basic property that applies to a "raw" IntervalMarkovProcess.
IntervalMDP.ProductProperty — TypeProductPropertyA property that applies to a ProductProcess.
IntervalMDP.satisfaction_mode — Functionsatisfaction_mode(spec::Specification)Return the satisfaction mode of a specification.
IntervalMDP.SatisfactionMode — TypeSatisfactionModeWhen computing the satisfaction probability of a property over an interval Markov process, be it IMC or IMDP, the desired satisfaction probability to verify can either be Optimistic or Pessimistic. That is, upper and lower bounds on the satisfaction probability within the probability uncertainty.
IntervalMDP.strategy_mode — Functionstrategy_mode(spec::Specification)Return the strategy mode of a specification.
IntervalMDP.StrategyMode — TypeStrategyModeWhen computing the satisfaction probability of a property over an IMDP, the strategy can either maximize or minimize the satisfaction probability (wrt. the satisfaction mode).
DFA Reachability
IntervalMDP.FiniteTimeDFAReachability — TypeFiniteTimeDFAReachability{VT <: Vector{<:Int32}, T <: Integer}Finite time reachability specified by a set of target/terminal states and a time horizon. That is, denote a trace by $z_1 z_2 z_3 \cdots$ with $z_k = (s_k, q_k)$ then if $T$ is the set of target states and $H$ is the time horizon, the property is
\[ \mathbb{P}(\exists k = \{0, \ldots, H\}, q_k \in T).\]
IntervalMDP.isfinitetime — Methodisfinitetime(prop::FiniteTimeDFAReachability)Return true for FiniteTimeDFAReachability.
IntervalMDP.terminal_states — Methodterminal_states(spec::FiniteTimeDFAReachability)Return the set of terminal states of a finite time reachability property.
IntervalMDP.reach — Methodreach(prop::FiniteTimeDFAReachability)Return the set of states with which to compute reachbility for a finite time reachability prop. This is equivalent for terminal_states(prop::FiniteTimeDFAReachability) for a DFA reachability property.
IntervalMDP.time_horizon — Methodtime_horizon(prop::FiniteTimeDFAReachability)Return the time horizon of a finite time reachability property.
IntervalMDP.InfiniteTimeDFAReachability — TypeInfiniteTimeDFAReachability{R <: Real, VT <: Vector{<:Int32}}InfiniteTimeDFAReachability is similar to FiniteTimeDFAReachability except that the time horizon is infinite, i.e., $H = \infty$. In practice it means, performing the value iteration until the value function has converged, defined by some threshold convergence_eps. The convergence threshold is that the largest value of the most recent Bellman residual is less than convergence_eps.
IntervalMDP.isfinitetime — Methodisfinitetime(prop::InfiniteTimeDFAReachability)Return false for InfiniteTimeDFAReachability.
IntervalMDP.terminal_states — Methodterminal_states(prop::InfiniteTimeDFAReachability)Return the set of terminal states of an infinite time reachability property.
IntervalMDP.reach — Methodreach(prop::InfiniteTimeDFAReachability)Return the set of states with which to compute reachbility for a infinite time reachability property. This is equivalent for terminal_states(prop::InfiniteTimeDFAReachability) for a DFA reachability property.
IntervalMDP.convergence_eps — Methodconvergence_eps(prop::InfiniteTimeDFAReachability)Return the convergence threshold of an infinite time reachability property.
Reachability
IntervalMDP.FiniteTimeReachability — TypeFiniteTimeReachability{VT <: Vector{<:CartesianIndex}, T <: Integer}Finite time reachability specified by a set of target/terminal states and a time horizon. That is, denote a trace by $s_1 s_2 s_3 \cdots$, then if $T$ is the set of target states and $H$ is the time horizon, the property is
\[ \mathbb{P}(\exists k = \{0, \ldots, H\}, s_k \in T).\]
IntervalMDP.isfinitetime — Methodisfinitetime(prop::FiniteTimeReachability)Return true for FiniteTimeReachability.
IntervalMDP.terminal_states — Methodterminal_states(spec::FiniteTimeReachability)Return the set of terminal states of a finite time reachability property.
IntervalMDP.reach — Methodreach(prop::FiniteTimeReachability)Return the set of states with which to compute reachbility for a finite time reachability prop. This is equivalent for terminal_states(prop::FiniteTimeReachability) for a regular reachability property. See FiniteTimeReachAvoid for a more complex property where the reachability and terminal states differ.
IntervalMDP.time_horizon — Methodtime_horizon(prop::FiniteTimeReachability)Return the time horizon of a finite time reachability property.
IntervalMDP.InfiniteTimeReachability — TypeInfiniteTimeReachability{R <: Real, VT <: Vector{<:CartesianIndex}}InfiniteTimeReachability is similar to FiniteTimeReachability except that the time horizon is infinite, i.e., $H = \infty$. In practice it means, performing the value iteration until the value function has converged, defined by some threshold convergence_eps. The convergence threshold is that the largest value of the most recent Bellman residual is less than convergence_eps.
IntervalMDP.isfinitetime — Methodisfinitetime(prop::InfiniteTimeReachability)Return false for InfiniteTimeReachability.
IntervalMDP.terminal_states — Methodterminal_states(prop::InfiniteTimeReachability)Return the set of terminal states of an infinite time reachability property.
IntervalMDP.reach — Methodreach(prop::InfiniteTimeReachability)Return the set of states with which to compute reachbility for a infinite time reachability property. This is equivalent for terminal_states(prop::InfiniteTimeReachability) for a regular reachability property. See InfiniteTimeReachAvoid for a more complex property where the reachability and terminal states differ.
IntervalMDP.convergence_eps — Methodconvergence_eps(prop::InfiniteTimeReachability)Return the convergence threshold of an infinite time reachability property.
IntervalMDP.ExactTimeReachability — TypeExactTimeReachability{VT <: Vector{<:CartesianIndex}, T <: Integer}Exact time reachability specified by a set of target/terminal states and a time horizon. That is, denote a trace by $s_1 s_2 s_3 \cdots$, then if $T$ is the set of target states and $H$ is the time horizon, the property is
\[ \mathbb{P}(s_H \in T).\]
IntervalMDP.isfinitetime — Methodisfinitetime(prop::ExactTimeReachability)Return true for ExactTimeReachability.
IntervalMDP.terminal_states — Methodterminal_states(spec::ExactTimeReachability)Return the set of terminal states of an exact time reachability property.
IntervalMDP.reach — Methodreach(prop::ExactTimeReachability)Return the set of states with which to compute reachbility for an exact time reachability prop. This is equivalent for terminal_states(prop::ExactTimeReachability) for a regular reachability property. See ExactTimeReachAvoid for a more complex property where the reachability and terminal states differ.
IntervalMDP.time_horizon — Methodtime_horizon(prop::ExactTimeReachability)Return the time horizon of an exact time reachability property.
Reach-avoid
IntervalMDP.FiniteTimeReachAvoid — TypeFiniteTimeReachAvoid{VT <: AbstractVector{<:CartesianIndex}}, T <: Integer}Finite time reach-avoid specified by a set of target/terminal states, a set of avoid states, and a time horizon. That is, denote a trace by $s_1 s_2 s_3 \cdots$, then if $T$ is the set of target states, $A$ is the set of states to avoid, and $H$ is the time horizon, the property is
\[ \mathbb{P}(\exists k = \{0, \ldots, H\}, s_k \in T, \text{ and } \forall k' = \{0, \ldots, k\}, s_k' \notin A).\]
IntervalMDP.isfinitetime — Methodisfinitetime(prop::FiniteTimeReachAvoid)Return true for FiniteTimeReachAvoid.
IntervalMDP.terminal_states — Methodterminal_states(prop::FiniteTimeReachAvoid)Return the set of terminal states of a finite time reach-avoid property. That is, the union of the reach and avoid sets.
IntervalMDP.reach — Methodreach(prop::FiniteTimeReachAvoid)Return the set of target states.
IntervalMDP.avoid — Methodavoid(prop::FiniteTimeReachAvoid)Return the set of states to avoid.
IntervalMDP.time_horizon — Methodtime_horizon(prop::FiniteTimeReachAvoid)Return the time horizon of a finite time reach-avoid property.
IntervalMDP.InfiniteTimeReachAvoid — TypeInfiniteTimeReachAvoid{R <: Real, VT <: AbstractVector{<:CartesianIndex}}InfiniteTimeReachAvoid is similar to FiniteTimeReachAvoid except that the time horizon is infinite, i.e., $H = \infty$.
IntervalMDP.isfinitetime — Methodisfinitetime(prop::InfiniteTimeReachAvoid)Return false for InfiniteTimeReachAvoid.
IntervalMDP.terminal_states — Methodterminal_states(prop::InfiniteTimeReachAvoid)Return the set of terminal states of an infinite time reach-avoid property. That is, the union of the reach and avoid sets.
IntervalMDP.reach — Methodreach(prop::InfiniteTimeReachAvoid)Return the set of target states.
IntervalMDP.avoid — Methodavoid(prop::InfiniteTimeReachAvoid)Return the set of states to avoid.
IntervalMDP.convergence_eps — Methodconvergence_eps(prop::InfiniteTimeReachAvoid)Return the convergence threshold of an infinite time reach-avoid property.
IntervalMDP.ExactTimeReachAvoid — TypeExactTimeReachAvoid{VT <: AbstractVector{<:CartesianIndex}}, T <: Integer}Exact time reach-avoid specified by a set of target/terminal states, a set of avoid states, and a time horizon. That is, denote a trace by $s_1 s_2 s_3 \cdots$, then if $T$ is the set of target states, $A$ is the set of states to avoid, and $H$ is the time horizon, the property is
\[ \mathbb{P}(s_H \in T, \text{ and } \forall k = \{0, \ldots, H\}, s_k \notin A).\]
IntervalMDP.isfinitetime — Methodisfinitetime(prop::ExactTimeReachAvoid)Return true for ExactTimeReachAvoid.
IntervalMDP.terminal_states — Methodterminal_states(prop::ExactTimeReachAvoid)Return the set of terminal states of an exact time reach-avoid property. That is, the union of the reach and avoid sets.
IntervalMDP.reach — Methodreach(prop::ExactTimeReachAvoid)Return the set of target states.
IntervalMDP.avoid — Methodavoid(prop::ExactTimeReachAvoid)Return the set of states to avoid.
IntervalMDP.time_horizon — Methodtime_horizon(prop::ExactTimeReachAvoid)Return the time horizon of an exact time reach-avoid property.
Safety
IntervalMDP.FiniteTimeSafety — TypeFiniteTimeSafety{VT <: Vector{<:CartesianIndex}, T <: Integer}Finite time safety specified by a set of avoid states and a time horizon. That is, denote a trace by $s_1 s_2 s_3 \cdots$, then if $A$ is the set of avoid states and $H$ is the time horizon, the property is
\[ \mathbb{P}(\forall k = \{0, \ldots, H\}, s_k \notin A).\]
IntervalMDP.isfinitetime — Methodisfinitetime(prop::FiniteTimeSafety)Return true for FiniteTimeSafety.
IntervalMDP.terminal_states — Methodterminal_states(spec::FiniteTimeSafety)Return the set of terminal states of a finite time safety property.
IntervalMDP.avoid — Methodavoid(prop::FiniteTimeSafety)Return the set of states with which to compute reachbility for a finite time reachability prop. This is equivalent for terminal_states(prop::FiniteTimeSafety).
IntervalMDP.time_horizon — Methodtime_horizon(prop::FiniteTimeSafety)Return the time horizon of a finite time safety property.
IntervalMDP.InfiniteTimeSafety — TypeInfiniteTimeSafety{R <: Real, VT <: Vector{<:CartesianIndex}}InfiniteTimeSafety is similar to FiniteTimeSafety except that the time horizon is infinite, i.e., $H = \infty$. In practice it means, performing the value iteration until the value function has converged, defined by some threshold convergence_eps. The convergence threshold is that the largest value of the most recent Bellman residual is less than convergence_eps.
IntervalMDP.isfinitetime — Methodisfinitetime(prop::InfiniteTimeSafety)Return false for InfiniteTimeSafety.
IntervalMDP.terminal_states — Methodterminal_states(prop::InfiniteTimeSafety)Return the set of terminal states of an infinite time safety property.
IntervalMDP.avoid — Methodavoid(prop::InfiniteTimeSafety)Return the set of states with which to compute safety for a infinite time safety property. This is equivalent for terminal_states(prop::InfiniteTimeSafety).
IntervalMDP.convergence_eps — Methodconvergence_eps(prop::InfiniteTimeSafety)Return the convergence threshold of an infinite time safety property.
Reward specification
IntervalMDP.FiniteTimeReward — TypeFiniteTimeReward{R <: Real, AR <: AbstractArray{R}, T <: Integer}FiniteTimeReward is a property of rewards $R : S \to \mathbb{R}$ assigned to each state at each iteration and a discount factor $\gamma$. The time horizon $H$ is finite, so the discount factor is optional and the optimal policy will be time-varying. Given a strategy $\pi : S \to A$, the property is
\[ V(s_0) = \mathbb{E}\left[\sum_{k=0}^{H} \gamma^k R(s_k) \mid s_0, \pi\right].\]
IntervalMDP.isfinitetime — Methodisfinitetime(prop::FiniteTimeReward)Return true for FiniteTimeReward.
IntervalMDP.reward — Methodreward(prop::FiniteTimeReward)Return the reward vector of a finite time reward optimization.
IntervalMDP.discount — Methoddiscount(prop::FiniteTimeReward)Return the discount factor of a finite time reward optimization.
IntervalMDP.time_horizon — Methodtime_horizon(prop::FiniteTimeReward)Return the time horizon of a finite time reward optimization.
IntervalMDP.InfiniteTimeReward — TypeInfiniteTimeReward{R <: Real, AR <: AbstractArray{R}}InfiniteTimeReward is a property of rewards assigned to each state at each iteration and a discount factor for guaranteed convergence. The time horizon is infinite, i.e. $H = \infty$, so the optimal policy will be stationary.
IntervalMDP.isfinitetime — Methodisfinitetime(prop::InfiniteTimeReward)Return false for InfiniteTimeReward.
IntervalMDP.reward — Methodreward(prop::FiniteTimeReward)Return the reward vector of a finite time reward optimization.
IntervalMDP.discount — Methoddiscount(prop::FiniteTimeReward)Return the discount factor of a finite time reward optimization.
IntervalMDP.convergence_eps — Methodconvergence_eps(prop::InfiniteTimeReward)Return the convergence threshold of an infinite time reward optimization.
Hitting time
IntervalMDP.ExpectedExitTime — TypeExpectedExitTime{R <: Real, VT <: Vector{<:CartesianIndex}}ExpectedExitTime is a property of hitting time with respect to an unsafe set. An equivalent characterization is that of the expected number of steps in the safe set until reaching the unsafe set. The time horizon is infinite, i.e., $H = \infty$, thus the package performs value iteration until the value function has converged. The convergence threshold is that the largest value of the most recent Bellman residual is less than convergence_eps. As this is an infinite horizon property, the resulting optimal policy will be stationary. In formal language, given a strategy $\pi : S \to A$ and an unsafe set $O$, the property is defined as
\[ V(s_0) = \mathbb{E}\left[\lvert \omega_{0:k-1} \rvert \mid s_0, \pi, \omega_{0:k-1} \notin O, \omega_k \in O \right]\]
where $\omega = s_0 s_1 \ldots s_k$ is the trajectory of the system, $\omega_{0:k-1} = s_0 s_1 \ldots s_{k-1}$ denotes the subtrajectory excluding the final state, and $\omega_k = s_k$.
IntervalMDP.isfinitetime — Methodisfinitetime(prop::ExpectedExitTime)Return true for ExpectedExitTime.
IntervalMDP.terminal_states — Methodterminal_states(prop::ExpectedExitTime)Return the set of terminal states of an expected hitting time property.
IntervalMDP.avoid — Methodavoid(prop::ExpectedExitTime)Return the set of unsafe states that we compute the expected hitting time with respect to. This is equivalent for terminal_states(prop::ExpectedExitTime).
IntervalMDP.convergence_eps — Methodconvergence_eps(prop::ExpectedExitTime)Return the convergence threshold of an expected exit time.