A spatial logic for concurrency. I

DOI10.1016/S0890-5401(03)00137-8zbMath1068.03022DBLPjournals/iandc/CairesC03OpenAlexW2076632469WikidataQ56982113 ScholiaQ56982113MaRDI QIDQ1887152

Luís Caires, Luca Cardelli

Publication date: 23 November 2004

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0890-5401(03)00137-8

zbMATH Keywords

concurrency\(\pi\)-calculusspatial logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (48)

Specification and refinement of mobile systems in MTLA and mobile UML ⋮ A spatial logic for concurrency. II ⋮ Linear and affine logics with temporal, spatial and epistemic operators ⋮ Fresh logic: Proof-theory and semantics for FM and nominal techniques ⋮ A proof theoretic view of spatial and temporal dependencies in biochemical systems ⋮ An exercise in structural congruence ⋮ A calculus and logic of resources and processes ⋮ Belief, knowledge, lies and other utterances in an algebra for space and extrusion ⋮ Axiomatisation and decidability of multi-dimensional Duration Calculus ⋮ Verification of finite-state machines: a distributed approach ⋮ Concurrent weighted logic ⋮ Process calculi for biological processes ⋮ A Logic for Distributed Higher Order π-Calculus ⋮ A decentralised graphical implementation of mobile ambients ⋮ A Spatial Logic for Simplicial Models ⋮ Deciding safety properties in infinite-state pi-calculus via behavioural types ⋮ Minimisation of spatial models using branching bisimilarity ⋮ Learning and Detecting Emergent Behavior in Networks of Cardiac Myocytes ⋮ Spatial and behavioral types in the pi-calculus ⋮ A Decentralized Implementation of Mobile Ambients ⋮ A Spatial Equational Logic for the Applied π-Calculus ⋮ PHYSARUM SPATIAL LOGIC ⋮ Spatial-behavioral types for concurrency and resource control in distributed systems ⋮ Team bisimilarity, and its associated modal logic, for BPP nets ⋮ Modular Markovian Logic ⋮ A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting ⋮ Relating reasoning methodologies in linear logic and process algebra ⋮ Hierarchical Design Rewriting with Maude ⋮ Name-passing in an ambient-like calculus and its proof using spatial logic ⋮ A Complete Axiomatic System for a Process-Based Spatial Logic ⋮ Elimination of quantifiers and undecidability in spatial logics for concurrency ⋮ Abstract interpretation based verification of temporal properties for BioAmbients ⋮ Graphical models of separation logic ⋮ A spatial equational logic for the applied \(\pi \)-calculus ⋮ Spatial-Behavioral Types, Distributed Services, and Resources ⋮ Model checking mobile stochastic logic ⋮ Decidable Extensions of Hennessy-Milner Logic ⋮ Compositionality for quantitative specifications ⋮ Verification of spatial and temporal modalities in biochemical systems ⋮ Bialgebraic methods and modal logic in structural operational semantics ⋮ A theory of structural stationarity in the \(\pi\)-calculus ⋮ Logical vs. behavioural specifications ⋮ A study on team bisimulation and H-team bisimulation for BPP nets ⋮ Kind Bigraphs ⋮ Manipulating Trees with Hidden Labels ⋮ Extensionality of Spatial Observations in Distributed Systems ⋮ Co-Algebraic Models for Quantitative Spatial Logics ⋮ A Name Abstraction Functor for Named Sets

Uses Software

• SLMC

Cites Work

• Modal logics for mobile processes
• A new approach to abstract syntax with variable binding
• Results on the propositional \(\mu\)-calculus
• Multisets and structural congruence of the pi-calculus with replication
• Model checking mobile processes
• Algebraic laws for nondeterminism and concurrency
• Functions as processes
• The Logic of Bunched Implications
• Anytime, anywhere
• Extensionality and intensionality of the ambient logics
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A spatial logic for concurrency. I