  Stochastic multiplayer games (SMGs) have gained attention in the field of
strategy synthesis for multi-agent reactive systems. However, standard SMGs are
limited to modeling systems where all agents have full knowledge of the state
of the game. In this paper, we introduce delayed-action games (DAGs) formalism
that simulates hidden-information games (HIGs) as SMGs, where hidden
information is captured by delaying a player's actions. The elimination of
private variables enables the usage of SMG off-the-shelf model checkers to
implement HIGs. Furthermore, we demonstrate how a DAG can be decomposed into
subgames that can be independently explored, utilizing parallel computation to
reduce the model checking time, while alleviating the state space explosion
problem that SMGs are notorious for. In addition, we propose a DAG-based
framework for strategy synthesis and analysis. Finally, we demonstrate
applicability of the DAG-based synthesis framework on a case study of a
human-on-the-loop unmanned-aerial vehicle system under stealthy attacks, where
the proposed framework is used to formally model, analyze and synthesize
security-aware strategies for the system.
