Co-Algebraic Models for Quantitative Spatial Logics 1

We introduce a class of coalgebraic models and a family of modal logics that support the specification of spatial properties of distributed applications. The evaluation of a formula yields a value in a suitable multi-valued algebraic structure, giving a measure of the satisfaction of a requirement, induced by the decomposition of a system into subsystems, meant as available resources. As semantic domain we consider certain algebraic structures, called c-semirings, that allow us to generalize boolean logics to the multi-valued case, while keeping a number of the axioms of boolean algebras. Under suitable conditions on the structure of c-semirings, we show that, even if our logical formalisms are equipped with spatial operators, the interpretation of formulas fully characterizes bisimilarity.