  With the primary objective of human-robot interaction being to support
humans' goals, there exists a need to formally synthesize robot controllers
that can provide the desired service. Synthesis techniques have the benefit of
providing formal guarantees for specification satisfaction. There is potential
to apply these techniques for devising robot controllers whose specifications
are coupled with human needs. This paper explores the use of formal methods to
construct human-aware robot controllers to support the productivity
requirements of humans. We tackle these types of scenarios via human
workload-informed models and reactive synthesis. This strategy allows us to
synthesize controllers that fulfill formal specifications that are expressed as
linear temporal logic formulas. We present a case study in which we reason
about a work delivery and pickup task such that the robot increases worker
productivity, but not stress induced by high work backlog. We demonstrate our
controller using the Toyota HSR, a mobile manipulator robot. The results
demonstrate the realization of a robust robot controller that is guaranteed to
properly reason and react in collaborative tasks with human partners.
