It is well-known that the until operator in linear temporal logic (LTL) cannot be expressed using next, always and eventually. We provide a simple proof of this fact.
Manuscripts
