Infinite-state model checking of LTLR formulas using narrowing

Kyungmin Bae, José Meseguer

Research output: Contribution to journalArticlepeer-review

Abstract

The linear temporal logic of rewriting (LTLR) is a simple extension of LTL that adds spatial action patterns to the logic, expressing that a specific instance of an action described by a rewrite rule has been performed. Although the theory and algorithms of LTLR for finite-state model checking are well-developed [2], no theoretical foundations have yet been developed for infinite-state LTLR model checking. The main goal of this paper is to develop such foundations for narrowing-based logical model checking of LTLR properties. A key theme in this paper is the systematic relationship, in the form of a simulation with remarkably good properties, between the concrete state space and the symbolic state space. A related theme is the use of additional state space reduction methods, such as folding and equational abstractions, that can in some cases yield a finite symbolic state space.

Keywords

  • Infinite-state systems
  • LTLR
  • Model checking
  • Narrowing

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Infinite-state model checking of LTLR formulas using narrowing'. Together they form a unique fingerprint.

Cite this