Model Checking Collaboration,Competition and Dense Fault Resilience

In this thesis, I introduce BSIL(basicstrategy-interactionlogic) and TCL(temporal cooperation logic) which can help in formally define and verify the strategy interaction property of a game. The former, BSIL, is an extension to ATL (alternating-timelogic)for the specification of strategies interaction of players in a system. BSIL is able to describe one system strategy that can cooperate with several strategies of the environment for different requirements. Such properties are important in practice and Is how that such properties are notexpressibleinATL*,GL(gamelogic),andAMC(alternatingμ-calculus). Specifically, BSIL is more expressive than ATL but incomparable with ATL*, GL, and AMC in expressiveness. I show that, for fulfilling a specification in BSIL, a memoryful strategy is necessary. I also show that the model checking complexity of BSIL is PSPACE-complete and is of lower complexity than those of ATL*, GL, AMC, and the general strategy logics. Which may imply that BSIL can be useful in closing the gap between large scale real-world projects and the time consuming game-theoretical results. I then show the feasibility of our techniques by implementation and experiment with our PSPACE model-checking algorithm for BSIL. On the other hand, TCL allows successive definition of strategies for agents and agencies. Like BSIL the expressiveness of TCL is still incompa rable with ATL*, GL and AMC. However, it can describe deterministic Nash equilibria while BSIL cannot. I prove that the model checking complexity of TCL is EXPTIME-complete. TCL enjoys this relatively cheap complexity by disallowing a too close entanglement between cooperation and competition while allowing such entanglement leads to an on-elementary complexity. I have implemented a model checker for TCL and shown the feasibility of model checking in the experimentonsomebenchmarks. Although BSIL and TCL have decent expressive power and benefit from relatively low complexity. PSPACE-complete and EXPTIME-complete is still not good enough for real problem. To adopt the game concept to real world problem, I introduce an algorithm to calculatethe highest degr ee of fault tolerance a system can achieve with the control of a safety critical systems. Which can be reduced to solving a game between a malicious environment and a controller. During the game play, the environment tries to break the system through injecting failures while the controller tries to keep the system safe by making correct decisions. I found a new control objective which offers a better balance between complexity and precision for such systems: we seek systems that are k-resilient. A systemisk-resilient means it is able to rapidly recover from a sequence of small number, up to k, of local faults infinitely many times if the blocks of up to k faults are separated by short recovery periods in which no fault occurs. k-resilience is a simple abstraction from the precise distribution of local faults, but I believe it is much more refined than the traditional objective to maximize the number of local faults. I will provide detail argument of why this is the right level of abstraction for safety critical systems when local faults are few and far between. I have proved, with respect to resilience, the computational complexity of constructing optimal control is low. And a demonstration of the feasibility through an implementation and experimental results will be in following chapters.