Computing at Glasgow University
Paper ID: 9322
DCS Tech Report Number: TR-2010-311

A SAT based algorithm for the matching problem in bigraphs with sharing
Sevegnani,M. Unsworth,C. Calder,M.

Publication Type: Tech Report (internal)
Appeared in: DCS Technical Report Series
Page Numbers :
Publisher: Dept of Computing Science, University of Glasgow
Year: 2010

Bigraphical reactive systems are a formalism for modelling mobile computation. A bigraph consists of a place graph and a link graph; reaction rules define how place and link graphs evolve. Bigraphs originally supported only tree structures as place graphs, we have extended the formalism to bigraphs with sharing, which allow directed acyclic graphs as place graphs. A major challenge for bigraph tool support (with or without sharing) is defining bigraph matching and providing an efficient algorithm. In the case of bigraphs with sharing, place graph matching is a special case of the NP-complete, sub-graph isomorphism problem. We present the details of place graph matching and give a sound and complete, efficient algorithm in SAT.

Keywords: bigraph, matching, formal models, SAT

PDF Bibtex entry Endnote XML