ICE-TCS Lectures Series - Joshua Sack - Characteristic formulae for fixed-point semantics: a general approach


The next ICE-TCS  talk for this semester will be delivered on Friday, 9 April,  by Joshua Sack (Reykjavik University). 

The talk, which is entitled Characteristic formulae for fixed-point semantics: a general approach, will be held at 14:00 in room M1.05 at the new premises of Reykjavik University in Nauthólsvík.


Characteristic formulae are tools for expressing essential properties of behavioral relations, typically expressing equivalence classes of bisimulation equivalence relations or the set of processes that can simulate or be simulated by a given process.  Characteristic formulae have a number of uses, such as reducing implementation verification to model checking, measuring the expressivity of a language, and proving completeness of a proof system.  The literature on concurrency theory offers a wealth of examples of characteristic formulae constructions that are defined in terms of fixed points of suitable functions.  Such constructions and their proofs of correctness have been developed independently, but have a common underlying structure. This talk presents joint work with Luca Aceto, Anna Ingolfsdottir, and Paul Blain Levy on providing a general view of characteristic formulae that are expressed in terms of logics with a facility for the recursive definition of formulae.