The next Comète seminar will take place on Thursday, January 20th at 2pm in Salle Philippe Flajolet (LIX - Alan Turing building, École Polytechnique). Valeria Vignudelli, postdoctoral researcher at ENS Lyon, will talk about “A powerset construction for nondeterministic and probabilistic systems”.

Abstract: The powerset construction provides a method for establishing trace equivalence of nondeterministic transition systems. The definition of trace equivalence requires to directly compare the traces that can be performed by two systems. The main idea of the powerset construction is that trace equivalence can be recovered alternatively by first determinizing the systems, i.e., transforming them into deterministic systems, and then by recovering trace equivalence on the original systems as bisimulation equivalence on the determinized systems. On transition systems combining nondeterministic and probabilistic choices, the definition of trace equivalence has itself some underlying intricacies. In this talk, I will show how a powerset-like construction can be defined for nondeterministic and probabilistic labelled transition systems. The construction we propose fits a generalization of the powerset construction based on coalgebra, an abstract framework to study transition system semantics. This allows us to recover many interesting properties of trace equivalence for nondeterministic and probabilistic transition systems. This talk is based on joint work with Filippo Bonchi and Ana Sokolova, available at https://arxiv.org/abs/1808.00923