Asynchronous correspondences between hybrid trajectory semantics

DOI10.1007/978-3-031-22337-2_7MaRDI QIDQ6113973zbMATH OpenOpenAlexFDO

Authors Patrick Cousot

Publication date 10 August 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2209.14945

zbMATH Keywords

abstract interpretationabstractionbisimulationsdiscretizationGalois connectionGalois relationhomomorphismhybrid systemslogical relationpreservationsrefinementsemanticssimulationsverification

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

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.

Recommendations

• scientific article; zbMATH DE number 2085342
• Abstractions for hybrid systems
• Compositional abstractions of hybrid control systems
• Abstractions of hybrid systems for verification
• Reconciling urgency and variable abstraction in a hybrid compositional setting

Cites work

• A lattice-theoretical fixpoint theorem and its applications
• A syntactic approach to type soundness
• A theory of timed automata
• Approximate bisimulation: a bridge between computer science and control theory
• Approximate simulation relations for hybrid systems
• Constructive design of a hierarchy of semantics of a transition system by abstract interpretation
• Continuous Action System Refinement
• Formal Methods for the Design of Real-Time Systems
• Formal Modeling and Analysis of Timed Systems
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 1263213 (Why is no real title available?)
• scientific article; zbMATH DE number 2060665 (Why is no real title available?)
• scientific article; zbMATH DE number 1444370 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Hybrid action systems
• Introduction to bisimulation and coinduction
• On Timed Simulation Relations for Hybrid Systems and Compositionality
• Principles of abstract interpretation
• Switching in systems and control
• The structure of Galois connections

This page was built for publication: Asynchronous correspondences between hybrid trajectory semantics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6113973)