The Patterns Tools supports the definition of temporal formulae for systems' verification.

The Patterns Tool has been developed in Java (you can download it below). We are also experimenting with a web-based version developed in SilverLight. You can try it here (still beta stage!).

Several Pattern collection are supported, including a Pattern collection for Discrete Event Systems.