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.
CITATION STYLE
Escobar, S., & Meseguer, J. (2019). Canonical Narrowing with Irreducibility Constraints as a Symbolic Protocol Analysis Method. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11565 LNCS, pp. 15–38). Springer Verlag. https://doi.org/10.1007/978-3-030-19052-1_4
Mendeley helps you to discover research relevant for your work.