In a seminal paper from 1985, Sistla and Clarke showed
 that the model-checking problem for Linear Temporal Logic (LTL) is either NP-complete
 or PSPACE-complete, depending on the set of temporal operators used.
 If, in contrast, the set of propositional operators is restricted, the complexity may decrease.
 ...
                	
            		    more >>>
                	
		
		
		
 In a seminal paper from 1985, Sistla and Clarke showed
 that satisfiability for Linear Temporal Logic (LTL) is either
 NP-complete or PSPACE-complete, depending on the set of temporal
 operators used
 If, in contrast, the set of propositional operators is restricted, the
 complexity may ...
                	
            		    more >>>