### 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 language | English (US) |
---|---|

Title of host publication | Rewriting Logic and Its Applications - 9th International Workshop, WRLA 2012, Held as a Satellite Event of ETAPS, Revised Selected Papers |

Pages | 99-117 |

Number of pages | 19 |

DOIs | |

State | Published - Nov 8 2012 |

Event | 9th 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 2012 → Mar 25 2012 |

### Publication series

Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 7571 LNCS |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Other

Other | 9th 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 |
---|---|

Country | Estonia |

City | Tallinn |

Period | 3/24/12 → 3/25/12 |

### Fingerprint

### ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)

### Cite this

*Rewriting Logic and Its Applications - 9th International Workshop, WRLA 2012, Held as a Satellite Event of ETAPS, Revised Selected Papers*(pp. 99-117). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7571 LNCS). https://doi.org/10.1007/978-3-642-34005-5_6