Analysis of permutation equivalence in $\mathcal{M}$-adhesive transformation systems with negative application conditions. (26th June 2014)

• Record Type: Journal Article
• Authors: HERMANN, FRANK; CORRADINI, ANDREA; EHRIG, HARTMUT
• Is Part Of: Mathematical structures in computer science. Volume 24:Number 4(2014)
• Publication Date: 2014-06-26
• Subjects: Computer science -- Mathematics -- Periodicals; 004.015105
• DOI: 10.1017/S0960129512000382
• Languages: English
• ISSNs: 0960-1295

Abstract

<abstract abstract-type="normal"> <title> <x content-type="archive" xml:space="preserve">Abstract</x> </title> <p> <inline-formula> <alternatives> <inline-graphic xlink:href="ark:/27927/pghmrxd3hm" xlink:type="simple" xmlns:xlink="http://www.w3.org/1999/xlink" /> <tex-math><![CDATA[$\mathcal{M}$]]></tex-math> </alternatives> </inline-formula>-adhesive categories provide an abstract framework for a large variety of specification frameworks for modelling distributed and concurrent systems. They extend the well-known frameworks of adhesive and weak adhesive HLR categories and integrate high-level constructs such as attribution as in the case of typed attributed graphs.</p> <p>In the current paper, we investigate <inline-formula><alternatives><inline-graphic xlink:href="ark:/27927/pghmrxd3hm" xlink:type="simple" xmlns:xlink="http://www.w3.org/1999/xlink" /><tex-math><![CDATA[$\mathcal{M}$]]></tex-math></alternatives></inline-formula>-adhesive transformation systems including negative application conditions (NACs) for transformation rules, which are often used in applications. For such systems, we propose an original equivalence on transformation sequences, called <italic>permutation equivalence</italic>, that is coarser than the classical switch equivalence. We also present a general construction of deterministic processes for <inline-formula><alternatives><inline-graphic xlink:href="ark:/27927/pghmrxd3hm" xlink:type="simple" xmlns:xlink="http://www.w3.org/1999/xlink" /><tex-math><![CDATA[$\mathcal{M}$]]></tex-math></alternatives></inline-formula>-adhesive transformation systems based on subobject transformation systems. As a main result, we show that the process obtained from a transformation sequence identifies its equivalence class of permutation-equivalent transformation sequences. Moreover, we show how the analysis of this process can be reduced to the analysis of the reachability graph of a generated Place/Transition Petri net. This net encodes the dependencies between rule applications of the transformation sequence, including the inhibiting effects of the NACs.</p> </abstract>