A logical characterization of well branching event structures

DOI10.1016/0304-3975(92)90181-EMaRDI QIDQ1190487zbMATH OpenOpenAlexFDO

Authors Madhavan Mukund, P. S. Thiagarajan

Publication date 26 September 1992

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(92)90181-e

zbMATH Keywords

causalityconcurrencyconflictdistributed systemreasoning about the occurrences of events

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

It is given a characterization of well branching event structures by using a suitable chosen version of temporal logic. The modalities of this version of temporal logic permit to talk about three basic features of distributed system: causality, conflict and concurrency. The notions of prime event structures and well branching event structures are presented. Then it is presented the language and developed a Kripke-style semantics for it with branching prime event structures serving as the frames. The main contribution is a sound and complete axiomatization of validity with respect to the chosen semantics.

Recommendations

• scientific article; zbMATH DE number 4208063
• scientific article; zbMATH DE number 218548
• Three logics for branching bisimulation
• scientific article; zbMATH DE number 4108727
• The temporal logic of branching time

Cites work

• Decidability for branching time
• scientific article; zbMATH DE number 4049019 (Why is no real title available?)
• scientific article; zbMATH DE number 1028831 (Why is no real title available?)
• scientific article; zbMATH DE number 4119602 (Why is no real title available?)

Cited in

(10)

• Context-free event domains are recognizable
• Verification of reactive systems using temporal logic with clocks
• Branching cells for asymmetric event structures
• scientific article; zbMATH DE number 4208063 (Why is no real title available?)
• Behavioural characterizations of partial order logics
• Context-free event domains are recognizable
• scientific article; zbMATH DE number 5587277 (Why is no real title available?)
• Event identifier logic
• Models and logics for true concurrency.
• Concurrent hyperproperties

This page was built for publication: A logical characterization of well branching event structures

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