Real world systems of interest often feature interactions between discrete and continuous dynamics. Various hybrid system formalisms have been used to model and analyze this combination of dynamics, ranging from mathematical descriptions, e.g., using impulsive differential equations and switching, to automata-theoretic and language-based approaches. This paper bridges two such formalisms by showing how various classes of switched systems can be modeled using the language of hybrid programs from differential dynamic logic (dL). The resulting models enable the formal specification and verification of switched systems using dL and its existing deductive verification tools such as KeYmaera X. Switched systems also provide a natural avenue for the generalization of dL's deductive proof theory for differential equations. The completeness results for switched system invariants proved in this paper enable effective safety verification of those systems in dL.
翻译:现实世界感兴趣的系统往往以离散动态和连续动态之间的相互作用为特点。 各种混合系统形式主义被用于模拟和分析这种动态组合,从数学描述,例如使用感应式差异方程式和转换,到自动成形理论和基于语言的方法。本文通过展示如何使用不同动态逻辑(dL)的混合程序语言模拟不同类别的交替系统,将两种此类形式主义连接起来。 由此形成的模型使得能够对调换系统进行正式的规格和核查,这些系统使用dL及其现有的扣减核查工具,如KeYmaera X。 切换式系统也为将dL的差别方程式的推论推理理论普遍化提供了自然的渠道。 本文所证明的变换系统的完整性结果使得DL系统能够有效地安全核查这些系统。