Transitive-closure-based model checking (TCMC) in Alloy
Software and Systems Modeling, pp. 1-20, 2020.
We present transitive-closure-based model checking (TCMC): a symbolic representation of the semantics of computational tree logic with fairness constraints (CTLFC) for finite models in first-order logic with transitive closure (FOLTC). TCMC is an expression of the complete model checking problem for CTLFC as a set of constraints in FOLTC ...More
Full Text (Upload PDF)
PPT (Upload PPT)