On Livelock Detection (and existentialy-quantified LTL)
There are various livelock-related properties that are interesting, however, some of them are hard to check as they include some kind of progress notion which is harder to extract from the unannotated source code. However, it seems to me, that there is an interesting subclass of livelocks which might be reasonably easy to express:
If there is a cycle in the state space which does not involve any memory, this is a livelock, as the system cannot progress from this state (minus non-determinism). This could be checked by CTL* formula EG(no writes), which can in fact be checked by standard LTL model checking algorithm as it has only top-level branching quantifier. I know this is an under-approximation of livelock, but nevertheless useful motivation for existential LTL properties.