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
Deciding safety properties in infinite-state pi-calculus via behavioural types
@INPROCEEDINGS{AB09,
title = {{Deciding safety properties in infinite-state pi-calculus via behavioural types}},
author = {{Lucia} {Acciai} and {Michele} {Boreale}},
booktitle = {Automata, Languages and Programming},
pages = {31-42},
abstract = {In the pi-calculus, we consider decidability of certain safety properties expressed in a simple spatial logic. We first introduce a behavioural type system that, for any process P, extracts a spatial-behavioural type T in the form of a ccs term that is logically equivalent to the given process. Using techniques based on well-structured transition systems, we prove that, for an interesting fragment of the logic, satisfiability T |= phi is decidable for types. As a consequence of logical equivalence between types and processes, we obtain decidability of this fragment of the logic for all well-typed pi-processes.},
publisher = {Springer Berlin / Heidelberg},
series = {LNCS},
volume = {5556},
year = {2009},
url = {http://rap.dsi.unifi.it/sensoriasite/decLog.pdf},
doi = {10.1007/978-3-642-02930-1_3},
institution = {Universit`a di Firenze},
isbn = { 978-3-642-02929-5},
keywords = {behavioral-types, pi-calculus, spatial logic},
partner = {DSIUF},
school = {University of Firenze},
task = {T3.3},
}
|
