Asynchronous Correspondences Between Hybrid Trajectory Semantics

Research output: Chapter in Book/Report/Conference proceedingChapter

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.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer Science and Business Media Deutschland GmbH
Pages131-159
Number of pages29
DOIs
StatePublished - 2022

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13660 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Keywords

  • Abstract interpretation
  • Abstraction
  • Bisimulations
  • Discretization
  • Galois connection
  • Galois relation
  • Homomorphism
  • Hybrid systems
  • Logical relation
  • Preservations
  • Progress
  • Refinement
  • Semantics
  • Simulations
  • Verification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Asynchronous Correspondences Between Hybrid Trajectory Semantics'. Together they form a unique fingerprint.

Cite this