- Titel
- Proof Everything Everywhere But Not All At Once
- Untertitel
- A Robotic Case Study
- Zitierfähige Url:
- https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa2-999174
- Übersetzter Titel (DE)
- Beweise alles aber nicht überall gleichzeitig : Eine Fallstudie aus der Robotik
- Erstveröffentlichung
- 2025
- DOI
- https://doi.org/10.25368/2025.369
- Abstract (EN)
- 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.
- (This talk was held during the 1st informal Bigraph Workshop on 'Bigraphs and Cyber-physical Spaces) at TU Dresden, Faculty of Computer Science.)
- Freie Schlagwörter (EN)
- bigraphs, cyber-physical spaces, bigraphical reactive systems, modularity, model checking
- Klassifikation (DDC)
- 004
- Klassifikation (RVK)
- SK 130
- ST 136
- ST 620
- Publizierende Institution
- Technische Universität Dresden, Dresden
- Förder- / Projektangaben
- Deutsche Forschungsgemeinschaft (DFG)
Exzellenzstrategie – EXC 2050/1
Centre for Tactile Internet with Human-in-the-Loop
(CeTI)
ID: 390696704 - Version / Begutachtungsstatus
- publizierte Version / Verlagsversion
- URN Qucosa
- urn:nbn:de:bsz:14-qucosa2-999174
- Veröffentlichungsdatum Qucosa
- 22.10.2025
- Dokumenttyp
- Vorlesung/Vortrag
- Sprache des Dokumentes
- Englisch
- Lizenz / Rechtehinweis
CC BY 4.0- Inhaltsverzeichnis
[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