Patrick Cousot<bR> Asynchronous Correspondences Between Hybrid Trajectory Semantics

Patrick Cousot.
Asynchronous Correspondences Between Hybrid Trajectory Semantics.
In J.-F. Raskin and K. Chatterjee (Eds.): Principles of Systems Design, LNCS 13660, Springer, 2023,
Keywords: Abstract interpretation, Hybrid systems, Semantics, Abstraction, Homomorphism, Simulation, Bisimulation, Preservation, Progress, Discretization, Verification, Refinement, Galois connection, Galois relation, Logical relation.

Abstract: 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.

Paper: PDF (8.2 MB) (the full version (14.2 MB) is available on ArXiv, https://arxiv.org/abs/2209.14945)

Bibliographic reference:

@inproceedings{THenzinger60,
  author    = {Patrick Cousot},
  title     = {Asynchronous Correspondences Between Hybrid Trajectory Semantics},
  editor   = {J.-F. Raskin and K. Chatterjee },
  booktitle = {Principles of Systems Design},
  series    = {Lecture Notes in Computer Science},
  volume    = {13660},
  publisher = {Springer},
  year      = {2023},
  notes     = {\url{https://link.springer.com/book/9783031223389}},
}

copyright notice
Last modified: Monday, 19-Dec-2022 18:42:58 EST