As the amount of information accessible to military intelligence continues to surge, manual surveillance becomes more and more inefficient. To process the information stream efficiently, automatic systems for threat detection are called for. These systems must be sufficiently robust to process incomplete or noisy data, and capable of dealing with uncertainties and probabilities. For safety reasons and accountability, it is imperative that the surveillance systems are specified in a formal framework that allows for rigorous mathematical verification. To this end, we demonstrate how the unobstructed keyhole plan recognition problem can be modeled within the framework of weighted unranked tree automata, and outline a software system for recognition of hostile behavior.