Hybrid Automata

For bounded-time BLTL mode properties, universal satisfaction in the hybrid automaton corresponds to probability-one satisfaction in the associated Markov chain. Hybrid automata models include finite modes, an initial mode, Lipschitz-continuous ODE systems per mode, guards, transitions, and bounded initial states. The method extends statistical model checking to hybrid automata that switch between ODE-governed modes through guards. The hybrid method associates the system with an acyclic, finitely branching, infinite-state discrete-time Markov chain. Hybrid verification focuses mainly on mode-sequence properties because quantitative reachability is undecidable for nonlinear hybrid automata.