Predicate abstraction of rewrite theories

Kyungmin Bae, Jose Meseguer

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

Abstract

For an infinite-state concurrent system with a set AP of state predicates, its predicate abstraction defines a finite-state system whose states are subsets of AP, and its transitions s∈→∈s' are witnessed by concrete transitions between states in satisfying the respective sets of predicates s and s'. Since it is not always possible to find such witnesses, an over-approximation adding extra transitions is often used. For systems described by formal specifications, predicate abstractions are typically built using various automated deduction techniques. This paper presents a new method - based on rewriting, semantic unification, and variant narrowing - to automatically generate a predicate abstraction when the formal specification of is given by a conditional rewrite theory. The method is illustrated with concrete examples showing that it naturally supports abstraction refinement and is quite accurate, i.e., it can produce abstractions not needing over-approximations.

Original languageEnglish (US)
Title of host publicationRewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings
PublisherSpringer-Verlag
Pages61-76
Number of pages16
ISBN (Print)9783319089171
DOIs
StatePublished - Jan 1 2014
Event25th International Conference on Rewriting Techniques and Applications, RTA 2014 and 12th International Conference on Typed Lambda Calculus and Applications, TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 - Vienna, Austria
Duration: Jul 14 2014Jul 17 2014

Publication series

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

Other

Other25th International Conference on Rewriting Techniques and Applications, RTA 2014 and 12th International Conference on Typed Lambda Calculus and Applications, TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014
CountryAustria
CityVienna
Period7/14/147/17/14

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Predicate abstraction of rewrite theories'. Together they form a unique fingerprint.

  • Cite this

    Bae, K., & Meseguer, J. (2014). Predicate abstraction of rewrite theories. In Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings (pp. 61-76). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8560 LNCS). Springer-Verlag. https://doi.org/10.1007/978-3-319-08918-8_5