Paper Info
Title
Behavioral and Spatial Observations in a Logic for the pi-Calculus
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 pi-calculus with recursion, based on a small set of behavioral and spatial observations. We give coin-ductive 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 pi-calculus.
Year
DOI
Venue
2004
10.1007/978-3-540-24727-2_7
LECTURE NOTES IN COMPUTER SCIENCE
Keywords
DocType
Volume
model checking
Conference
2987
ISSN
Citations 
PageRank 
0302-9743
24
0.98
References 
Authors
13
1
Name
Order
Citations
PageRank
Luís Caires1103763.30