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 条
  • [21] On the formal verification of hybrid systems
    Guéguen, H
    Zaytoon, J
    CONTROL ENGINEERING PRACTICE, 2004, 12 (10) : 1253 - 1267
  • [22] Compositional verification of concurrent systems by combining bisimulations
    Lang, Frederic
    Mateescu, Radu
    Mazzanti, Franco
    FORMAL METHODS IN SYSTEM DESIGN, 2021, 58 (1-2) : 83 - 125
  • [23] Compositional verification of concurrent systems by combining bisimulations
    Frédéric Lang
    Radu Mateescu
    Franco Mazzanti
    Formal Methods in System Design, 2021, 58 : 83 - 125
  • [24] Verification criteria for a compositional model for reactive systems
    Bellini, P
    Bruno, MA
    Nesi, P
    SIXTH IEEE INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS, PROCEEDINGS, 2000, : 25 - 35
  • [25] Reachability Games for Linear Hybrid Systems
    Benerecetti, Massimo
    Faella, Marco
    Minopoli, Stefano
    HSCC 12: PROCEEDINGS OF THE 15TH ACM INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL, 2012, : 65 - 74
  • [26] Current Challenges in the Verification of Hybrid Systems
    Schupp, Stefan
    Abraham, Erika
    Chen, Xin
    Ben Makhlouf, Ibtissem
    Frehse, Goran
    Sankaranarayanan, Sriram
    Kowalewski, Stefan
    CYBER PHYSICAL SYSTEMS: DESIGN, MODELING, AND EVALUATION, CYPHY 2015, 2015, 9361 : 8 - 24
  • [27] ΣK-constraints for Hybrid Systems
    Korovina, Margarita
    Kudinov, Oleg
    PERSPECTIVES OF SYSTEMS INFORMATICS, 2010, 5947 : 230 - +
  • [28] Compositional verification of concurrent systems using Petri-net-based condensation rules
    Juan, EYT
    Tsai, JJP
    Murata, T
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1998, 20 (05): : 917 - 979
  • [29] Compositional Verification of Multi-Agent Systems in Temporal Multi-Epistemic Logic
    Engelfriet J.
    Jonker C.M.
    Treur J.A.N.
    Journal of Logic, Language and Information, 2002, 11 (2) : 195 - 225
  • [30] STL Model Checking of Continuous and Hybrid Systems
    Roehm, Hendrik
    Oehlerking, Jens
    Heinz, Thomas
    Althoff, Matthias
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2016, 2016, 9938 : 412 - 427