Satisfiability Checking of LTL Specifications for Verifiable UAV Mission Planning

摘要

Formal methods – mathematically-based languages, tools, and techniques traditionally used for specification, design, and verification of hardware and software systems – have recently been applied to more complex systems. One example is human-automation mission planning systems for mobile robots, in which mission goals and constraints are expressed as formalized specifications that can then be used to synthesize “correct-by-construction” mission plans for the robots. However, a problem occurs if the specifications are unsatisfiable, i.e. if they are inherently contradictory. Here, we discuss how satisfiability checking can be performed on linear temporal logic specifications for unmanned aerial vehicle (UAV) intelligence, surveillance, and reconnaissance (ISR) missions using a “reduction to model checking” technique, which can be implemented using several different algorithms. In particular, we focus on BDDand SAT-based algorithms and show how computation time for these two classes of algorithms varies depending on specification type, length, and satisfiability status. a