Simplifying LTL Model Checking Given Prior Knowledge

Alexandre Duret-Lutz, Denis Poitrenaud, Yann Thierry-Mieg

We consider the problem of the verification of an LTL specification $\phi$ on a system $S$ given some prior knowledge $K$, an LTL formula that $S$ is known to satisfy. The automata-th…