Model Checking. Part II
Kazuhisa Ishida (2008)
Formalized Mathematics
Similarity:
This article provides the definition of linear temporal logic (LTL) and its properties relevant to model checking based on [9]. Mizar formalization of LTL language and satisfiability is based on [2, 3].