The declarative and relational aspects of Alloy make it a desirable language to use for high-level modeling of transition systems. However, currently, these models must be translated to another tool to carry out full temporal logic model checking. In this article, we show how a symbolic representation of the semantics of computational tree logic with fairness constraints (CTLFC) can be written in first-order logic with the transitive closure operator, and therefore described in Alloy. Using this encoding, the question of whether a declarative model of a transition system satisfies a temporal logic formula can be solved using the Alloy Analyzer directly. Also, since a declarative description of a model may actually represent a family of transition systems, we define two distinct model checking questions on this family (existential and universal model checking) and show how these properties can be evaluated in the Alloy Analyzer.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{VakiliD12,
author = {Amirhossein Vakili and
Nancy A. Day},
editor = {John Derrick and
John S. Fitzgerald and
Stefania Gnesi and
Sarfraz Khurshid and
Michael Leuschel and
Steve Reeves and
Elvinia Riccobene},
title = {Temporal Logic Model Checking in Alloy},
booktitle = {Abstract State Machines, Alloy, B, VDM, and {Z} - Third International
Conference, {ABZ} 2012, Pisa, Italy, June 18-21, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7316},
pages = {150--163},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-30885-7\_11},
doi = {10.1007/978-3-642-30885-7\_11},
timestamp = {Sun, 02 Jun 2019 21:23:59 +0200},
biburl = {https://dblp.org/rec/conf/asm/VakiliD12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}