A Platform-Based Approach To Verification And Synthesis Of Linear Temporal Logic Specifications