# Dynamic Epistemic Logic with Communication Actions

## TL;DR

This paper introduces a new Dynamic Epistemic Logic framework incorporating concurrent communication actions using process calculus, enabling proofs of soundness, completeness, and decidability.

## Contribution

It presents a novel approach combining process calculus with Action Models Logic for dynamic epistemic logic with concurrency, ensuring formal proof properties.

## Key findings

- Proof of soundness, completeness, and decidability for the logic
- Axiomatization of the proposed logic
- Reduction method for proofs

## Abstract

This work proposes a Dynamic Epistemic Logic with Communication Actions that can be performed concurrently. Unlike Concurrent Epistemic Action Logic introduced by Ditmarsch, Hoek and Kooi, where the concurrency mechanism is the so called true concurrency, here we use an approach based on process calculus, like CCS and CSP, and Action Models Logic. Our approach makes possible the proof of soundness, completeness and decidability, different from the others approaches. We present an axiomatization and show that the proof of soundness, completeness and decidability can be done using a reduction method.