Formalizing Requirements Is $$\Diamond \Box $$ Hard

The use of formal methods in software engineering requires that the user adopt a suitable level of precision in the description of both design artifacts and the properties that should hold for those artifacts. The level of precision must be sufficiently high that the logical consistency of the design and the logic properties can be verified mechanically.