  In this paper we address the synthesis problem for specifications given in
linear temporal single-agent epistemic logic, KLTL (or $KL_1$), over
single-agent systems having imperfect information of the environment state. Van
der Meyden and Vardi have shown that this problem is 2Exptime complete.
However, their procedure relies on complex automata constructions that are
notoriously resistant to efficient implementations as they use Safra-like
determinization.
  We propose a "Safraless" synthesis procedure for a large fragment of KLTL.
The construction transforms first the synthesis problem into the problem of
checking emptiness for universal co-B\"{u}chi tree automata using an
information-set construction. Then we build a safety game that can be solved
using an antichain-based symbolic technique exploiting the structure of the
underlying automata. The technique is implemented and applied to a couple of
case studies.
