Epistemic logic has been successfully applied to modeling of epistemic and doxastic attitudes of agents in distributed systems. Dynamic Epistemic Logic (DEL) adds communication via model transformation updates. Since agents in distributed systems often exchange information without other agents knowing about it, however, the inherent assumption that agents possess common knowledge of the model is generally not adequate when describing fully private communication. In this talk, I will present the following results of my forthcoming PhD thesis, which addresses this deficiency: 1) A slight variation of standard action models enriched by a new idea of postcondition. 2) A novel synthesis procedure that, based on a goal formula, generates a pointed action model s.t. when this action model is applied to a pointed epistemic model, the goal formula holds at the point of the epistemic model (given some assumptions), without introducing new unrelated beliefs and preserving consistency of agents' beliefs as much as possible. The many technical statements and proofs I encountered in the course of my PhD work suggested to use an epistemic model checker for verifying their correctness. As none of the (few) existing tools provided the features I needed, I decided some years ago to develop my own high-performance epistemic model checking and visualization tool. Whereas it is still work in progress, it already supports the model synthesis approach described above. I will hence complement the first part of my talk with a live demo of my model checking and visualization tool.