Intelligence, Surveillance and Reconnaissance Task Specifications in Temporal Logics

The DoD desires to incorporate autonomous systems into its capabilities. These systems are notoriously difficult to validate, though they require assurance to be used. One area of interest is Intelligence, Surveillance and Reconnaissance (ISR), whose tasks are typically written in natural language. Temporal logics, e.g., Linear Temporal Logic (LTL) and Signal Temporal Logic (STL), have been used in robotics, cyber-physical systems, and electronics design domains to provide confidence and assurance in the correctness, reliability, and safety of system designs. ISR tasks written as temporal logic specifications enables their properties to be validated. We found that recent natural language to LTL/STL specification translators incorrectly translate natural language ISR descriptions. In this paper, we provide manual translations of ten ISR tasks to temporal logic and validate the specifications. We believe this is the first research to provide a set of ISR tasks specified in temporal logic and checked by a satisfiability solver.