📝 SummarXiv

Abstract

We present methods for repairing traces against specifications given as temporal behavior trees (TBT). TBT are a specification formalism for action sequences in robotics and cyber-physical systems, where specifications of sub-behaviors, given in signal temporal logic, are composed using operators for sequential and parallel composition, fallbacks, and repetition. Trace repairs are useful to explain failures and as training examples that avoid the observed problems. In principle, repairs can be obtained via mixed-integer linear programming (MILP), but this is far too expensive for practical applications. We present two practical repair strategies: (1) incremental repair, which reduces the MILP by splitting the trace into segments, and (2) landmark-based repair, which solves the repair problem iteratively using TBT's robust semantics as a heuristic that approximates MILP with more efficient linear programming. In our experiments, we were able to repair traces with more than 25,000 entries in under ten minutes, while MILP runs out of memory.