Asynchronous Transition System Games for Two Processes and Their Analysis
摘要
We propose and investigate a new model of a distributed game played on a non-deterministic asynchronous transition system over two processes. This game is played between an environment and a distributed team of the two processes where each process has only partial information of the ongoing play – namely complete information up to the last synchronization and only its own local evolution since this last synchronization. The key algorithmic decision problem, for a given winning objective, is the existence of a distributed co-operative winning strategy for the team to meet that objective. We address this question for global safety, local reachability and global/simultaneous reachability objectives. We carry out a thorough analysis of these games and present natural fixpoint based algorithms for solving them. This allows us to construct distributed winning strategies with an explicit distributed finite-memory in the form of key past information, and also yields near optimal decision procedures. Specifically, our analysis shows that the decision problems for global safety and local reachability objectives are NP-complete. We also establish that the decision problem for global reachability objective is PSPACE-hard and provide an NEXPTIME algorithm for the same.