## 3 Optimal Controller Design Using SDCS
In this study, two synthesis algorithms are considered: one for safety objectives and the other for optimization objectives. The safety objective operates as an invariant, ensuring the precise fulfillment of desired rigid system behaviors, such as mutual exclusions in shared resources. These operations are achieved using the at least fixpoint method, similar to the computational steps in DCS. The optimization objective, on the other hand, aims to iteratively minimize a given cost function over a time window cumulatively. Through an optimization algorithm parameterized by a parameter k, it enables optimization over states within the time window up to a desired distance in the future. Since it encompasses the safety objective, the working principle of the optimization algorithm focuses on avoiding the worst case scenario, thus being pessimistic. Utilizing the computational framework of the aforementioned DCS and the environment provided by ReaX, a systematic modeling environment was presented for the yet uncontrolled UAV plant, along with the desired control objectives, as outlined below. Figure 7 provides an overview of the proposed approach. As seen in Figure 7, firstly, the plant which is the part of the dynamic model of the quadcopter is combined with the objectives as a symbolic system in line with the proposed strategy. The SDCS approach is represented as an automaton which makes a state transition guarded with the input (U) in each time interval. The system under consideration involves states characterized by velocity and position. During each transition, these values are updated according to the passage of time, the control input U, and the current state of velocity and position. The primary objective of the proposed SDCS method is to minimize the time required to reach the final state, ensuring that the velocity is zero when the position aligns with the desired target. This entails optimizing the control inputs to achieve rapid convergence to the target position while satisfying the condition of zero velocity at the final state. The controller that forces the plant to provide desired objectives is generated considering the SDCS method. Finally, the SDCS controller is integrated into the Simulink model of the quadcopter within the scope of software in the loop (SIL) approach. Initially, the given plant was encoded along with specifications using the strategy outlined in Figure 8. Subsequently, the controller was compiled and obtained, which, when added to the initially uncontrolled plant, ensured the desired system behaviors. Figure 7: Overview of the SDCS approach [29]. The proposed strategy, depicted as an automaton in Figure 8, orchestrates state transitions based on the thrust force (U) exerted at each time interval. States encompass velocity and position valuations, with values updating on transitions through time, U, and current velocity and position. The primary objective is the swift attainment of the final state (qr), where velocity reaches zero upon reaching the desired target position. The process involves (i) activating the braking mechanism at state qn to prevent overshooting using an optimization algorithm, (ii) maintaining thrust force at limit U\({}_{\text{L}}\) until the braking mechanism activates, denoted as enough, and (iii) dividing the remaining tmin into phases with appropriate U pairs (p1 and p2) to ensure the simultaneous achievement of the desired velocity and position at state qc. This section elaborates on the model and control objectives to establish a UAV controller. The uncontrolled behaviors of the quadcopter at the \(x\), \(y\), and \(z\)-axis are modeled as parallel data flow equations. The quadcopter discussed above is encoded within the ReaX environment using the same plant model. Additionally, after specifying target \(x\), \(y\), and \(z\) positions and limiting values for U, controller synthesis algorithms are employed to synthesize a controller that exhibits the desired system behaviors.