Specification
IntervalMDPAbstractions.FiniteTimeRegionReachability — TypeFiniteTimeRegionReachabilityA struct representing a finite-time reachability property.
IntervalMDPAbstractions.InfiniteTimeRegionReachability — TypeInfiniteTimeRegionReachabilityA struct representing a infinite-time reachability property.
IntervalMDPAbstractions.FiniteTimeRegionReachAvoid — TypeFiniteTimeRegionReachAvoidA struct representing a finite-time reach-avoid property.
IntervalMDPAbstractions.InfiniteTimeRegionReachAvoid — TypeInfiniteTimeRegionReachAvoidA struct representing a infinite-time reach-avoid property.
IntervalMDPAbstractions.ExactTimeRegionReachAvoid — TypeExactTimeRegionReachAvoidA struct representing a Exact-time reach-avoid property.
IntervalMDPAbstractions.FiniteTimeRegionSafety — TypeFiniteTimeRegionSafetyA struct representing a finite-time safety property.
IntervalMDPAbstractions.InfiniteTimeRegionSafety — TypeInfiniteTimeRegionSafetyA struct representing a infinite-time safety property.
IntervalMDPAbstractions.ExactTimeRegionReachability — TypeExactTimeRegionReachabilityA struct representing a exact-time reachability property.
IntervalMDPAbstractions.reach — FunctionreachReturn the reach region of a reachability or reach-avoid property.
IntervalMDPAbstractions.avoid — FunctionavoidReturn the avoid region of a reach-avoid or safety property.
IntervalMDPAbstractions.dim — FunctiondimReturn the dimension of the reach and avoid regions of a regional property.
Abstraction problem
IntervalMDPAbstractions.AbstractionProblem — TypeAbstractionProblemA struct of a system and a specification to be used in the abstraction process.
IntervalMDPAbstractions.system — FunctionsystemReturn the system of an abstraction problem.
IntervalMDPAbstractions.specification — FunctionspecificationReturn the specification of an abstraction problem.
IntervalMDPAbstractions.decouple — FunctiondecoupleDecoupled 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.