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.