Premium
PROPOSITIONAL DYNAMIC LOGIC FOR REASONING ABOUT FIRST‐CLASS AGENT INTERACTION PROTOCOLS
Author(s) -
Miller Tim,
McBurney Peter
Publication year - 2011
Publication title -
computational intelligence
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.353
H-Index - 52
eISSN - 1467-8640
pISSN - 0824-7935
DOI - 10.1111/j.1467-8640.2011.00387.x
Subject(s) - mathematical proof , computer science , executable , class (philosophy) , protocol (science) , theoretical computer science , flexibility (engineering) , programming language , artificial intelligence , mathematics , medicine , statistics , geometry , alternative medicine , pathology
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.