Protocolized Modeling and Verification of Cyber Physical Systems - Giovanni Merlino

Giovanni Merlino, professor of computer science engineering at the University of Messina, presents the redesigned final module of his cyber-physical systems (CPS) course, framing formal verification techniques—linear temporal logic (LTL), finite state machine equivalence/refinement, and model checking—as a form of 'protocolization' that makes hidden assumptions, tradeoffs, and human-machine interactions explicit. He walks through concepts like safety vs. liveness properties, simulation vs. bisimulation, the CEGAR (counter-example guided abstraction refinement) technique, and Büchi automata, ultimately proposing a layered model (robot-level, swarm-level, smart-city-level) where engineering tensions like hyper-safety vs. liveness or pedestrian priority vs. system efficiency require explicit governance levers.