Logical Lyapunov functions for analysis of dynamic behavior of hybrid models of switching circuits.