HomeResearch-feedChannelRankingsGCTTHU AI TROpen DataMust Reading

Transitive-closure-based model checking (TCMC) in Alloy

Sabria Farheen
Sabria Farheen
Nancy A. Day
Nancy A. Day
Amirhossein Vakili
Amirhossein Vakili
Ali Abbassi
Ali Abbassi

Software and Systems Modeling, pp. 1-20, 2020.

Cited by: 1|Bibtex|Views3|DOI:https://doi.org/10.1007/s10270-019-00763-8
EI
Other Links: academic.microsoft.com|dblp.uni-trier.de|link.springer.com
Keywords:
Symbolic model checking Alloy Declarative models

Abstract:

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

Code:

Data:

Your rating :
0

 

Tags
Comments