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

behavioural equivalencescausalityevent structureshistory-preserving bisimilaritymu-calculustrue 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

• A logic for true concurrency
• Algebraic laws for nondeterminism and concurrency
• Bisimulation from open maps
• Computer Science Logic
• Concurrent bisimulations in Petri nets
• 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?)
• 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

(25)

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

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)