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.
Bibliographical noteFunding 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