Problem

VerificationProblem{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.

ControlSynthesisProblem{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).

system(prob::VerificationProblem)

Return the system of a problem.

system(prob::ControlSynthesisProblem)

Return the system of a problem.

specification(prob::VerificationProblem)

Return the specification of a problem.

specification(prob::ControlSynthesisProblem)

Return the specification of a problem.

strategy(prob::VerificationProblem)

Return the strategy of a problem, if provided.

Specification{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.

system_property(spec::Specification)

satisfaction_mode(spec::Specification)

Return the satisfaction mode of a specification.

SatisfactionMode

When 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.

strategy_mode(spec::Specification)

Return the strategy mode of a specification.

StrategyMode

When computing the satisfaction probability of a property over an IMDP, the strategy can either maximize or minimize the satisfaction probability (wrt. the satisfaction mode).

FiniteTimeReachability{VT <: Vector{Union{<:Integer, <:Tuple, <:CartesianIndex}}, T <: Integer}

Finite time reachability specified by a set of target/terminal states and a time horizon. That is, denote a trace by $\omega = s_1 s_2 s_3 \cdots$, then if $G$ is the set of target states and $K$ is the time horizon, the property is

\[ \mathbb{P}^{\pi, \eta}_{\mathrm{reach}}(G, K) = \mathbb{P}^{\pi, \eta} \left[\omega \in \Omega : \exists k \in \{0, \ldots, K\}, \, \omega[k] \in G \right].\]

reach(prop::FiniteTimeReachability)

Return the set of states with respect to which to compute reachbility for a finite time reachability property.

time_horizon(prop::FiniteTimeReachability)

Return the time horizon of a finite time reachability property.

InfiniteTimeReachability{VT <: Vector{Union{<:Integer, <:Tuple, <:CartesianIndex}}, R <: Real}

InfiniteTimeReachability is similar to FiniteTimeReachability except that the time horizon is infinite, i.e., $K = \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.

reach(prop::InfiniteTimeReachability)

Return the set of states with which to compute reachbility for a infinite time reachability property.

convergence_eps(prop::InfiniteTimeReachability)

Return the convergence threshold of an infinite time reachability property.

ExactTimeReachability{VT <: Vector{Union{<:Integer, <:Tuple, <:CartesianIndex}}, T <: Integer}

Exact time reachability specified by a set of target/terminal states and a time horizon. That is, denote a trace by $\omega = s_1 s_2 s_3 \cdots$, then if $G$ is the set of target states and $K$ is the time horizon, the property is

\[ \mathbb{P}^{\pi, \eta}_{\mathrm{exact-reach}}(G, K) = \mathbb{P}^{\pi, \eta} \left[\omega \in \Omega : \omega[K] \in G \right].\]

reach(prop::ExactTimeReachability)

Return the set of states with which to compute reachbility for an exact time reachability prop.

time_horizon(prop::ExactTimeReachability)

Return the time horizon of an exact time reachability property.

FiniteTimeReachAvoid{VT <: Vector{Union{<:Integer, <:Tuple, <: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 $\omega = s_1 s_2 s_3 \cdots$, then if $G$ is the set of target states, $O$ is the set of states to avoid, and $K$ is the time horizon, the property is

\[ \mathbb{P}^{\pi, \eta}_{\mathrm{reach-avoid}}(G, O, K) = \mathbb{P}^{\pi, \eta} \left[\omega \in \Omega : \exists k \in \{0, \ldots, K\}, \, \omega[k] \in G, \; \forall k' \in \{0, \ldots, k' \}, \, \omega[k] \notin O \right].\]

reach(prop::FiniteTimeReachAvoid)

Return the set of target states.

avoid(prop::FiniteTimeReachAvoid)

Return the set of states to avoid.

time_horizon(prop::FiniteTimeReachAvoid)

Return the time horizon of a finite time reach-avoid property.

InfiniteTimeReachAvoid{VT <: Vector{Union{<:Integer, <:Tuple, <:CartesianIndex}}, R <: Real}

InfiniteTimeReachAvoid is similar to FiniteTimeReachAvoid except that the time horizon is infinite, i.e., $K = \infty$.

reach(prop::InfiniteTimeReachAvoid)

Return the set of target states.

avoid(prop::InfiniteTimeReachAvoid)

Return the set of states to avoid.

convergence_eps(prop::InfiniteTimeReachAvoid)

Return the convergence threshold of an infinite time reach-avoid property.

ExactTimeReachAvoid{VT <: Vector{Union{<:Integer, <:Tuple, <: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 $\omega = s_1 s_2 s_3 \cdots$, then if $G$ is the set of target states, $O$ is the set of states to avoid, and $K$ is the time horizon, the property is

\[ \mathbb{P}^{\pi, \eta}_{\mathrm{exact-reach-avoid}}(G, O, K) = \mathbb{P}^{\pi, \eta} \left[\omega \in \Omega : \omega[K] \in G, \; \forall k \in \{0, \ldots, K\}, \, \omega[k] \notin O \right].\]

reach(prop::ExactTimeReachAvoid)

Return the set of target states.

avoid(prop::ExactTimeReachAvoid)

Return the set of states to avoid.

time_horizon(prop::ExactTimeReachAvoid)

Return the time horizon of an exact time reach-avoid property.

FiniteTimeSafety{VT <: Vector{Union{<:Integer, <:Tuple, <:CartesianIndex}}, T <: Integer}

Finite time safety specified by a set of avoid states and a time horizon. That is, denote a trace by $\omega = s_1 s_2 s_3 \cdots$, then if $O$ is the set of avoid states and $K$ is the time horizon, the property is

\[ \mathbb{P}^{\pi, \eta}_{\mathrm{safe}}(O, K) = \mathbb{P}^{\pi, \eta} \left[\omega \in \Omega : \forall k \in \{0, \ldots, K\}, \, \omega[k] \notin O \right].\]

avoid(prop::FiniteTimeSafety)

Return the set of states with which to compute reachbility for a finite time reachability prop.

time_horizon(prop::FiniteTimeSafety)

Return the time horizon of a finite time safety property.

InfiniteTimeSafety{VT <: Vector{Union{<:Integer, <:Tuple, <:CartesianIndex}}, R <: Real}

InfiniteTimeSafety is similar to FiniteTimeSafety except that the time horizon is infinite, i.e., $K = \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.

avoid(prop::InfiniteTimeSafety)

Return the set of states with which to compute safety for a infinite time safety property.

convergence_eps(prop::InfiniteTimeSafety)

Return the convergence threshold of an infinite time safety property.

FiniteTimeReward{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 $\nu$. The time horizon $K$ is finite, so the discount factor can be greater than or equal to one. The property is

\[ \mathbb{E}^{\pi,\eta}_{\mathrm{reward}}(r, \nu, K) = \mathbb{E}^{\pi,\eta}\left[\sum_{k=0}^{K} \nu^k r(\omega[k]) \right].\]

reward(prop::FiniteTimeReward)

Return the reward vector of a finite time reward optimization.

discount(prop::FiniteTimeReward)

Return the discount factor of a finite time reward optimization.

time_horizon(prop::FiniteTimeReward)

Return the time horizon of a finite time reward optimization.

InfiniteTimeReward{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. $K = \infty$.

reward(prop::FiniteTimeReward)

Return the reward vector of a finite time reward optimization.

discount(prop::FiniteTimeReward)

Return the discount factor of a finite time reward optimization.

convergence_eps(prop::InfiniteTimeReward)

Return the convergence threshold of an infinite time reward optimization.

ExpectedExitTime{VT <: Vector{Union{<:Integer, <:Tuple, <:CartesianIndex}}, R <: Real}

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., $K = \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. Given an unsafe set $O$, the property is defined as

\[ \mathbb{E}^{\pi,\eta}_{\mathrm{exit}}(O) = \mathbb{E}^{\pi,\eta}\left[k : \omega[k] \in O, \, \forall k' \in \{0, \ldots, k - 1\}, \, \omega[k'] \notin O \right].\]

where $\omega = s_0 s_1 \ldots s_k$ is a trace of the system.

avoid(prop::ExpectedExitTime)

Return the set of unsafe states that we compute the expected hitting time with respect to.

convergence_eps(prop::ExpectedExitTime)

Return the convergence threshold of an expected exit time.

FiniteTimeDFAReachability{VT <: Vector{<:Integer}, 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).\]

reach(prop::FiniteTimeDFAReachability)

Return the set of DFA states with respect to which to compute reachbility for a finite time DFA reachability property.

time_horizon(prop::FiniteTimeDFAReachability)

Return the time horizon of a finite time DFA reachability property.

InfiniteTimeDFAReachability{VT <: Vector{<:Integer}, R <: Real}

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.

reach(prop::InfiniteTimeDFAReachability)

Return the set of DFA states with respect to which to compute reachbility for a infinite time DFA reachability property.

convergence_eps(prop::InfiniteTimeDFAReachability)

Return the convergence threshold of an infinite time DFA reachability property.

FiniteTimeDFASafety{VT <: Vector{<:Integer}, T <: Integer}

Finite time Safety 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).\]

avoid(prop::FiniteTimeDFASafety)

Return the set of DFA states with respect to which to compute safety for a finite time DFA safety property.

time_horizon(prop::FiniteTimeDFASafety)

Return the time horizon of a finite time DFA safety property.

InfiniteTimeDFASafety{VT <: Vector{<:Integer}, R <: Real}

InfiniteTimeDFASafety is similar to FiniteTimeDFASafety 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.

avoid(prop::InfiniteTimeDFASafety)

Return the set of DFA states with respect to which to compute safety for a infinite time DFA safety property.

convergence_eps(prop::InfiniteTimeDFASafety)

Return the convergence threshold of an infinite time DFA safety property.