Communication in concurrent dynamic logic

DOI10.1016/0022-0000(87)90035-3MaRDI QIDQ1095653zbMATH OpenOpenAlexFDO

Authors David Peleg

Publication date 1987

Published in Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0022-0000(87)90035-3

zbMATH Keywords

communicationConcurrent dynamic logicdecidabilityExpressivenessreasoning about isolated concurrent programs

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Review text

Concurrent dynamic logic (CDL) is a variant of dynamic logic, which attempts to provide a framework for reasoning about isolated concurrent programs. This paper investigates three extensions in CDL, tailored towards incorporating communication mechanisms into the programs. Communication via channels gives rise to channel-CDL, communication based on shared variables is modeled by shared-CDL, and, finally, a communication allowing only the transmission of messages to a main control process leads to a system named count-CDL. Both the propositional and the first-order levels are considered. Expressiveness and decidability results are given. A brief comparative discussion concludes the paper.

Recommendations

• Concurrent dynamic logic
• A propositional dynamic logic for concurrent programs based on the -calculus
• Propositional dynamic logics for communicating concurrent programs with CCS's parallel operator
• Dynamic epistemic logic with communication actions
• A Propositional Dynamic Logic for CCS Programs

Cites work

• A calculus of communicating systems
• A programming language for the inductive sets, and applications
• A Proof System for Communicating Sequential Processes
• A Theory of Communicating Sequential Processes
• Alternation
• Alternation and the computational complexity of logic programs
• And/Or Programs: A New Approach to Structured Programming
• Communicating sequential processes
• Concurrent dynamic logic
• Concurrent Processes and Their Syntax
• Definability in dynamic logic
• scientific article; zbMATH DE number 3664336 (Why is no real title available?)
• scientific article; zbMATH DE number 3731310 (Why is no real title available?)
• scientific article; zbMATH DE number 3755842 (Why is no real title available?)
• scientific article; zbMATH DE number 3468252 (Why is no real title available?)
• scientific article; zbMATH DE number 1032009 (Why is no real title available?)
• Propositional dynamic logic of looping and converse is elementarily decidable
• Propositional dynamic logic of nonregular programs
• Propositional dynamic logic of regular programs
• Recurring Dominoes: Making the Highly Undecidable Highly Understandable
• Semantics of nondeterminism, concurrency, and communication
• The correctness of nondeterministic programs

Cited in

(22)

• Concurrent program schemes and their logics
• Parallel action: Concurrent dynamic logic with independent modalities
• Towards reasoning about Petri nets: a propositional dynamic logic based approach
• Dynamic epistemic logic with communication actions
• Bisimilar and logically equivalent programs in PDL with parallel operator
• Kleisli, Parikh and Peleg compositions and liftings for multirelations
• Tableaux for constructive concurrent dynamic logic
• Bisimilar and logically equivalent programs in PDL
• Complexity analysis of propositional concurrent programs using domino tiling
• Propositional dynamic logic for Petri nets with iteration
• A propositional dynamic logic for concurrent programs based on the -calculus
• A Propositional Dynamic Logic for CCS Programs
• A Complete STIT Logic for Knowledge and Action, and Some of Its Applications
• Quantificational modal logic with sequential Kripke semantics
• Concurrent dynamic logic
• A dynamic logic for deductive verification of multi-threaded programs
• Propositional dynamic logic with storing, recovering and parallel composition
• Concurrent dynamic algebra
• Taming multirelations
• Endowing concurrent Kleene algebra with communication actions
• Constructive modal logics. I
• Semantics of communication in simple multimodular programs

This page was built for publication: Communication in concurrent dynamic logic

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