A Logical Way to Negotiate Services

TL;DR

This paper introduces a formal language for automated service negotiation, allowing service providers to efficiently manage complex interactions and dependencies using logical constraints and process algebra.

Contribution

It presents a novel formal negotiation policy language that supports recursive service composition and uses quantifier elimination for efficient constraint handling.

Findings

The language enables automated, correct service negotiation.

Supports recursive service composition from sub-providers.

Ensures positive responses propagate up the service chain.

Abstract

Service providers commonly provide only a fixed catalog of services to their clients. Both clients and service providers can benefit from service negotiation, in which a client makes a query for a specific service, and the provider counters with an offer. The query could include parameters that control the performance, reliability, and function of the service. However, a problem with service negotiation is that it can be expensive for a service provider to support. In this paper we define a formal negotiation policy language that enables automated service negotiation. In the model supported by the language, service providers can recursively obtain the services they need from sub-providers. The queries made by clients, and the offers returned from service providers, are expressed in quantifier-free first-order logic. Quantifier elimination is used to transform constraints between providers and sub-providers. The pattern of interaction between clients and service providers is defined in process algebra. We show a correctness property of our language: if sub-providers respond positively to queries, then so does the provider itself.