Abstract
We present a logic that can express properties of freshness, secrecy, structure, and behavior of concurrent systems. In addition to standard logical and temporal operators, our logic includes spatial operations corresponding to composition, local name restriction, and a primitive fresh name quantifier. Properties can also be defined by recursion; a central aim of this paper is then the combination of a logical notion of freshness with inductive and coinductive definitions of properties.
Original language | English |
---|---|
Pages (from-to) | 194-235 |
Number of pages | 42 |
Journal | Information and Computation |
Volume | 186 |
Issue number | 2 |
DOIs | |
Publication status | Published - 1 Nov 2003 |
Event | 4th Symposium on Theoretical Aspects of Computer Software - Sendai, Japan Duration: 29 Oct 2001 → 31 Oct 2001 |
Keywords
- Semantics
- Models
- Bigraphical reactive