混合轨迹语义之间的异步对应
Asynchronous Correspondences Between Hybrid Trajectory Semantics
摘要：
我们形式化的混合动力系统的语义集的混合动力轨迹，包括由一个混合动力过渡系统所产生的。我们研究的混合轨迹语义的抽象验证，静态分析，和细化。我们主要考虑混合语义的抽象，它建立了一个对应的轨迹之间的对应关系，来自状态之间的对应关系，如同态，模拟，互模拟，并与进展的conventions。我们还考虑了不能像离散化那样逐步定义的抽象。所有这些抽象都是具体和抽象混合轨迹或离散迹语义之间的伽罗瓦连接。相反，基于语义的抽象，我们调查的问题基于轨迹的抽象组合。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
