Imperfect Information in Reactive Modules Games

Such a goal can represent either the behaviour model checking systems (e.g., MOCHA (Alur et al. 1998) of the computer system one wants to synthesize and Prism (Kwiatkowska, Norman, and Parker 2011)). Reactive (an automated design problem (Pnueli and Rosner 1989)) Modules supports succinct and high-level modelling or a particular system property which one wants to check of concurrent and multi-agent systems. In the games we (an automated verification problem (Clarke, Grumberg, and study, the preferences of system components are specified Peled 2000)). In this framework, it is assumed that the system by associating with each player in the game a temporal logic plays against an adversarial environment, that is, that (LTL) formula that the player desires to be satisfied. Reactive the goal of the environment is to prevent the system from Modules Games with perfect information (where each player achieving its goal. In game-theoretic terms, this means that can see the entire system state) have been extensively studied the problem is modelled as a zero-sum game, and hence that (Gutierrez, Harrenstein, and Wooldridge 2015a), but in its solution is given by the computation of a winning strategy this paper we focus on imperfect information cases. We study for either the system or the environment.