Communication in concurrent dynamic logic (Q1095653)

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.