On Optimal Design of Highly Dependable Hybrid Dynamical Systems

在高可靠性混合动力系统（EDS）的设计上，我们的目标是将各种形式化方法的技术与最优控制问题相结合，并取得了以下结果。(1)我们已经开发了一个计算机工具，称为KCLP-HS，作为处理HDS的各种计算的基础。KCLP-HS配备了线性和二次求解器，凸多面体的操作和区间运算。(2)本文将量词消去法应用于求解分段仿射系统的最优控制问题，量词消去法是一种从一阶公式中消去量词的符号计算方法。我们已经通过计算机实验验证了该方法的有效性。(3)在HDS模型预测控制中，作为处理时序逻辑公式所给出的逻辑约束的框架，我们提出了有界偏似的概念。我们还开发了一个预先计算的方法来获得近似的解决方案。(4)我们提出了MLD系统中逻辑动力学的一种新表示。我们已经通过计算机实验验证了所提出的表示对以前的优势。(5)我们已将上述HDS结果应用于流化技术，一种用连续流近似离散状态转变的技术。我们已经开发了一个可扩展的方法来评估大型信息系统的性能。

On the design of highly dependable hybrid dynamical systems (EDS), we aim to incorporate various techniques on formal approaches with problems on optimal control, and have obtained the following results.(1) We have developed a computer tool, called KCLP-HS, as a basis of dealing with various kinds of computations on HDS. KCLP-HS is equipped with linear and quadratic solver, manipulation of convex polyhedra, and interval arithmetic.(2) We have applied quantifier elimination, which is a symbolic computation technique to remove quantifiers from first-order formula, to solving optimal control problem for piecewise affine systems. We have verified effectiveness of the approach through computer experiments.(3) As a framework for dealing with logical constraints, given by temporal logic formula, in model predictive control of HDS, we have proposed notion of bounded bisimilation. We have also developed a pre-computation method for obtaining approximated solutions.(4) We have proposed a new representation of logical dynamics in MLD system. We have verified advantages of the proposed representation against the previous one through computer experiments.(5) We have applied the above results on HDS to the fluidification technique, a technique for approximating discrete state transition by continuous flows. We have developed a scalable method to evaluate performance of large information systems.