Proof Everything Everywhere But Not All At Once : A Robotic Case Study
Dominik Grzelak · 2025
This talk presents a robotic case study that demonstrates a modular and formal approach to verifying complex cyber-physical systems (CPS). Using 'bigraphical reactive automata,' the talk models and proves correct behaviors in distributed robotic workcells, such as collision-free navigation, and cooperative pick-and-place tasks. The study combines algebraic, geometric, and model-checking methods to make robotic proof construction scalable and interpretable. That is, “everywhere,” across multiple subsystems or views, but “not all at once.” It emphasizes compositional verification, modular scene decomposition for systematic robotic system design.:[English] I Introduction II Case Study: Robotic Workcell Demonstrator III Modeling with Bigraphical Reactive Automata IV Verification Methodology * Algebraic-Geometric Proof Approach * Model Checking * Compositional Verification V Representative Proofs VI Outlook VII Appendix [German] I Einleitung II Fallstudie: Robotic Workcell Demonstrator III Modellierung mit Bigraphischen Reaktiven Automaten IV Verifikationsmethodik * Algebraisch-geometrischer Beweisansatz * Modellprüfung (Model Checking) * Kompositionale Verifikation V Beispielhafte Nachweise VI Ausblick VII Anhang