Master Thesis - Edge Case Scenario Generation for Signal-Temporal-Logic Described Traffic Rules

23.04.2026, Abschlussarbeiten, Bachelor- und Masterarbeiten

Formalizing traffic rules in temporal logic is a key step toward the verification and validation of autonomous driving systems. Recent work has shown that interstate traffic rules can be represented in temporal logic and checked algorithmically. However, even if a rule is syntactically well-formed, it is often difficult to judge whether the formal specification truly matches the intended meaning of the natural-language traffic rule. Small modeling errors may lead to specifications that accept undesirable behaviors or reject valid ones, especially in rare, extreme, and boundary-case scenarios. There are methods that can automatically verify whether a given specification with a set of mutants that specifies certain types of formulation errors.

However, these methods are limited to checking the consistency of the original specification with a predefined set of mutants, and they do not provide easy-to-understand examples of the behaviors that are accepted or rejected by the specification. At the same time, methods for synthesizing traffic scenarios from formal specifications have opened the door to systematically exploring the behavior induced by a specification. This thesis builds on these ideas and investigates how automatically generated scenarios can support an example-driven workflow for validating and refining temporal-logic traffic rules.

Signal temporal logic (STL) will be used as the determination criterion for the generated scenarios, which will be optimized to be representative, extreme, or boundary cases with respect to the given specification. Specifically, STL robustness will be used as a measure of criticality, and the generated scenarios will be optimized to approach zero robustness and therefore be considered as corner cases. Rule-compliant reachable set [2] can be computed to provide a reference and limit the search space during the scenario generation. After the scenarios are generated, they will be evaluated by human users to determine whether they are valid and representative examples of the intended traffic rule through conducting user surveys. This would provide a first step toward semi-automatic repair or refinement of traffic-rule specifications based on counterexamples and representative scenarios.

Details can be found in the attached file.

Kontakt: shuaiyi.li@tum.de

Mehr Information