  We consider the problem of automatic generation of control strategies for
robotic vehicles given a set of high-level mission specifications, such as
"Vehicle x must eventually visit a target region and then return to a base,"
"Regions A and B must be periodically surveyed," or "None of the vehicles can
enter an unsafe region." We focus on instances when all of the given
specifications cannot be reached simultaneously due to their incompatibility
and/or environmental constraints. We aim to find the least-violating control
strategy while considering different priorities of satisfying different parts
of the mission. Formally, we consider the missions given in the form of linear
temporal logic formulas, each of which is assigned a reward that is earned when
the formula is satisfied. Leveraging ideas from the automata-based model
checking, we propose an algorithm for finding an optimal control strategy that
maximizes the sum of rewards earned if this control strategy is applied. We
demonstrate the proposed algorithm on an illustrative case study.
