@Article{AB12,
   status = {public},
   task = {T1.2},
   doi = {10.1016/j.ic.2012.01.006},
   joint-pub = {false},
   year = {2012},
   invited = {no},
   timestamp = {2012.10.31},
   volume = {212},
   main = {no},
   issn = {0890-5401},
   title = {{Deciding Safety Properties in Infinite-State Pi-Calculus Via BehaviouralTypes}},
   author = {Lucia Acciai and Michele Boreale},
   period = {year1},
   journal = {Inf. Comput},
   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, given a process P, tries to extract 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 then prove that, for an interesting fragment of the considered logic, satisfiability (T ⊧ φ) 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.},
   owner = {kroiss},
   accessible = {true},
   partner = {UDF},
   ascens_ref = {true},
   wp = {wp5,wp2},
   pages = {92-117}
}