Search

This position paper on the (meta-)theory of Structural Operational Semantic (SOS) is motivated by the following two questions: (1) Is the (meta-)theory of SOS dying out as a research field? (2) If so, is it possible to rejuvenate this field with a redefined purpose? In this article, we will consider possible answers to those questions by first analysing the history of the EXPRESS/SOS workshops and the data concerning the authors and the presentations featured in the editions of those workshops as well as their subject matters. The results of our quantitative and qualitative analyses all indicate a diminishing interest in the theory of SOS as a field of research. Even though `all good things must come to an end', we strive to finish this position paper on an upbeat note by addressing our second motivating question with some optimism. To this end, we use our personal reflections and an analysis of recent trends in two of the flagship conferences in the field of Programming Languages (namely POPL and PDLI) to draw some conclusions on possible future directions that may rejuvenate research on the (meta-)theory of SOS. We hope that our musings will entice members of the research community to breathe new life into a field of research that has been kind to three of the authors of this article., Comment: In Proceedings EXPRESS/SOS2023, arXiv:2309.05788

A temporal graph is a graph in which edges are assigned a time label. Two nodes u and v of a temporal graph are connected one to the other if there exists a path from u to v with increasing edge time labels. We consider the problem of assigning time labels to the edges of a digraph in order to maximize the total reachability of the resulting temporal graph (that is, the number of pairs of nodes which are connected one to the other). In particular, we prove that this problem is NP-hard. We then conjecture that the problem is approximable within a constant approximation ratio. This conjecture is a consequence of the following graph theoretic conjecture: any strongly connected directed graph with n nodes admits an out-arborescence and an in-arborescence that are edge-disjoint, have the same root, and each spans $\Omega$(n) nodes.

A temporal graph is a graph whose edges appear only at certain points in time. Recently, the second and the last three authors proposed a natural temporal analog of the Erd\H{o}s-R\'enyi random graph model. The proposed model is obtained by randomly permuting the edges of an Erd\H{o}s-R\'enyi random graph and interpreting this permutation as an ordering of presence times. It was shown that the connectivity threshold in the Erd\H{o}s-R\'enyi model fans out into multiple phase transitions for several distinct notions of reachability in the temporal setting. In the present paper, we identify a sharp threshold for the emergence of a giant temporally connected component. We show that at $p = \log n/n$ the size of the largest temporally connected component increases from $o(n)$ to~$n-o(n)$. This threshold holds for both open and closed connected components, i.e. components that allow, respectively forbid, their connecting paths to use external nodes.

We revisit the planning problem in the blocks world, and we implement a known heuristic for this task. Importantly, our implementation is biologically plausible, in the sense that it is carried out exclusively through the spiking of neurons. Even though much has been accomplished in the blocks world over the past five decades, we believe that this is the first algorithm of its kind. The input is a sequence of symbols encoding an initial set of block stacks as well as a target set, and the output is a sequence of motion commands such as "put the top block in stack 1 on the table". The program is written in the Assembly Calculus, a recently proposed computational framework meant to model computation in the brain by bridging the gap between neural activity and cognitive function. Its elementary objects are assemblies of neurons (stable sets of neurons whose simultaneous firing signifies that the subject is thinking of an object, concept, word, etc.), its commands include project and merge, and its execution model is based on widely accepted tenets of neuroscience. A program in this framework essentially sets up a dynamical system of neurons and synapses that eventually, with high probability, accomplishes the task. The purpose of this work is to establish empirically that reasonably large programs in the Assembly Calculus can execute correctly and reliably; and that rather realistic -- if idealized -- higher cognitive functions, such as planning in the blocks world, can be implemented successfully by such programs.

We consider the problem of assigning appearing times to the edges of a digraph in order to maximize the (average) temporal reachability between pairs of nodes. Motivated by the application to public transit networks, where edges cannot be scheduled independently one of another, we consider the setting where the edges are grouped into certain walks (called trips) in the digraph and where assigning the appearing time to the first edge of a trip forces the appearing times of the subsequent edges. In this setting, we show that, quite surprisingly, it is NP-complete to decide whether there exists an assignment of times connecting a given pair of nodes. This result allows us to prove that the problem of maximising the temporal reachability cannot be approximated within a factor better than some polynomial term in the size of the graph. We thus focus on the case where, for each pair of nodes, there exists an assignment of times such that one node is reachable from the other. We call this property strong temporalisability. It is a very natural assumption for the application to public transit networks. On the negative side, the problem of maximising the temporal reachability remains hard to approximate within a factor $\sqrt$ n/12 in that setting. Moreover, we show the existence of collections of trips that are strongly temporalisable but for which any assignment of starting times to the trips connects at most an O(1/ $\sqrt$ n) fraction of all pairs of nodes. On the positive side, we show that there must exist an assignment of times that connects a constant fraction of all pairs in the strongly temporalisable and symmetric case, that is, when the set of trips to be scheduled is such that, for each trip, there is a symmetric trip visiting the same nodes in reverse order. Keywords:edge labeling edge scheduled network network optimisation temporal graph temporal path temporal reachability time assignment

Consider a sub-population of rebels that wish to initiate a revolution. In order to avoid initializing a failed revolution, rebels would first strive to estimate their relative "power", which is often correlated with their fraction in the population. However, and especially in non-democratic countries, rebels refrain from disclosing themselves. This poses a significant challenge for rebels: estimating their fraction in the population while minimizing the risk of being identified as rebels. This paper introduces a distributed computing framework aiming to study this question. Our main takeaway message is that the communication pattern has a crucial role in achieving such a task. Specifically, we show that relying on the inherent noise in the communication, "public communication", characterized by the fact that each message announced by an individual can be viewed by all its neighbors, allows rebels to estimate their fraction in the population while keeping a negligible risk of each rebel being identified as such. The suggested estimation protocol, inspired by historical events, is extremely simple and can be executed covertly even under extreme conditions of surveillance. Conversely, we show that under peer-to-peer communication, protocols of similar simplicity are either inefficient or non-covert.

A weighted point-availability time-dependent network is a list of temporal edges, where each temporal edge has an appearing time value, a travel time value, and a cost value. In this paper we consider the single source Pareto problem in weighted point-availability time-dependent networks, which consists of computing, for any destination d, all Pareto optimal pairs (t, c), where t and c are the arrival time and the cost of a path from s to d, respectively (a pair (t, c) is Pareto optimal if there is no path with arrival time smaller than t and cost no worse than c or arrival time no greater than t and better cost). We design and analyse a general algorithm for solving this problem, whose time complexity is O(M log P), where M is the number of temporal edges and P is the maximum number of Pareto optimal pairs for each node of the network. This complexity significantly improves the time complexity of the previously known solution. Our algorithm can be used to solve several different minimum cost path problems in weighted point-availability time-dependent networks with a vast variety of cost definitions, and it can be easily modified in order to deal with the single destination Pareto problem. All our results apply to directed networks, but they can be easily adapted to undirected networks with no edges with zero travel time.

Betweenness centrality is a graph parameter that has been successfully applied to network analysis. In the context of computer networks, it was considered for various objectives, ranging from routing to service placement. However, as observed by Maccari et al. [INFOCOM 2018], research on betweenness centrality for improving protocols was hampered by the lack of a usable, fully distributed algorithm for computing this parameter. We resolve this issue by designing an efficient algorithm for computing betweenness centrality, which can be implemented by minimal modifications to any distance-vector routing protocol based on Bellman-Ford. The convergence time of our implementation is shown to be proportional to the diameter of the network

The study of interactive proofs in the context of distributed network computing is a novel topic, recently introduced by Kol, Oshman, and Saxena [PODC 2018]. In the spirit of sequential interactive proofs theory, we study the power of distributed interactive proofs. This is achieved via a series of results establishing trade-offs between various parameters impacting the power of interactive proofs, including the number of interactions, the certificate size, the communication complexity, and the form of randomness used. Our results also connect distributed interactive proofs with the established field of distributed verification. In general, our results contribute to providing structure to the landscape of distributed interactive proofs., Comment: To be presented in DISC 2019

Given a connected graph $G=(V,E)$, the closeness centrality of a vertex $v$ is defined as $\frac{n-1}{\sum_{w \in V} d(v,w)}$. This measure is widely used in the analysis of real-world complex networks, and the problem of selecting the $k$ most central vertices has been deeply analysed in the last decade. However, this problem is computationally not easy, especially for large networks: in the first part of the paper, we prove that it is not solvable in time $\O(|E|^{2-\epsilon})$ on directed graphs, for any constant $\epsilon>0$, under reasonable complexity assumptions. Furthermore, we propose a new algorithm for selecting the $k$ most central nodes in a graph: we experimentally show that this algorithm improves significantly both the textbook algorithm, which is based on computing the distance between all pairs of vertices, and the state of the art. For example, we are able to compute the top $k$ nodes in few dozens of seconds in real-world networks with millions of nodes and edges. Finally, as a case study, we compute the $10$ most central actors in the IMDB collaboration network, where two actors are linked if they played together in a movie, and in the Wikipedia citation network, which contains a directed edge from a page $p$ to a page $q$ if $p$ contains a link to $q$.

In this paper we propose applying the crowdsourcing approach to a software platform that uses a modern and state-of-the-art 3D game engine. This platform could facilitate the generation and manipulation of interactive 3D environments by a community of users producing different content such as cultural heritage, scientific virtual labs, games, novel art forms and virtual museums., Comment: translated from the paper published in the conference proceedings for GARR 2017

Betweenness is a well-known centrality measure that ranks the nodes according to their participation in the shortest paths of a network. In several scenarios, having a high betweenness can have a positive impact on the node itself. Hence, in this paper we consider the problem of determining how much a vertex can increase its centrality by creating a limited amount of new edges incident to it. In particular, we study the problem of maximizing the betweenness score of a given node -- Maximum Betweenness Improvement (MBI) -- and that of maximizing the ranking of a given node -- Maximum Ranking Improvement (MRI). We show that MBI cannot be approximated in polynomial-time within a factor $(1-\frac{1}{2e})$ and that MRI does not admit any polynomial-time constant factor approximation algorithm, both unless $P=NP$. We then propose a simple greedy approximation algorithm for MBI with an almost tight approximation ratio and we test its performance on several real-world networks. We experimentally show that our algorithm highly increases both the betweenness score and the ranking of a given node ant that it outperforms several competitive baselines. To speed up the computation of our greedy algorithm, we also propose a new dynamic algorithm for updating the betweenness of one node after an edge insertion, which might be of independent interest. Using the dynamic algorithm, we are now able to compute an approximation of MBI on networks with up to $10^5$ edges in most cases in a matter of seconds or a few minutes., Comment: Accepted to ACM Journal of Experimental Algorithmics (JEA)

In recent years, researchers proposed several algorithms that compute metric quantities of real-world complex networks, and that are very efficient in practice, although there is no worst-case guarantee. In this work, we propose an axiomatic framework to analyze the performances of these algorithms, by proving that they are efficient on the class of graphs satisfying certain axioms. Furthermore, we prove that the axioms are verified asymptotically almost surely by several probabilistic models that generate power law random graphs, such as the In recent years, researchers proposed several algorithms that compute metric quantities of real-world complex networks, and that are very efficient in practice, although there is no worst-case guarantee. In this work, we propose an axiomatic framework to analyze the performances of these algorithms, by proving that they are efficient on the class of graphs satisfying certain properties. Furthermore, we prove that these properties are verified asymptotically almost surely by several probabilistic models that generate power law random graphs, such as the Configuration Model, the Chung-Lu model, and the Norros-Reittu model. Thus, our results imply average-case analyses in these models. For example, in our framework, existing algorithms can compute the diameter and the radius of a graph in subquadratic time, and sometimes even in time $n^{1+o(1)}$. Moreover, in some regimes, it is possible to compute the $k$ most central vertices according to closeness centrality in subquadratic time, and to design a distance oracle with sublinear query time and subquadratic space occupancy. In the worst case, it is impossible to obtain comparable results for any of these problems, unless widely-believed conjectures are false.

Closeness is an important centrality measure widely used in the analysis of real-world complex networks. In particular, the problem of selecting the k most central nodes with respect to this measure has been deeply analyzed in the last decade. However, even for not very large networks, this problem is computationally intractable in practice: indeed, Abboud et al have recently shown that its complexity is strictly related to the complexity of the All-Pairs Shortest Path (in short, APSP) problem, for which no subcubic "combinatorial" algorithm is known. In this paper, we propose a new algorithm for selecting the k most closeness central nodes in a graph. In practice, this algorithm significantly improves over the APSP approach, even though its worst-case time complexity is the same. For example, the algorithm is able to compute the top k nodes in few dozens of seconds even when applied to real-world networks with millions of nodes and edges. We will also experimentally prove that our algorithm drastically outperforms the most recently designed algorithm, proposed by Olsen et al. Finally, we apply the new algorithm to the computation of the most central actors in the IMDB collaboration network, where two actors are linked if they played together in a movie.

This paper will analyze several quadratic-time solvable problems, and will classify them into two classes: problems that are solvable in truly subquadratic time (that is, in time $O(n^{2-\epsilon})$ for some $\epsilon>0$) and problems that are not, unless the well known Strong Exponential Time Hypothesis (SETH) is false. In particular, we will prove that some quadratic-time solvable problems are indeed easier than expected. We will provide an algorithm that computes the transitive closure of a directed graph in time $O(mn^{\frac{\omega+1}{4}})$, where $m$ denotes the number of edges in the transitive closure and $\omega$ is the exponent for matrix multiplication. As a side effect, we will prove that our algorithm runs in time $O(n^{\frac{5}{3}})$ if the transitive closure is sparse. The same time bounds hold if we want to check whether a graph is transitive, by replacing m with the number of edges in the graph itself. As far as we know, this is the fastest algorithm for sparse transitive digraph recognition. Finally, we will apply our algorithm to the comparability graph recognition problem (dating back to 1941), obtaining the first truly subquadratic algorithm. The second part of the paper deals with hardness results. Starting from an artificial quadratic-time solvable variation of the k-SAT problem, we will construct a graph of Karp reductions, proving that a truly subquadratic-time algorithm for any of the problems in the graph falsifies SETH. The analyzed problems are the following: computing the subset graph, finding dominating sets, computing the betweenness centrality of a vertex, computing the minimum closeness centrality, and computing the hyperbolicity of a pair of vertices. We will also be able to include in our framework three proofs already appeared in the literature, concerning the graph diameter computation, local alignment of strings and orthogonality of vectors., Comment: Submitted at SODA 2015

Synchronous Context-Free Grammars (SCFGs), also known as syntax-directed translation schemata, are unlike context-free grammars in that they do not have a binary normal form. In general, parsing with SCFGs takes space and time polynomial in the length of the input strings, but with the degree of the polynomial depending on the permutations of the SCFG rules. We consider linear parsing strategies, which add one nonterminal at a time. We show that for a given input permutation, the problems of finding the linear parsing strategy with the minimum space and time complexity are both NP-hard.

Randomized gossip is one of the most popular way of disseminating information in large scale networks. This method is appreciated for its simplicity, robustness, and efficiency. In the "push" protocol, every informed node selects, at every time step (a.k.a. round), one of its neighboring node uniformly at random and forwards the information to this node. This protocol is known to complete information spreading in $O(\log n)$ time steps with high probability (w.h.p.) in several families of $n$-node "static" networks. The Push protocol has also been empirically shown to perform well in practice, and, specifically, to be robust against dynamic topological changes. In this paper, we aim at analyzing the Push protocol in "dynamic" networks. We consider the "edge-Markovian" evolving graph model which captures natural temporal dependencies between the structure of the network at time $t$, and the one at time $t+1$. Precisely, a non-edge appears with probability $p$, while an existing edge dies with probability $q$. In order to fit with real-world traces, we mostly concentrate our study on the case where $p=\Omega(1/n)$ and $q$ is constant. We prove that, in this realistic scenario, the Push protocol does perform well, completing information spreading in $O(\log n)$ time steps w.h.p. Note that this performance holds even when the network is, w.h.p., disconnected at every time step (e.g., when $p << (\log n) / n$). Our result provides the first formal argument demonstrating the robustness of the Push protocol against network changes. We also address other ranges of parameters $p$ and $q$ (e.g., $p+q=1$ with arbitrary $p$ and $q$, and $p=1/n$ with arbitrary $q$). Although they do not precisely fit with the measures performed on real-world traces, they can be of independent interest for other settings. The results in these cases confirm the positive impact of dynamism.