On the Complexity of Ltl Model-Checking of Recursive State Machines