Reasoning About Web Services in a Temporal Action Logic

The paper presents an approach to reasoning about Web services in a temporal action theory. Web services are described by specifying their interaction protocols in an action theory based on a dynamic, linear-time, temporal logic. The proposed framework is based on a social approach to agent communication, where the effects of communicative actions allow changes in the social state, and interaction protocols are defined in terms of the creation and fulfillment of commitments and permissions among the agents. We show how to introduce epistemic operators in the action theory to deal with incomplete information, and we address the problem of verifying properties of Web services, as well as the problem of reasoning about the composition of Web services.