Model checking LTLR formulas under localized fairness

Kyungmin Bae, José Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Many temporal logic properties of interest involve both state and action predicates and only hold under suitable fairness assumptions. Temporal logics supporting both state and action predicates such as the Temporal Logic of Rewriting (TLR) can be used to express both the desired properties and the fairness assumptions. However, model checking such properties directly can easily become impossible for two reasons: (i) the exponential blowup in generating the Büchi automaton for the implication formula including the fairness assumptions in its condition easily makes such generation unfeasible; and (ii) 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 localized to the parameter o in object fairness conditions. We summarize the foundations and present the language design and implementation of the new Maude LTLR Model Checker under localized fairness. This is the first tool we are aware of which can model check temporal logic properties under parametric fairness assumptions.

Original languageEnglish (US)
Title of host publicationRewriting Logic and Its Applications - 9th International Workshop, WRLA 2012, Held as a Satellite Event of ETAPS, Revised Selected Papers
Pages99-117
Number of pages19
DOIs
StatePublished - Nov 8 2012
Event9th International Workshop on Rewriting Logic and Its Applications, WRLA 2012, Held as a Satellite Event of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012 - Tallinn, Estonia
Duration: Mar 24 2012Mar 25 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7571 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other9th International Workshop on Rewriting Logic and Its Applications, WRLA 2012, Held as a Satellite Event of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012
CountryEstonia
CityTallinn
Period3/24/123/25/12

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Model checking LTLR formulas under localized fairness'. Together they form a unique fingerprint.

Cite this