Behavioral and spatial observations in a logic for the π-calculus

Research output: Chapter in Book/Report/Conference proceedingConference contribution

44 Citations (Scopus)

Abstract

In addition to behavioral properties, spatial logics can talk about other key properties of concurrent systems such as secrecy, freshness, usage of resources, and distribution. We study an expressive spatial logic for systems specified in the synchronous π-calculus with recursion, based on a small set of behavioral and spatial observations. We give coinductive and equational characterizations of the equivalence induced on processes by the logic, and conclude that it strictly lies between structural congruence and strong bisimulation. We then show that model-checking is decidable for a useful class of processes that includes the finite-control fragment of the π-calculus.

Original languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures, Proceedings
EditorsI. Walukiewicz
PublisherSpringer-Verlag
Pages72-89
Number of pages18
Publication statusPublished - 1 Dec 2004
Event7th International Conference on Foundations of Software Science and Computation Structures - Barcelona, Spain
Duration: 30 Mar 2004 → …

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer-Verlag
Volume2987
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference7th International Conference on Foundations of Software Science and Computation Structures
CountrySpain
CityBarcelona
Period30/03/04 → …

Keywords

  • Semantics
  • Models
  • Bigraphical reactive

Fingerprint Dive into the research topics of 'Behavioral and spatial observations in a logic for the π-calculus'. Together they form a unique fingerprint.

  • Cite this

    Caires, L. (2004). Behavioral and spatial observations in a logic for the π-calculus. In I. Walukiewicz (Ed.), Foundations of Software Science and Computation Structures, Proceedings (pp. 72-89). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2987). Springer-Verlag.