Speaker: Kais Klai, LIPN, Université Sorbonne Paris Nord.
Monday 11 April 2022, 11:00, (room 1Z25 ENS Paris-Saclay and online)
Abstract: In this talk, I will present different variants of an hybrid graph structure called Symbolic Observation Graph (SOG) that preserves stutter-invariant temporal properties of finite systems. The SOG is an explicit graph where nodes are encoded symbolically with decision diagram techniques and allows on-the-fly LTL model checking. Despite its theoretical exponential complexity, it reduces in practice the state space explosion problem and performs better than explicite and symbolic exhaustive verification approaches. The second part of the talk illustrates the adoption of such a graph for the verification and the supervision of the opacity property. Finally, I will introduce a current work on model checking of vulnerability and specific properties of Blockchain smart contracts -based processes.