This paper formalizes a variant of inductive game Eleusis. A model of the game is an interpreted system with perfect recall agents for the players and the dealer. The pecularity of Eleusis multi-agent system is that the agents have to guess the behavior of the system, rather than some static information about the system. We express some Eleusis rules and properties of the system by the formulas of propositional knowledge logic and branching time Act-CTL-K_n.