Veilige en Robuuste Doelgerichte Planning voor Autonome Systemen

Safety, liveness, and robustness are fundamental for deploying reliable autonomous systems. These systems must avoid unsafe states and actions and ensure task completion, even in uncertain, non-deterministic environments. However, existing planning approaches often separate safety from decision-making, treating it as an external verification step. This leads to an iterative, costly, and often error-prone process, especially when faced with real-world conditions where contingencies are numerous, making verification or safe planning difficult. This dissertation introduces Tumato 2.0, a constraint-based planning framework that embeds safety directly into the decision-making process. Instead of generating plans first and verifying safety afterward, Tumato inherently prevents unsafe behaviors from being considered in the first place. By enforcing constraints that guarantee safety while maintaining goal-directed behavior, Tumato eliminates the need for separate safety verification. Unlike probabilistic models, which require predefined transition probabilities, Tumato operates without such dependencies, assuming (biased) non-deterministic outcomes instead. Its policies are generated through constraint-solving techniques, ensuring that safety and liveness are maintained by construction. The research follows a structured approach to establish and then validate Tumato's effectiveness. First, formal verification techniques are applied to an autonomous robotic system, highlighting the limitations of traditional post hoc safety verification. Next, a comprehensive survey of existing decision-making frameworks—including probabilistic planning and temporal scheduling—hints at their struggles in balancing safety, robustness, and usability. Tumato 2.0 is then introduced as a constraint-based alternative and formally specified using Linear Temporal Logic (LTL), ensuring that its guarantees are both rigorous and verifiable. To assess its practical viability, an empirical evaluation is conducted, comparing Tumato to ad hoc planning methods. The results confirm that Tumato not only enforces safety and liveness constraints but also remains usable for practitioners. Finally, the integration of Tumato with Systems-Theoretic Process Analysis (STPA) demonstrates how high-level safety requirements can be automatically translated into enforceable constraints within autonomous planning, addressing a common gap between safety engineering and real-world deployment. Apart from simulations, Tumato's approach has been validated on a real Autonomous Mobile Robot (AMR) operating in an industrial-like environment. This practical application demonstrates the framework's ability to maintain safety and goal-directed behavior while further emphasizing its robustness and usability. This dissertation makes several contributions to the field of autonomous systems. It confirms that safety, liveness, and robustness are inherently linked and should not be treated as separate concerns. It provides an alternative to probabilistic models by introducing a constraint-based approach that ensures safety without requiring explicit probability distributions. Additionally, it demonstrates how formal aspects, such as LTL, can enhance verification but also usability, making constraint-based planning more accessible to practitioners. The empirical validation further solidifies Tumato's effectiveness, showing that it provides strong safety guarantees without sacrificing practical applicability. As autonomous systems continue to play a larger role in industry, transportation, and safety-critical applications, the need for reliable and inherently safe decision-making frameworks will only grow. Tumato 2.0 represents a step toward bridging the gap between theoretical formal methods and real-world autonomous behavior. By embedding safety (engineering) directly into planning, it offers a verifiable and practical solution for ensuring that autonomous agents operate reliably in complex environments.