Canonical Narrowing with Irreducibility Constraints as a Symbolic Protocol Analysis Method

Santiago Escobar, José Meseguer

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

Abstract

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
PublisherSpringer
Pages15-38
Number of pages24
ISBN (Print)9783030190514
DOIs
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

Conference

ConferenceCatherine Meadows Festschrift Symposium, 2019
Country/TerritoryUnited States
CityFredericksburg
Period5/22/195/23/19

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

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