理工学のさまざまな問題が、制約解消(constraint solving)や最適化(optimization)問題として定式化される。したがって、制約解消及び最適化問題を解くアルゴリズムの研究の進展が各分野へ与える影響は大きい。システム制御理論の分野では、1990年代以降、数値最適化に基づく制御系設計が精力的に研究されてきた。その典型的な例は、ロバスト制御の解析・設計問題を線形行列不等式(LMI)で表した凸最適化問題に帰着し、半正定値計画法(SDP)を用いて解く方法である。それまで解析的には解けなかった問題に対する大域的な最適解を求めることが可能となり、ロバスト制御系設計の新しい解法を与えた。これらの制御系設計法は、計算機能力の進展および精度や効率に優れたアルゴリズムの開発によって実用的な設計手法となってきた。しかし、数値最適化に基づく制御系設計の研究が進展するに従い、固定次数制御器・多目的設計問題などより実用的な問題は、数値的な方法では取り扱いが困難な非凸最適化問題となることも明らかになってきた。設計パラメータが与えられた場合に、設計仕様が満たされるかどうかを判定する解析問題において、広範なクラスの問題が凸制約・最適化問題として数値計算によって取り扱い可能であるのに対し、同じ仕様について設計問題を考えると、設計パラメータについてのパラメトリックな制約問題となり、一般に非凸な制約問題となるケースが多い。このように設計問題が非凸となる場合、最近では、元の非凸最適化問題にLMIによる凸緩和を巧みに用いて、SDPを適用することで設計を行う方法も提案され、より実用的になってきている。しかし、保守的でない解を正確に求めたり、ロバストな解を得るために実行可能解を全て領域として求めることは非常に難しい。そのため近年では、制御問題と関連するクラスの非凸最適化問題の有効な解法の開発が望まれている。

一方、固定次数制御器の設計や複数仕様を同時に満たす設計に対しては、パラメータ空間法などのパラメトリックなアプローチによる設計法が有効な方法の一つとして知られている。パラメータ空間法では、設計パラメータをシンボリックに扱って制約式を解き実行可能領域を(正確に)求めることが鍵である。それが実現すれば、得られた実行可能領域から、よりロバストな解を求めることや複数の仕様に対する実行可能領域をパラメータ空間で重ね合わせて多目的最適化を実現できる。しかし、既存の数値計算に基づく手法では、実行可能解はパラメータ空間の点として得られるため、解のロバスト性を検証するなどその実現は困難である。数値計算に基づく設計では、通常設計パラメータを変えて数値シミュレーションを繰り返し所望のパラメータ値を求めることも多く、パラメータの選択等で設計者の知識や経験に依存し、通常多くの繰り返しが必要なため設計者はとりあえず解が見つかるとその解で妥協したり、解がない問題で解の探索を延々と継続する場合も多いという問題もある。このため、多くの制御系設計問題に対して系統的に実行可能領域を求めることができる有効な方法が望まれている。

本学位論文では、このような点を解決するため数式処理の代数的算法に基づく制約問題・最適化問題の手法を提案し、さまざまなシステム制御理論における設計・検証の問題に適用しその有効性について議論する。特に、制約解消・最適化問題の代数的算法として限量記号消去(quantifier elimination: QE)に着目する。QEは、(1)全ての実行可能解をパラメータ空間内の領域(等式・不等式のブール的組合せである半代数的集合)として正確に求めることができる (2)非凸な最適化問題も正確に解くことができる (3) 実行可能解が存在しない場合も正確に判定できる、という特長を持っている。したがって、QEは多目的・固定次数制御器の設計など非凸制約問題となる制御問題のパラメータ設計法に有効である。また、パラメータ空間における可能領域の重ね合わせにより多目的・固定次数制御器設計も容易に実現でき、よりロバストでより保守的でない解を求めることができる。さらに、従来からシステムのモデリングや制御系設計問題の記述まで、多項式制約が非常に多く用いられてきたため、QEを用いるアプローチは、問題の定式化から解法まで非常に適した性質を持っており、数値計算による設計に対して相補的な機能を提供できることが期待できる。これらの点を念頭に、QEに基づく最適化手法を用いたパラメータ空間法による制御系設計法を提案し、実際の制御系の設計や検証に適用してその有効性を示す。また、本学位論文で述べた設計手法を実用的な問題に適用可能とするために、対象となる制御問題の特徴をうまく捉えQEのアルゴリズムが扱いやすい形に問題を帰着し(数値最適化との効果的組み合わせも含めて)その問題に適したQEアルゴリズムを構築する。

本学位論文は3部からなり、それぞれQEのアルゴリズム、QEに基づく制御系設計、QEに基づく制御系検証の各問題を扱った。第1章では、本研究の背景と工学的意義について触れ、研究にいたる動機と課題を述べ、本学位論文の構成を示した。

QEのアルゴリズムを扱った第1部では、QEとその基本的アルゴリズムである cylindrical algebraic decomposition (CAD)について説明し、有意なサブクラスの制約式に対する効率的なアルゴリズムや、数値・数式ハイブリッド計算によるアルゴリズムを示した。また、三角関数を含む制約に対するQEアルゴリズムも提案した。

第2章では、QEとCADについて概説し、続いてCADを高速化するための数値・数式ハイブリッド計算を用いた計算の枠組みを示した。第2部において制御系設計問題にて利用される2つの特別なクラスの制約式に対する効率的なアルゴリズムとその改良を示した。最後にQEに基づく制約解消・最適化の手法について説明した。

第3章では、理工学で広く利用されている半正定値計画法(SDP)について、正確な解を効率よく導く方法を提案した。提案手法は、CADに基づく方法で問題の凸性を巧みに利用することで効率化を実現した。SDPの代数幾何への応用で最適解の正確な代数的表現が必要とされる場合や、悪条件下で数値的方法では誤った解が得られる場合に有効である。

第4章では、理工学の問題でしばしば現れる三角関数を含む制約問題についての決定問題を解く代数的アルゴリズムを提案した。一般に、三角関数やπを含む場合には、実数体上の一階述語論理は決定不能である。ここでは、線形式に三角関数を含むクラスについて考察した。

第2部では、QEに基づくパラメータ空間法による制御系設計手法を提案し、伝達関数表現に基づく周波数領域におけるロバスト制御系設計問題やLQ最適制御問題へ適用しその有効性を確認した。提案手法の効率化に共通するポイントは、各問題が非常に簡単な形をした多項式制約問題に帰着でき、より効率的なQEアルゴリズムを適用できる点である。

第5章では、周波数領域におけるロバスト制御系設計について、QEに基づくパラメータ空間法による設計手法を提案した。具体的には、低次の固定構造制御器の周波数領域での複数仕様に対する多目的設計を行う設計法を提案した。特に,ロバスト制御の多くの重要な設計仕様が一変数多項式の正定値条件という特別なクラスの制約式に帰着できることを指摘し、それに特化したQEアルゴリズムを使うことでQEに基づくパラメータ空間設計を効率化し実用的な問題に適用可能であることを確認した。

第6章では、系のロバスト安定性を保証するために有効な安定半径についての設計問題を検討した。制御系の安定半径についての設計問題も、一変数多項式の正定値条件に定式化できることを指摘し、第5章と同様の枠組みでQEに基づく効率的な設計手法を提案した。

第7章では、LQ最適制御問題を扱った。この問題において、系統的な決定方法がなくヒューリスティックに決められていた重みの選択の問題を、ある多項式の根の和に着目してグレブナ基底の理論を用いることで、一変数多項式の正定値条件を解く問題に帰着でき、さらに、QEを適用することで新しい選択指標を与え得ることを示した。

第8章では、安定性に関わるフィードバック系の極の配置問題について、QEを用いたより柔軟に細やかな配置の指定を実現する方法を提案した。提案方法は、極をガウス平面内の指定された点(の近傍)に配置する。また、提案手法は不確かさを持つ制御対象に対しても適用可能で、どの程度近く指定された位置に配置が可能かその限界を見積もることもできる。ここでは、極配置問題がパラメータを含む線形制約式となり、線形式に特化したQEアルゴリズムを使うことで効率的に計算可能である。

第3部では、制御系の検証問題について検討した。制御系の検証は、系が正しく設計され安全な動作をすることを保証するために非常に重要である。ここでは、離散時間多項式系と線形微分方程式系の2種類の系についてQEに基づく検証手法を提案した。

第9章では、離散時間多項式系に対して可観測性・接近可能性を検証する効率的な代数的方法を提案した。提案手法は、アルゴリズムの支配的部分であるイデアルの等価性判定などをQEだけでなくグレブナ基底や実根の数え上げの方法を組み合わせることで効率化を図った。

第10章では、パラメータを含む非同次線形微分方程式系に対して、到達可能集合を計算するQEに基づく方法を提案した。一般に、到達可能集合を正確には計算できないため、到達可能集合が正確に計算できる有意なクラスを与えることは重要である。この提案方法により、制御の分野においても意義のある新しい決定可能クラスを定義し、同時に正確に可到達集合を計算する方法を与えた。

第11章では、本学位論文のまとめとして、提案した各手法が制御系設計・検証に有効であり、理工学やものづくりのさまざまな場面で現れるシステムの設計・検証問題にも対応するものであると結論付けた。

なお、本文は英語により記述されていることを付記する。

本論文は、「Effective Quantifier Elimination with Applications to Control System Design and Verification (効率的な限量記号消去法とその制御系設計及び検証への応用)」と題し、数式処理の有効なツールの一つである限量記号消去法(以下QEと記す)を制御工学の実問題に適用可能とするための手法を提案し、制御系設計及び検証への応用を通してその有用性を確認している。本論文は3部構成で、Part I 「Algorithms」では効率的な限量記号消去法を、Part II 「Applications: Control System Design」では制御系設計への応用を、Part III 「Applications: Control System Verification」では制御系検証への応用を、それぞれ扱っている。本論文は、「Effective Quantifier Elimination with Applications to Control System Design and Verification (効率的な限量記号消去法とその制御系設計及び検証への応用)」と題し、数式処理の有効なツールの一つである限量記号消去法(以下QEと記す)を制御工学の実問題に適用可能とするための手法を提案し、制御系設計及び検証への応用を通してその有用性を確認している。本論文は3部構成で、Part I 「Algorithms」では効率的な限量記号消去法を、Part II 「Applications: Control System Design」では制御系設計への応用を、Part III 「Applications: Control System Verification」では制御系検証への応用を、それぞれ扱っている。

第1章「Introduction」では、本論文の背景、動機と目的を述べた後、本論文の主たるアプローチを紹介し、論文の構成を示している。

第2章から第4章までで構成される第1部は、QEのアルゴリズムに関するパートで、第2部と第3部での応用に必要となる制御工学の実問題に適用可能とするための手法が提案されている。

第2章「Cylindrical Algebraic Decomposition and Real Quantifier Elimination」では、まずQEとその主要な計算法であるCAD(Cylindrical Algebraic Decomposition) について概説し、ついでCAD を高速に計算するための数値・数式ハイブリッド計算を用いたCAD構成の枠組みを提案している。また、第2部の制御系設計問題において利用される「一変数多項式の正定値条件」と「低次数の制約式」の2つの特別なクラスの制約式に対する効率的なアルゴリズムを導出している。さらに、一変数多項式の正定値条件に対するQEアルゴリズムについては、設計問題で必要とされる改良を行っている。

第3章「Convex Quantifier Elimination for Semidefinite Programming」では、理工学のさまざまな場面で広く利用されている半正定値計画法(SDP)について、正確な解を効率よく導く方法を提案している。提案手法はCADに基づく方法であり、問題の凸性を巧みに利用することで効率化を実現している。この方法は、SDPの代数幾何への応用において最適解の正確な代数的表現が必要とされる場合や、悪条件下で数値的方法では誤った解が得られる場合などに非常に有効な方法である。

第4章「Deciding Linear-Trigonometric Problems」では、理工学の問題でしばしば現れる三角関数を制約式に含む決定問題を解くための代数的アルゴリズムを提案している。一般に、三角関数やπを含む制約式が存在する場合には、実数体上の一階述語論理は決定不能である。ここでは、線形式に三角関数を含むクラスに対して有効なQEアルゴリズムを提案している。

第5章から第8章で構成される第2部では、第2、第3章において提案されたQEアルゴリズムをどのように制御系設計問題に適用するかを述べ、アルゴリズムの実装を通してその有用性を確認している。

第5章「Robust Parametric Control Based on Sign Definite Condition」では、周波数領域におけるロバスト制御系設計について、QEに基づくパラメータ空間法による固定構造制御器設計手法を提案している。まず,ロバスト制御における多くの重要な設計仕様が一変数多項式の正定値条件という特別なクラスの制約式に帰着できることを指摘している。つぎに、それに特化したQEアルゴリズムを用いることで、QEに基づくパラメータ空間設計を効率化し実用的な問題に適用可能であることを確認している。

第6章「Robust Stability Radius Synthesis」では、制御系のロバスト安定性を保証する最大の変動幅を表す安定半径に関する設計問題を検討している。この設計問題も適切な問題の等価変換を行うことにより、一変数多項式の正定値条件という制約式に定式化できることを指摘し、第5章と同様の枠組みでQEに基づく効率的な設計手法が構成できることを示している。

第7章「Average Stability Degree in LQ Optimal Regulator」では、LQ最適制御問題における重みの選択と平均安定度との関係を扱っている。まず、閉ループ系の平均安定度を与えるある多項式の根の和に着目して、代数的算法 (特に、グレブナ基底の理論) を駆使することで、この問題が一変数多項式の正定値条件を解く問題に帰着できることを導いている。さらに、その結果に対してQEを適用することで、新しい重みの選択指標が導出できることを示している。これは、設計過程において試行錯誤が必要な問題に対して、代数的アプローチが系統的な手順を与える一つの好例である。

第8章「Robust Pole Assignment for Interval Plants」では、フィードバック制御系の極配置問題に関して、より柔軟にきめ細かい配置を実現するQEを用いた手法を提案している。提案手法はQEを用いているため、不確かなパラメータを持つ制御対象に対しても適用可能で、さらにどの程度指定された位置に近く配置が可能かの限界を見積もることもできる。この極配置問題がパラメータを含む線形制約式となり、それに特化したQE アルゴリズムを使うことができ効率的に計算可能であることを示している。

第9章および第10章を構成する第3部では、離散時間多項式系と線形微分方程式系で表される2種類の制御系に対して、検証問題が正確に実行可能となるQEに基づく検証手法を提案している。

第9章「An Adaptive Resonant Modes Compensation」では、離散時間多項式系に対して可観測性と接近可能性を検証する効率的な代数的方法を提案している。提案手法は代数的な手法に基づいており、正確に検証できる利点を有している。提案アルゴリズムの効率化を図るために、その支配的な部分であるイデアルの等価性判定などにおいて、QEだけでなくグレブナ基底や実根の数え上げの方法を組合わせている。

第10章「Reach Set Computation of Continuous and Hybrid Systems」では、パラメータを含む非同次線形微分方程式系に対して、到達可能集合を計算するQEに基づく手法を提案している。一般に、到達可能集合は正確には計算できないため、到達可能集合が正確に計算できる有意なクラスを与えることは重要である。提案手法により、制御の分野において意義のある新しい有意なクラスが定義でき、そのクラスの系に対して可到達集合を正確に計算する方法を与えている。

第11章「Concluding Remarks」では、本論文で得られた結果をまとめ、提案した各手法が制御系設計および検証に有効であることを確認するとともに、今後の研究の課題を列挙している。

以上を要するに、本論文は数式処理の有効なツールの一つである限量記号消去法の効率的なアルゴリズムを提案かつ実装し、制御系設計および検証への応用を通してその有用性を示したもので、情報理工学上貢献するところ大である。よって本論文は、博士(情報理工学)の学位請求論文として合格と認められる。