Characteristic formulae for fixed-point semantics: a general framework
LUCA ACETO, ANNA INGOLFSDOTTIR, PAUL BLAIN LEVY, JOSHUA SACK
Source record
Source: Crossref
Published: Feb 28, 2012
DOI: 10.1017/s0960129511000375
Open original source ↗Source abstract
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.
Evidence graph
No public relationships recorded yet.
Integrity note: This page is a factual metadata record created by deterministic ingestion. It is not a claim that the work moves a mathematical frontier or has been independently verified.