Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other
copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying
this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
show main publications
Graphical verification of a spatial logic for the pi-calculus @INPROCEEDINGS{GL:GTVC2005:GVSLP, title = {{Graphical verification of a spatial logic for the pi-calculus}}, author = {{Fabio} {Gadducci} and {Alberto} {Lluch Lafuente}}, booktitle = {Proceedings of GT-VC 2005, Workshop on Graph Transformation for Verification and Concurrency}, editor = {Arend Rensink and Reiko Heckel and Barbara Koenig}, pages = {31-46}, abstract = {The paper introduces a novel approach to the verification of spatial properties for finite pi-calculus specifications. The mechanism is based on a recently proposed graphical encoding for mobile calculi: Each process is mapped into a (ranked) graph, such that the denotation is fully abstract with respect to the usual structural congruence (i.e., two processes are equivalent exactly when the corresponding encodings yield the same graph). Spatial properties for reasoning about the behavior and the structure of pi- calculus processes are then expressed in a logic introduced by Caires, and they are verified on the graphical encoding of a process, rather than on its textual representation. More precisely, the graphical presentation allows for providing a simple and easy to implement verification algorithm based on the graphical encoding (returning true if and only if a given process verifies a given spatial formula).}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, volume = {154}, number = {2}, year = {2006}, url = {http://rap.dsi.unifi.it/sensoriasite/154_2_003.pdf}, partner = {PISA}, status = {public}, task = {T3.4, T7.1}, }
|