A computable and compositional semantics for hybrid systems

被引:0
作者
Bresolin, Davide [1 ]
Collins, Pieter [2 ]
Geretti, Luca [3 ]
Segala, Roberto [3 ]
Villa, Tiziano [3 ]
Gonzalez, Sanja Zivanovic [4 ]
机构
[1] Univ Padua, Padua, Italy
[2] Maastricht Univ, Maastricht, Netherlands
[3] Univ Verona, Verona, Italy
[4] AlphaStaff, Sunrise, FL USA
关键词
Hybrid automata; Composition; Computability; Computable analysis; REACHABILITY ANALYSIS; TEMPORAL LOGIC; VERIFICATION;
D O I
10.1016/j.ic.2024.105189
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Hybrid Systems are systems having a mixed discrete and continuous behaviour that cannot be characterised faithfully using either discrete or continuous models only. Due to the intrinsic complexity of hybrid systems, it is highly desirable to describe them compositionally, where large systems are seen as the composition of several simpler subparts that are studied independently. Furthermore, since several problems, including reachability, are undecidable for hybrid systems, the availability of approximate decision procedures is another important feature. In this paper, we propose a purely behavioural formalism for hybrid systems that is compositional and supports approximate decision procedures. The formalism is abstract and sufficiently general to subsume or be a semantic framework for most of the concrete formalisms or languages proposed in the literature. (c) 2024 Elsevier Inc. All rights are reserved, including those for text and data mining, AI training, and similar technologies.
引用
收藏
页数:38
相关论文
共 50 条
  • [31] Tracking smooth trajectories in linear hybrid systems
    Benerecetti, Massimo
    Faella, Marco
    INFORMATION AND COMPUTATION, 2017, 257 : 114 - 138
  • [32] Computational methods for verification of stochastic hybrid systems
    Koutsoukos, Xenofon D.
    Riley, Derek
    IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS, 2008, 38 (02): : 385 - 396
  • [33] On Optimal Control of Stochastic Linear Hybrid Systems
    Jha, Susmit
    Raman, Vasumathi
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, FORMATS 2016, 2016, 9884 : 69 - 84
  • [34] Symbolic algorithm analysis of rectangular hybrid systems
    Zhang, Haibin
    Duan, Zhenhua
    THEORY AND APPLICATIONS OF MODELS OF COMPUTATION, PROCEEDINGS, 2008, 4978 : 294 - 305
  • [35] Approximate Probabilistic Relations for Compositional Abstractions of Stochastic Systems
    Lavaei, Abolfazl
    Soudjani, Sadegh
    Zamani, Majid
    NUMERICAL SOFTWARE VERIFICATION, 2019, 11652 : 101 - 109
  • [36] Model-Bounded Monitoring of Hybrid Systems
    Waga, Masaki
    Andre, Etienne
    Hasuo, Ichiro
    ICCPS'21: PROCEEDINGS OF THE 2021 ACM/IEEE 12TH INTERNATIONAL CONFERENCE ON CYBER-PHYSICAL SYSTEMS (WITH CPS-IOT WEEK 2021), 2021, : 21 - 32
  • [37] Model-bounded Monitoring of Hybrid Systems
    Waga, Masaki
    Andre, Etienne
    Hasuo, Ichiro
    ACM TRANSACTIONS ON CYBER-PHYSICAL SYSTEMS, 2022, 6 (04)
  • [38] Towards a compositional approach to the design and verification of distributed systems
    Charpentier, M
    Chandy, KM
    FM'99-FORMAL METHODS, 1999, 1708 : 570 - 589
  • [39] Compositional Abstraction Refinement for Component-Based Systems
    Zhang, Lianyi
    Meng, Qingdi
    Lo, Kueiming
    JOURNAL OF APPLIED MATHEMATICS, 2014,
  • [40] Compositional Analysis of Probabilistic Timed Graph Transformation Systems
    Maximova, Maria
    Schneider, Sven
    Giese, Holger
    FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING (FASE 2021), 2021, 12649 : 196 - 217