A logic for true concurrency

DOI10.1145/2629638zbMATH Open1321.68355arXiv1110.4094OpenAlexW1766510866WikidataQ130864088 ScholiaQ130864088MaRDI QIDQ5501929FDOQ5501929

Authors: Paolo Baldan, Silvia Crafa 

Publication date: 14 August 2015

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

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.

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

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

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)

Cites Work

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

Cited In (22)

• Behavioural logics for configuration 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
• Title not available (Why is that?)
• 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
• Characterising spectra of equivalences for event structures, logically
• Team bisimilarity, and its associated modal logic, for BPP nets
• Contextual equivalences in configuration structures and reversibility
• Event identifier logic
• Logics and Bisimulation Games for Concurrency, Causality and Conflict
• Title not available (Why is that?)
• Truly concurrent logic via in-between specification
• Title not available (Why is that?)
• 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)