A New Tableau-based Satisfiability Checker for Linear Temporal Logic