Showing 1–50 of 62 results for author: Pérez, J A

Around Classical and Intuitionistic Linear Processes

Authors: Juan C. Jaramillo, Dan Frumin, Jorge A. Pérez

Abstract: Curry-Howard correspondences between Linear Logic (LL) and session types provide a firm foundation for concurrent processes. As the correspondences hold for intuitionistic and classic versions of LL (ILL and CLL), we obtain two different families of type systems for concurrency. An open question remains: how do these two families exactly relate to each other? Based upon a translation from CLL to I… ▽ More Curry-Howard correspondences between Linear Logic (LL) and session types provide a firm foundation for concurrent processes. As the correspondences hold for intuitionistic and classic versions of LL (ILL and CLL), we obtain two different families of type systems for concurrency. An open question remains: how do these two families exactly relate to each other? Based upon a translation from CLL to ILL due to Laurent (2018), we provide two complementary answers, in the form of full abstraction results based on a typed observational equivalence due to Atkey (2017). Our results elucidate hitherto missing formal links between seemingly related yet different type systems for concurrency. △ Less

Submitted 8 July, 2024; originally announced July 2024.

Comments: Initial version, 16 pages + appendices

Comparing Session Type Systems derived from Linear Logic

Authors: Bas van den Heuvel, Jorge A. Pérez

Abstract: Session types are a typed approach to message-passing concurrency, where types describe sequences of intended exchanges over channels. Session type systems have been given strong logical foundations via Curry-Howard correspondences with linear logic, a resource-aware logic that naturally captures structured interactions. These logical foundations provide an elegant framework to specify and (static… ▽ More Session types are a typed approach to message-passing concurrency, where types describe sequences of intended exchanges over channels. Session type systems have been given strong logical foundations via Curry-Howard correspondences with linear logic, a resource-aware logic that naturally captures structured interactions. These logical foundations provide an elegant framework to specify and (statically) verify message-passing processes. In this paper, we rigorously compare different type systems for concurrency derived from the Curry-Howard correspondence between linear logic and session types. We address the main divide between these type systems: the classical and intuitionistic presentations of linear logic. Along the years, these presentations have given rise to separate research strands on logical foundations for concurrency; the differences between their derived type systems have only been addressed informally. To formally assess these differences, we develop $π\mathsf{ULL}$, a session type system that encompasses type systems derived from classical and intuitionistic interpretations of linear logic. Based on a fragment of Girard's Logic of Unity, $π\mathsf{ULL}$ provides a basic reference framework: we compare existing session type systems by characterizing fragments of $π\mathsf{ULL}$ that coincide with classical and intuitionistic formulations. We analyze the significance of our characterizations by considering the locality principle (enforced by intuitionistic interpretations but not by classical ones) and forms of process composition induced by the interpretations. △ Less

Submitted 26 January, 2024; originally announced January 2024.

Comments: Revised/extended version of https://doi.org/10.4204/EPTCS.314.1

Termination in Concurrency, Revisited

Authors: Joseph W. N. Paulus, Jorge A. Pérez, Daniele Nantes-Sobrinho

Abstract: Termination is a central property in sequential programming models: a term is terminating if all its reduction sequences are finite. Termination is also important in concurrency in general, and for message-passing programs in particular. A variety of type systems that enforce termination by ty** have been developed. In this paper, we rigorously compare several type systems for $π$-calculus proce… ▽ More Termination is a central property in sequential programming models: a term is terminating if all its reduction sequences are finite. Termination is also important in concurrency in general, and for message-passing programs in particular. A variety of type systems that enforce termination by ty** have been developed. In this paper, we rigorously compare several type systems for $π$-calculus processes from the unifying perspective of termination. Adopting session types as reference framework, we consider two different type systems: one follows Deng and Sangiorgi's weight-based approach; the other is Caires and Pfenning's Curry-Howard correspondence between linear logic and session types. Our technical results precisely connect these very different type systems, and shed light on the classes of client/server interactions they admit as correct. △ Less

Submitted 2 August, 2023; originally announced August 2023.

Monitoring Blackbox Implementations of Multiparty Session Protocols

Authors: Bas van den Heuvel, Jorge A. Pérez, Rares A. Dobre

Abstract: We present a framework for the distributed monitoring of networks of components that coordinate by message-passing, following multiparty session protocols specified as global types. We improve over prior works by (i) supporting components whose exact specification is unknown ("blackboxes") and (ii) covering protocols that cannot be analyzed by existing techniques. We first give a procedure for syn… ▽ More We present a framework for the distributed monitoring of networks of components that coordinate by message-passing, following multiparty session protocols specified as global types. We improve over prior works by (i) supporting components whose exact specification is unknown ("blackboxes") and (ii) covering protocols that cannot be analyzed by existing techniques. We first give a procedure for synthesizing monitors for blackboxes from global types, and precisely define when a blackbox correctly satisfies its global type. Then, we prove that monitored blackboxes are sound (they correctly follow the protocol) and transparent (blackboxes with and without monitors are behaviorally equivalent). △ Less

Submitted 3 October, 2023; v1 submitted 7 June, 2023; originally announced June 2023.

Comments: Full version with appendices of our RV'23 paper

Debunking Cantor: New Set-Theoretical and Logical Considerations

Authors: Juan A Perez

Abstract: For more than a century, Cantor's theory of transfinite numbers has played a pivotal role in set theory, with ramifications that extend to many areas of mathematics. This article extends earlier findings with a fresh look at the critical facts of Cantor's theory: i) Cantor's widely renowned Diagonalization Argument (CDA) is fully refuted by a set of counter-examples that expose the fallacy of this… ▽ More For more than a century, Cantor's theory of transfinite numbers has played a pivotal role in set theory, with ramifications that extend to many areas of mathematics. This article extends earlier findings with a fresh look at the critical facts of Cantor's theory: i) Cantor's widely renowned Diagonalization Argument (CDA) is fully refuted by a set of counter-examples that expose the fallacy of this proof. ii) The logical inconsistencies of CDA are revisited, exposing the short-comings of CDA's implementation of the method of proof by contradiction. iii) The denumerability of the power set of the set of the natural numbers, P(N), is substantiated by a proof that takes full account of all the infinite subsets of N. Such a result confirms the denumerability of the set of the real numbers, R, and with it the countable nature of the continuum. iv) Given that the denumerable character of (probably) all infinite sets makes their comparison in terms of one-to-one correspondences a rather pointless exercise, a new concept of relative cardinality is introduced which facilitates a quantitative evaluation of their different magnitudes. △ Less

Submitted 14 March, 2023; originally announced May 2023.

Comments: 22 pages, 2 figures, 1 table

MSC Class: Primary 03B10; 03B30; 03B50; Secondary 03F07; 03F40

A Minimal Formulation of Session Types

Authors: Alen Arslanagić, Jorge A. Pérez, Dan Frumin

Abstract: Session types are a type-based approach to the verification of message-passing programs. They specify communication structures essential for program correctness; a session type says what and when should be exchanged through a channel. Central to session-typed languages are sequencing constructs in types and processes that explicitly specify the order of actions in a protocol. In this paper we st… ▽ More Session types are a type-based approach to the verification of message-passing programs. They specify communication structures essential for program correctness; a session type says what and when should be exchanged through a channel. Central to session-typed languages are sequencing constructs in types and processes that explicitly specify the order of actions in a protocol. In this paper we study session types without sequencing. The resulting framework of minimal session types is arguably the simplest form of session types one could conceive. In the context of a core process calculus with sessions and higher-order concurrency (abstraction-passing), we establish two main technical results. First, we prove that every process $P$ typable with standard session types can be compiled down into a process $\mathcal{D}(P)$ typable with minimal session types. Second, we prove that $P$ and $\mathcal{D}(P)$ are behaviorally equivalent. These results indicate that having sequencing constructs in processes and session types is convenient but redundant: only sequentiality in processes is truly indispensable, as it can correctly codify sequentiality in types. Our developments draw inspiration from work by Parrow on behavior-preserving decompositions of untyped processes. By casting Parrow's results in the realm of typed processes, our developments reveal a conceptually simple formulation of session types and a principled avenue to the integration of session types into programming languages without sequencing in types. △ Less

Submitted 12 January, 2023; originally announced January 2023.

Comments: arXiv admin note: text overlap with arXiv:1906.03836

Asynchronous Functional Sessions: Cyclic and Concurrent

Authors: Bas van den Heuvel, Jorge A. Pérez

Abstract: We present Concurrent GV (CGV), a functional calculus with message-passing concurrency governed by session types. With respect to prior calculi, CGV has increased support for concurrent evaluation and for cyclic network topologies. The design of CGV draws on APCP, a session-typed asynchronous pi-calculus developed in prior work. Technical contributions are (i) the syntax, semantics, and type syste… ▽ More We present Concurrent GV (CGV), a functional calculus with message-passing concurrency governed by session types. With respect to prior calculi, CGV has increased support for concurrent evaluation and for cyclic network topologies. The design of CGV draws on APCP, a session-typed asynchronous pi-calculus developed in prior work. Technical contributions are (i) the syntax, semantics, and type system of CGV; (ii) a correct translation of CGV into APCP; (iii) a technique for establishing deadlock-free CGV programs, by resorting to APCP's priority-based type system. △ Less

Submitted 6 September, 2022; originally announced September 2022.

Comments: In Proceedings EXPRESS/SOS 2022, arXiv:2208.14777. arXiv admin note: substantial text overlap with arXiv:2208.07644

Journal ref: EPTCS 368, 2022, pp. 75-94

A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency

Authors: Dan Frumin, Emanuele D'Osualdo, Bas van den Heuvel, Jorge A. Pérez

Abstract: The emergence of propositions-as-sessions, a Curry-Howard correspondence between propositions of Linear Logic and session types for concurrent processes, has settled the logical foundations of message-passing concurrency. Central to this approach is the resource consumption paradigm heralded by Linear Logic. In this paper, we investigate a new point in the design space of session type systems fo… ▽ More The emergence of propositions-as-sessions, a Curry-Howard correspondence between propositions of Linear Logic and session types for concurrent processes, has settled the logical foundations of message-passing concurrency. Central to this approach is the resource consumption paradigm heralded by Linear Logic. In this paper, we investigate a new point in the design space of session type systems for message-passing concurrent programs. We identify O'Hearn and Pym's Logic of Bunched Implications (BI) as a fruitful basis for an interpretation of the logic as a concurrent programming language. This leads to a treatment of non-linear resources that is radically different from existing approaches based on Linear Logic. We introduce a new $π$-calculus with sessions, called $π$BI; its most salient feature is a construct called spawn, which expresses new forms of sharing that are induced by structural principles in BI. We illustrate the expressiveness of $π$BI and lay out its fundamental theory: type preservation, deadlock-freedom, and weak normalization results for well-typed processes; an operationally sound and complete typed encoding of an affine $λ$-calculus; and a non-interference result for access of resources. △ Less

Submitted 12 September, 2022; originally announced September 2022.

Comments: 27 pages + the appendices

Asynchronous Functional Sessions: Cyclic and Concurrent (Extended Version)

Authors: Bas van den Heuvel, Jorge A. Pérez

Abstract: We present Concurrent GV (CGV), a functional calculus with message-passing concurrency governed by session types. With respect to prior calculi, CGV has increased support for concurrent evaluation and for cyclic network topologies. The design of CGV draws on APCP, a session-typed asynchronous pi-calculus developed in prior work. Technical contributions are (i) the syntax, semantics, and type syste… ▽ More We present Concurrent GV (CGV), a functional calculus with message-passing concurrency governed by session types. With respect to prior calculi, CGV has increased support for concurrent evaluation and for cyclic network topologies. The design of CGV draws on APCP, a session-typed asynchronous pi-calculus developed in prior work. Technical contributions are (i) the syntax, semantics, and type system of CGV; (ii) a correct translation of CGV into APCP; (iii) a technique for establishing deadlock-free CGV programs, by resorting to APCP's priority-based type system. △ Less

Submitted 19 September, 2022; v1 submitted 16 August, 2022; originally announced August 2022.

Comments: Extended version of a paper accepted at EXPRESS'22. arXiv admin note: substantial text overlap with arXiv:2111.13091

Typed Non-determinism in Functional and Concurrent Calculi

Authors: Bas van den Heuvel, Joseph W. N. Paulus, Daniele Nantes-Sobrinho, Jorge A. Pérez

Abstract: We study functional and concurrent calculi with non-determinism, along with type systems to control resources based on linearity. The interplay between non-determinism and linearity is delicate: careless handling of branches can discard resources meant to be used exactly once. Here we go beyond prior work by considering non-determinism in its standard sense: once a branch is selected, the rest are… ▽ More We study functional and concurrent calculi with non-determinism, along with type systems to control resources based on linearity. The interplay between non-determinism and linearity is delicate: careless handling of branches can discard resources meant to be used exactly once. Here we go beyond prior work by considering non-determinism in its standard sense: once a branch is selected, the rest are discarded. Our technical contributions are three-fold. First, we introduce a $π$-calculus with non-deterministic choice, governed by session types. Second, we introduce a resource $λ$-calculus, governed by intersection types, in which non-determinism concerns fetching of resources from bags. Finally, we connect our two typed non-deterministic calculi via a correct translation. △ Less

Submitted 29 September, 2023; v1 submitted 2 May, 2022; originally announced May 2022.

Scalable Typestate Analysis for Low-Latency Environments

Authors: Alen Arslanagić, Pavle Subotić, Jorge A. Pérez

Abstract: Static analyses based on typestates are important in certifying correctness of code contracts. Such analyses rely on Deterministic Finite Automata (DFAs) to specify properties of an object. We target the analysis of contracts in low-latency environments, where many useful contracts are impractical to codify as DFAs and/or the size of their associated DFAs leads to sub-par performance. To address t… ▽ More Static analyses based on typestates are important in certifying correctness of code contracts. Such analyses rely on Deterministic Finite Automata (DFAs) to specify properties of an object. We target the analysis of contracts in low-latency environments, where many useful contracts are impractical to codify as DFAs and/or the size of their associated DFAs leads to sub-par performance. To address this bottleneck, we present a lightweight typestate analyzer, based on an expressive specification language that can succinctly specify code contracts. By implementing it in the static analyzer Infer, we demonstrate considerable performance and usability benefits when compared to existing techniques. A central insight is to rely on a sub-class of DFAs with efficient bit-vector operations. △ Less

Submitted 18 July, 2022; v1 submitted 25 January, 2022; originally announced January 2022.

Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes (Extended Version)

Authors: Joseph W. N. Paulus, Daniele Nantes-Sobrinho, Jorge A. Pérez

Abstract: Type-preserving translations are effective rigorous tools in the study of core programming calculi. In this paper, we develop a new typed translation that connects sequential and concurrent calculi; it is governed by type systems that control resource consumption. Our main contribution is the source language, a new resource $λ$-calculus with non-determinism and failures, dubbed \ulamf. In \ulamf,… ▽ More Type-preserving translations are effective rigorous tools in the study of core programming calculi. In this paper, we develop a new typed translation that connects sequential and concurrent calculi; it is governed by type systems that control resource consumption. Our main contribution is the source language, a new resource $λ$-calculus with non-determinism and failures, dubbed \ulamf. In \ulamf, resources are split into linear and unrestricted; failures are explicit and arise from this distinction. We define a type system based on intersection types to control resources and fail-prone computation. The target language is \spi, an existing session-typed $π$-calculus that results from a Curry-Howard correspondence between linear logic and session types. Our typed translation subsumes our prior work; interestingly, it treats unrestricted resources in \lamrfailunres as client-server session behaviours in \spi. △ Less

Submitted 30 May, 2022; v1 submitted 2 December, 2021; originally announced December 2021.

Comments: 24 pages, plus appendices. Extended version of a paper in the Post-proceedings of TYPES 2021. arXiv admin note: text overlap with arXiv:2104.14759

Asynchronous Session-Based Concurrency: Deadlock-freedom in Cyclic Process Networks

Authors: Bas van den Heuvel, Jorge A. Pérez

Abstract: We tackle the challenge of ensuring the deadlock-freedom property for message-passing processes that communicate asynchronously in cyclic process networks. Our contributions are twofold. First, we present Asynchronous Priority-based Classical Processes (APCP), a session-typed process framework that supports asynchronous communication, delegation, and recursion in cyclic process networks. Building… ▽ More We tackle the challenge of ensuring the deadlock-freedom property for message-passing processes that communicate asynchronously in cyclic process networks. Our contributions are twofold. First, we present Asynchronous Priority-based Classical Processes (APCP), a session-typed process framework that supports asynchronous communication, delegation, and recursion in cyclic process networks. Building upon the Curry-Howard correspondences between linear logic and session types, we establish essential meta-theoretical results for APCP, most notably deadlock freedom. Second, we present a new concurrent $λ$-calculus with asynchronous session types, dubbed LASTn. We illustrate LASTn by example and establish its meta-theoretical results; in particular, we show how to soundly transfer the deadlock-freedom guarantee from APCP. To this end, we develop a translation of terms in LASTn into processes in APCP that satisfies a strong formulation of operational correspondence. △ Less

Submitted 4 July, 2024; v1 submitted 25 November, 2021; originally announced November 2021.

Comments: Extended version of arXiv:2110.00146, doi:10.4204/EPTCS.347.3 and arXiv:2209.06820, doi:10.4204/EPTCS.368.5

Deadlock Freedom for Asynchronous and Cyclic Process Networks

Authors: Bas van den Heuvel, Jorge A. Pérez

Abstract: This paper considers the challenging problem of establishing deadlock freedom for message-passing processes using behavioral type systems. In particular, we consider the case of processes that implement session types by communicating asynchronously in cyclic process networks. We present APCP, a typed process framework for deadlock freedom which supports asynchronous communication, delegation, recu… ▽ More This paper considers the challenging problem of establishing deadlock freedom for message-passing processes using behavioral type systems. In particular, we consider the case of processes that implement session types by communicating asynchronously in cyclic process networks. We present APCP, a typed process framework for deadlock freedom which supports asynchronous communication, delegation, recursion, and a general form of process composition that enables specifying cyclic process networks. We discuss the main decisions involved in the design of APCP and illustrate its expressiveness and flexibility using several examples. △ Less

Submitted 30 September, 2021; originally announced October 2021.

Comments: In Proceedings ICE 2021, arXiv:2109.14908. arXiv admin note: text overlap with arXiv:2101.09038

Journal ref: EPTCS 347, 2021, pp. 38-56

Minimal Session Types for the $π$-calculus (Extended Version)

Authors: Alen Arslanagic, Jorge A. Pérez, Anda-Amelia Palamariuc

Abstract: Session types are a discipline for the static verification of message-passing programs. A session type specifies a channel's protocol as sequences of exchanges. It is most relevant to investigate session-based concurrency by identifying the essential notions that enable program specification and verification. Following that perspective, prior work identified minimal session types (MSTs), a sub-cla… ▽ More Session types are a discipline for the static verification of message-passing programs. A session type specifies a channel's protocol as sequences of exchanges. It is most relevant to investigate session-based concurrency by identifying the essential notions that enable program specification and verification. Following that perspective, prior work identified minimal session types (MSTs), a sub-class of session types without the sequentiality construct, which specifies the structure of communication actions. This formulation of session types led to establish a minimality result: every process typable with standard session types can be compiled down to a process typable using MSTs, which mimics sequentiality in types via additional process synchronizations. Such a minimality result is significant because it justifies session types in terms of themselves, without resorting to external notions; it was proven for a higher-order session pi-calculus, in which values are abstractions (functions from names to processes). In this paper, we study MSTs and their associated minimality result but now for the session pi-calculus, the (first-order) language in which values are names and for which session types have been more widely studied. We first show that this new minimality result can be obtained by composing known results. Then, we develop optimizations of this new minimality result and prove that the associated transformation into processes with MSTs satisfies dynamic correctness. △ Less

Submitted 22 January, 2024; v1 submitted 22 July, 2021; originally announced July 2021.

Comments: Extended version of a PPDP 2021 paper

Non-Deterministic Functions as Non-Deterministic Processes (Extended Version)

Authors: Joseph W. N. Paulus, Daniele Nantes-Sobrinho, Jorge A. Pérez

Abstract: We study encodings of the lambda-calculus into the pi-calculus in the unexplored case of calculi with non-determinism and failures. On the sequential side, we consider lambdafail, a new non-deterministic calculus in which intersection types control resources (terms); on the concurrent side, we consider spi, a pi-calculus in which non-determinism and failure rest upon a Curry-Howard correspondence… ▽ More We study encodings of the lambda-calculus into the pi-calculus in the unexplored case of calculi with non-determinism and failures. On the sequential side, we consider lambdafail, a new non-deterministic calculus in which intersection types control resources (terms); on the concurrent side, we consider spi, a pi-calculus in which non-determinism and failure rest upon a Curry-Howard correspondence between linear logic and session types. We present a typed encoding of lambdafail into spi and establish its correctness. Our encoding precisely explains the interplay of non-deterministic and fail-prone evaluation in lambdafail via typed processes in spi. In particular, it shows how failures in sequential evaluation (absence/excess of resources) can be neatly codified as interaction protocols. △ Less

Submitted 9 October, 2023; v1 submitted 30 April, 2021; originally announced April 2021.

Journal ref: Logical Methods in Computer Science, Volume 19, Issue 4 (October 10, 2023) lmcs:8812

A Decentralized Analysis of Multiparty Protocols

Authors: Bas van den Heuvel, Jorge A. Pérez

Abstract: Protocols provide the unifying glue in concurrent and distributed software today; verifying that message-passing programs conform to such governing protocols is important but difficult. Static approaches based on multiparty session types (MPST) use protocols as types to avoid protocol violations and deadlocks in programs. An elusive problem for MPST is to ensure both protocol conformance and deadl… ▽ More Protocols provide the unifying glue in concurrent and distributed software today; verifying that message-passing programs conform to such governing protocols is important but difficult. Static approaches based on multiparty session types (MPST) use protocols as types to avoid protocol violations and deadlocks in programs. An elusive problem for MPST is to ensure both protocol conformance and deadlock freedom for implementations with interleaved and delegated protocols. We propose a decentralized analysis of multiparty protocols, specified as global types and implemented as interacting processes in an asynchronous $π$-calculus. Our solution rests upon two novel notions: router processes and relative types. While router processes use the global type to enable the composition of participant implementations in arbitrary process networks, relative types extract from the global type the intended interactions and dependencies between pairs of participants. In our analysis, processes are typed using APCP, a type system that ensures protocol conformance and deadlock freedom with respect to binary protocols, developed in prior work. Our decentralized, router-based analysis enables the sound and complete transference of protocol conformance and deadlock freedom from APCP to multiparty protocols. △ Less

Submitted 23 May, 2022; v1 submitted 22 January, 2021; originally announced January 2021.

Comments: extended proofs following anonymous reviews

Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols

Authors: Alex C. Keizer, Henning Basold, Jorge A. Pérez

Abstract: Compositional methods are central to the development and verification of software systems. They allow to break down large systems into smaller components, while enabling reasoning about the behaviour of the composed system. For concurrent and communicating systems, compositional techniques based on behavioural type systems have received much attention. By abstracting communication protocols as typ… ▽ More Compositional methods are central to the development and verification of software systems. They allow to break down large systems into smaller components, while enabling reasoning about the behaviour of the composed system. For concurrent and communicating systems, compositional techniques based on behavioural type systems have received much attention. By abstracting communication protocols as types, these type systems can statically check that programs interact with channels according to a certain protocol, whether the intended messages are exchanged in a certain order. In this paper, we put on our coalgebraic spectacles to investigate session types, a widely studied class of behavioural type systems. We provide a syntax-free description of session-based concurrency as states of coalgebras. As a result, we rediscover type equivalence, duality, and subty** relations in terms of canonical coinductive presentations. In turn, this coinductive presentation makes it possible to elegantly derive a decidable type system with subty** for $π$-calculus processes, in which the states of a coalgebra will serve as channel protocols. Going full circle, we exhibit a coalgebra structure on an existing session type system, and show that the relations and type system resulting from our coalgebraic perspective agree with the existing ones. △ Less

Submitted 11 November, 2020; originally announced November 2020.

Comments: 36 pages, submitted

Session Type Systems based on Linear Logic: Classical versus Intuitionistic

Authors: Bas van den Heuvel, Jorge A. Pérez

Abstract: Session type systems have been given logical foundations via Curry-Howard correspondences based on both intuitionistic and classical linear logic. The type systems derived from the two logics enforce communication correctness on the same class of pi-calculus processes, but they are significantly different. Caires, Pfenning and Toninho informally observed that, unlike the classical type system, the… ▽ More Session type systems have been given logical foundations via Curry-Howard correspondences based on both intuitionistic and classical linear logic. The type systems derived from the two logics enforce communication correctness on the same class of pi-calculus processes, but they are significantly different. Caires, Pfenning and Toninho informally observed that, unlike the classical type system, the intuitionistic type system enforces locality for shared channels, i.e. received channels cannot be used for replicated input. In this paper, we revisit this observation from a formal standpoint. We develop United Linear Logic (ULL), a logic encompassing both classical and intuitionistic linear logic. Then, following the Curry-Howard correspondences for session types, we define piULL, a session type system for the pi-calculus based on ULL. Using piULL we can formally assess the difference between the intuitionistic and classical type systems, and justify the role of locality and symmetry therein. △ Less

Submitted 2 April, 2020; originally announced April 2020.

Comments: In Proceedings PLACES 2020, arXiv:2004.01062

Journal ref: EPTCS 314, 2020, pp. 1-11

Proceedings Combined 26th International Workshop on Expressiveness in Concurrency and 16th Workshop on Structural Operational Semantics

Authors: Jorge A. Pérez, Jurriaan Rot

Abstract: This volume contains the proceedings of EXPRESS/SOS 2019: the Combined 26th International Workshop on Expressiveness in Concurrency and the 16th Workshop on Structural Operational Semantics, which was held on August 26, 2019, in Amsterdam (The Netherlands), as an affiliated workshop of CONCUR 2019, the 30th International Conference on Concurrency Theory. The EXPRESS/SOS workshop series aims at… ▽ More This volume contains the proceedings of EXPRESS/SOS 2019: the Combined 26th International Workshop on Expressiveness in Concurrency and the 16th Workshop on Structural Operational Semantics, which was held on August 26, 2019, in Amsterdam (The Netherlands), as an affiliated workshop of CONCUR 2019, the 30th International Conference on Concurrency Theory. The EXPRESS/SOS workshop series aims at bringing together researchers interested in the formal semantics of systems and programming concepts, and in the expressiveness of computational models. △ Less

Submitted 22 August, 2019; originally announced August 2019.

Journal ref: EPTCS 300, 2019

Domain-Aware Session Types (Extended Version)

Authors: Luís Caires, Jorge A. Pérez, Frank Pfenning, Bernardo Toninho

Abstract: We develop a generalization of existing Curry-Howard interpretations of (binary) session types by relying on an extension of linear logic with features from hybrid logic, in particular modal worlds that indicate domains. These worlds govern domain migration, subject to a parametric accessibility relation familiar from the Kripke semantics of modal logic. The result is an expressive new typed proce… ▽ More We develop a generalization of existing Curry-Howard interpretations of (binary) session types by relying on an extension of linear logic with features from hybrid logic, in particular modal worlds that indicate domains. These worlds govern domain migration, subject to a parametric accessibility relation familiar from the Kripke semantics of modal logic. The result is an expressive new typed process framework for domain-aware, message-passing concurrency. Its logical foundations ensure that well-typed processes enjoy session fidelity, global progress, and termination. Ty** also ensures that processes only communicate with accessible domains and so respect the accessibility relation. Remarkably, our domain-aware framework can specify scenarios in which domain information is available only at runtime; flexible accessibility relations can be cleanly defined and statically enforced. As a specific application, we introduce domain-aware multiparty session types, in which global protocols can express arbitrarily nested sub-protocols via domain migration. We develop a precise analysis of these multiparty protocols by reduction to our binary domain-aware framework: complex domain-aware protocols can be reasoned about at the right level of abstraction, ensuring also the principled transfer of key correctness properties from the binary to the multiparty setting. △ Less

Submitted 2 July, 2019; originally announced July 2019.

Comments: Extended version of a CONCUR 2019 paper

ACM Class: D.3.1; F.3.2

Minimal Session Types (Extended Version)

Authors: Alen Arslanagić, Jorge A. Pérez, Erik Voogd

Abstract: Session types are a type-based approach to the verification of message-passing programs. They have been much studied as type systems for the pi-calculus and for languages such as Java. A session type specifies what and when should be exchanged through a channel. Central to session-typed languages are constructs in types and processes that specify sequencing in protocols. Here we study minimal sess… ▽ More Session types are a type-based approach to the verification of message-passing programs. They have been much studied as type systems for the pi-calculus and for languages such as Java. A session type specifies what and when should be exchanged through a channel. Central to session-typed languages are constructs in types and processes that specify sequencing in protocols. Here we study minimal session types, session types without sequencing. This is arguably the simplest form of session types. By relying on a core process calculus with sessions and higher-order concurrency (abstraction passing), we prove that every process typable with usual (non minimal) session types can be compiled down into a process typed with minimal session types. This means that having sequencing constructs in both processes and session types is redundant; only sequentiality in processes is indispensable, as it can precisely codify sequentiality in types. Our developments draw inspiration from work by Parrow on behavior-preserving decompositions of untyped processes. By casting Parrow's results in the realm of typed processes, our results reveal a conceptually simple formulation of session types and a principled avenue to the integration of session types into languages without sequencing in types. △ Less

Submitted 12 June, 2019; v1 submitted 10 June, 2019; originally announced June 2019.

Comments: Extended version of an ECOOP 2019 paper

Development of an adjustable Kirkpatrick-Baez microscope for laser driven x-ray sources at CLPU

Authors: G. Zeraouli, G. gatti, A. Longman, J. A. Perez, D. Arana, D. Batani, L. Volpe, L. Roso, R. Fedosejevs

Abstract: A promising prototype of a highly adjustable Kirkpatrick-Baez (KB) microscope has been designed, built and tested in a number of laser driven x-ray experiments using the high power (200TW) VEGA-2 laser system of the Spanish Centre for Pulsed Lasers (CLPU). The presented KB version consists of two, perpendicularly mounted, 500μm thick Silicon wafers, coated with a few tens of nm layer of Platinum u… ▽ More A promising prototype of a highly adjustable Kirkpatrick-Baez (KB) microscope has been designed, built and tested in a number of laser driven x-ray experiments using the high power (200TW) VEGA-2 laser system of the Spanish Centre for Pulsed Lasers (CLPU). The presented KB version consists of two, perpendicularly mounted, 500μm thick Silicon wafers, coated with a few tens of nm layer of Platinum unlike the conventional, coated, millimetre thick glass substrates, affording more bending flexibility and large adjustment range. According to simulations, and based on total external reflection, this KB offers a broad-band multi-keV reflection spectra, allowing more spectral tunablity than conventional Bragg crystals. In addition to be vacuum compatible, the prototype is characterised by a relatively small size (21cm x 31cm x 27cm) and permits remote control and modification of both the radius of curvature (down to 10m) and the grazing incidence angle (up to 60mrad). A few examples of focusing performance tests, limitations and experimental campaign results are discussed. △ Less

Submitted 12 November, 2018; originally announced November 2018.

Comparing Type Systems for Deadlock Freedom

Authors: Ornela Dardha, Jorge A. Pérez

Abstract: Message-passing software systems exhibit non-trivial forms of concurrency and distribution; they are expected to follow intended protocols among communicating services, but also to never "get stuck". This intuitive requirement has been expressed by liveness properties such as progress or (dead)lock freedom and various type systems ensure these properties for concurrent processes. Unfortunately, ve… ▽ More Message-passing software systems exhibit non-trivial forms of concurrency and distribution; they are expected to follow intended protocols among communicating services, but also to never "get stuck". This intuitive requirement has been expressed by liveness properties such as progress or (dead)lock freedom and various type systems ensure these properties for concurrent processes. Unfortunately, very little is known about the precise relationship between these type systems and the classes of typed processes they induce. This paper puts forward the first comparative study of different type systems for message-passing processes that guarantee deadlock freedom. We compare two classes of deadlock-free typed processes, here denoted L and K. The class L stands out for its canonicity: it results from Curry-Howard interpretations of linear logic propositions as session types. The class K, obtained by encoding session types into Kobayashi's linear types with usages, includes processes not typable in other type systems. We show that L is strictly included in K, and identify the precise conditions under which they coincide. We also provide two type-preserving translations of processes in K into processes in L. △ Less

Submitted 6 September, 2021; v1 submitted 1 October, 2018; originally announced October 2018.

Comments: 39 pages, plus appendices. Extended and revised version of an EXPRESS/SOS'15 paper (https://doi.org/10.4204/EPTCS.190.1)

ACM Class: D.3.1; F.3.2

Proceedings Combined 25th International Workshop on Expressiveness in Concurrency and 15th Workshop on Structural Operational Semantics

Authors: Jorge A. Pérez, Simone Tini

Abstract: This volume contains the proceedings of the Combined 25th International Workshop on Expressiveness in Concurrency and the 15th Workshop on Structural Operational Semantics (EXPRESS/SOS 2018), which was held on September 3, 2018, in Bei**g, China, as an affiliated workshop of CONCUR 2018, the 29th International Conference on Concurrency Theory. The EXPRESS workshops aim at bringing together resear… ▽ More This volume contains the proceedings of the Combined 25th International Workshop on Expressiveness in Concurrency and the 15th Workshop on Structural Operational Semantics (EXPRESS/SOS 2018), which was held on September 3, 2018, in Bei**g, China, as an affiliated workshop of CONCUR 2018, the 29th International Conference on Concurrency Theory. The EXPRESS workshops aim at bringing together researchers interested in the expressiveness of various formal systems and semantic notions, particularly in the field of concurrency. Their focus has traditionally been on the comparison between programming concepts (such as concurrent, functional, imperative, logic and object-oriented programming) and between mathematical models of computation (such as process algebras, Petri nets, event structures, modal logics, and rewrite systems) on the basis of their relative expressive power. The SOS workshops aim at being a forum for researchers, students and practitioners interested in new developments, and directions for future investigation, in the field of structural operational semantics. One of the specific goals of the SOS workshop series is to establish synergies between the concurrency and programming language communities working on the theory and practice of SOS. Since 2012, the EXPRESS and SOS communities have organized an annual combined EXPRESS/SOS workshop on the expressiveness of mathematical models of computation and the formal semantics of systems and programming concepts. △ Less

Submitted 24 August, 2018; originally announced August 2018.

Journal ref: EPTCS 276, 2018

Minimum Labelling bi-Connectivity

Authors: Jose' Andres Moreno Perez, Sergio Consoli

Abstract: A labelled, undirected graph is a graph whose edges have assigned labels, from a specific set. Given a labelled, undirected graph, the well-known minimum labelling spanning tree problem is aimed at finding the spanning tree of the graph with the minimum set of labels. This combinatorial problem, which is NP-hard, can be also formulated as to give the minimum number of labels that provide single co… ▽ More A labelled, undirected graph is a graph whose edges have assigned labels, from a specific set. Given a labelled, undirected graph, the well-known minimum labelling spanning tree problem is aimed at finding the spanning tree of the graph with the minimum set of labels. This combinatorial problem, which is NP-hard, can be also formulated as to give the minimum number of labels that provide single connectivity among all the vertices of the graph. Here we consider instead the problem of finding the minimum set of labels that provide bi-connectivity among all the vertices of the graph. A graph is bi-connected if there are at least two disjoint paths joining every pair of vertices. We consider both bi-connectivity concept: the edge bi-connectivity where these paths cannot have a common edge and the vertex bi-connectivity where the paths cannot have a common vertex. We describe our preliminary investigation on the problem and provide the details on the solution approaches for the problem under current development. △ Less

Submitted 2 July, 2018; originally announced July 2018.

Comments: 3 pages, MIC/MAEB 2017, Barcelona, Spain

Journal ref: Proceedings of MIC 2017: The XII Metaheuristics International Conference, Barcelona, Spain, pages 241-243

Collatz Conjecture: Is It False?

Authors: Juan A. Perez

Abstract: For a long time, Collatz Conjecture has been assumed to be true, although a formal proof has eluded all efforts to date. In this article, evidence is presented that suggests such an assumption is incorrect. By analysing the stop** times of various Collatz sequences, a pattern emerges that indicates the existence of non-empty sets of integers with stop** times greater than any given integer. Th… ▽ More For a long time, Collatz Conjecture has been assumed to be true, although a formal proof has eluded all efforts to date. In this article, evidence is presented that suggests such an assumption is incorrect. By analysing the stop** times of various Collatz sequences, a pattern emerges that indicates the existence of non-empty sets of integers with stop** times greater than any given integer. This implies the existence of an infinite set of integers with non-finite stop** times, thus indicating the conjecture is false. Furthermore, a simple algorithm is constructed that finds integers with ever-greater stop** times. Such an algorithm does not halt, further supporting the conclusion that the conjecture is false. △ Less

Submitted 28 August, 2017; v1 submitted 15 August, 2017; originally announced August 2017.

Comments: 14 pages, 4 figures and 6 tables Correction of typographic error in eq.(4.1), page 12

MSC Class: 11B83 (Primary); 11B37; 68Q99 (Secondary)

Causal Consistency for Reversible Multiparty Protocols

Authors: Claudio Antares Mezzina, Jorge A. Pérez

Abstract: In programming models with a reversible semantics, computational steps can be undone. This paper addresses the integration of reversible semantics into process languages for communication-centric systems equipped with behavioral types. In prior work, we introduced a monitors-as-memories approach to seamlessly integrate reversible semantics into a process model in which concurrency is governed by s… ▽ More In programming models with a reversible semantics, computational steps can be undone. This paper addresses the integration of reversible semantics into process languages for communication-centric systems equipped with behavioral types. In prior work, we introduced a monitors-as-memories approach to seamlessly integrate reversible semantics into a process model in which concurrency is governed by session types (a class of behavioral types), covering binary (two-party) protocols with synchronous communication. The applicability and expressiveness of the binary setting, however, is limited. Here we extend our approach, and use it to define reversible semantics for an expressive process model that accounts for multiparty (n-party) protocols, asynchronous communication, decoupled rollbacks, and abstraction passing. As main result, we prove that our reversible semantics for multiparty protocols is causally-consistent. A key technical ingredient in our developments is an alternative reversible semantics with atomic rollbacks, which is conceptually simple and is shown to characterize decoupled rollbacks. △ Less

Submitted 30 September, 2021; v1 submitted 17 March, 2017; originally announced March 2017.

ACM Class: D.3.1; F.3.2

Journal ref: Logical Methods in Computer Science, Volume 17, Issue 4 (October 1, 2021) lmcs:6997

Charge-induced force-noise on free-falling test masses: results from LISA Pathfinder

Authors: M. Armano, H. Audley, G. Auger, J. T. Baird, P. Binetruy, M. Born, D. Bortoluzzi, N. Brandt, A. Bursi, M. Caleno, A. Cavalleri, A. Cesarini, M. Cruise, K. Danzmann, M. de Deus Silva, I. Diepholz, R. Dolesi, N. Dunbar, L. Ferraioli, V. Ferroni, E. D. Fitzsimons, R. Flatscher, M. Freschi, J. Gallegos, C. García Marirrodriga , et al. (69 additional authors not shown)

Abstract: We report on electrostatic measurements made on board the European Space Agency mission LISA Pathfinder. Detailed measurements of the charge-induced electrostatic forces exerted on free-falling test masses (TMs) inside the capacitive gravitational reference sensor are the first made in a relevant environment for a space-based gravitational wave detector. Employing a combination of charge control a… ▽ More We report on electrostatic measurements made on board the European Space Agency mission LISA Pathfinder. Detailed measurements of the charge-induced electrostatic forces exerted on free-falling test masses (TMs) inside the capacitive gravitational reference sensor are the first made in a relevant environment for a space-based gravitational wave detector. Employing a combination of charge control and electric-field compensation, we show that the level of charge-induced acceleration noise on a single TM can be maintained at a level close to 1.0 fm/s^2/sqrt(Hz) across the 0.1-100 mHz frequency band that is crucial to an observatory such as LISA. Using dedicated measurements that detect these effects in the differential acceleration between the two test masses, we resolve the stochastic nature of the TM charge build up due to interplanetary cosmic rays and the TM charge-to-force coupling through stray electric fields in the sensor. All our measurements are in good agreement with predictions based on a relatively simple electrostatic model of the LISA Pathfinder instrument. △ Less

Submitted 15 February, 2017; originally announced February 2017.

Comments: 9 Pages, 3 figures

Journal ref: Phys. Rev. Lett. 118, 171101 (2017)

Reversible Sessions Using Monitors

Authors: Claudio A. Mezzina, Jorge A. Pérez

Abstract: Much research has studied foundations for correct and reliable communication-centric systems. A salient approach to correctness uses session types to enforce structured communications; a recent approach to reliability uses reversible actions as a way of reacting to unanticipated events or failures. This note develops a simple observation: the machinery required to define asynchronous semantics and… ▽ More Much research has studied foundations for correct and reliable communication-centric systems. A salient approach to correctness uses session types to enforce structured communications; a recent approach to reliability uses reversible actions as a way of reacting to unanticipated events or failures. This note develops a simple observation: the machinery required to define asynchronous semantics and monitoring can also support reversible protocols. We propose a process framework of session communication in which monitors support reversibility. A key novelty in our approach are session types with present and past, which allow us to streamline the semantics of reversible actions. △ Less

Submitted 19 June, 2016; originally announced June 2016.

Comments: In Proceedings PLACES 2016, arXiv:1606.05403

Journal ref: EPTCS 211, 2016, pp. 56-64

Flexible Multibody System Linear Modeling for Control using Component Modes Synthesis and Double-Port Approach

Authors: Jose Alvaro Perez, Daniel Alazard, Thomas Loquen, Christelle Pittet, Christelle Cumer

Abstract: The main objective of this study is to propose a methodology to build a parametric linear model of Flexible Multibody Systems for control design. This approach uses a combined Finite Element - State Space Approach based on component modes synthesis and double-port approach. The proposed scheme offers the advantage of automatic assembly of substructures, preserving the elastic dynamical behavior of… ▽ More The main objective of this study is to propose a methodology to build a parametric linear model of Flexible Multibody Systems for control design. This approach uses a combined Finite Element - State Space Approach based on component modes synthesis and double-port approach. The proposed scheme offers the advantage of automatic assembly of substructures, preserving the elastic dynamical behavior of the whole system. Substructures are connected following the double-port approach; i.e, through the transfer of accelerations and loads at the connection points, which take into account the dynamic coupling among them. In addition, parametric variations can be included in the model for accomplishing integrated control/structure design purposes. The method can be applied to combinations of chain-like or/and star-like flexible systems, and it is validated through its comparison with the assumed modes method for the case of a rotatory spacecraft. △ Less

Submitted 10 August, 2016; v1 submitted 1 April, 2016; originally announced April 2016.

Comments: This paper has been withdrawn by the author due to significant changes in the article's content

Integrated Control/Structure Design of a Large Space Structure using Structured $\mathcal{H}_\infty$ Control

Authors: Jose Alvaro Perez, Christelle Pittet, Daniel Alazard, Thomas Loquen

Abstract: This study presents the integrated control/structure design of a Large Flexible Structure, the Extra Long Mast Observatory (ELMO). The integrated design is performed using structured $\mathcal{H}_\infty$ control tools, develo** the Two-Input Two-Output Port (TITOP) model of the flexible multi-body structure and imposing integrated design specifications as $\mathcal{H}_\infty$ constraints. The in… ▽ More This study presents the integrated control/structure design of a Large Flexible Structure, the Extra Long Mast Observatory (ELMO). The integrated design is performed using structured $\mathcal{H}_\infty$ control tools, develo** the Two-Input Two-Output Port (TITOP) model of the flexible multi-body structure and imposing integrated design specifications as $\mathcal{H}_\infty$ constraints. The integrated control/structure design for ELMO consists of optimizing simultaneously its payload mass and control system for low-frequency perturbation rejection respecting bandwidth requirements. △ Less

Submitted 1 April, 2016; originally announced April 2016.

Comments: submitted to IFAC ACA 2016

Proceedings of the Eleventh International Workshop on Developments in Computational Models

Authors: César A. Muñoz, Jorge A. Pérez

Abstract: This volume contains the proceedings of DCM 2015, the 11th International Workshop on Developments in Computational Models held on October 28, 2015 in Cali, Colombia. DCM 2015 was organized as a one-day satellite event of the 12th International Colloquium on Theoretical Aspects of Computing (ICTAC 2015). Several new models of computation have emerged in the last few years, and many developments o… ▽ More This volume contains the proceedings of DCM 2015, the 11th International Workshop on Developments in Computational Models held on October 28, 2015 in Cali, Colombia. DCM 2015 was organized as a one-day satellite event of the 12th International Colloquium on Theoretical Aspects of Computing (ICTAC 2015). Several new models of computation have emerged in the last few years, and many developments of traditional computational models have been proposed with the aim of taking into account the new demands of computer systems users and the new capabilities of computation engines. A new computational model, or a new feature in a traditional one, usually is reflected in a new family of programming languages, and new paradigms of software development. The aim of the DCM workshop series is to bring together researchers who are currently develo** new computational models or new features for traditional computational models, in order to foster their interaction, to provide a forum for presenting new ideas and work in progress, and to enable newcomers to learn about current activities in this area. Topics of interest include all abstract models of computation and their applications to the development of programming languages and systems. △ Less

Submitted 1 March, 2016; originally announced March 2016.

Journal ref: EPTCS 204, 2016

Linear Modeling of a Flexible Substructure Actuated through Piezoelectric Components for Use in Integrated Control/Structure Design

Authors: Jose Alvaro Perez, Thomas Loquen, Daniel Alazard, Christelle Pittet

Abstract: This study presents a generic TITOP (Two-Input Two-Output Port) model of a substructure actuated with embedded piezoelectric materials as actuators (PEAs), previously modeled with the FE technique. This allows intuitive assembly of actuated flexible substructures in large flexible multi-body systems. The modeling technique is applied to an illustrative example of a flexible beam with bonded piezoe… ▽ More This study presents a generic TITOP (Two-Input Two-Output Port) model of a substructure actuated with embedded piezoelectric materials as actuators (PEAs), previously modeled with the FE technique. This allows intuitive assembly of actuated flexible substructures in large flexible multi-body systems. The modeling technique is applied to an illustrative example of a flexible beam with bonded piezoelectric strip and vibration attenuation of a chain of flexible beams. △ Less

Submitted 24 February, 2016; originally announced February 2016.

Comments: submitted to IFAC ACA 2016

A Typed Model for Dynamic Authorizations

Authors: Silvia Ghilezan, Svetlana Jakšić, Jovanka Pantović, Jorge A. Pérez, Hugo Torres Vieira

Abstract: Security requirements in distributed software systems are inherently dynamic. In the case of authorization policies, resources are meant to be accessed only by authorized parties, but the authorization to access a resource may be dynamically granted/yielded. We describe ongoing work on a model for specifying communication and dynamic authorization handling. We build upon the pi-calculus so as to e… ▽ More Security requirements in distributed software systems are inherently dynamic. In the case of authorization policies, resources are meant to be accessed only by authorized parties, but the authorization to access a resource may be dynamically granted/yielded. We describe ongoing work on a model for specifying communication and dynamic authorization handling. We build upon the pi-calculus so as to enrich communication-based systems with authorization specification and delegation; here authorizations regard channel usage and delegation refers to the act of yielding an authorization to another party. Our model includes: (i) a novel sco** construct for authorization, which allows to specify authorization boundaries, and (ii) communication primitives for authorizations, which allow to pass around authorizations to act on a given channel. An authorization error may consist in, e.g., performing an action along a name which is not under an appropriate authorization scope. We introduce a ty** discipline that ensures that processes never reduce to authorization errors, even when authorizations are dynamically delegated. △ Less

Submitted 10 February, 2016; originally announced February 2016.

Comments: In Proceedings PLACES 2015, arXiv:1602.03254

Journal ref: EPTCS 203, 2016, pp. 73-84

Combining behavioural types with security analysis

Authors: Massimo Bartoletti, Ilaria Castellani, Pierre-Malo Deniélou, Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Jovanka Pantovic, Jorge A. Pérez, Peter Thiemann, Bernardo Toninho, Hugo Torres Vieira

Abstract: Today's software systems are highly distributed and interconnected, and they increasingly rely on communication to achieve their goals; due to their societal importance, security and trustworthiness are crucial aspects for the correctness of these systems. Behavioural types, which extend data types by describing also the structured behaviour of programs, are a widely studied approach to the enforc… ▽ More Today's software systems are highly distributed and interconnected, and they increasingly rely on communication to achieve their goals; due to their societal importance, security and trustworthiness are crucial aspects for the correctness of these systems. Behavioural types, which extend data types by describing also the structured behaviour of programs, are a widely studied approach to the enforcement of correctness properties in communicating systems. This paper offers a unified overview of proposals based on behavioural types which are aimed at the analysis of security properties. △ Less

Submitted 8 October, 2015; originally announced October 2015.

Journal ref: Journal of Logical and Algebraic Methods in Programming, Elsevier, 2015, pp.18

An intelligent extension of Variable Neighbourhood Search for labelling graph problems

Authors: Sergio Consoli, Josè Andrès Moreno Pèrez

Abstract: In this paper we describe an extension of the Variable Neighbourhood Search (VNS) which integrates the basic VNS with other complementary approaches from machine learning, statistics and experimental algorithmic, in order to produce high-quality performance and to completely automate the resulting optimization strategy. The resulting intelligent VNS has been successfully applied to a couple of opt… ▽ More In this paper we describe an extension of the Variable Neighbourhood Search (VNS) which integrates the basic VNS with other complementary approaches from machine learning, statistics and experimental algorithmic, in order to produce high-quality performance and to completely automate the resulting optimization strategy. The resulting intelligent VNS has been successfully applied to a couple of optimization problems where the solution space consists of the subsets of a finite reference set. These problems are the labelled spanning tree and forest problems that are formulated on an undirected labelled graph; a graph where each edge has a label in a finite set of labels L. The problems consist on selecting the subset of labels such that the subgraph generated by these labels has an optimal spanning tree or forest, respectively. These problems have several applications in the real-world, where one aims to ensure connectivity by means of homogeneous connections. △ Less

Submitted 27 September, 2015; originally announced September 2015.

Comments: MIC 2015: The XI Metaheuristics International Conference, 3 pages, Agadir, June 7-10, 2015

On Compensation Primitives as Adaptable Processes

Authors: Jovana Dedeić, Jovanka Pantović, Jorge A. Pérez

Abstract: We compare mechanisms for compensation handling and dynamic update in calculi for concurrency. These mechanisms are increasingly relevant in the specification of reliable communicating systems. Compensations and updates are intuitively similar: both specify how the behavior of a concurrent system changes at runtime in response to an exceptional event. However, calculi with compensations and update… ▽ More We compare mechanisms for compensation handling and dynamic update in calculi for concurrency. These mechanisms are increasingly relevant in the specification of reliable communicating systems. Compensations and updates are intuitively similar: both specify how the behavior of a concurrent system changes at runtime in response to an exceptional event. However, calculi with compensations and updates are technically quite different. We investigate the relative expressiveness of these calculi: we develop encodings of core process languages with compensations into a calculus of adaptable processes developed in prior work. Our encodings shed light on the (intricate) semantics of compensation handling and its key constructs. They also enable the transference of existing verification and reasoning techniques for adaptable processes to core languages with compensation handling. △ Less

Submitted 26 August, 2015; originally announced August 2015.

Comments: In Proceedings EXPRESS/SOS 2015, arXiv:1508.06347

ACM Class: F.3.2

Journal ref: EPTCS 190, 2015, pp. 16-30

Comparing Deadlock-Free Session Typed Processes

Authors: Ornela Dardha, Jorge A. Pérez

Abstract: Besides respecting prescribed protocols, communication-centric systems should never "get stuck". This requirement has been expressed by liveness properties such as progress or (dead)lock freedom. Several ty** disciplines that ensure these properties for mobile processes have been proposed. Unfortunately, very little is known about the precise relationship between these disciplines--and the class… ▽ More Besides respecting prescribed protocols, communication-centric systems should never "get stuck". This requirement has been expressed by liveness properties such as progress or (dead)lock freedom. Several ty** disciplines that ensure these properties for mobile processes have been proposed. Unfortunately, very little is known about the precise relationship between these disciplines--and the classes of typed processes they induce. In this paper, we compare L and K, two classes of deadlock-free, session typed concurrent processes. The class L stands out for its canonicity: it results naturally from interpretations of linear logic propositions as session types. The class K, obtained by encoding session types into Kobayashi's usage types, includes processes not typable in other type systems. We show that L is strictly included in K. We also identify the precise condition under which L and K coincide. One key observation is that the degree of sharing between parallel processes determines a new expressiveness hierarchy for typed processes. We also provide a type-preserving rewriting procedure of processes in K into processes in L. This procedure suggests that, while effective, the degree of sharing is a rather subtle criteria for distinguishing typed processes. △ Less

Submitted 26 August, 2015; originally announced August 2015.

Comments: In Proceedings EXPRESS/SOS 2015, arXiv:1508.06347

ACM Class: F.3.2

Journal ref: EPTCS 190, 2015, pp. 1-15

On the Minimum Labelling Spanning bi-Connected Subgraph problem

Authors: J. A. Moreno Perez, S. Consoli

Abstract: We introduce the minimum labelling spanning bi-connected subgraph problem (MLSBP) replacing connectivity by bi-connectivity in the well known minimum labelling spanning tree problem (MLSTP). A graph is bi-connected if, for every two vertices, there are, at least, two vertex-disjoint paths joining them. The problem consists in finding the spanning bi-connected subgraph or block with minimum set of… ▽ More We introduce the minimum labelling spanning bi-connected subgraph problem (MLSBP) replacing connectivity by bi-connectivity in the well known minimum labelling spanning tree problem (MLSTP). A graph is bi-connected if, for every two vertices, there are, at least, two vertex-disjoint paths joining them. The problem consists in finding the spanning bi-connected subgraph or block with minimum set of labels. We adapt the exact method of the MLSTP to solve the MLSTB and the basic greedy constructive heuristic, the maximum vertex covering algorithm (MVCA). This proce- dure is a basic component in the application of metaheuristics to solve the problem. △ Less

Submitted 7 May, 2015; originally announced May 2015.

Comments: MIC 2015: The XI Metaheuristics International Conference, 3 pages, Agadir, June 7-10, 2015

Towards an intelligent VNS heuristic for the k-labelled spanning forest problem

Authors: Sergio Consoli, Josè Andrès Moreno Pèrez, Nenad Mladenovic

Abstract: In a currently ongoing project, we investigate a new possibility for solving the k-labelled spanning forest (kLSF) problem by an intelligent Variable Neighbourhood Search (Int-VNS) metaheuristic. In the kLSF problem we are given an undirected input graph G and an integer positive value k, and the aim is to find a spanning forest of G having the minimum number of connected components and the upper… ▽ More In a currently ongoing project, we investigate a new possibility for solving the k-labelled spanning forest (kLSF) problem by an intelligent Variable Neighbourhood Search (Int-VNS) metaheuristic. In the kLSF problem we are given an undirected input graph G and an integer positive value k, and the aim is to find a spanning forest of G having the minimum number of connected components and the upper bound k on the number of labels to use. The problem is related to the minimum labelling spanning tree (MLST) problem, whose goal is to get the spanning tree of the input graph with the minimum number of labels, and has several applications in the real world, where one aims to ensure connectivity by means of homogeneous connections. The Int-VNS metaheuristic that we propose for the kLSF problem is derived from the promising intelligent VNS strategy recently proposed for the MLST problem, and integrates the basic VNS for the kLSF problem with other complementary approaches from machine learning, statistics and experimental algorithmics, in order to produce high-quality performance and to completely automate the resulting strategy. △ Less

Submitted 5 March, 2015; originally announced March 2015.

Comments: 2 pages, Fifteenth International Conference on Computer Aided Systems Theory (EUROCAST 2015), Las Palmas de Gran Canaria, Spain

Journal ref: Computer Aided Systems Theory, pages 79-80 (2015)

Core Higher-Order Session Processes: Tractable Equivalences and Relative Expressiveness

Authors: Dimitrios Kouzapas, Jorge A. Pérez, Nobuko Yoshida

Abstract: This work proposes tractable bisimulations for the higher-order pi-calculus with session primitives (HOpi) and offers a complete study of the expressivity of its most significant subcalculi. First we develop three typed bisimulations, which are shown to coincide with contextual equivalence. These characterisations demonstrate that observing as inputs only a specific finite set of higher-order valu… ▽ More This work proposes tractable bisimulations for the higher-order pi-calculus with session primitives (HOpi) and offers a complete study of the expressivity of its most significant subcalculi. First we develop three typed bisimulations, which are shown to coincide with contextual equivalence. These characterisations demonstrate that observing as inputs only a specific finite set of higher-order values (which inhabit session types) suffices to reason about HOp} processes. Next, we identify HO, a minimal, second-order subcalculus of HOpi in which higher-order applications/abstractions, name-passing, and recursion are absent. We show that HO can encode HOpi extended with higher-order applications and abstractions and that a first-order session pi-calculus can encode HOpi. Both encodings are fully abstract. We also prove that the session pi-calculus with passing of shared names cannot be encoded into HOpi without shared names. We show that HOpi, HO, and pi are equally expressive; the expressivity of HO enables effective reasoning about typed equivalences for higher-order processes. △ Less

Submitted 10 February, 2015; v1 submitted 9 February, 2015; originally announced February 2015.

Comments: 90 pages

ACM Class: D.3.1; F.3.2

Free-flight experiments in LISA Pathfinder

Authors: M. Armano, H. Audley, G. Auger, J. Baird, P. Binetruy, M. Born, D. Bortoluzzi, N. Brandt, A. Bursi, M. Caleno, A. Cavalleri, A. Cesarini, M. Cruise, C. Cutler, K. Danzmann, I. Diepholz, R. Dolesi, N. Dunbar, L. Ferraioli, V. Ferroni, E. Fitzsimons, M. Freschi, J. Gallegos, C. Garcia. Marirrodriga, R. Gerndt , et al. (67 additional authors not shown)

Abstract: The LISA Pathfinder mission will demonstrate the technology of drag-free test masses for use as inertial references in future space-based gravitational wave detectors. To accomplish this, the Pathfinder spacecraft will perform drag-free flight about a test mass while measuring the acceleration of this primary test mass relative to a second reference test mass. Because the reference test mass is co… ▽ More The LISA Pathfinder mission will demonstrate the technology of drag-free test masses for use as inertial references in future space-based gravitational wave detectors. To accomplish this, the Pathfinder spacecraft will perform drag-free flight about a test mass while measuring the acceleration of this primary test mass relative to a second reference test mass. Because the reference test mass is contained within the same spacecraft, it is necessary to apply forces on it to maintain its position and attitude relative to the spacecraft. These forces are a potential source of acceleration noise in the LISA Pathfinder system that are not present in the full LISA configuration. While LISA Pathfinder has been designed to meet it's primary mission requirements in the presence of this noise, recent estimates suggest that the on-orbit performance may be limited by this `suspension noise'. The drift-mode or free-flight experiments provide an opportunity to mitigate this noise source and further characterize the underlying disturbances that are of interest to the designers of LISA-like instruments. This article provides a high-level overview of these experiments and the methods under development to analyze the resulting data. △ Less

Submitted 29 December, 2014; originally announced December 2014.

Comments: 13 pages, 5 figures. Accepted to Journal Of Physics, Conference Series. Presented at 10th International LISA Symposium, May 2014, Gainesville, FL, USA

Self-Adaptation and Secure Information Flow in Multiparty Structured Communications: A Unified Perspective

Authors: Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Jorge A. Pérez

Abstract: We present initial results on a comprehensive model of structured communications, in which self- adaptation and security concerns are jointly addressed. More specifically, we propose a model of self-adaptive, multiparty communications with secure information flow guarantees. In this model, security violations occur when processes attempt to read or write messages of inappropriate security levels w… ▽ More We present initial results on a comprehensive model of structured communications, in which self- adaptation and security concerns are jointly addressed. More specifically, we propose a model of self-adaptive, multiparty communications with secure information flow guarantees. In this model, security violations occur when processes attempt to read or write messages of inappropriate security levels within directed exchanges. Such violations trigger adaptation mechanisms that prevent the violations to occur and/or to propagate their effect in the choreography. Our model is equipped with local and global mechanisms for reacting to security violations; type soundness results ensure that global protocols are still correctly executed, while the system adapts itself to preserve security. △ Less

Submitted 25 August, 2014; originally announced August 2014.

Comments: In Proceedings BEAT 2014, arXiv:1408.5564

ACM Class: D.3.1; F.3.2

Journal ref: EPTCS 162, 2014, pp. 9-18

Dynamic Role Authorization in Multiparty Conversations

Authors: Silvia Ghilezan, Svetlana Jakšić, Jovanka Pantović, Jorge A. Pérez, Hugo Torres Vieira

Abstract: Protocol specifications often identify the roles involved in communications. In multiparty protocols that involve task delegation it is often useful to consider settings in which different sites may act on behalf of a single role. It is then crucial to control the roles that the different parties are authorized to represent, including the case in which role authorizations are determined only at ru… ▽ More Protocol specifications often identify the roles involved in communications. In multiparty protocols that involve task delegation it is often useful to consider settings in which different sites may act on behalf of a single role. It is then crucial to control the roles that the different parties are authorized to represent, including the case in which role authorizations are determined only at runtime. Building on previous work on conversation types with flexible role assignment, here we report initial results on a typed framework for the analysis of multiparty communications with dynamic role authorization and delegation. In the underlying process model, communication prefixes are annotated with role authorizations and authorizations can be passed around. We extend the conversation type system so as to statically distinguish processes that never incur in authorization errors. The proposed static discipline guarantees that processes are always authorized to communicate on behalf of an intended role, also covering the case in which authorizations are dynamically passed around in messages. △ Less

Submitted 25 August, 2014; originally announced August 2014.

Comments: In Proceedings BEAT 2014, arXiv:1408.5564

ACM Class: D.3.1; F.3.2

Journal ref: EPTCS 162, 2014, pp. 1-8

A Typeful Characterization of Multiparty Structured Conversations Based on Binary Sessions

Authors: Luís Caires, Jorge A. Pérez

Abstract: Relating the specification of the global communication behavior of a distributed system and the specifications of the local communication behavior of each of its nodes/peers (e.g., to check if the former is realizable by the latter under some safety and/or liveness conditions) is a challenging problem addressed in many relevant scenarios. In the context of networked software services, a widespread… ▽ More Relating the specification of the global communication behavior of a distributed system and the specifications of the local communication behavior of each of its nodes/peers (e.g., to check if the former is realizable by the latter under some safety and/or liveness conditions) is a challenging problem addressed in many relevant scenarios. In the context of networked software services, a widespread programming language-based approach relies on global specifications defined by session types or behavioral contracts. Static type checking can then be used to ensure that components follow the prescribed interaction protocols. In the case of session types, developments have been mostly framed within quite different type theories for either binary (two-party) or multiparty (n-party) protocols. Unfortunately, the precise relationship between analysis techniques for multiparty and binary protocols is yet to be understood. In this work, we bridge this previously open gap in a principled way: we show that the analysis of multiparty protocols can also be developed within a much simpler type theory for binary protocols, ensuring protocol fidelity and deadlock-freedom. We present characterization theorems which provide new insights on the relation between two existing, yet very differently motivated, session type systems---one based on linear logic, the other based on automata theory---and suggest useful type-based verification techniques for multiparty systems relying on reductions to the binary case. △ Less

Submitted 16 July, 2014; originally announced July 2014.

ACM Class: D.3.1; F.3.2

Towards Formal Interaction-Based Models of Grid Computing Infrastructures

Authors: Carlos Alberto Ramírez Restrepo, Jorge A. Pérez, Jesús Aranda, Juan Francisco Díaz-Frias

Abstract: Grid computing (GC) systems are large-scale virtual machines, built upon a massive pool of resources (processing time, storage, software) that often span multiple distributed domains. Concurrent users interact with the grid by adding new tasks; the grid is expected to assign resources to tasks in a fair, trustworthy way. These distinctive features of GC systems make their specification and verific… ▽ More Grid computing (GC) systems are large-scale virtual machines, built upon a massive pool of resources (processing time, storage, software) that often span multiple distributed domains. Concurrent users interact with the grid by adding new tasks; the grid is expected to assign resources to tasks in a fair, trustworthy way. These distinctive features of GC systems make their specification and verification a challenging issue. Although prior works have proposed formal approaches to the specification of GC systems, a precise account of the interaction model which underlies resource sharing has not been yet proposed. In this paper, we describe ongoing work aimed at filling in this gap. Our approach relies on (higher-order) process calculi: these core languages for concurrency offer a compositional framework in which GC systems can be precisely described and potentially reasoned about. △ Less

Submitted 31 March, 2014; originally announced April 2014.

Comments: In Proceedings DCM 2013, arXiv:1403.7685

ACM Class: D.2.4; D.3.1; F.3.1

Journal ref: EPTCS 144, 2014, pp. 57-72

Session Types with Runtime Adaptation: Overview and Examples

Authors: Cinzia Di Giusto, Jorge A. Pérez

Abstract: In recent work, we have developed a session types discipline for a calculus that features the usual constructs for session establishment and communication, but also two novel constructs that enable communicating processes to be stopped, duplicated, or discarded at runtime. The aim is to understand whether known techniques for the static analysis of structured communications scale up to the challen… ▽ More In recent work, we have developed a session types discipline for a calculus that features the usual constructs for session establishment and communication, but also two novel constructs that enable communicating processes to be stopped, duplicated, or discarded at runtime. The aim is to understand whether known techniques for the static analysis of structured communications scale up to the challenging context of context-aware, adaptable distributed systems, in which disciplined interaction and runtime adaptation are intertwined concerns. In this short note, we summarize the main features of our session-typed framework with runtime adaptation, and recall its basic correctness properties. We illustrate our framework by means of examples. In particular, we present a session representation of supervision trees, a mechanism for enforcing fault-tolerant applications in the Erlang language. △ Less

Submitted 10 December, 2013; originally announced December 2013.

Comments: In Proceedings PLACES 2013, arXiv:1312.2218

ACM Class: D.2.4; F.3.1; F.3.2

Journal ref: EPTCS 137, 2013, pp. 21-32

State space modelling and data analysis exercises in LISA Pathfinder

Authors: M Nofrarias, F Antonucci, M Armano, H Audley, G Auger, M Benedetti, P Binetruy, J Bogenstahl, D Bortoluzzi, N Brandt, M Caleno, A Cavalleri, G Congedo, M Cruise, K Danzmann, F De Marchi, M Diaz-Aguilo, I Diepholz, G Dixon, R Dolesi, N Dunbar, J Fauste, L Ferraioli, V Ferroni W Fichter, E Fitzsimons , et al. (61 additional authors not shown)

Abstract: LISA Pathfinder is a mission planned by the European Space Agency to test the key technologies that will allow the detection of gravitational waves in space. The instrument on-board, the LISA Technology package, will undergo an exhaustive campaign of calibrations and noise characterisation campaigns in order to fully describe the noise model. Data analysis plays an important role in the mission an… ▽ More LISA Pathfinder is a mission planned by the European Space Agency to test the key technologies that will allow the detection of gravitational waves in space. The instrument on-board, the LISA Technology package, will undergo an exhaustive campaign of calibrations and noise characterisation campaigns in order to fully describe the noise model. Data analysis plays an important role in the mission and for that reason the data analysis team has been develo** a toolbox which contains all the functionalities required during operations. In this contribution we give an overview of recent activities, focusing on the improvements in the modelling of the instrument and in the data analysis campaigns performed both with real and simulated data. △ Less

Submitted 21 June, 2013; v1 submitted 19 June, 2013; originally announced June 2013.

Comments: Plenary talk presented at the 9th International LISA Symposium, 21-25 May 2012, Paris

Journal ref: 2013ASPC..467..161N

Adaptable processes

Authors: Mario Bravetti, Cinzia Di Giusto, Jorge A Perez, Gianluigi Zavattaro

Abstract: We propose the concept of adaptable processes as a way of overcoming the limitations that process calculi have for describing patterns of dynamic process evolution. Such patterns rely on direct ways of controlling the behavior and location of running processes, and so they are at the heart of the adaptation capabilities present in many modern concurrent systems. Adaptable processes have a location… ▽ More We propose the concept of adaptable processes as a way of overcoming the limitations that process calculi have for describing patterns of dynamic process evolution. Such patterns rely on direct ways of controlling the behavior and location of running processes, and so they are at the heart of the adaptation capabilities present in many modern concurrent systems. Adaptable processes have a location and are sensible to actions of dynamic update at runtime; this allows to express a wide range of evolvability patterns for concurrent processes. We introduce a core calculus of adaptable processes and propose two verification problems for them: bounded and eventual adaptation. While the former ensures that the number of consecutive erroneous states that can be traversed during a computation is bound by some given number k, the latter ensures that if the system enters into a state with errors then a state without errors will be eventually reached. We study the (un)decidability of these two problems in several variants of the calculus, which result from considering dynamic and static topologies of adaptable processes as well as different evolvability patterns. Rather than a specification language, our calculus intends to be a basis for investigating the fundamental properties of evolvable processes and for develo** richer languages with evolvability capabilities. △ Less

Submitted 15 November, 2012; v1 submitted 23 October, 2012; originally announced October 2012.

ACM Class: D.2.4; F.3.1; F.3.2; F.4.3

Journal ref: Logical Methods in Computer Science, Volume 8, Issue 4 (November 19, 2012) lmcs:982