Abstract: In this talk I will discuss the interplay between two important topics in programming language research: dependent types and computational effects; by defining a small dependently-typed language, combining the features of Martin-Löf type theory and computational languages such as Call-By-Push-Value and the Enriched Effect Calculus. Our language has both value types and terms and computation types and terms, with the value and computation types only allowed to depend on values. A novel aspect of our language is the use of computational sigma-types to account for type-dependency in the sequential composition of computations.
The design of our language is inspired by a class of categorical models we call fibred adjunction models. These naturally combine i) comprehension categories arising from the semantics of dependent types; and ii) adjunctions arising from the semantics of computational effects. We also discuss a variety of examples, some arising from EM-algebras of monads, some from other decompositions of monads into adjunctions and some from considering general recursion as a computational effect.
Finally, we also comment on some ongoing work on understanding parametrized adjunctions and parametrized computational effects in this fibred setting. In particular, we show how the clear distinction between values and computations sheds new light on how to model parametrized computational effects where the result parameters need to depend on result values, for example, to model the possible failure of opening a file.
This is joint work with Neil Ghani and Gordon Plotkin.
Slides from the talk [pdf]
Abstract: Illumination enhancement has been a challenging topic in the field of image/video processing, not only because it plays an important role in many image processing applications, but also because it directly effects on the scene. This talk is divided into two parts. Firstly we will talk about some state-of-the-art techniques, which are being used in illumination enhancement of 8-bit images, such as singular value decomposition based illumination enhancement, wavelet transform based illumination enhancement, and Gaussian distribution mapping based contrast stretching. Then we will introduce the new era of digital imaging, which is known as high dynamic range (HDR) imaging. In the latter part we will talk about the challenges present in HDR imaging as well as the importance of illumination enhancement on solving flickers problems in this field.
Slides from the talk [pptx]
Abstract: This talk will outline a method for diagnosing behavioral differences between pairs of business process models. Given two process models, the method determines if they are behaviorally equivalent, and if not, it describes their differences in terms of behavioral relations captured in one model but not in the other. The method is based on a translation from process models to event structures. A naive version of this translation suffers from two limitations. First, this translation is not applicable to process models with cycles. Second, it produces redundant difference diagnostic statements because an event structure may contain unnecessary event duplication. To tackle the first limitation, we propose a notion of unfolding that captures all possible causes of each task, where tasks that can occur more than once in a run are distinguished from those that cannot. From this unfolding, an event structure is derived, thus enabling the diagnosis of behavioral differences in terms of repetition and behavioral relations that hold in one model but not in the other. For the second limitation, we put forward a technique to reduce event duplication in an event structure while preserving canonicity, by applying a set of behavior-preserving event folding rules. The proposed method has been implemented as a prototype that takes pairs of process models in the Business Process Model and Notation (BPMN) and produces difference diagnostics both in the form of statements in natural language and graphically overlaid on the process models.
Slides from the talk [pdf]
Abstract: Cellular automata (briefly, CA) are parallel synchronous systems on regular grids where the next state of a point depends on the current state of a finite neighborhood. The grid is determined by a finitely generated group and can be visualized as the Cayley graph of the group according to a suitable set of generators. In addition to being a useful tool for simulations, CA also raise important and interesting questions, such as how properties of the global transition function (obtained by synchronous application of the local update rule at each point) are linked to each other, and to properties of the underlying group.
We call a cellular automaton post-surjective if, however given a configuration X and a preimage Y to X, every configuration asymptotic (i.e., equal outside a finite set) to X has a preimage asymptotic to Y. The well known dual concept is pre-injectivity: a cellular automaton is pre-injective if distinct asymptotic configurations have distinct images. We prove that, under an assumption on the underlying group for which no counterexamples are known, cellular automata which are both pre-injective and post-surjective admit a reverse CA. In particular, because of the famous Garden of Eden theorem, d-dimensional post-surjective CA are reversible.
This is joint work with Jarkko Kari and Siamak Taati, presented at AUTOMATA 2015.
Slides from the talk [pdf]
Abstract: This paper deals with computational aspects of attack trees, more precisely, evaluating the expected adversarial utility in the failurefree game, where the adversary is allowed to re-run failed atomic attacks an unlimited number of times. It has been shown by Buldas and Lenin that exact evaluation of this utility is an NP-complete problem, so a computationally feasible approximation is needed. In this paper we consider a genetic approach for this challenge. Since genetic algorithms depend on a number of non-trivial parameters, we now have a multi-objective optimization problem and we consider several heuristic criteria to solve it.
This is joint work with Aleksandr Lenin and Jan Willemson.
Slides from the talk [pdf]
Abstract: Process mining is a family of methods to analyze event logs produced during the execution of business processes in order to extract insights regarding their performance and conformance with respect to normative or expected behavior. The landscape of process mining methods and use cases has expanded considerably in the past decade. However, the field has evolved in a rather ad hoc manner without a unifying foundational theory that would allow algorithms and theoretical results developed for one process mining problem to be reused when addressing other related problems. In this talk we will advocate a foundational approach to process mining based on a well-known model of concurrency, namely event structures. We outline how event structures can serve as a unified representation of behavior captured in process models and behavior captured in event logs. We then sketch how process mining operations, specifically automated process discovery, conformance checking and deviance mining, can be recast as operations on event structures.
Abstract: The problem of business process conformance checking is defined as follows: Given an event log recording the actual execution of a business process, and given a process model capturing its expected or normative execution, describe the differences between the behavior captured in the event log and that captured in the process model.
This talk will outline a novel business process conformance checking method based on event structures. The talk will show that the problem of conformance checking can be approached by folding the event log into an event structure, unfolding the process model into another event structure, and comparing the two event structures via an error-correcting synchronized product.
Abstract: The use of cellular phones has increased in recent years, as has the amount of data collected about the devices and their users. This collected information can be used to understand human mobility as well as human behavior. However, the fact that cellular data is sparse and spatio-temporal rises up many challenges regarding the temporal and geographical representation of human mobility or movement. From this perspective, analyzing and investigating the data helps significantly when constructing models to represent the real movement of people and also predict their mobility behavior.
Slides from the talk [pdf]
Abstract: Business process matching is the activity of checking whether a given business process can interoperate with another one in a correct manner. In case the check fails, it is desirable to obtain information about how the first process can be corrected with as few modifications as possible to achieve interoperability. In case the two business processes belong to two separate enterprises that want to build a virtual enterprise, business process matching based on revealing the business processes poses a clear threat to privacy, as it may expose sensitive information about the inner operation of the enterprises.
In this talk we propose a solution to this problem for business processes described by means of service automata. We propose a measure for similarity between service automata and use this measure to devise an algorithm that constructs the most similar automaton to the first one that can interoperate with the second one. To achieve privacy, we implement this algorithm on the Sharemind platform for secure multiparty computation. As a result, only the correction information is leaked to the first enterprise and no more.
This is joint work with Dilian Gurov and Roberto Guanciale, appeared at PST 2015.
Slides from the talk [pptx]
Abstract: We consider the problem of minimizing the communication in single-database private information retrieval protocols in the case where the length of the data to be transmitted is large. We present first rate-optimal protocols for 1-out-of-n computationally private information retrieval (CPIR), oblivious transfer (OT), and strong conditional oblivious transfer (SCOT). These protocols are based on a new optimalrate leveled homomorphic encryption scheme for large-out putpolynomial-size branching programs, that might be of independent interest. The analysis of the new scheme is intricate: the optimal rate is achieved if a certain parameter s is set equal to the only positive root of a degree-(m + 1) polynomial, where m is the length of the branching program. We show, by using Galois theory, that even when m = 4, this polynomial cannot be solved in radicals. We employ the Newton-Puiseux algorithm to find a Puiseux series for s, and based on this, propose a Θ (log m)-time algorithm to find an integer approximation to s.
This is joint work with Aggelos Kiayias, Nikos Leonardos, Kateryna Pavlyk and Qiang Tang. It appeared in PoPETs.
Slides from the talk [pdf]
Abstract: Oriented coloring is a coloring of the vertices of an oriented graph such that: (1) no two neighbors have the same color, (2) if there is an arc directed from the color a to b, then no arc is directed from b to a. In this talk, I will present a work in progress about the bounds on the oriented chromatic of rectangular grids. Moreover, I will describe an integer program which finds oriented colorings of grids.
This is joint work with Bahman Ghandchi and Dirk Oliver Theis.
Slides from the talk [pdf]
Abstract: Benchmark results for solving a differential equation using the Fourier Transform are reported on a variety of supercomputers. They show that total on chip bandwidth is a very good performance indicator until network communication costs dominate. For large data problems, similar benchmarks may be useful in indicating what kind of computing system to use. A discussion of some of the computational cost estimation and possibilities for extension will be made.
This is joint work with S. Aseeri, O. Batrašev, M. Icardi, B. Leu, A. Liu, N. Li, E. Müller, B. Palen, M. Quell, H. Servat, P. Sheth, R. Speck, M. Van Moer, J. Vienne.
Slides from the talk [pdf]
Abstract: In our previous works, we presented a generic method for turning passively secure protocols into protocols secure against covert attacks, adding an offline preprocessing and a cheap post-execution verification phase. One problem of our method was that it has protected honest parties from dishonest parties only, but not from other honest parties. In this work, we propose a varaint of universal composability model that protects honest parties from other honest parties. We modify our verification protocol in such a way that the honest parties are no longer afraid of leaking their secrets to other honest parties.
This is joint work with Peeter Laud.
Slides from the talk [pdf]
Abstract: We consider how to perform privacy-preserving analyses on private data from different data providers and containing personal information of many different individuals. We combine differential privacy and secret sharing based secure multiparty computation in the same system to protect the privacy of both the data providers and the individuals. We have implemented a prototype of this combination and have found that the overhead of adding differential privacy to secure multiparty computation is small enough to be usable in practice.
This is joint work with Peeter Laud, accepted to ACSAC 2015.
Slides from the talk [pdf]
Abstract: The rectangle covering number of an n × n Boolean matrix M is the smallest number of 1-rectangles which are needed to cover all the 1-entries of M. The concept is an important lower bound in Communication Complexity and Combinatorial Optimization. It is also known as the Boolean rank of M: the smallest k such that M is the product of an n × k and a k × n matrix under Boolean arithmetic (1+1 = 1). Under the name of \textit{biclique covering number} of a bipartite graph, the concept is important in graph theory and algorithmics.
By a construction of Lovász and Saks, the rectangle covering number is the chromatic number of a graph constructed from M: The Lovász-Saks matrix-graph Graphd(M) has as its vertex set the set of pairs (k,l) with Mk,l=1, and two vertices (k,l), (k',l') are adjacent iff Mk,l'Mk',l = 0.
In our paper, we study the rectangle covering number of random n × n matrices, where each entry is 1 with probability p, and the entries are independent. As usual, we are interested in n → ∞ and p is allowed to vary with n. To bound the rectangle covering number, i.e., the chromatic number of the Lovász-Saks graph, we also study its clique number (cliques are called "fooling sets" in communication complexity vernacular and "sets of independent entries" in matrix theory) and its independence number.
This is joint work with Dirk Oliver Theis.
Slides from the talk [pdf]
Abstract: Sharemind is an efficient framework for secure multiparty computations (SMC). Its efficiency is in part achieved through a large set of primitive, optimized SMC protocols that it makes available to applications built on its top. The size of this set has brought with it an issue not present in frameworks with a small number of supported operations: the set of protocols must be maintained, as new protocols are still added to it and possible optimizations for a particular sub-protocol should be propagated into larger protocols working with data of different types.
To ease the maintenance of existing and implementation of new protocols, we have devised a domain-specific language (DSL) and its optimizing compiler for specifying protocols for secure computation. In this talk, we give the rationale of the design, describe the translation steps, the location of the compiler in the whole Sharemind protocol stack, and the results obtained with this system.
This is joint work with Peeter Laud, accepted to CCS 2015.
Slides from the talk [pdf]
Abstract: Extremal graph theory studies among other things the following question. For a given number n, what is the maximum number of edges in an n-vertex graph that contains no copy of a fixed subgraph, such as a triangle, or 4-cycle, or any other. Here by a subgraph, we do not necessarily mean an induced subgraph, so for example the complete graph on 4 vertices will contain the 4-cycle as a subgraph. You could also ask about the minimum number of edges in a triangle- or 4-cycle- etc. free graph, with the property that upon adding an arbitrary edge to it, we necessarily create a triangle or 4-cycle etc. This maximum is known as the extremal or Tur'an number ex(n, H), whereas this minimum is known as the saturation number Sat(n,H) where H is the forbidden subgraph. We study the game version of these two numbers, which is sort of an average of the two -- we study it in this and some related contexts. I will talk about early work, our results and outline some strategies for the players in different games.
This is joint work with Jonathan D. Lee.
Slides from the talk [pdf]
Abstract: One of the most promising candidates for universal and scalable quantum computing is linear optics with single photon sources and detectors. It is universal because any unitary operator can be implemented by a sequence of beam splitters and phase shifters acting on a suitable number of modes. It is scalable when implemented as a photonic integrated circuit.
In this talk, I will describe some general ideas for constructing linear optical quantum circuits using unitary matrix decompositions. In particular, I will describe recursive schemes for quantum Fourier transforms and the inversion about the mean in Grover's algorithm.
Slides from the talk [pdf]
Abstract: Residual finite state automata (RFSA) are a subclass of nondeterministic finite automata with the property that every state of an RFSA defines a residual language (a left quotient) of the language accepted by the RFSA. Every regular language has a unique canonical RFSA which is a minimal RFSA accepting the language. We study the relationship of RFSAs with atoms of regular languages. We generalize the double-reversal method of finding a canonical RFSA, presented by Denis, Lemay, and Terlutte.
This work was presented at DCFS 2015.
Slides from the talk [pdf]
Abstract: In the Haskell community, there is a controversy about what the laws of the MonadPlus type constructor class ought to be. We suggest that there is no single universal correct answer, however there is a universal method. Important classes of notions of finitary nondeterminism are captured by what we call monads of semigroups and monads of monoids, but also by monads of different specializations of semigroups and monoids. Some of these specializations of monads are exotic and amusing too.
Slides from the talk [pdf]
Abstract: In this paper we address the problem of large space consumption for protocols in the Bounded Retrieval Model (BRM), which require users to store large secret keys subject to adversarial leakage. We propose a method to derive keys for such protocols on-the-fly from weakly random private data (like text documents or photos, users keep on their disks anyway for non-cryptographic purposes) in such a way that no extra storage is needed. We prove that any leakage-resilient protocol (belonging to a certain, arguably quite broad class) when run with a key obtained this way retains a similar level of security as the original protocol had. Additionally, we guarantee privacy of the data the actual keys are derived from. That is, an adversary can hardly gain any knowledge about the private data except that he could otherwise obtain via leakage. Our reduction works in the Random Oracle model.
As an important tool in the proof we use a newly established bound for min-entropy, which can be of independent interest. It may be viewed as an analogue of the chain rule -- a weaker form of the well-known formula H(X | Y) = H(X, Y) - H(Y) for random variables X, Y, and Shannon entropy, which our result originates from. For min-entropy only a much more limited version of this relation is known to hold. Namely, the min-entropy of X may decrease by up to the bitlength of Y when X is conditioned on Y, in short: \widetilde H(X | Y) ≥ H∞(X) - |Y|. In many cases this inequality does not offer tight bounds, and such significant entropy loss makes it inadequate for our particular application. In the quasi chain rule we propose, we inject some carefully crafted side information (spoiling knowledge) to show that with large probability the average min-entropy of X conditioned on both: Y and this side information can be almost lower bounded by the min-entropy of (X, Y) decreased by the min-entropy of Y conditioned on the side information.
This is joint work with Konrad Durnoga, Tomasz Kazana and Maciej Zdanowicz.
Slides from the talk [pdf]
Abstract: Multiport switches are commonly used as data processing and routing devices in computer networks. A network switch routes data packets between its multiple input and output ports. Packets from input ports are stored upon arrival in a switch fabric comprising multiple memory banks. This can lead to memory contention when distinct output ports request packets from the same memory bank, resulting in a degraded switching bandwidth. To solve this problem, switch codes are introduced as a tradeoff between redundancy and service. Using techniques from combinatorial design and graph theory, constructions for switch codes serving different types of requests are given.
This is joint work with Yeow Meng Chee, Fei Gao and Samuel Tien Ho Teo.