Persons and affiliations

Date

Description

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.