BLC 2010

Characteristic Formulae for Fixed-Point Semantics: A General Framework
Paul Levy
Joint work with Luca Aceto, Anna Ingólfsdóttir and Joshua Sack of Reykjavik University The literature on concurrency theory offers a wealth of examples of characteristic-formula constructions for various behavioural relations over finite labelled transition systems and Kripke structures 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 provides a general view of characteristic formulae that are expressed in terms of logics with a facility for the recursive definition of formulae. Several examples of characteristic-formula constructions from the literature can be recovered as instances of the proposed general framework, and it can also be used to yield novel constructions.