LTS semantics for process calculi from their graphical encodings

Abstract

The behaviour of a computational device is often naturally defined by means of reduction semantics: a set representing the possible states of the device, and an unlabelled relation among them, usually inductively defined, representing the possible evolutions of the device. Despite the advantage of conveying the semantics with few compact rewriting rules, freely instantiated and contextualized, the main drawback of reduction-based solutions is that the dynamic behaviour of a system is described in a monolithic way, and so it can be interpreted only by inserting the system in appropriate contexts, where a reduction may take place. © 2010 Springer-Verlag.