Characteristic formulae for fixed-point semantics: a general framework

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 o...

Full description

Saved in:
Bibliographic Details
Published in:Mathematical structures in computer science 2012-04, Vol.22 (2), p.125-173
Main Authors: ACETO, LUCA, INGOLFSDOTTIR, ANNA, LEVY, PAUL BLAIN, SACK, JOSHUA
Format: Article
Language:English
Subjects:
Behavioural
Computer science
Concurrency
Construction
Fixed points (mathematics)
Logic
Mathematical analysis
Mathematical models
Recursive
Semantics
Temporal logic
Theory
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0960-1295
1469-8072
DOI:10.1017/S0960129511000375