Backdoors for Linear Temporal Logic