Diagram Models for Interacting Components (Extended Version)

We present a semantic model and a logic for systems of concurrent components. Following the categorical approach, we define a category of component models in which limits can be used to construct systems from simpler components. A novel idea is to use diagrams in this category, not just limit objects, as models for the logic. The resulting “diagram logic ” allows one to specify both behavioural and structural aspects of systems: temporal operators and structural predicates can be freely interleaved. As in first-order logic, system components can be quantified over, bound to variables and classified by predicates. There is a price we must pay for the expressive power of the logic: the set of valid formulae is not recursively enumerable.