Propositional Dynamic Logic for Reasoning about First-Class Agent Interaction Protocols.

For agents to fulfill their potential of being intelligent and adaptive, it is useful to model their interaction protocols as executable entities that can be referenced, inspected, composed, shared, and invoked between agents, all at runtime. We use the term first-class protocol to refer to such protocols. Rather than having hard-coded decision-making mechanisms for choosing their next move, agents can inspect the protocol specification at runtime to do so, increasing their flexibility. In this article, we show that propositional dynamic logic (PDL) can be used to represent and reason about the outcomes of first-class protocols. We define a proof system for PDL that permits reasoning about recursively defined protocols. The proof system is divided into two parts: one for reasoning about terminating protocols, and one for reasoning about nonterminating protocols. We prove that proofs about terminating protocols can be automated, while proofs about nonterminating protocols are unable to be automated in some cases. We prove that, for a restricted class of nonterminating protocols, proofs about them can be transformed to proofs about terminating protocols, making them automatable.