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.
