Abstract
ó Simulation relations can be used to verify re- nement between a system and its specication, or between models of different complexity. It is known that for the verication of safety properties, simulation between hybrid systems can be dened based on their labeled transition system semantics. We show that for hybrid systems without shared variables, which therefore only interact at discrete events, this simulation preorder is compositional, and present assume-guarantee rules that help to counter the state explosion problem. Some experimental results for simulation checking of linear hybrid automata are provided using a prototype tool with exact arithmetic and unlimited digits. I. INTRODUCTION The complexity of verifying hybrid systems increases exponentially with the number of system components and, particularly, with the number of continuous variables in- volved, which requires abstraction and divide-and-conquer, i.e., compositional, strategies. Hybrid automata (1) have been successfully used to model and verify hybrid systems. To be able to apply compositional reasoning, we restrict ourselves to hybrid automata with disjunct variables, so that they interact only via synchronization on discrete events. We compare hybrid automata by computing a simulation relation between their states. A state of an automaton sim- ulates that of another if it can exhibit the same discrete and timed behavior. Other than trace or language containment, simulation also captures the branching behavior. In a hybrid setting, it provides a compact and intuitive way to specify desired behavior and can be applied to verify renement and abstraction, if systems exhibit a continuous behavior too complex to be analyzed or even modeled accurately. We present an extension of simulation to compare au- tomata of arbitrary alphabets that allows more compact models and proofs, and show that it supports compositional reasoning for hybrid systems with no shared variables. In particular, we use simulation to establish non-circular and circular assume-guarantee rules that do not require non-blocking or receptiveness. Finally, we provide some experimental data obtained with a tool prototype for linear hybrid automata. In our denition of simulation for hybrid automata we follow the approach of (2), which is based on labeled transition system semantics and takes into account a given equivalence relation between states. Simulation without state equivalence was presented for modal hybrid systems in (3). A rule for assumme-guarantee reasoning for Moore machines based on simulation relation has been presented in (4). It requires non-blocking and is a special case of the assume-guarantee rule in Sect. IV-C. In (5), assume- guarantee reasoning for renement based on trace inclusion is shown to be sound for receptive timed and hybrid mod- ules. In contrast, we do not require receptiveness, abstract from continuous o ws with labeled transition system (LTS) semantics and retain the branching structure of simulation. The next section denes hybrid automata and their LTS- semantics. Then Sect. III denes simulation relations for hybrid automata with equivalence between states, for which compositional proof rules are given in Sect. IV. Finally, some implementation results are presented in Sect. V. II. HYBRID SYSTEMS WITH DISCRETE INTERACTION This section briey recalls basic denitions, which slightly differ from those in (1), (2) in that automata interact only on discrete transitions and have no shared variables.

This publication has 10 references indexed in Scilit: