Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems

2003 ◽  
Author(s):  
Edmund Clarke ◽  
Ansgar Fehnker ◽  
Zhi Han ◽  
Bruce Krogh ◽  
Joel Ouaknine ◽  
...  
Keyword(s):  
Model Checking ◽  
Hybrid Systems

Model Checking Multirate Hybrid Systems with Dense Timed Interval Temporal Logic

2012 ◽  
Vol 198-199 ◽  
pp. 889-893
Author(s):  
Hai Bin Zhang ◽  
Li Ya Yang
Keyword(s):  
Model Checking ◽  
Hybrid Systems ◽  
Temporal Logic ◽  
Desirable Property ◽  
Interval Temporal Logic

This paper investigates the model checking issue of multirate hybrid systems. To this end, multirate automata are used to represent the possible behavior of multirate hybrid systems, and a dense timed interval temporal logic (DTITL) is defined to describe the desirable property. To check whether a multirate automaton satisfies a DTITL formula, a corresponding region automaton and a propositional interval temporal logic (PITL) formula are constructed. After each vertex of the region automaton being labeled with propositions appearing in the corresponding PITL formula, the model checking problem for mutirate hybrid systems is reduced to the same issue for PITL, which can be solved readily.

A two-step scheme for approximate model checking of stochastic hybrid systems

2011 ◽  
Vol 44 (1) ◽  
pp. 4519-4524 ◽  
Author(s):  
A. Abate ◽  
J.P. Katoen ◽  
J. Lygeros ◽  
M. Prandini
Keyword(s):  
Model Checking ◽  
Hybrid Systems ◽  
Approximate Model ◽  
Stochastic Hybrid Systems
Sign in / Sign up

Export Citation Format

Share Document