摘要：AbstractTemporal logics are widely used to express (desired) system properties in controller synthesis and verification. In linear temporal logics, the semantics of the formulae are defined on the execution trajectories of the system. Recently, there have been a lot of interest in using dense-time linear temporal logic, such as Signal Temporal Logic (STL) in characterizing system trajectories. In this paper, we present a new method to derive an STL formula that characterizes the motion of a robot arm. Our work generalizes earlier work in this area by (i) allowing the use of polyhedral predicates, and (ii) incorporating a priori knowledge about the predicates. The formula is defined by a set of parameters, whose values are determined by minimizing a cost function that balances the trade-off between the formula's match with the trajectories and the the similarity between its predicate and an a priori known predicate. We apply our algorithm on experimental trajectories generated using a PHANToM Omni robot.
