State space c-reductions of concurrent systems in rewriting logic

Alberto Lluch Lafuente, José Meseguer, Andrea Vandin

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

Abstract

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 (US)
Title of host publicationFormal Methods and Software Engineering - 14th International Conference on Formal Engineering Methods, ICFEM 2012, Proceedings
Pages430-446
Number of pages17
DOIs
StatePublished - 2012
Event14th International Conference on Formal Engineering Methods, ICFEM 2012 - Kyoto, Japan
Duration: Nov 12 2012Nov 16 2012

Publication series

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

Other

Other14th International Conference on Formal Engineering Methods, ICFEM 2012
CountryJapan
CityKyoto
Period11/12/1211/16/12

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'State space c-reductions of concurrent systems in rewriting logic'. Together they form a unique fingerprint.

Cite this