ABSTRACT. In this talk we study the relationship between privacy and accuracy in the context of correlated datasets. We use a model of quantitative information flow to describe the the trade-off between privacy of individuals’ data and and the utility of queries to that data by modelling the effectiveness of adversaries attempting to make inferences after a data release. We show that, where correlations exist in datasets, it is not possible to implement optimal noise-adding mechanisms that give the best possible accuracy or the best possible privacy in all situations. Finally we illustrate the trade-off between accuracy and privacy for local and oblivious differentially private mechanisms in terms of inference attacks on medium-scale datasets.

ABSTRACT. This article improves the time bound for calculating the weak/branching bisimulation minimisation quotient on state-labelled discrete-time Markov chains from O(mn) to an expected-time O(m log⁴ n), where n is the number of states and m the number of transitions. For these results we assume that the set of state labels AP is small (|AP| ∈ O(m/n log⁴ n)). It follows the ideas of Groote et al. (ACM ToCL 2017) in combination with an efficient algorithm to handle decremental strongly connected components (Bernstein et al., STOC 2019).

ABSTRACT. This paper introduces the counterpart of strong bisimilarity for labelled transition systems extended with time-out transitions. It supports this concept through a modal characterisation, congruence results for a standard process algebra with recursion, and complete axiomatisations.

ABSTRACT. Reversible computation opens up the possibility of overcoming some of the hardware’s current physical limitations. It also offers theoretical insights, as it enriches multiple paradigms and models of computation, and sometimes retrospectively enlightens them. Concurrent reversible computation, for instance, offered interesting extensions to the Calculus of Communicating Systems, but was still lacking a natural and pertinent bisimulation to study processes equivalences. Our paper formulates an equivalence exploiting the two aspects of reversibility: backward moves and memory mechanisms. This bisimulation captures classical equivalences relations for denotational models of concurrency (History- and hereditary history-preserving bisimulation, (H)HPB), that were up to now only partially characterized by process algebras. This result gives an insight on the expressiveness of reversibility, as both backward moves and a memory mechanism—providing ‘backward determinism’—are needed to capture HHPB.

ABSTRACT. Automatic garbage collection (GC) prevents a wide class of bugs and reduces programming overhead. However, standard GC techniques that rely on reachability analysis are not useful for actor systems. This is because many actor frameworks provide access to file I/O or to a global storage--thus an actor with pending messages may potentially write to a shared resource even if it is currently unreachable from the root set. For this reason, actor GC is based on termination detection. Previous solutions to this problem have required coordination mechanisms such as causal message delivery or monitoring actors for mutation. These mechanisms adversely affect concurrency and can therefore be expensive to implement in distributed systems. We present a low-overhead reference listing technique that enables termination detection in shared-nothing systems with unordered messaging: given an arbitrary temporally distributed set of actor-local snapshots, a GC process can either deduce that some actors have terminated or request additional snapshots from non-terminated actors. Because snapshots do not need to be synchronized and network partitions are tolerated, our algorithm can be implemented in existing distributed actor systems with lower overhead than other approaches. The paper presents a formal specification of our algorithm, a proof that all actors identified as garbage have indeed terminated (safety), and a proof that all terminated actors, under certain reasonable assumptions, will eventually be identified (liveness). Because our algorithm is message-based, it is applicable to any implementation of the actor model. Moreover, the lack of ordering constraints makes our algorithm amenable to new optimizations, such as decentralized termination detection.

ABSTRACT. We conduct a systematic study of asynchronous models of distributed computing consisting of identical finite-state devices that cooperate in a network to decide if the network satisfies a given graph-theoretical property. Models discussed in the literature differ in the detection capabilities of the agents residing at the nodes of the network (detecting the set of states of their neighbors, or counting the number of neighbors in each state), the notion of acceptance (acceptance by halting in a particular configuration, or by stable consensus), the notion of step (synchronous move, interleaving, or arbitrary timing), and the fairness assumptions (non-starving, or stochastic-like). We study the expressive power of the combinations of these features, and show that the initially twenty possible combinations fit into seven equivalence classes. The classification is the consequence of several equi-expressivity results with a clear interpretation. In particular, we show that acceptance by halting configuration only has non-trivial expressive power if it is combined with counting, and that synchronous and interleaving models have the same power as those in which an arbitrary set of nodes can move at the same time. We also identify simple graph properties that distinguish the expressive power of the seven classes.

ABSTRACT. The Heard-Of model is a simple and relatively expressive model of distributed computation. Because of this, it has gained a considerable attention of the verification community. We give a characterization of all algorithms solving consensus in a fragmentof this model. The fragment is big enough to cover many prominent consensus algorithms. The characterization is purely syntactic: it is expressed in terms of some conditions on the text of the algorithm. One of the recent methods of verification of distributed algorithms is to abstract an algorithm to the Heard-Of model and then to verify the abstract algorithm using semi-automatic procedures. Our results allow, in some cases, to avoid the second step in this methodology.

ABSTRACT. We study a variant of binary session types in which choices and branches are decorated with probabilities. These decorations enable the reasoning on the probability that a session terminates successfully, for some user-definable notion of successful termination. We develop a type system for a simple session calculus featuring probabilistic choices and show that the success probability of well-typed processes agrees with that of the sessions they use. To this aim, the type system needs to track the propagation of probabilistic choices across different sessions.

ABSTRACT. Session types statically prescribe bidirectional communication protocols for message-passing processes. However, simple session types cannot specify properties beyond the type of exchanged messages. In this paper we extend the type system by using index refinements from linear arithmetic capturing intrinsic attributes of data structures and algorithms. We show that, despite the decidability of Presburger arithmetic, type equality and therefore also subtyping and type checking are now undecidable, which stands in contrast to analogous dependent refinement type systems from functional languages. We also present a practical, but incomplete algorithm for type equality, which we have used in our implementation of Rast, a concurrent session-typed language with arithmetic index refinements as well as ergometric and temporal types. Moreover, if necessary, the programmer can propose additional type bisimulations that are smoothly integrated into the type equality algorithm.

ABSTRACT. We present a structural proof theory for multi-party sessions, exploiting the expressive power of non-commutative logic which can capture explicitly the message sequence order in sessions. The approach in this work uses a more flexible form of subtyping than standard, for example, allowing a single thread to be substituted by multiple parallel threads which fulfil the role of the single thread. The resulting subtype system has the advantage that it can be used to capture compatibility in the multiparty setting (addressing limitations of pairwise duality). We establish standard results: that the type system is algorithmic, that multiparty compatible processes which are race free are also deadlock free, and that subtyping is sound with respect the substitution principle. Interestingly, each of these results can be established using cut elimination. We remark that global types are optional in this approach to typing sessions; indeed we show that this theory can be presented independently of the concept of global session types, or even named participants.

ABSTRACT. Automata theory provides us with fundamental notions such as languages, membership, emptiness and inclusion that in turn allow us to specify and verify properties of reactive systems in a useful manner. However, these notions all yield "yes"/"no" answers that sometimes fall short of being satisfactory answers when the models being analyzed are imperfect, and the observations made are prone to errors. As a result, a common engineering approach is not just to verify that a system satisfies a property, but whether it does so robustly. In this paper, we present notions of robustness that place a metric on words, thus providing a natural notion of distance between words. Such a metric naturally leads to a topological neighborhood of words and languages, leading to quantitative and robust versions of the membership, emptiness and inclusion problems. More generally, we consider weighted transducers to finely model the cost of errors, i.e., the cost of rewriting a word into another, and hence they naturally define word neighborhoods. The main contribution of this work is to study robustness verification problems in the context of weighted transducers. We provide algorithms for solving the robust and quantitative versions of the membership and inclusion problems while providing useful motivating case studies including modeling an error-prone human operator and an approximate pattern matching problem in a large type-1 diabetes dataset.

ABSTRACT. We address the separability problem of straight-line string constraints. The separability problem for languages of a class C by a class S asks: given two languages A and B in C, does there exist a language I in S separating A and B (i.e., I is a superset of A and disjoint from B)? The separability of string constraints is the same as the fundamental problem of interpolation of string constraints. We first show that regular separability of straight line string constraints is undecidable. Our second result is the decidability of piece-wise separability of straight line string constraints, though the precise complexity is open. In our third result, we consider the positive fragment of piece wise testable languages as a separator, and obtain an EXPSPACE algorithm for the separability of a useful class of straight line string constraints, and PSPACE completeness for the separability of context-free languages. The latter result is interesting since the complexity of piece-wise testable separability is still open for context-free languages.

ABSTRACT. We consider the problem of synthesising polynomial ranking functions for single-path loops over the reals with continuous semi-algebraic update function and compact semi-algebraic guard set. We show that a loop of this form has a polynomial ranking function if and only if it terminates. We further show that termination is decidable for such loops in the special case where the update function is affine.