%0 Conference Proceedings
%T Model Checking of Hybrid Systems Using Shallow Synchronization
%+ State Key Laboratory of Novel Software Technology [Nanjing University]
%+ Fondazione Bruno Kessler [Trento, Italy] (FBK)
%A Bu, Lei
%A Cimatti, Alessandro
%A Li, Xuandong
%A Mover, Sergio
%A Tonetta, Stefano
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 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)
%C Amsterdam, Netherlands
%Y John Hatcliff; Elena Zucca
%I Springer
%3 Formal Techniques for Distributed Systems
%V LNCS-6117
%P 155-169
%8 2010-06-07
%D 2010
%R 10.1007/978-3-642-13464-7_13
%Z Computer Science [cs]/Digital Libraries [cs.DL]Conference papers
%X 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.
%G English
%2 https://inria.hal.science/hal-01055156/document
%2 https://inria.hal.science/hal-01055156/file/61170153.pdf
%L hal-01055156
%U https://inria.hal.science/hal-01055156
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-LNCS-6117
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-FMOODS
%~ IFIP-2010