Characteristic formulae for fixed-point semantics: A general framework

Luca Aceto*, Anna Ingolfsdottir, Paul Blain Levy, Joshua Sack

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

14 Citations (Scopus)


The concurrency theory literature 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 paper provides a general view of characteristic formulae that are expressed in terms of logics that have a facility for the recursive definition of formulae. We show how several examples of characteristic-formula constructions in the literature can be recovered as instances of the proposed general framework, and how the framework can be used to yield novel constructions. The paper also offers general results pertaining to the definition of co-characteristic formulae and of characteristic formulae expressed in terms of infinitary modal logics.

Original languageEnglish
Pages (from-to)125-173
Number of pages49
JournalMathematical Structures in Computer Science
Issue number2
Early online date28 Feb 2012
Publication statusPublished - Apr 2012

Bibliographical note

Funding Information:
The work of Luca Aceto, Anna Ingolfsdottir and Joshua Sack was partially supported by the projects ‘New Developments in Operational Semantics’ (nr. 080039021) and ‘Processes and Modal Logics’ of the Icelandic Research Fund. Joshua Sack was further supported by a grant from Reykjavik University’s Development Fund. Paul Blain Levy was supported by the ESPRC Advanced Research Fellowship EP/E056091/1.

ASJC Scopus subject areas

  • Mathematics (miscellaneous)
  • Computer Science Applications


Dive into the research topics of 'Characteristic formulae for fixed-point semantics: A general framework'. Together they form a unique fingerprint.

Cite this