二値変数を削減した信号時相論理の混合整数計画法
Mixed-Integer Programming for Signal Temporal Logic with Fewer Binary Variables
信号時相論理(STL)の軌道合成を混合整数凸計画で解く際、選言を対数個の二値変数で符号化し連言は二値変数なしで扱うことで、長く複雑な仕様でも大幅に効率化する手法を提案した。
著者: Vince Kurtz, Hai Lin
分類: eess.SY, cs.RO, cs.SY
原文アブストラクト
Signal Temporal Logic (STL) provides a convenient way of encoding complex control objectives for robotic and cyber-physical systems. The state-of-the-art in trajectory synthesis for STL is based on Mixed-Integer Convex Programming (MICP). The MICP approach is sound and complete, but has limited scalability due to exponential complexity in the number of binary variables. In this letter, we propose a more efficient MICP encoding for STL. Our new encoding is based on the insight that disjunction can be encoded using a logarithmic number of binary variables and conjunction can be encoded without binary variables. We demonstrate in simulation examples that our proposed approach significantly outperforms the state-of-the-art for long and complex specifications. Open-source software is available at https://stlpy.readthedocs.io.
