The increasing application of formal methods to the design of autonomous systems often requires extending the existing specification and modeling formalisms, and addressing new challenges for formal verification and synthesis. In this talk, I will focus on the application of reactive synthesis to the problem of automatically deriving strategies for autonomous mobile sensors conducting surveillance, that is, maintaining knowledge of the location of a moving, possibly adversarial target. By extending linear temporal logic with atomic surveillance predicates, complex temporal surveillance objectives can be formally specified in a way that allows for seamless combination with other task specifications. I will discuss two key challenges for applying state-of-the-art methods for reactive synthesis to temporal surveillance specifications. First, naively keeping track of the knowledge of the surveillance agent leads to a state-space explosion. Second, while sensor networks with a large number of dynamic sensors can achieve better coverage, synthesizing coordinated surveillance strategies is challenging computationally. I will outline how abstraction, refinement, and compositional synthesis techniques can be used to address these challenges.