Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs