A pattern-based approach to the presentation,  codification and reuse of property specifications for finite state verification which was proposed by Matthew B. Dwyer and his colleagues . The patterns enable non-experts to read and write formal specifications  for realistic systems and facilitate easy conversion of specifications between formalisms such as LTL, computational tree logic (CTL), quantified regular expressions (QRE), and other state-based and event-based formalisms.

It is often natural to express properties using changes of state - edges. As the original pattern system was state-based, we tried to extend it by incorporating edge-based events. These events  can be used for specifying the conditions as well as for defining the bounding scopes. For example, we may want to express properties like "Event S precedes event P between states Q and R" or "State S precedes state P between events Q and R". These properties are often hard to specify correctly, and since all of them contain the "next" operator (either directly or indirectly through the use of edges), it is not trivial to determine if they are  closed under stuttering.

In this web site, we present LTL patterns containing events.  For more information about the theory underlying this work, please consult our papers.