A logic for true concurrency

DOI10.1145/2629638MaRDI QIDQ5501929zbMATH OpenOpenAlexWikidataFDO

Authors Paolo Baldan, Silvia Crafa

Publication date 14 August 2015

Published in Journal of the ACM (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1110.4094

zbMATH Keywords

causalityhistory-preserving bisimilaritymu-calculusevent structuresbehavioural equivalencestrue concurrency

Mathematics Subject Classification ID

Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: We propose a logic for true concurrency whose formulae predicate about events in computations and their causal dependencies. The induced logical equivalence is hereditary history preserving bisimilarity, and fragments of the logic can be identified which correspond to other true concurrent behavioural equivalences in the literature: step, pomset and history preserving bisimilarity. Standard Hennessy-Milner logic, and thus (interleaving) bisimilarity, is also recovered as a fragment. We also propose an extension of the logic with fixpoint operators, thus allowing to describe causal and concurrency properties of infinite computations. We believe that this work contributes to a rational presentation of the true concurrent spectrum and to a deeper understanding of the relations between the involved behavioural equivalences.

Recommendations

• A logic for true concurrency
• Local model checking in a logic for true concurrency
• Truly concurrent logic via in-between specification
• scientific article; zbMATH DE number 4210118
• Model checking a logic for true concurrency

Cites work

• scientific article; zbMATH DE number 1809623 (Why is no real title available?)
• scientific article; zbMATH DE number 4074506 (Why is no real title available?)
• scientific article; zbMATH DE number 70113 (Why is no real title available?)
• scientific article; zbMATH DE number 176758 (Why is no real title available?)
• scientific article; zbMATH DE number 1241703 (Why is no real title available?)
• scientific article; zbMATH DE number 794261 (Why is no real title available?)
• scientific article; zbMATH DE number 1418351 (Why is no real title available?)
• A logic for true concurrency
• Algebraic laws for nondeterminism and concurrency
• Bisimulation from open maps
• Computer Science Logic
• Concurrent bisimulations in Petri nets
• Logics and Bisimulation Games for Concurrency, Causality and Conflict
• Model checking mobile processes
• Model-Checking Games for Fixpoint Logics with Partial Order Models
• Model-checking games for fixpoint logics with partial order models
• Model-checking processes with data
• Petri nets, event structures and domains. I
• Refinement of actions and equivalence notions for concurrent systems
• The linear time -- branching time spectrum. I: The semantics of concrete, sequential processes.
• The power of the future perfect in program logics
• Undecidability of domino games and hhp-bisimilarity.

Cited in

(22)

• Behavioural logics for configuration structures
• Conflict vs causality in event structures
• Conflict vs causality in event structures
• Foundations of Software Science and Computational Structures
• Un)Decidability for History Preserving True Concurrent Logics.
• When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus
• Verification of finite-state machines: a distributed approach
• Local model checking in a logic for true concurrency
• Logical Concurrency Control from Sequential Proofs
• A logic with reverse modalities for history-preserving bisimulations
• scientific article; zbMATH DE number 7559463 (Why is no real title available?)
• A coalgebraic semantics for causality in Petri nets
• Model checking a logic for true concurrency
• A study on team bisimulation and H-team bisimulation for BPP nets
• Team bisimilarity, and its associated modal logic, for BPP nets
• Characterising spectra of equivalences for event structures, logically
• Contextual equivalences in configuration structures and reversibility
• Event identifier logic
• Logics and Bisimulation Games for Concurrency, Causality and Conflict
• Truly concurrent logic via in-between specification
• scientific article; zbMATH DE number 4085006 (Why is no real title available?)
• A logic for true concurrency

This page was built for publication: A logic for true concurrency

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5501929)