The Linear Temporal Logic of Rewriting Model Checker in Maude

Abstract

The Linear Temporal Logic of Rewriting (LTLR) extends linear temporal logic with spatial action patterns which represent properties related to events. LTLR generalizes and extends various state-based and event-based logics and aims to avoid certain types of mismatches between a system and its temporal logic properties. We have implemented the LTLR model checker within the Maude system by extending the existing Maude LTL model checker. Our LTLR model checker provides very expressive methods to define event-related properties as well as state-related properties, or more generally properties involving both event and state predicates. This greater expressiveness is gained without compromising performance, because the LTLR implementation minimizes the extra costs involved in handling the events of systems.

Short bio

Resources

• talk slide