Try Lustre Encoding using Online Kind2 Modle Checker.

References:

1. Havelund, Klaus, and Grigore Roşu. "Synthesizing monitors for safety properties." International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, Berlin, Heidelberg, 2002.
2. Roşu, Grigore, and Klaus Havelund. "Rewriting-based techniques for runtime verification." Automated Software Engineering 12.2 (2005): 151-197.