Jorge A. Perez: Research

Coauthors and Collaborators 

Jesus Aranda, Gerard Assayag, Mario Bravetti, Luis Caires, Alberto Delgado, Juan F. Diaz, Cinzia Di Giusto, Julian Gutierrez, Rafael Jordan, Ivan Lanese, Hugo A. Lopez, Roland Meyer, Carlos Olarte, Gustavo Pabon, Catuscia Palamidessi, Camilo Rueda, Davide Sangiorgi, Alan Schmitt, Joao C. Seco, Mauricio Toro, Frank D. Valencia, Hugo T. Vieira, Gianluigi Zavattaro

Additional Information on Papers 

This page collects additional information related to published and submitted papers, such as extended versions, appendixes, corrections, and slides. Any comments and suggestions are welcome!

  • On the Expressiveness of Polyadic and Synchronous Communication in Higher-Order Process Calculi
    Ivan Lanese  Laboratory FOCUS (University of Bologna, Italy - INRIA, France) 
    Jorge A. Perez  FCT New University of Lisbon, Portugal 
    Davide Sangiorgi Laboratory FOCUS (University of Bologna, Italy - INRIA, France)
    Alan Schmitt INRIA Grenoble Rhone-Alpes, France

    Higher-order process calculi are process calculi in which processes can be communicated. We study the expressiveness of strictly higher-order process calculi, and focus on two issues well-understood for first-order calculi but not in the higher-order setting: synchronous vs. asynchronous communication and polyadic vs. monadic communication. First, and similarly as in the first-order setting, synchronous process passing is shown to be encodable into asynchronous process passing. Then, the absence of name passing is shown to induce a hierar- chy of higher-order process calculi based on the arity of polyadic communication, thus revealing a striking point of contrast with respect to first-order calculi. Finally, the passing of abstractions (i.e., functions from processes to processes) is shown to be more expressive than process passing alone..
    Download:
    Extended Abstract (In Proc. of ICALP'10, pp. 442-453, volume 6199 of LNCS, Springer 2010    ): [PDF]
    Slides (as presented in ICALP): [PDF]
    See Chapter 6 of Perez's PhD thesis (below) for further details.
    20/06/2010: A "standalone" technical report is in preparation, and will appear soon.

  • Higher-Order Concurrency: Expressiveness and Decidability Results (PhD Thesis)
    Jorge A. Perez, University of Bologna, Italy
    Download:
    Draft (Submitted, January 19, 2010):     [PDF]
    .
  • On the Expressiveness of Polyadicity in Higher-Order Communication
    Ivan Lanese, Jorge A. Perez, Davide Sangiorgi University of Bologna, Italy
    Alan Schmitt INRIA Grenoble Rhone-Alpes, France

    In higher-order process calculi the values exchanged in communications may contain processes. We describe a study of the expressive power of strictly higher-order pro- cess calculi, i.e. calculi in which only process passing is allowed and no name-passing is present. In this setting, the polyadicity (i.e. the number of parameters) allowed in commu- nications is shown to induce a hierarchy of calculi of strictly increasing expressiveness: a higher-order calculus with n-adic communication cannot be encoded into a calculus with n ? 1-adic communication. In this note we outline this result, and discuss on how it relies on a notion of encoding that takes a rather fine standpoint with respect to internal behavior.
    Download:
    Extended Abstract (In Informal Proc. of     ICTCS'09): [PDF].

  • On the Expressiveness of Forwarding in Higher-Order Communication
    Cinzia Di Giusto, Jorge A. Perez, and Gianluigi Zavattaro University of Bologna, Italy

    In higher-order process calculi the values exchanged in communications may contain processes. There are only two capabilities for received processes: execution and forwarding. Here we propose a limited form of forwarding: output actions can only communicate the parallel composition of statically known closed processes and processes received through previously executed input actions. We study the expressiveness of a higher-order process calculus featuring this style of communication. Our main result shows that in this calculus termination is decidable while convergence is undecidable. Then, as a way of recovering the expressiveness loss due to limited forwarding, we extend the calculus with a form of process suspension called passivation. Somewhat surprisingly, in the calculus extended with passivation both termination and convergence are undecidable. 
    Download:
    Conference Version (in Proc. of     ICTAC'09, pp. 155-169, volume 5684 of LNCS, Springer, 2009): [PDF]
    Extended and Revised Version, with proofs (34pp) ---DRAFT, 06/12/2009---: [PDF] 
    Slides:     [PDF]

  • On the Expressiveness and Decidability of Higher-Order Process Calculi 
    Ivan Lanese, Jorge A. Perez, Davide Sangiorgi University of Bologna, Italy
    Alan Schmitt INRIA Grenoble Rhone-Alpes, France

    In higher-order process calculi the values exchanged in communications may contain processes. A core calculus of higher-order concurrency is studied; it has only the operators necessary to express higher-order communications: input prefix, process output, and parallel composition. By exhibiting a nearly deterministic encoding of Minsky Machines, the calculus is shown to be Turing Complete andtherefore its termination problem is undecidable. Strong bisimilarity, however, is proved to be decidable. Further, the main forms of strong bisimilarity for higher-order processes (higher-order bisimilarity, context bisimilarity, normal bisimilarity, barbed congruence) coincide. They also coincide with their asynchronous versions. A sound and complete axiomatization of bisimilarity is given. Finally, bisimilarity is shown to become undecidable if at least four static (i.e., top-level) restrictions are added to the calculus. 
    Download: 
    Conference Version (in Proc. of     LICS'08, pp. 145--155, IEEE Computer Society, 2008.): [PDF]
    Extended and Revised Version, with proofs ---DRAFT, 01/06/2010---: [PDF] 
    Slides (as presented in the     COPLAS Seminar, August 12, 2008): [PDF]