A spatial logic for the hybrid π-calculus

Abstract

We present a formal logic for stating properties of systems expressed in the hybrid π-calculus, or Φ-calculus. It is a very expressive logic, subsuming many standard logics like CTL and the modal μ-calculus. Because the π-calculus and the Φ-calculus allow passing of names to achieve reconfigurability of hybrid systems, and because we must abstract over these names, the logic (a hybrid extension of a logic by Caires and Cardelli for the π-calculus) uses a new method of defining abstractions - FM set theory - for expressing syntax and semantics of Φ-calculus models, and for expressing the semantics of spatial logic. We provide several new constructions for this logic, including an assumeguarantee principle, and illustrate many of the semantic features using an extended example of a robotic parts feeder and parts carrier in a minifactory. © Springer-Verlag 2004.