Skip to Main content Skip to Navigation
Conference papers

Model Checking of Hybrid Systems Using Shallow Synchronization

Abstract : Hybrid automata are a widely accepted modeling framework for systems with discrete and continuous variables. The traditional semantics of a network of automata is based on interleaving, and requires the construction of a monolithic hybrid automaton based on the composition of the automata. This destroys the structure of the network and results in a loss of efficiency, especially using bounded model checking techniques. An alternative compositional semantics, called "shallow synchronization", exploits the locality of transitions and relaxes time synchronization. The semantics is obtained by composing traces of the local automata, and superimposing compatibility constraints resulting from synchronization. In this paper, we investigate the different symbolic encodings of the reachability problem of a network of hybrid automata. We propose a novel encoding based on the shallow synchronization semantics, which allows different strategies for searching local paths that can be synchronized. We implemented a bounded reachability search based on the use of an incremental Satisfiability-Modulo-Theory solver. The experimental results confirm that the new encoding often performs better than the one based on interleaving.
Document type :
Conference papers
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Monday, August 11, 2014 - 4:32:25 PM
Last modification on : Wednesday, January 19, 2022 - 10:06:01 AM
Long-term archiving on: : Wednesday, November 26, 2014 - 10:15:49 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Lei Bu, Alessandro Cimatti, Xuandong Li, Sergio Mover, Stefano Tonetta. Model Checking of Hybrid Systems Using Shallow Synchronization. Joint 12th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 30th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2010, Amsterdam, Netherlands. pp.155-169, ⟨10.1007/978-3-642-13464-7_13⟩. ⟨hal-01055156⟩



Record views


Files downloads