A Decidable Characterization of a Graphical Pi-calculus with Iterators

A Decidable Characterization of a Graphical Pi-calculus with Iterators

This paper presents the Pi-graphs, a visual paradigm for the modelling and verification of mobile systems. The language is a graphical variant of the Pi-calculus with iterators to express non-terminating behaviors. The operational semantics of Pi-graphs use ground notions of labelled transition and...

Full description

Bibliographic Details
Main Authors: Raymond Devillers, Hanna Klaudel, Frédéric Peschanski
Format: Article
Language:English
Published: Open Publishing Association 2010-10-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1011.0220v1
id doaj-a3c81d928d584cd0a6980edff7a9b355
record_format Article
spelling doaj-a3c81d928d584cd0a6980edff7a9b3552020-11-24T23:36:49ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802010-10-0139Proc. INFINITY 2010476110.4204/EPTCS.39.4A Decidable Characterization of a Graphical Pi-calculus with IteratorsRaymond DevillersHanna KlaudelFrédéric PeschanskiThis paper presents the Pi-graphs, a visual paradigm for the modelling and verification of mobile systems. The language is a graphical variant of the Pi-calculus with iterators to express non-terminating behaviors. The operational semantics of Pi-graphs use ground notions of labelled transition and bisimulation, which means standard verification techniques can be applied. We show that bisimilarity is decidable for the proposed semantics, a result obtained thanks to an original notion of causal clock as well as the automatic garbage collection of unused names. http://arxiv.org/pdf/1011.0220v1
collection DOAJ
language English
format Article
sources DOAJ
author Raymond Devillers
Hanna Klaudel
Frédéric Peschanski
spellingShingle Raymond Devillers
Hanna Klaudel
Frédéric Peschanski
A Decidable Characterization of a Graphical Pi-calculus with Iterators
Electronic Proceedings in Theoretical Computer Science
author_facet Raymond Devillers
Hanna Klaudel
Frédéric Peschanski
author_sort Raymond Devillers
title A Decidable Characterization of a Graphical Pi-calculus with Iterators
title_short A Decidable Characterization of a Graphical Pi-calculus with Iterators
title_full A Decidable Characterization of a Graphical Pi-calculus with Iterators
title_fullStr A Decidable Characterization of a Graphical Pi-calculus with Iterators
title_full_unstemmed A Decidable Characterization of a Graphical Pi-calculus with Iterators
title_sort decidable characterization of a graphical pi-calculus with iterators
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2010-10-01
description This paper presents the Pi-graphs, a visual paradigm for the modelling and verification of mobile systems. The language is a graphical variant of the Pi-calculus with iterators to express non-terminating behaviors. The operational semantics of Pi-graphs use ground notions of labelled transition and bisimulation, which means standard verification techniques can be applied. We show that bisimilarity is decidable for the proposed semantics, a result obtained thanks to an original notion of causal clock as well as the automatic garbage collection of unused names.
url http://arxiv.org/pdf/1011.0220v1
work_keys_str_mv AT raymonddevillers adecidablecharacterizationofagraphicalpicalculuswithiterators
AT hannaklaudel adecidablecharacterizationofagraphicalpicalculuswithiterators
AT fredericpeschanski adecidablecharacterizationofagraphicalpicalculuswithiterators
AT raymonddevillers decidablecharacterizationofagraphicalpicalculuswithiterators
AT hannaklaudel decidablecharacterizationofagraphicalpicalculuswithiterators
AT fredericpeschanski decidablecharacterizationofagraphicalpicalculuswithiterators
_version_ 1725521576831483904

Similar Items