LTL property - safety or liveness? How can I check if an LTL (Linear Temporal Logic) property is safety or liveness? Is it right to say that a property is safety OR liveness (or neither)?

How can I evaluate this:

G(x -&gt; (a U y) )
Your first question is answered in this paper: https://www.cs.cornell.edu/fbs/publications/RecSafeLive.pdf
Given an LTL formula, translate it into a B&uuml;chi automaton, and remove states that have no path to an accepting state. Then, change all states to be accepting. If the language of the automaton does not change, then the property is a safety property. If the language of the automaton becomes $\Sigma^\omega$, then it is a liveness property.