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.

Att undersöka konsten att fatta välavvägda beslut är av största intresse inom flertalet akademiska områden. Vare sig det gäller att utveckla artificiell intelligens med pålitilig prestanda, eller att undersöka det mänskliga psyket, så är förmågan att basera kritiska avgöranden på en begränsad mängd datapunkter definitivt mycket viktig. Detta är ett ämne som flitigt tas upp inom spelteori. Spelteori är ett matematiskt område som studerar spel och deras egenskaper. Spelen kan representera nästan vilket scenario som helst där en mängd spelare försöker nå ett mål. Denna rapport behandlar ett särskilt område inom spelteorin, som beskriver s.k. flerspelar-spel med ofullständig information och ofullständigt minne. I sådana spel kan flera spelare delta, men de är inte alltid medvetna om spelets nuvarande tillstånd (ofullständig information), och de kan inte minnas något av sina tidigare drag (ofullständigt minne). För att ytterligare förtydliga: Ofullständig information syftar på fall där vissa (eller samtliga) spelare inte kan skilja på vissa tillstånd i spelet. En sådan grupp av sammanblandade tillstånd kallas för en observation; spelaren i fråga observerar att den befinner sig i något av gruppens tillstånd, men inte vilket. Observationerna är också individuella - olika spelare har i regel olika observationer. Ofullständigt minne innebär att spelaren eller spelarna inte minns vilka tidigare tillstånd de befunnit sig i; de kan således bara fatta beslut med avseende på vad de de observerar i nuläget. Man kan föreställa sig att spelarna är robotar utan minneslagring - de läser av spelets läge via sina sensorer, men de kan inte minnas vad som tidigare skett.

I sådana spel kan det vara intressant att finna någon metod som alltid garanterar att spelarna lyckas. Detta görs genom att analysera spelet och skapa, eller syntetisera, ett antal regler som spelarna följer - en strategi - som baseras på spelets nuvarande tillstånd. Spelarna behöver tilldelas drag som ger gynnsamma utfall oavsett vad de observerar. Om detta går att göra så kallas den resulterande strategin observationsbaserad, eller enhetlig.

Vid syntesen av dylika strategier är det vanligt att beskriva spelarnas mål med hjälp av temporallogik-formler, och utvärdera dessa (Se stycke 2.2). Dessvärre är utvärderingsprocessen mycket prestandakrävande, och nya tekniker krävs för att göra den genomförbar. Denna rapport syftar till att utforska och jämföra några av de nuvarande verktyg som finns tillgängliga för att finna och skapa enhetliga strategier i spel med flera spelare, ofullständig information och ofullständigt minne. Denna typ av modeller kan användas för att undersöka många typer av scenarion, både inom beteendevetenskaper som ekonomi såväl som datalogiska ämnen, exempelvis AI och robotik. De senare kategorierna tjänar väl som konkreta exempel, eftersom AI-system kan hamna i situationer där de har tillgång till begränsad information om det rådande läget, och behöver fatta välgrundade, säkra beslut.