State Space c-Reductions of Concurrent Systems in Rewriting Logic

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


We present c − reductions, a simple, flexible and very general state space reduction technique that exploits an equivalence relation on states that is a bisimulation. Reduction is achieved by a canonizer function, which maps each state into a not necessarily unique canonical representative of its equivalence class. The approach contains symmetry reduction and name reuse and name abstraction as special cases, and exploits the expressiveness of rewriting logic and its realization in Maude to automate c-reductions and to seamlessly integrate model checking and the discharging of correctness proof obligations. The performance of the approach has been validated over a set of representative case studies.
Original languageEnglish
Title of host publicationFormal Methods and Software Engineering : 14th International Conference on Formal Engineering Methods, ICFEM 2012, Kyoto, Japan, November 12-16, 2012. Proceedings
PublisherSpringer Berlin Heidelberg
Publication date2012
ISBN (Print)978-3-642-34280-6
ISBN (Electronic)978-3-642-34281-3
Publication statusPublished - 2012
Externally publishedYes
Event14th International Conference on Formal Engineering Methods - Kyoto, Japan
Duration: 12 Nov 201216 Nov 2012
Conference number: 14


Conference14th International Conference on Formal Engineering Methods
SeriesLecture Notes in Computer Science

Cite this