Formalization of (some) Temporal Logics in Lean Definitions used are from Baier, Christel, and Joost-Pieter Katoen. Principles of model checking. MIT press, 2008.