Using Patterns and Composite Propositions to Automate the Generation of LTL Specifications