Spyware detection using temporal logic