Specification
IntervalMDPAbstractions.FiniteTimeRegionReachability — Type
FiniteTimeRegionReachabilityA struct representing a finite-time reachability property.
IntervalMDPAbstractions.InfiniteTimeRegionReachability — Type
InfiniteTimeRegionReachabilityA struct representing a infinite-time reachability property.
IntervalMDPAbstractions.FiniteTimeRegionReachAvoid — Type
FiniteTimeRegionReachAvoidA struct representing a finite-time reach-avoid property.
IntervalMDPAbstractions.InfiniteTimeRegionReachAvoid — Type
InfiniteTimeRegionReachAvoidA struct representing a infinite-time reach-avoid property.
IntervalMDPAbstractions.ExactTimeRegionReachAvoid — Type
ExactTimeRegionReachAvoidA struct representing a Exact-time reach-avoid property.
IntervalMDPAbstractions.FiniteTimeRegionSafety — Type
FiniteTimeRegionSafetyA struct representing a finite-time safety property.
IntervalMDPAbstractions.InfiniteTimeRegionSafety — Type
InfiniteTimeRegionSafetyA struct representing a infinite-time safety property.
IntervalMDPAbstractions.ExactTimeRegionReachability — Type
ExactTimeRegionReachabilityA struct representing a exact-time reachability property.
IntervalMDPAbstractions.reach — Function
reachReturn the reach region of a reachability or reach-avoid property.
IntervalMDPAbstractions.avoid — Function
avoidReturn the avoid region of a reach-avoid or safety property.
IntervalMDPAbstractions.dim — Function
dimReturn the dimension of the reach and avoid regions of a regional property.
Abstraction problem
IntervalMDPAbstractions.AbstractionProblem — Type
AbstractionProblemA struct of a system and a specification to be used in the abstraction process.
IntervalMDPAbstractions.system — Function
systemReturn the system of an abstraction problem.
IntervalMDPAbstractions.specification — Function
specificationReturn the specification of an abstraction problem.
IntervalMDPAbstractions.decouple — Function
decoupleDecoupled the noise in the system dynamics of an AbstractionProblem if possible, and transform the specification accordingly.
If the system dynamics cannot be decoupled, an error is thrown.
Returns a tuple of the decoupled AbstractionProblem and the transformation used.