  I consider the following generic scenario: an abstract model M of some 'real'
system is only partially presented, or partially known to us, and we have to
ensure that the actual system satisfies a given specification, formalised in
some logical language. This scenario has at least two essentially different
interpretations, leading to two, essentially different, formal logical and
algorithmic problems: "Model Synthesis from Partial Models", where some
'admissible' extension of M to a full model must satisfy the specification, and
"Model Checking of Partial Models", where all 'admissible' extensions of M to a
full model must satisfy the specification. These problems naturally extend the
classical logical decision problems of Satisfiability, Validity, and Model
Checking.
  Here I briefly discuss both problems in the contexts of classical, modal and
temporal logics. I make some observations, state some open questions, and
outline a general tableaux-style procedure that solves the problem of
unconstrained model synthesis from finite partial models for several well-known
modal and temporal logics, incl. K, LTL, CTL, ATL.
