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

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:

- Elaboration of DACFrame, a scalable cloud computing framework to support intensive distributed computation.
- Development of a methodology to perform distributed model-checking of security properties in imperfect information agent systems with the help of DACFrame.
- Conducting a series of model-checking experiments of several classes of properties in several classes of models for which distributed model-checking brings benefits.
- 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).
- Investigation of possible distributed model-checking and optimization techniques for several classes of properties and models, especially in the domain of security.