[g9yuayon]

Specifying a system correctly can be hard with the previous generation of tools. For instance, using LTL to describe system properties is not necessarily easy. I remember there used to be pattern library for model checking or for temporal logic. For something as simple as checking bounded existence, one has to write LTL formula like below. That certainly is out of most people's interest. Fortunately tools have improved a lot, and engineers do not really need to study temporal logic deeply for many cases.

``` []((Q & <>R) -> ((!P & !R) U (R | ((P & !R) U (R | ((!P & !R) U (R | ((P & !R) U (R | (!P U R)))))))))) ```

[Davidbrcz]

Dwyer patterns https://matthewbdwyer.github.io/psp/patterns.html

[g9yuayon]

Thanks! I used to use the same pattern library hosted in either CMU or PSU, IIRC. Glad that it has a new home.