Modelling Concurrent Programs as Multi-Player Games of Imperfect Information against Nature

Abstract: Concurrent programs exists all around us. Whether someone is liking a photo on a social media platform or whether someone is doing a bank-transaction, concurrency is acting behind the scenes. Due to the nature of concurrent pro- grams having multiple Users, or Threads, a range of different problems can emerge. Some of these problems stem from the limited knowledge of each Thread. Similar to how people use their knowledge to make decisions in everyday life, a Thread’s knowledge of a program’s state can aid the decision of which action to take. An interesting question is thus whether we can model the knowledge of a concurrent system in order to aid the execution of instructions. In this report we investigate the plausibility of modelling problematic concur- rent programs as games of imperfect information against nature. Successfully modelled programs are analysed from the perspective of each Thread’s distributed knowledge by applying Multi-Player Knowledge Based Subset Construction (MKBSC). In this report we have successfully modelled three different programs that each handle a concurrency-related problem. We have also shown how we can synthesise winning strategies from the knowledge of each Player for two out of three game models.