Hybrid systems describe the interaction of software, described by finite models such as finite-state machines, with the physical world, described by infinite models such as differential equations. This book addresses problems of verification and controller synthesis for hybrid systems. Although these problems are very difficult to solve for general hybrid systems, several authors have identified classes of hybrid systems that admit symbolic or finite models. The novelty of the book lies on the systematic presentation of these classes of hybrid systems along with the relationships between the hybrid systems and the corresponding symbolic models. To show how the existence of symbolic models can be used for verification and controller synthesis, the book also outlines several key results for the verification and controller design of finite systems. Several examples illustrate the different methods and techniques discussed in the book.
Cited By
- Platzer A (2025). Hybrid dynamical systems logic and its refinements, Science of Computer Programming, 239:C, Online publication date: 1-Jan-2025.
- Sharf M, Besselink B and Johansson K (2024). Contract composition for dynamical control systems, Automatica (Journal of IFAC), 164:C, Online publication date: 1-Jun-2024.
- Nejati A, Prakash Nayak S and Schmuck A Context-triggered Games for Reactive Synthesis over Stochastic Systems via Control Barrier Certificates Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, (1-12)
- Calbert J, Mattenet S, Girard A and Jungers R Memoryless concretization relation Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, (1-9)
- Anand A, Schmuck A and Prakash Nayak S Contract-Based Distributed Logical Controller Synthesis Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, (1-11)
- Murali V, Trivedi A and Zamani M Closure Certificates Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, (1-11)
- Kumar M and Choppella V Enhancing MVC architecture pattern description using its System of Systems model Proceedings of the 17th Innovations in Software Engineering Conference, (1-11)
- Krook J, Malik R, Mohajerani S and Fabian M (2024). Robust stutter bisimulation for abstraction and controller synthesis with disturbance, Automatica (Journal of IFAC), 160:C, Online publication date: 1-Feb-2024.
- Banach R (2024). Core Hybrid Event-B III, Science of Computer Programming, 231:C, Online publication date: 1-Jan-2024.
- Salamati A, Lavaei A, Soudjani S and Zamani M (2024). Data-driven verification and synthesis of stochastic systems via barrier certificates, Automatica (Journal of IFAC), 159:C, Online publication date: 1-Jan-2024.
- Hamadneh T, Abu-Falahah I, Hamadneh M and Zraiqat A Bernstein Coefficients for Computing Rational Lyapunov and Control Functions of Dynamical Systems Proceedings of the 2023 6th International Conference on Mathematics and Statistics, (114-119)
- Mehdipour N, Althoff M, Tebbens R and Belta C (2023). Formal methods to comply with rules of the road in autonomous driving, Automatica (Journal of IFAC), 152:C, Online publication date: 1-Jun-2023.
- Anand A, Nayak S and Schmuck A Poster Abstract: Permissiveness for Strategy Adaptation Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, (1-2)
- Egidio L, Nayak S, Rossa M, Schmuck A and Jungers R Poster Abstract: Towards Seamless Reactivity of Hybrid Control Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, (1-2)
- Van Huijgevoort B, Schön O, Soudjani S and Haesaert S SySCoRe: Synthesis via Stochastic Coupling Relations Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, (1-11)
- Chong S, Lanotte R, Merro M, Tini S and Xiang J Quantitative Robustness Analysis of Sensor Attacks on Cyber-Physical Systems Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, (1-12)
- Hou J, Yin X, Li S and Zamani M Abstraction-Based Synthesis of Opacity-Enforcing Controllers using Alternating Simulation Relations 2019 IEEE 58th Conference on Decision and Control (CDC), (7653-7658)
- Saoud A, Ivanova E and Girard A Efficient Synthesis for Monotone Transition Systems and Directed Safety Specifications* 2019 IEEE 58th Conference on Decision and Control (CDC), (6255-6260)
- Abate M, Feron E and Coogan S Monitor-Based Runtime Assurance for Temporal Logic Specifications 2019 IEEE 58th Conference on Decision and Control (CDC), (1997-2002)
- Zhang K and Johansson K Synthesis for controllability and observability of logical control networks 2019 IEEE 58th Conference on Decision and Control (CDC), (108-113)
- Hashimoto K, Saoud A, Kishida M, Ushio T and Dimarogonas D (2022). Learning-based symbolic abstractions for nonlinear control systems, Automatica (Journal of IFAC), 146:C, Online publication date: 1-Dec-2022.
- Lavaei A, Soudjani S, Abate A and Zamani M (2022). Automated verification and synthesis of stochastic hybrid systems, Automatica (Journal of IFAC), 146:C, Online publication date: 1-Dec-2022.
- Cai K, Giua A and Seatzu C (2022). Consistent reduction in discrete-event systems, Automatica (Journal of IFAC), 142:C, Online publication date: 1-Aug-2022.
- Gleizer G, Madnani K and Mazo Jr. M A Simpler Alternative: Minimizing Transition Systems Modulo Alternating Simulation Equivalence Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control, (1-11)
- Delimpaltadakis G, de Albuquerque Gleizer G, van Straalen I and Mazo Jr. M ETCetera: beyond Event-Triggered Control Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control, (1-11)
- Verdier C, Kochdumper N, Althoff M and Mazo M (2022). Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications, Automatica (Journal of IFAC), 139:C, Online publication date: 1-May-2022.
- Ivanova E, Saoud A and Girard A (2022). Lazy controller synthesis for monotone transition systems and directed safety specifications, Automatica (Journal of IFAC), 135:C, Online publication date: 1-Jan-2022.
- Calbert J, Legat B, Egidio L and Jungers R Alternating Simulation on Hierarchical Abstractions 2021 60th IEEE Conference on Decision and Control (CDC), (593-598)
- Apaza-Perez W and Girard A Compositional Synthesis of Symbolic Controllers for Attractivity Specifications 2021 60th IEEE Conference on Decision and Control (CDC), (2008-2013)
- Schillinger P, García S, Makris A, Roditakis K, Logothetis M, Alevizos K, Ren W, Tajvar P, Pelliccione P, Argyros A, Kyriakopoulos K and Dimarogonas D (2021). Adaptive heterogeneous multi-robot collaboration from formal task specifications, Robotics and Autonomous Systems, 145:C, Online publication date: 1-Nov-2021.
- Choppella V, Viswanath K and Kumar M Algodynamics: Algorithms as systems 2021 IEEE Frontiers in Education Conference (FIE), (1-9)
- Berger G and Jungers R (2021). p-dominant switched linear systems, Automatica (Journal of IFAC), 132:C, Online publication date: 1-Oct-2021.
- Sinyakov V and Girard A (2021). Formal controller synthesis from specifications given by discrete-time hybrid automata, Automatica (Journal of IFAC), 131:C, Online publication date: 1-Sep-2021.
- Bai Y, Gan T, Jiao L, Xia B, Xue B and Zhan N Switching controller synthesis for delay hybrid systems under perturbations Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control, (1-11)
- Chen J, Williams B and Fan C Optimal mixed discrete-continuous planning for linear hybrid systems Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control, (1-12)
- Girard A and Eqtami A (2022). Least-violating symbolic controller synthesis for safety, reachability and attractivity specifications, Automatica (Journal of IFAC), 127:C, Online publication date: 1-May-2021.
- Belta C Formal synthesis of control strategies for dynamical systems 2016 IEEE 55th Conference on Decision and Control (CDC), (3407-3431)
- Apaza-Perez W, Combastel C and Zolghadri A A symbolic approach to distributed control of interconnected systems 2020 59th IEEE Conference on Decision and Control (CDC), (887-892)
- Jiang F, Gao Y, Xie L and Johansson K Ensuring safety for vehicle parking tasks using Hamilton-Jacobi reachability analysis 2020 59th IEEE Conference on Decision and Control (CDC), (1416-1421)
- Shahamat M, Askari J, Swikir A, Noroozi N and Zamani M Construction of continuous abstractions for discrete-time time-delay systems 2020 59th IEEE Conference on Decision and Control (CDC), (881-886)
- Weber A and Knoll A Approximately Optimal Controllers for Quantitative Two-Phase Reach-Avoid Problems on Nonlinear Systems 2020 59th IEEE Conference on Decision and Control (CDC), (430-437)
- Jagtap P, Pappas G and Zamani M Control Barrier Functions for Unknown Nonlinear Systems using Gaussian Processes* 2020 59th IEEE Conference on Decision and Control (CDC), (3699-3704)
- Jackson J, Laurenti L, Frew E and Lahijanian M Safety Verification of Unknown Dynamical Systems via Gaussian Process Regression 2020 59th IEEE Conference on Decision and Control (CDC), (860-866)
- Apaza-Perez W, Combastel C and Zolghadri A (2020). On distributed symbolic control of interconnected systems under persistency specifications, International Journal of Applied Mathematics and Computer Science, 30:4, (629-639), Online publication date: 1-Dec-2020.
- Jagtap P, Abdi F, Rungger M, Zamani M and Caccamo M (2020). Software Fault Tolerance for Cyber-Physical Systems via Full System Restart, ACM Transactions on Cyber-Physical Systems, 4:4, (1-20), Online publication date: 31-Oct-2020.
- Luckcuck M, Farrell M, Dennis L, Dixon C and Fisher M (2019). Formal Specification and Verification of Autonomous Robotic Systems, ACM Computing Surveys, 52:5, (1-41), Online publication date: 30-Sep-2020.
- Du P, Huang Z, Liu T, Ji T, Xu K, Gao Q, Sibai H, Driggs-Campbell K and Mitra S Online Monitoring for Safe Pedestrian-Vehicle Interactions 2020 IEEE 23rd International Conference on Intelligent Transportation Systems (ITSC), (1-8)
- Fan C, Miller K and Mitra S Fast and Guaranteed Safe Controller Synthesis for Nonlinear Vehicle Models Computer Aided Verification, (629-652)
- Jarvis D Machine learning of an approximate morphism of an electronic warfare simulation component Proceedings of the 2020 Spring Simulation Conference, (1-12)
- Samuel S, Mallik K, Schmuck A and Neider D Resilient abstraction-based controller design Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, (1-2)
- Ashok P, Jackermeier M, Jagtap P, Křetínský J, Weininger M and Zamani M dtControl Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, (1-7)
- Majumdar R, Ozay N and Schmuck A On abstraction-based controller design with output feedback Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, (1-11)
- Majumdar R, Mallik K and Soudjani S Symbolic controller synthesis for Büchi specifications on stochastic systems Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, (1-11)
- Qi H and Qiao Y (2019). Dynamics and control of singular boolean networks, Asian Journal of Control, 21:6, (2604-2613), Online publication date: 23-Jan-2020.
- Jagtap P and Zamani M (2020). Symbolic models for retarded jump–diffusion systems, Automatica (Journal of IFAC), 111:C, Online publication date: 1-Jan-2020.
- Gambier A, Li Z and Yang Q Supervisory Control of a Wind Energy System by Using a Hybrid System Approach IECON 2019 - 45th Annual Conference of the IEEE Industrial Electronics Society, (553-558)
- Masuda R, Kobayashi K and Yamashita Y Dynamic Surveillance by Multiple Agents with Fuel Constraints 2019 IEEE International Conference on Systems, Man and Cybernetics (SMC), (3351-3356)
- Roehm H, Oehlerking J, Woehrle M and Althoff M (2019). Model Conformance for Cyber-Physical Systems, ACM Transactions on Cyber-Physical Systems, 3:3, (1-26), Online publication date: 3-Oct-2019.
- Lavaei A, Soudjani S and Zamani M (2019). Compositional construction of infinite abstractions for networks of stochastic control systems, Automatica (Journal of IFAC), 107:C, (125-137), Online publication date: 1-Sep-2019.
- Cremona F, Lohstroh M, Broman D, Lee E, Masin M and Tripakis S (2019). Hybrid co-simulation, Software and Systems Modeling (SoSyM), 18:3, (1655-1679), Online publication date: 1-Jun-2019.
- He Z, Chen Y, Huang E, Wang Q, Pei Y and Yuan H A system identification based Oracle for control-CPS software fault localization Proceedings of the 41st International Conference on Software Engineering, (116-127)
- Yin X and Zamani M Towards approximate opacity of cyber-physical system Proceedings of the 10th ACM/IEEE International Conference on Cyber-Physical Systems, (310-311)
- Khaled M and Zamani M pFaces Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, (252-257)
- Ghosh S, Bansal S, Sangiovanni-Vincentelli A, Seshia S and Tomlin C A new simulation metric to determine safe environments and controllers for systems with unknown dynamics Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, (185-196)
- Tan F, Liu L, Winter S, Wang Q, Suri N, Bu L, Peng Y, Liu X and Peng X (2018). Cross-Domain Noise Impact Evaluation for Black Box Two-Level Control CPS, ACM Transactions on Cyber-Physical Systems, 3:1, (1-25), Online publication date: 31-Jan-2019.
- Ehlers R On Improving the Efficiency of Game Solving for Hybrid System Control 2018 IEEE Conference on Decision and Control (CDC), (2426-2432)
- Serry M and Reissig G Hyper-Rectangular Over-Approximations of Reachable Sets for Linear Uncertain Systems 2018 IEEE Conference on Decision and Control (CDC), (6275-6282)
- Nilsson P and Ames A Barrier Functions: Bridging the Gap between Planning from Specifications and Safety-Critical Control 2018 IEEE Conference on Decision and Control (CDC), (765-772)
- Bai X Verification of Eventuality Properties for Discrete-time Affine Systems 2018 IEEE Conference on Decision and Control (CDC), (1560-1565)
- Saoud A and Girard A (2018). Optimal multirate sampling in symbolic models for incrementally stable switched systems, Automatica (Journal of IFAC), 98:C, (58-65), Online publication date: 1-Dec-2018.
- Kobayashi K, Kido M and Yamashita Y Computationally Efficient Model Predictive Control for Multi-agent Surveillance Systems 2018 IEEE International Conference on Systems, Man, and Cybernetics (SMC), (2019-2024)
- Saoud A, Girard A and Fribourg L Contract based Design of Symbolic Controllers for Vehicle Platooning Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), (277-278)
- Swikir A, Girard A and Zamani M Compositional Synthesis of Finite Abstractions for Networks of Systems Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), (275-276)
- Sinyakov V and Girard A Formal Controller Synthesis from Hybrid Programs Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), (271-272)
- Sadraddini S and Belta C Formal Guarantees in Data-Driven Model Identification and Control Synthesis Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), (147-156)
- Kim E, Arcak M and Zamani M Constructing Control System Abstractions from Modular Components Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), (137-146)
- Hsu K, Majumdar R, Mallik K and Schmuck A Multi-Layered Abstraction-Based Controller Synthesis for Continuous-Time Systems Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), (120-129)
- Dutreix M and Coogan S Efficient verification for stochastic mixed monotone systems Proceedings of the 9th ACM/IEEE International Conference on Cyber-Physical Systems, (150-161)
- Zhang K and Zamani M Infinite-step opacity of nondeterministic finite transition systems: A bisimulation relation approach 2017 IEEE 56th Annual Conference on Decision and Control (CDC), (5615-5619)
- Rungger M and Reissig G Arbitrarily precise abstractions for optimal controller synthesis 2017 IEEE 56th Annual Conference on Decision and Control (CDC), (1761-1768)
- Bai X and Moor T Consistent abstractions for the supervision of sequential behaviours 2017 IEEE 56th Annual Conference on Decision and Control (CDC), (565-570)
- Mallik K, Soudjani S, Schmuck A and Majumdar R Compositional construction of finite state abstractions for stochastic control systems 2017 IEEE 56th Annual Conference on Decision and Control (CDC), (550-557)
- Deshmukh J, Horvat M, Jin X, Majumdar R and Prabhu V (2017). Testing Cyber-Physical Systems through Bayesian Optimization, ACM Transactions on Embedded Computing Systems, 16:5s, (1-18), Online publication date: 10-Oct-2017.
- Deshmukh J, Majumdar R and Prabhu V (2017). Quantifying conformance using the Skorokhod metric, Formal Methods in System Design, 50:2-3, (168-206), Online publication date: 1-Jun-2017.
- Banach R (2017). The landing gear system in multi-machine Hybrid Event-B, International Journal on Software Tools for Technology Transfer (STTT), 19:2, (205-228), Online publication date: 1-Apr-2017.
- Cowlagi R (2017). Hierarchical trajectory optimization for a class of hybrid dynamical systems, Automatica (Journal of IFAC), 77:C, (112-119), Online publication date: 1-Mar-2017.
- Baştuğ M, Petreczky M, Wisniewski R and Leth J (2016). Reachability and observability reduction for linear switched systems with constrained switching, Automatica (Journal of IFAC), 74:C, (162-170), Online publication date: 1-Dec-2016.
- Wagenmaker A and Ozay N A bisimulation-like algorithm for abstracting control systems 2016 54th Annual Allerton Conference on Communication, Control, and Computing (Allerton), (569-576)
- Khaled M, Rungger M and Zamani M Symbolic models of networked control systems: A feedback refinement relation approach 2016 54th Annual Allerton Conference on Communication, Control, and Computing (Allerton), (187-193)
- Platzer A Logic & Proofs for Cyber-Physical Systems Proceedings of the 8th International Joint Conference on Automated Reasoning - Volume 9706, (15-21)
- Sahin Y and Ozay N Distributed reactive control synthesis for aircraft electric power systems via SAT solving Proceedings of the 7th International Conference on Cyber-Physical Systems, (1-1)
- Alur R, Moarref S and Topcu U Compositional Synthesis with Parametric Reactive Controllers Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, (215-224)
- Rungger M and Zamani M SCOTS Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, (99-104)
- Nilsson P and Ozay N Control Synthesis for Large Collections of Systems with Mode-Counting Constraints Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, (205-214)
- Roehm H, Oehlerking J, Woehrle M and Althoff M Reachset Conformance Testing of Hybrid Automata Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, (277-286)
- Majumdar R Robots at the Edge of the Cloud Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9636, (3-13)
- Dokhanchi A, Zutshi A, Sriniva R, Sankaranarayanan S and Fainekos G Requirements driven falsification with coverage metrics Proceedings of the 12th International Conference on Embedded Software, (31-40)
- Adyanthaya S, Ara H, Bastos J, Behrouzian A, Sánchez R, van Pinxten J, van der Sanden B, Waqas U, Basten T, Corporaal H, Frijns R, Geilen M, Goswami D, Stuijk S, Reniers M and Voeten J xCPS Proceedings of the WESE'15: Workshop on Embedded and Cyber-Physical Systems Education, (1-8)
- Banach R, Butler M, Qin S, Verma N and Zhu H (2015). Core Hybrid Event-B I, Science of Computer Programming, 105:C, (92-123), Online publication date: 1-Jul-2015.
- Raman V, Piterman N, Finucane C and Kress-Gazit H (2015). Timing Semantics for Abstraction and Execution of Synthesized High-Level Robot Control, IEEE Transactions on Robotics, 31:3, (591-604), Online publication date: 1-Jun-2015.
- Kurt A (2015). Discrete-State Encoding in Hybrid-State Systems for Intelligent Vehicle Control and Estimation, IEEE Transactions on Intelligent Transportation Systems, 16:3, (1595-1600), Online publication date: 1-Jun-2015.
- Meyer P, Girard A and Witrant E Symbolic control of monotone systems application to ventilation regulation in buildings Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, (281-282)
- Broman D, Greenberg L, Lee E, Masin M, Tripakis S and Wetter M Requirements for hybrid cosimulation standards Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, (179-188)
- Majumdar R and Prabhu V Computing the Skorokhod distance between polygonal traces Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, (199-208)
- Ames A, Tabuada P, Schürmann B, Ma W, Kolathaya S, Rungger M and Grizzle J First steps toward formal controller synthesis for bipedal robots Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, (209-218)
- Coogan S and Arcak M Efficient finite abstraction of mixed monotone systems Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, (58-67)
- Banach R, Zhu H, Su W and Wu X (2014). ASM, controller synthesis, and complete refinement, Science of Computer Programming, 94:P2, (109-129), Online publication date: 1-Nov-2014.
- Banach R, Zhu H, Su W and Wu X (2014). A Continuous ASM Modelling Approach to Pacemaker Sensing, ACM Transactions on Software Engineering and Methodology, 24:1, (1-40), Online publication date: 14-Oct-2014.
- Dimitrova R and Majumdar R Deductive control synthesis for alternating-time logics Proceedings of the 14th International Conference on Embedded Software, (1-10)
- Mitsch S, Quesel J and Platzer A Refactoring, Refinement, and Reasoning Proceedings of the 19th International Symposium on FM 2014: Formal Methods - Volume 8442, (481-496)
- Liu J and Ozay N Abstraction, discretization, and robustness in temporal logic control of dynamical systems Proceedings of the 17th international conference on Hybrid systems: computation and control, (293-302)
- Rungger M and Tabuada P Abstracting and refining robustness for cyber-physical systems Proceedings of the 17th international conference on Hybrid systems: computation and control, (223-232)
- Tkachev I and Abate A On approximation metrics for linear temporal model-checking of stochastic systems Proceedings of the 17th international conference on Hybrid systems: computation and control, (193-202)
- Zamani M, Tkachev I and Abate A Bisimilar symbolic models for stochastic control systems without state-space discretization Proceedings of the 17th international conference on Hybrid systems: computation and control, (41-50)
- Ehlers R, Seshia S and Kress-Gazit H Synthesis with Identifiers Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 8318, (415-433)
- Duggirala P and Tiwari A Safety verification for linear systems Proceedings of the Eleventh ACM International Conference on Embedded Software, (1-10)
- Zamani M and Abate A Symbolic control of stochastic switched systems via finite abstractions Proceedings of the 10th international conference on Quantitative Evaluation of Systems, (305-321)
- Rungger M, Mazo M and Tabuada P Specification-guided controller synthesis for linear systems and safe linear-time temporal logic Proceedings of the 16th international conference on Hybrid systems: computation and control, (333-342)
- Tkachev I and Abate A Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems Proceedings of the 16th international conference on Hybrid systems: computation and control, (283-292)
- Mouelhi S, Girard A and Gössler G CoSyMA Proceedings of the 16th international conference on Hybrid systems: computation and control, (83-88)
- Kloos J and Majumdar R Supervisor synthesis for controller upgrades Proceedings of the Conference on Design, Automation and Test in Europe, (1105-1110)
- Banach R Pliant modalities in hybrid event-B Theories of Programming and Formal Methods, (37-53)
- Bauer K and Schneider K Teaching cyber-physical systems Proceedings of the Workshop on Embedded and Cyber-Physical Systems Education, (1-8)
- Majumdar R and Zamani M Approximately bisimilar symbolic models for digital control systems Proceedings of the 24th international conference on Computer Aided Verification, (362-377)
- Borri A, Pola G and Di Benedetto M A symbolic approach to the design of nonlinear networked control systems Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control, (255-264)
- Li T, Tan F, Wang Q, Bu L, Cao J and Liu X From Offline toward Real-Time Proceedings of the 2012 IEEE/ACM Third International Conference on Cyber-Physical Systems, (13-22)
- Abbas H and Fainekos G Linear hybrid system falsification through local search Proceedings of the 9th international conference on Automated technology for verification and analysis, (503-510)
- Alur R Formal verification of hybrid systems Proceedings of the ninth ACM international conference on Embedded software, (273-278)
- Colombo A and Del Vecchio D (2011). Enforcing safety of cyberphysical systems using flatness and abstraction, ACM SIGBED Review, 8:2, (11-14), Online publication date: 1-Jun-2011.
- Bu L, Wang Q, Chen X, Wang L, Zhang T, Zhao J and Li X (2011). Toward online hybrid systems model checking of cyber-physical systems' time-bounded short-run behavior, ACM SIGBED Review, 8:2, (7-10), Online publication date: 1-Jun-2011.
- Wongpiromsarn T, Topcu U, Ozay N, Xu H and Murray R TuLiP Proceedings of the 14th international conference on Hybrid systems: computation and control, (313-314)
- Cámara J, Girard A and Gössler G Synthesis of switching controllers using approximately bisimilar multiscale abstractions Proceedings of the 14th international conference on Hybrid systems: computation and control, (191-200)
- Mazo M, Davitian A and Tabuada P PESSOA Proceedings of the 22nd international conference on Computer Aided Verification, (566-569)
- Dennis L, Fisher M, Lincoln N, Lisitsa A and Veres S Declarative abstractions for agent based hybrid control systems Proceedings of the 8th international conference on Declarative agent languages and technologies VIII, (96-111)
- Girard A Synthesis using approximately bisimilar abstractions Proceedings of the 13th ACM international conference on Hybrid systems: computation and control, (111-120)
Recommendations
Verification of hybrid systems based on counterexample-guided abstraction refinement
TACAS'03: Proceedings of the 9th international conference on Tools and algorithms for the construction and analysis of systemsHybrid dynamic systems include both continuous and discrete state variables. Properties of hybrid systems, which have an infinite state space, can often be verified using ordinary model checking together with a finite-state abstraction. Model checking ...
Modeling and Verification of Reactive Systems using Rebeca
Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their ...
Hybrid automata-based CEGAR for rectangular hybrid systems
In this paper, we present a counterexample guided abstraction refinement (CEGAR) framework for systems modelled as rectangular hybrid automata. The main difference, between our approach and previous proposals for CEGAR for hybrid automata, is that we ...