Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2509.08610 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917421418283008 |
|---|---|
| author | Schirmer, Sebastian Schitz, Philipp Dauer, Johann C. Finkbeiner, Bernd Sankaranarayanan, Sriram |
| author_facet | Schirmer, Sebastian Schitz, Philipp Dauer, Johann C. Finkbeiner, Bernd Sankaranarayanan, Sriram |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_08610 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Trace Repair for Temporal Behavior Trees Schirmer, Sebastian Schitz, Philipp Dauer, Johann C. Finkbeiner, Bernd Sankaranarayanan, Sriram Logic in Computer Science 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. |
| title | Trace Repair for Temporal Behavior Trees |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2509.08610 |