Saturated LTSs for adhesive rewriting systems

Abstract

G-Reactive Systems (GRSs) are a framework for the derivation of labelled transition systems (LTSs) from a set of unlabelled rules. A label for a transition from A to B is a context C[-] such that C[A] may perform a reaction and reach B. If either all contexts, or just the "minimal" ones, are considered, the resulting LTS is called saturated (GIPO, respectively). The borrowed contexts (BCs) technique addresses the issue in the setting of the DPO approach. Indeed, from an adhesive rewriting system (ARS) a GRS can be defined such that DPO derivations correspond to reactions, and BC derivations to transitions of the GIPO LTS. This paper extends the BCs technique in order to derive saturated LTSs for ARSs, applying it to capture bisimilarity for asynchronous calculi. © 2010 Springer-Verlag.