论文标题
混合轨迹语义之间的异步对应关系
Asynchronous Correspondences Between Hybrid Trajectory Semantics
论文作者
论文摘要
我们将混合系统的语义形式化为混合轨迹集，包括由混合过渡系统生成的轨迹。我们研究了杂种轨迹语义的抽象，以验证，静态分析和改进。我们主要考虑混合语义的抽象，这些杂种语义的抽象在诸如同态，模拟，双仿真和进步的状态等状态之间的对应关系之间建立了对应关系。我们还考虑无法像离散化那样逐步定义的抽象。所有这些抽象都是混凝土和抽象混合轨迹或离散痕量语义之间的GALOIS连接。与基于语义的摘要相反，我们研究了基于痕量的有问题的抽象组成。
We formalize the semantics of hybrid systems as sets of hybrid trajectories, including those generated by an hybrid transition system. We study the abstraction of hybrid trajectory semantics for verification, static analysis, and refinement. We mainly consider abstractions of hybrid semantics which establish a correspondence between trajectories derived from a correspondence between states such as homomorphisms, simulations, bisimulations, and preservations with progress. We also consider abstractions that cannot be defined stepwise like discretization. All these abstractions are Galois connections between concrete and abstract hybrid trajectory or discrete trace semantics. In contrast to semantic based abstractions, we investigate the problematic trace-based composition of abstractions.
