Representing and reasoning about utilization of cloud computing as Bayesian games with epistemic logic

In order to advise a cloud client whether to use cloud services or not, we model the scenario of utilization of cloud computing based on Bayesian games. These games are strategic games with incomplete information for modeling the interaction between a client and a cloud provider with uncertainty about load capacity. However these games do not normally consider the reasoning abilities of players. One solution is to use formal logics which allow for modeling the reasoning abilities of agents as well as allowing formal reasoning about certain properties of games such as the solution of games. In this paper, we propose an epistemic logic to study strategic games with incomplete information. In this logic we can for instance precisely describe what the requirements and consequences of informative actions are in the cloud services scenario. We can reason what rational agents should do if they can choose between different available actions. In addition, this language can be used as a semantically well-defined query language for model checkers to automatically verify the game descriptions with respect to their intended specifications. (C) 2013 The Authors. Published by Elsevier B.V.