Show simple item record

dc.contributor.authorFarheen, Sabria
dc.contributor.authorDay, Nancy A.
dc.contributor.authorVakili, Amirhossein
dc.contributor.authorAbbassi, Ali 14:36:36 (GMT) 14:36:36 (GMT)
dc.descriptionThis is a post-peer-review, pre-copyedit version of an article published in Software and Systems Modeling. The final authenticated version is available online at:
dc.description.abstractWe 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 without induction, iteration, or invariants. We implement TCMC in the Alloy Analyzer, showing how a transition system can be expressed declaratively and concisely in the Alloy language. Since the total state space is rarely representable due to the state-space explosion problem, we present scoped TCMC where the property is checked for state spaces of a size smaller than the total state space. We address the problem of spurious instances and carefully describe the meaning of results from scoped TCMC with respect to the complete model checking problem. Using case studies, we demonstrate scoped TCMC and compare it with bounded model checking, highlighting how TCMC can check infinite paths.en
dc.relation.ispartofseriesSoftware and Systems Modeling (SoSyM);
dc.subjectsymbolic model checkingen
dc.subjectdeclarative modelsen
dc.titleTransitive-closure-based model checking (TCMC) in Alloyen
dcterms.bibliographicCitationFarheen, S., Day, N. A., Vakili, A., & Abbassi, A. (2020). Transitive-closure-based model checking (TCMC) in alloy. Software and Systems Modeling, 19(3), 721–740.
uws.contributor.affiliation1Faculty of Mathematicsen
uws.contributor.affiliation2David R. Cheriton School of Computer Scienceen

Files in this item


This item appears in the following Collection(s)

Show simple item record


University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages