  Machine teaching is an algorithmic framework for teaching a target hypothesis
via a sequence of examples or demonstrations. We investigate machine teaching
for temporal logic formulas -- a novel and expressive hypothesis class amenable
to time-related task specifications. In the context of teaching temporal logic
formulas, an exhaustive search even for a myopic solution takes exponential
time (with respect to the time span of the task). We propose an efficient
approach for teaching parametric linear temporal logic formulas. Concretely, we
derive a necessary condition for the minimal time length of a demonstration to
eliminate a set of hypotheses. Utilizing this condition, we propose a myopic
teaching algorithm by solving a sequence of integer programming problems. We
further show that, under two notions of teaching complexity, the proposed
algorithm has near-optimal performance. The results strictly generalize the
previous results on teaching preference-based version space learners. We
evaluate our algorithm extensively under a variety of learner types (i.e.,
learners with different preference models) and interactive protocols (e.g.,
batched and adaptive). The results show that the proposed algorithms can
efficiently teach a given target temporal logic formula under various settings,
and that there are significant gains of teaching efficacy when the teacher
adapts to the learner's current hypotheses or uses oracles.
