Communication in concurrent dynamic logic
type: Item
instance of: scholarly article
title: Communication in concurrent dynamic logic
zbMATH Open document ID: 0632.68032
DOI: 10.1016/0022-0000(87)90035-3
published in: Journal of Computer and System Sciences
publication date: 1987-01-01T00:00:00Z
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.
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03B70
zbMATH DE Number: 4028888
zbMATH Keywords: Concurrent dynamic logic
zbMATH Keywords: reasoning about isolated concurrent programs
zbMATH Keywords: communication
zbMATH Keywords: Expressiveness
zbMATH Keywords: decidability
author: David Peleg
reviewed by: Luboš Brim
MaRDI profile type: Publication
full work available at URL: 0022-0000(87)90035-3
OpenAlex ID: W1991259963
cites work: A Proof System for Communicating Sequential Processes
cites work: Q4053084
cites work: Alternation
cites work: Q3919057
cites work: Semantics of nondeterminism, concurrency, and communication
cites work: Propositional dynamic logic of regular programs
cites work: Q4343990
cites work: Recurring Dominoes: Making the Highly Undecidable Highly Understandable
cites work: And/Or Programs: A New Approach to Structured Programming
cites work: Communicating sequential processes
cites work: A Theory of Communicating Sequential Processes
cites work: A programming language for the inductive sets, and applications
cites work: Propositional dynamic logic of nonregular programs
cites work: Q3862380
cites work: The correctness of nondeterministic programs
cites work: A calculus of communicating systems
cites work: Q3939208
cites work: Concurrent Processes and Their Syntax
cites work: Definability in dynamic logic
cites work: Concurrent dynamic logic
cites work: Alternation and the computational complexity of logic programs
cites work: Propositional dynamic logic of looping and converse is elementarily decidable
description: scientific article; zbMATH DE number 4028888