Current languages for specifying multiagent protocols either over-constrain protocol enactments or complicate capturing their meanings. We propose Langshaw, a declarative protocol language based on (1) sayso, a new construct that captures who has priority over setting each attribute, and (2) nono and nogo, two constructs to capture conflicts between actions. Langshaw combines flexibility with an information model to express meaning. We give a formal semantics for Langshaw, procedures for determining the safety and liveness of a protocol, and a method to generate a message-oriented protocol (embedding needed coordination) suitable for flexible asynchronous enactment.
more »
« less
An Evaluation of Communication Protocol Languages for Engineering Multiagent Systems
Communication protocols are central to engineering decentralized multiagent systems. Modern protocol languages are typically formal and address aspects of decentralization, such as asynchrony. However, modern languages differ in important ways in their basic abstractions and operational assumptions. This diversity makes a comparative evaluation of protocol languages a challenging task. We contribute a rich evaluation of diverse and modern protocol languages. Among the selected languages, Scribble is based on session types; Trace-C and Trace-F on trace expressions; HAPN on hierarchical state machines, and BSPL on information causality. Our contribution is four-fold. One, we contribute important criteria for evaluating protocol languages. Two, for each criterion, we compare the languages on the basis of whether they are able to specify elementary protocols that go to the heart of the criterion. Three, for each language, we map our findings to a canonical architecture style for multiagent systems, highlighting where the languages depart from the architecture. Four, we identify design principles for protocol languages as guidance for future research.
more »
« less
- Award ID(s):
- 1908374
- PAR ID:
- 10274300
- Date Published:
- Journal Name:
- Journal of Artificial Intelligence Research
- Volume:
- 69
- ISSN:
- 1076-9757
- Page Range / eLocation ID:
- 1351 to 1393
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
We report an experimental realization of a modified counterfactual communication protocol that eliminates the dominant environmental trace left by photons passing through the transmission channel. Compared to Wheeler’s criterion for inferring past particle paths, as used in prior protocols, our trace criterion provides stronger support for the claim of the counterfactuality of the communication. We verify the lack of trace left by transmitted photons via tagging the propagation arms of an interferometric device by distinct frequency-shifts and finding that the collected photons have no frequency shift which corresponds to the transmission channel. As a proof of principle, we counterfactually transfer a quick response code image with sufficient fidelity to be scanned with a cell phone.more » « less
-
An interaction protocol specifies a decentralized multiagent system operationally by specifying constraints on messages exchanged by its member agents. Engineering with protocols requires support for a notion of refinement, whereby a protocol may be substituted without loss of correctness by one that refines it. We identify two desiderata for refinement. One, generality: refinement should not restrict enactments by limiting protocols or infrastructures under consideration. Two, preservation: to facilitate modular verification, refinement should preserve liveness and safety. We contribute a novel formal notion of protocol refinement based on enactments. We demonstrate generality by tackling the declarative framework of information protocols. We demonstrate preservation by formally establishing that our notion of refinement is safety and liveness preserving. We show the practical benefits of refinement by implementing a checker. We demonstrate that it is less time-intensive to check refinement (and thereby gain safety and liveness) than to recheck safety and liveness of a composition.more » « less
-
An interaction protocol specifies a decentralized multiagent system operationally by specifying constraints on messages exchanged by its member agents. Engineering with protocols requires support for a notion of refinement, whereby a protocol may be substituted without loss of correctness by one that refines it. We identify two desiderata for refinement. One, generality: refinement should not restrict enactments by limiting protocols or infrastructures under consideration. Two, preservation: to facilitate modular verification, refinement should preserve liveness and safety. We contribute a novel formal notion of protocol refinement based on enactments. We demonstrate generality by tackling the declarative framework of information protocols. We demonstrate preservation by formally establishing that our notion of refinement is safety and liveness preserving. We show the practical benefits of refinement by implementing a checker. We demonstrate that it is less time-intensive to check refinement (and thereby gain safety and liveness) than to recheck safety and liveness of a composition.more » « less
-
null (Ed.)A flexible communication protocol is necessary to build a decentralized multiagent system whose member agents are not coupled to each other's decision making.Information-based protocol languages capture a protocol in terms of causality and integrity constraints based on the information exchanged by the agents. Thus, they enable highly flexible enactments in which the agents proceed asynchronously and messages may be arbitrarily reordered. However, the existing semantics for such languages can produce a large number of protocol enactments, which makes verification of a protocol property intractable.This paper formulates a protocol semantics declaratively via inference rules that determine when a message emission or reception becomes enabled during an enactment, and its effect on the local state of an agent.The semantics enables heuristics for determining when alternative extensions of a current enactment would be equivalent, thereby helping produce parsimonious models and yielding improved protocol verification methods.more » « less