SIGMSS2016-03 Talk
時相論理式の反証を用いた制御器のチューニング
峰尾太陽, 石井大輔, 渡部卓雄
電子情報通信学会 システム数理と応用研究会,
信学技報, Vol. 115, No. 480, MSS2015-79, pp. 61-66, Mar. 3-4, 2016.
(海峡メッセ下関, 山口県下関市)
概要
時間及び空間上で連続的に動作するシステムは, 離散状態空間を持つシステムとは異なり状態の網羅的な検査が一般に困難である. そこで近年, 広範な連続システムに対する検査を実施するための時相論理式の反証手法が注目されつつある. この反証手法は, 連続システムの数値シミュレーションと統計的最適化により, 時相論理式を満たさない動作（反例）を効率良く求める事ができる. 本研究では, 制御器を含む連続システムを対象に, 制御仕様を簡潔に記述し, 仕様の定量的評価に基づいて制御器のパラメタを自動設定する事を目的とする. その為, 制御仕様を時相論理式で記述し, パラメタに関する最適化問題の定式化を行い, この問題を統計的手法によって効率的に解くアルゴリズムを提案する. これにより, 様々な制御の仕様を記述することで, 一般の制御器を含む系に対して定量的評価基準による効率的なパラメタ最適化が可能になる. 典型的な物理系に含まれるPID制御器のパラメタを設定する比較実験において, 提案手法は限界感度法によるパラメタ設定よりも定量的に有効なパラメタを与える事を確かめた.
Controller Tuning with Falsification of Temporal Logic Formulae
Taiyo Mineo, Daisuke Ishii & Takuo Watanabe
IEICE Technical Report, Vol. 115, No. 480, MSS2015-79, pp. 61-66, Mar., 2016.
Abstract
In general, it is hard to check exhaustively states of systems that behave continuously over time and space, unlike the systems with discrete state space. Therefore, falsification methods of temporal logic formulae have been proposed as a prominent approach to verify various continuous systems. The falsification methods efficiently compute a counterexample of continuous systems that does not satisfy a considered property based on the numerical simulation and statistical optimization. In this research, we consider continuous systems that involve controllers, and aim for a simple description of controller specifications and the automated tuning of controller parameters based on the quantitative evaluation of the specification. To achieve this goal, we encode the specifications as temporal logic formulae, formalize an optimization problem about the parameters, and propose an algorithm that solves this optimization problem with a statistical method. The proposed method enables to describe various controller specifications, to evaluate the specifications quantitatively, and to optimize parameters efficiently for the generic controllers. We experimentally tuned PID controllers connected with typical physical systems, and confirmed that our method computed quantitatively better parameter configurations than the classical Ziegler-Nichols method.