Guest Talk: Prof. Lenore Zuck: P^3 and P^5

Wednesday, November 20, 2019, 10:30am

Location: RWTH Aachen University, Department of Computer Science - Ahornstr. 55, building E3, room 9u10

Speaker: Prof. Lenore Zuck (Univ. of Illinois at Chicago)

 

Abstract:

The method of Invisible Invariants was conceived to verify Properties of Parameterized Protocols (P^3), for any instantiation, in one fell swoop. Given a deductive proof rule for the desired property, the method calls for two steps: (1) An heuristic to generate the hypothesis of the proof rule, and (2) a method to validate the premises of the proof rule once an hypothesis is generated. At the time of its conception, the method was carried out by model checkers based on BDDs, and both steps were performed without ever having to explicitly generate the hypotheses, which rendered them ``Invisible." Moreover, initially the method was applied to generate invariants, but shortly after its introduction, it was used to generate other types of hypotheses. Nowadays, the method can be applied without BDDs, which renders Invisible Invariants to be neither invisible nor invariants. The first part of the talk will attempt to demystify the fundamental ideas behind the methods and its applicability for a large class of infinite-state systems.

The second part of the talk will add the other two P’s: Probabilistic and Planner-less. There, the thesis is that, unlike the common approach where one first converts a parameterized MDP into a (probability-less) parameterized system by the aid of a Planner and then proves it property, one can instead abstract the parameterized MDP into a finite MDP, and only then prove its properties. That is, instead of dealing first with the randomized aspects and only then with the parameterized ones, P^5 swaps the order by dealing first with the parameterized aspects and then with the randomized ones, while obtaining new abilities to prove the properties of such systems.