Strategy Synthesis for Multi-Agent Systems with Imperfect Information and Imperfect Recall
Abstract: This report aims to study and compare currently available tools for uniform strategy synthesis in multi-player versus environment games of imperfect information and imperfect recall. These games are represented as a graph of game states, and goal sequences of states are typically represented using temporal logic formulae. Strategies for achieving those goals can then be found by evaluating the formulae. Specifically the time complexity and addressed game objectives of the tools were of interest. Not too much is known about this particular field of game theory, and strategy synthesis is complicated and computationally heavy. Today there is only one completed tool specialized for the particular game structure of interest, the Strategic Model Checker (SMC). Three tools were found which could be used for the task, out of which two seemed worthy of further investigation. Firstly, the aforementioned Strategic Model Checker (SMC) provided a good reference as a completed program. Secondly, an experimental version of the ATLir Model Checker, a newer tool still under development specialized for the same task, could provide an example at the cutting edge of the field. The evaluation of the literature as well as the tools confirmed and corroborated earlier findings in that there are few implementations available, that the time complexity of their performance is steep, albeit improving, and that they deal with a potentially very wide range of game objectives, which can be described using Alternating Time Temporal Logic, or ATL. The performance analysis concluded that the newer tool shows promising results for smaller games, but that SMC still produces more reliable results for larger instances as well as more complicated test cases.
AT THIS PAGE YOU CAN DOWNLOAD THE WHOLE ESSAY. (follow the link to the next page)