The verification of liveness properties is an important challenge in the
design of real-time and hybrid systems.

In contrast to the verification of safety properties, for which there
are several solutions available, there are really few tools that
support liveness properties such as general LTL formulas for hybrid
systems, even in the case of timed automata.

In the context of finite-state model checking, K-Liveness is a recently proposed
algorithm that tackles the problem by proving that an accepting condition can be
visited at most K times. K-Liveness has shown to be very efficient, thanks also
to its tight integration with IC3, a very efficient technique for safety verification.
Unfortunately, the approach is neither complete nor effective (even for simple
properties) in the case of infinite-state systems with continuous time.

In this talk, we extend K-Liveness to deal with LTL for hybrid
systems. On the theoretical side, we show how to extend the reduction
from LTL to the reachability of an accepting condition in order to
make the algorithm work with continuous time. In particular, we prove
that the new reduction is complete for a class of rectangular hybrid
automata, in the sense that the LTL property holds if and only if
there exists K such that the accepting condition is visited at most K
times. On the practical side, we present an efficient integration of
K-Liveness in an SMT version of IC3, and demonstrate its effectiveness
on several benchmarks.