TY - JOUR
T1 - Model checking linear temporal logic of rewriting formulas under localized fairness
AU - Bae, Kyungmin
AU - Meseguer, José
N1 - We thank the anonymous reviewers for their constructive comments that helped to improve the paper. This work has been supported in part by NSF Grants CNS 09-04749 , CCF 09-05584 , and CNS 13-19109 , AFOSR Grant FA8750-11-2-0084 , and Boeing Corporation Grant C8088-557395 .
PY - 2015/3/1
Y1 - 2015/3/1
N2 - This paper presents the linear temporal logic of rewriting (LTLR) model checker under localized fairness assumptions for the Maude system. The linear temporal logic of rewriting extends linear temporal logic (LTL) with spatial action patterns that describe patterns of rewriting events. Since LTLR generalizes and extends various state-based and event-based logics, mixed properties involving both state propositions and actions, such as fairness properties, can be naturally expressed in LTLR. However, often the needed fairness assumptions cannot even be expressed as propositional temporal logic formulas because they are parametric, that is, they correspond to universally quantified temporal logic formulas. Such universal quantification is succinctly captured by the notion of localized fairness; for example, fairness is localized to the object name parameter in object fairness conditions. We summarize the foundations, and present the language design and implementation of the Maude Fair LTLR model checker, developed at the C++ level within the Maude system by extending the existing Maude LTL model checker. Our tool provides not only an efficient LTLR model checking algorithm under parameterized fairness assumptions but also suitable specification languages as part of its user interface. The expressiveness and effectiveness of the Maude Fair LTLR model checker are illustrated by five case studies. This is the first tool we are aware of that can model check temporal logic properties under parameterized fairness assumptions.
AB - This paper presents the linear temporal logic of rewriting (LTLR) model checker under localized fairness assumptions for the Maude system. The linear temporal logic of rewriting extends linear temporal logic (LTL) with spatial action patterns that describe patterns of rewriting events. Since LTLR generalizes and extends various state-based and event-based logics, mixed properties involving both state propositions and actions, such as fairness properties, can be naturally expressed in LTLR. However, often the needed fairness assumptions cannot even be expressed as propositional temporal logic formulas because they are parametric, that is, they correspond to universally quantified temporal logic formulas. Such universal quantification is succinctly captured by the notion of localized fairness; for example, fairness is localized to the object name parameter in object fairness conditions. We summarize the foundations, and present the language design and implementation of the Maude Fair LTLR model checker, developed at the C++ level within the Maude system by extending the existing Maude LTL model checker. Our tool provides not only an efficient LTLR model checking algorithm under parameterized fairness assumptions but also suitable specification languages as part of its user interface. The expressiveness and effectiveness of the Maude Fair LTLR model checker are illustrated by five case studies. This is the first tool we are aware of that can model check temporal logic properties under parameterized fairness assumptions.
KW - Linear temporal logic of rewriting
KW - Model checking
KW - Parameterized fairness
UR - http://www.scopus.com/inward/record.url?scp=84919846725&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84919846725&partnerID=8YFLogxK
U2 - 10.1016/j.scico.2014.02.006
DO - 10.1016/j.scico.2014.02.006
M3 - Article
AN - SCOPUS:84919846725
SN - 0167-6423
VL - 99
SP - 193
EP - 234
JO - Science of Computer Programming
JF - Science of Computer Programming
ER -