Systems Modelling via Resources and Processes: Philosophy, Calculus, Semantics, and Logic

DOI10.1016/j.entcs.2007.02.020zbMath1277.68202MaRDI QIDQ2864163

David J. Pym, Chris Tofts

Publication date: 6 December 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2007.02.020

zbMATH Keywords

synchrony; model checking; semantics; location; access control; resource; process calculus; bunched logic; field theory; discrete event simulation

Mathematics Subject Classification ID

03B70: Logic in computer science

68Q60: Specification and verification (program logics, model checking, etc.)

68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Related Items

Counting the Cost in the Picalculus (Extended Abstract), Bunched sequential information, A logic of separating modalities, Temporal BI: proof system, semantics and translations, Algebra and logic for access control, Erratum to: ``Algebra and logic for access control, Errata for ``A calculus and logic of resources and processes and their consequences, A Modal BI Logic for Dynamic Resource Properties, Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding

Cites Work

• A calculus and logic of resources and processes
• Proof systems for satisfiability in Hennessy-Milner logic with recursion
• Calculi for synchrony and asynchrony
• A calculus of communicating systems
• The semantics of entailment. II
• A process algebra of communicating shared resources with dense time and priorities
• Possible worlds and resources: The semantics of \(\mathbf{BI}\)
• The semantics and proof theory of the logic of bunched implications
• Reports of the Midwest category seminar. IV
• A domain equation for bisimulation
• The semantics of BI and resource tableaux
• A term model for synchronous processes
• A Powerdomain Construction
• The Logic of Bunched Implications
• A simple process algebra based on atomic actions with resources
• A denotational semantics for a process-based simulation language
• Getting Demos models right. (I). Practice
• Getting Demos models right. (II) … and theory
• Anytime, anywhere
• BI as an assertion language for mutable data structures
• Computer Science Logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item