Home | Search | Help  
Home Page Università di Genova

Technical Report Details

Date 6-6-2005
Number DISI-TR-05-08
Title Constraint Multiset Rewriting
Authors Giorgio Delzanno
Bibtex Entry
E-mail giorgio@disi.unige.it
Link http://www.disi.unige.it/person/DelzannoG/MSR/del02.ps.gz
Abstract We investigate the foundations of the specification language MSR(C), that combines multiset rewriting over first order atomic formulas and a generic constraints system C, and of a corresponding verification procedure for checking safety properties. Our method has been applied to the analysis of mutual exclusion, cache coherence and security protocols. All the case-studies belong to a class of concurrent systems for which verification is often undecidable. Indeed their state-space is infinite in more than one dimension: they are parametric in the number of components (processes/sessions) and have local data defined over infinite domains. Our verification procedure is based on symbolic backward exploration. Infinite sets of configurations of an MSR(C) specification are represented symbolically via assertions defined over multisets and constraints. Constraints and term manipulation operations are combined together in order to effectively manipulate assertions. All operations are defined for a generic constraint system C. By a careful choice of the constraints system and of the syntax of rules, we isolate a new class of constraint multiset rewriting specifications (hence of infinite-state systems) for which verification of safety properties is decidable. Decidability is obtained by applying the theory of well and better quasi orderings.
Back to Technical Reports