Formalizations of theorems related to model checking

Source: doi:10.1007/3-540-60915-6_6, url:https://github.com/kuruczgy/lean-model-checking Authors: György Kurucz Status: verified Main declarations: LeanModelChecking.for_any_LTL_formula_exists_an_equivalent_NBW Tags: model-checking, linear-temporal-logic, buchi-automaton, safety-liveness, omega-automata MSC: 68Q60, 03B44, 68Q45