salle A. Pnueli CE3
27 juin 2013 - 14h00
Synchronization Invariants
par Klaus Draeger de University of Oxford
Abstract: Invariants are an important tool for the verification of
complex systems. One very simple class of invariants for compositional
reasoning is given by linear constraints on the occurrences of
synchronization sequences. This class of invariants exhibits some
quite interesting properties, including connections to mathematical
fields such as topology. I am currently investigating generalizations
of these concepts to more general structures than words, and more
general kinds of systems, such as probabilistic ones. In this talk, I
will give an overview of this work in progress.
