Distributed model-checking of security properties in games with incomplete information

Marek A. Bednarczyk (Institute of Computer Science) m.bednarczyk >at>

Description: The project aims to use distributed computation techniques to speed-up the model-checking of (security) properties of agents in systems with imperfect information. Technically this leads to the imperfect information variant of strategic logic ATL (Alternating-time Temporal Logic, a branching-time temporal logic that naturally describes computations of multi-agent system and multiplayer games), cf. (Alur et al., 2002),(Schobbens, 2004),(Kacprzak and Penczek, 2005). Model-checking of agent systems can be supported by a number of optimization techniques, such as symbolic model-checking, automatic abstraction, partial order reduction, etc. This applies especially to specifications written in temporal logic where such optimization techniques are relatively well developed. Recently, work on optimization has been initiated also for ATL (Kacprzak and Penczek, 2005). However, the results in this area apply mostly to the case of "classical" ATL, in which agents are assumed to have perfect information about the current global state of the system.
This assumption is clearly unrealistic when real life systems are considered. Unfortunately, theoretical results on strategic logics with imperfect information, see (Schobbens, 2004) and (Jamroga and Âgotnes, 2007), show that optimization similar to that for perfect information ATL is hard to achieve. Even more importantly, the incremental algorithm that computes winning strategies in "classical" ATL does not work for imperfect information agents. This is because, for imperfect information, optimality of a fragment of a strategy crucially depends on the rest of the strategy. On the logical level, this is reflected by the fact that the typical fixpoint characteristics of strategic-temporal operators do not hold any more. As a result, the brute force approach seems to be the only method to compute the optimal strategy, which leads to exponential-time algorithms. Luckily, models in the area of security tend to have relatively small state spaces. Thus, even brute force techniques become plausible, especially if one can speed up model-checking computations with help of a distributed scalable cloud computing framework (see Buyya et al., 2009) such as DACFrame (Bednarczyk et al., 2009).
The tasks to be performed within the project include, among others:
  1. Elaboration of DACFrame, a scalable cloud computing framework to support intensive distributed computation.
  2. Development of a methodology to perform distributed model-checking of security properties in imperfect information agent systems with the help of DACFrame.
  3. Conducting a series of model-checking experiments of several classes of properties in several classes of models for which distributed model-checking brings benefits.
  4. Initiation of research on optimization techniques based on current state of the art research on temporal logic (LTL and CTL) as well as strategic logics with full information (classical ATL).
  5. Investigation of possible distributed model-checking and optimization techniques for several classes of properties and models, especially in the domain of security.

 Alur R., Henzinger T.A, Kupferman O. Alternating-time Temporal Logic. Journal of the ACM, 49:672–713, 2002.

 Schobbens P.Y. Alternating-time logic with imperfect recall. Electronic Notes in Theoretical Computer Science, 85(2), 2004.

 Kacprzak M., Penczek W. Fully Symbolic Unbounded Model Checking for Alternating-time Temporal Logic, Autonomous Agents and Multi-Agent Systems, 11(1):69–89, 2005.

 Jamroga W., Âgotnes T. Constructive knowledge: What agents can achieve under incomplete information. Journal of Applied Non-Classical Logics, 17(4):423–475, 2007.

 Buyya R., Yeo C.S., Venugopal S., Broberg J., Brandic I. Cloud computing and emerging it platforms: Vision, hype, and reality for delivering computing as the 5th utility. Future Generation Computer Systems, 25(6):599–616, June 2009.

 Bednarczyk M.A, Neumann J, Pawłowski W., Siekielski A., Sławiński J. Towards an Object-Oriented Framework for Higher Order Genetic Algorithms, Proc. 24th Intern. Conf. on Artificial Intelligence, Kraków, Proceedings of Artificial Intelligence Studies, 6(29): 65-69, 2009.

You are here: Home Projects Distributed model-checking of security properties in games with incomplete information