Using formal tools in computer science to describe games is an interesting problem. We give games, exactly two person games, an axiomatical foundation based on the process algebra ACP (Algebra of Communicating Process). A fresh operator called opponent's alternative composition operator (OA) is introduced into ACP to describe game trees and game strategies, called GameACP. And its sound and complete axiomatical system is naturally established. To model the outcomes of games (the co-action of the player and the opponent), correspondingly in GameACP, the execution of GameACP processes, another operator called playing operator (PO) is extended into GameACP. We also establish a sound and complete axiomatical system for PO. Finally, we give the correctness theorem between the outcomes of games and the deductions of GameACP processes.
Game-CTR @cite_0 introduces games into CTR (Concurrent Transaction Logic) to model and reason about runtime properties of workflows that are composed of non-cooperative services -- such as Web Services. Game-CTR includes a model and proof theory which can be used to specify executions under some temporal and causality constraints, and also a game solver algorithm to convert such constraints into other equivalent Game-CTR formulas to be executed more efficiently. @cite_20 develop a game semantics for a certain kind of process calculus with two interacting agents. Games and strategies on this process calculus are defined, and strategies of the two agents determine the execution of the process. And also, a certain class of strategies correspond to the so-called syntactic schedulers of Chatzikokolakis and Palamidessi. In these works, the games used are not dialogue games, and there are no interactions such as questions and answers and also no wining concept.
@cite_0 @cite_20
2498434591 2013667259
A workflow is a collection of cooperating, coordinated activities designed to carry out a well-defined complex process, such as trip planning, graduate student registration procedure, or a business process in a large enterprise. Executing a workflow, thus, involves coordinated execution of multiple long-running steps in an environment of distributed, heterogeneous processing entities. Workflow management systems provide a framework for capturing the interaction among the activities in a workflow and are recognized as a new paradigm for integrating disparate systems, including legacy systems. However, in order to realize its full potential a number of limitations of the current workflow models, including lack of a clear theoretical basis has to be addressed. Workflows must be specified declaratively, verified formally, and scheduled automatically. In this dissertation first we show that Concurrent Transaction Logic (abbr. CTR) is a natural logical formalism for representing workflow control graphs, temporal and causality constraints that workflow executions must obey, for reasoning about the consistency of workflow specifications, and for scheduling workflows in the presence of those constraints. Next, we develop Game-CTR, a natural extension of CTR designed for modeling and reasoning about run-time properties of workflows that are composed of non-cooperating services—such as Web services. We develop a model and proof theory for Game-CTR and show how it can be used to specify executions under a fairly large class of temporal and causality constraints. We then develop a game solver algorithm that converts such specifications (which are formulas in Game-CTR) into other, equivalent Game-CTR formulas, a coordinator, that can be executed more efficiently and without backtracking. We develop a game semantics for process algebra with two interacting agents. The purpose of our semantics is to make manifest the role of knowledge and information flow in the interactions between agents and to control the information available to interacting agents. We define games and strategies on process algebras, so that two agents interacting according to their strategies determine the execution of the process, replacing the traditional scheduler. We show that different restrictions on strategies represent different amounts of information being available to a scheduler. We also show that a certain class of strategies corresponds to the syntactic schedulers of Chatzikokolakis and Palamidessi, which were developed to overcome problems with traditional schedulers modelling interaction. The restrictions on these strategies have an explicit epistemic flavour.