Applications of the Enhanced Decomposition Procedure
Laurent Fribourg, Romain Soulat · 2013
Applications of the Enhanced Decomposition ProcedureWe now apply the decomposition procedure (enhanced for safety properties) for several examples.For each example, we are given a global control box R and a safety set S that contains it.We generate a k-invariant decomposition Δ of R satisfying Unf Δ (R) ⊂ S, thus proving that Unf Δ (R) is a controlled invariant, and that the system is safe.EXAMPLE A2.1.-Letus consider the helicopter motion example 2.3 of Chapter 2. We take R =[ -0 .3 ,0 .3] × [-0.5, 0.5] in plane (x 1 ,x 2 ).This corresponds to an equilibrium zone centered at the state (0, 0) of the ground vehicle, and a variability of ±0.3 for position and ±0.5 for velocity.We take S =[ -0 .4 ,0 .4] × [-0.7, 0.7] for the safety region, which corresponds to an additional variability of ±0.1 for position and velocity.(This is the same safety zone S as in [DIN 11].)The application of algorithm 4.1 to R and S with k =6and d =4 is successful, yielding a k-invariant decomposition Δ of R of the form {(V i , π i )} i=1,...,10 1 satisfying Unf Δ (R) ⊂ S. The decomposition Δ is