Download PDF - Safety- and liveness-properties in propositional temporal logic: characterizations and decidability