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.

翻译：服务提供商通常仅向其客户提供固定的服务目录。客户和服务提供商均可从服务协商中获益——客户提出特定服务请求，而提供商以提议作为回应。该请求可包含控制服务性能、可靠性和功能的参数。然而，服务协商面临的一个问题是，支持该过程对服务提供商而言成本高昂。本文定义了一种形式化协商策略语言，可实现自动化服务协商。在该语言支持的模型中，服务提供商可以递归地向下级提供商获取所需服务。客户提出的请求以及服务提供商返回的提议均以无量词一阶逻辑表达。量词消去用于转换提供商与下级提供商之间的约束。客户与服务提供商之间的交互模式通过进程代数定义。我们证明了该语言的一个正确性属性：若下级提供商对请求作出肯定响应，则服务提供商本身也会作出肯定响应。