Open Access System for Information Sharing

Login Library

 

Article
Cited 20 time in webofscience Cited 25 time in scopus
Metadata Downloads

Model checking linear temporal logic of rewriting formulas under localized fairness SCIE SCOPUS

Title
Model checking linear temporal logic of rewriting formulas under localized fairness
Authors
Bae, KMeseguer, J
Date Issued
2015-03-07
Publisher
Elsevier
Abstract
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. (C) 2014 Elsevier B.V. All rights reserved.
URI
https://oasis.postech.ac.kr/handle/2014.oak/36400
DOI
10.1016/J.SCICO.2014.02.006
ISSN
0167-6423
Article Type
Article
Citation
SCIENCE OF COMPUTER PROGRAMMING, vol. 99, page. 193 - 234, 2015-03-07
Files in This Item:
There are no files associated with this item.

qr_code

  • mendeley

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

Related Researcher

Researcher

배경민BAE, KYUNGMIN
Dept of Computer Science & Enginrg
Read more

Views & Downloads

Browse