Problem

Problem{S <: IntervalMarkovProcess, F <: Specification}

A 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::Problem)

Return the system of a problem.

specification(prob::Problem)

Return the specification of a problem.

strategy(prob::Problem)

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)

Property

Super type for all system Property

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

LTLFormula

Linear Temporal Logic (LTL) property (first-order logic + next and until operators) [1]. Let $ϕ$ denote the formula and $M$ denote an interval Markov process. Then compute $M ⊧ ϕ$.

[1] Vardi, M.Y. (1996). An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds) Logics for Concurrency. Lecture Notes in Computer Science, vol 1043. Springer, Berlin, Heidelberg.

isfinitetime(prop::LTLFormula)

Return false for an LTL formula. LTL formulas are not finite time property.

LTLfFormula

An LTL formula over finite traces [1]. See LTLFormula for the structure of LTL formulas. Let $ϕ$ denote the formula, $M$ denote an interval Markov process, and $H$ the time horizon. Then compute $M ⊧ ϕ$ within traces of length $H$.

Fields

• formula::String: LTL formula
• time_horizon::T: Time horizon of the finite traces

[1] Giuseppe De Giacomo and Moshe Y. Vardi. 2013. Linear temporal logic and linear dynamic logic on finite traces. In Proceedings of the Twenty-Third international joint conference on Artificial Intelligence (IJCAI '13). AAAI Press, 854–860.

isfinitetime(spec::LTLfFormula)

Return true for an LTLf formula. LTLf formulas are specifically over finite traces.

time_horizon(spec::LTLfFormula)

Return the time horizon of an LTLf formula.

PCTLFormula

A Probabilistic Computation Tree Logic (PCTL) formula [1]. Let $ϕ$ denote the formula and $M$ denote an interval Markov process. Then compute $M ⊧ ϕ$.

[1] M. Lahijanian, S. B. Andersson and C. Belta, "Formal Verification and Synthesis for Discrete-Time Stochastic Systems," in IEEE Transactions on Automatic Control, vol. 60, no. 8, pp. 2031-2045, Aug. 2015, doi: 10.1109/TAC.2015.2398883.

AbstractReachability

Super type for all reachability-like properties.

FiniteTimeReachability{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).\]

isfinitetime(prop::FiniteTimeReachability)

Return true for FiniteTimeReachability.

terminal_states(spec::FiniteTimeReachability)

Return the set of terminal states of a finite time reachability property.

reach(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.

time_horizon(prop::FiniteTimeReachability)

Return the time horizon of a finite time reachability property.

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

isfinitetime(prop::InfiniteTimeReachability)

Return false for InfiniteTimeReachability.

terminal_states(prop::InfiniteTimeReachability)

Return the set of terminal states of an infinite time reachability property.

reach(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.

convergence_eps(prop::InfiniteTimeReachability)

Return the convergence threshold of an infinite time reachability property.

AbstractReachAvoid

A property of reachability that includes a set of states to avoid.

FiniteTimeReachAvoid{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).\]

isfinitetime(prop::FiniteTimeReachAvoid)

Return true for FiniteTimeReachAvoid.

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

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{R <: Real, VT <: AbstractVector{<:CartesianIndex}}

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

isfinitetime(prop::InfiniteTimeReachAvoid)

Return false for InfiniteTimeReachAvoid.

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

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.

AbstractSafety

Super type for all safety properties.

FiniteTimeSafety{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).\]

isfinitetime(prop::FiniteTimeSafety)

Return true for FiniteTimeSafety.

terminal_states(spec::FiniteTimeSafety)

Return the set of terminal states of a finite time safety property.

avoid(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).

time_horizon(prop::FiniteTimeSafety)

Return the time horizon of a finite time safety property.

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

isfinitetime(prop::InfiniteTimeSafety)

Return false for InfiniteTimeSafety.

terminal_states(prop::InfiniteTimeSafety)

Return the set of terminal states of an infinite time safety property.

avoid(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).

convergence_eps(prop::InfiniteTimeSafety)

Return the convergence threshold of an infinite time safety property.

AbstractReward{R <: Real}

Super type for all reward properties.

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 $\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].\]

isfinitetime(prop::FiniteTimeReward)

Return true for FiniteTimeReward.

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. $H = \infty$, so the optimal policy will be stationary.

isfinitetime(prop::InfiniteTimeReward)

Return false for InfiniteTimeReward.

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.

AbstractHittingTime

Super type for all HittingTime properties.

ExpectedExitTime{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$.

isfinitetime(prop::ExpectedExitTime)

Return true for ExpectedExitTime.

terminal_states(prop::ExpectedExitTime)

Return the set of terminal states of an expected hitting time property.

avoid(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).

convergence_eps(prop::ExpectedExitTime)

Return the convergence threshold of an expected exit time.