Canonical Narrowing with Irreducibility Constraints as a Symbolic Protocol Analysis Method

Santiago Escobar, José Meseguer

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


This work proposes canonical constrained narrowing, a new symbolic reachability analysis technique applicable to topmost rewrite theories where the equational theory has the finite variant property. Our experiments suggest that canonical constrained narrowing is more efficient than both standard narrowing and the previously studied contextual narrowing. These results are relevant not only for Maude-NPA, but also for symbolically analyzing many other concurrent systems specified by means of rewrite theories.

Original languageEnglish (US)
Title of host publicationFoundations of Security, Protocols, and Equational Reasoning - Essays Dedicated to Catherine A. Meadows
EditorsJoshua D. Guttman, Carl E. Landwehr, José Meseguer, Dusko Pavlovic
Number of pages24
ISBN (Print)9783030190514
StatePublished - 2019
EventCatherine Meadows Festschrift Symposium, 2019 - Fredericksburg, United States
Duration: May 22 2019May 23 2019

Publication series

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


ConferenceCatherine Meadows Festschrift Symposium, 2019
Country/TerritoryUnited States

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Canonical Narrowing with Irreducibility Constraints as a Symbolic Protocol Analysis Method'. Together they form a unique fingerprint.

Cite this