Luis Miguel Danielsson, PhD Student, Instituto IMDEA Software
We study the problem of timed asynchronous decentralized monitoring of stream runtime verification specifications. In decentralized runtime verification, monitors are deployed in a network that provides a (sufficiently) synchronized shared clock. These monitors communicate via an asynchronous network, where messages can take arbitrarily long but cannot be duplicated or lost. This is a communication setting common in many cyber-physical systems like smart buildings, ambient living or Industry 4.0. This kind of network ressembles more closely every day networks. Previous approaches to decentralized monitoring were limited to synchronous networks, which are not easily implemented in practice. In this work we propose a solution to the timed asynchronous monitoring problem and show that this problem generalizes the synchronous case. We study the specifications and conditions on the network behavior that allow the monitoring to take place with bounded resources, independently of the trace length.
Fedor Ryabinin, PhD Student, Instituto IMDEA Software
Cloud services improve their availability by replicating data across sites in different geographical regions. A variety of state-machine replication protocols have been proposed for this setting that reduce the latency under workloads with low contention. However, when contention increases, these protocols may deliver lower performance than well-known Paxos algorithm. In this talk I will present SwiftPaxos – a protocol that lowers the best-case latency in comparison to Paxos without hurting the worst-case one. SwiftPaxos executes a command in a single round trip if there is no contention, and in 1.5 round trips otherwise. Differently from previous protocols, SwiftPaxos permits a replica to vote twice: first for its own proposal, and then to follow the leader. This mechanism avoids restarting the voting process when a disagreement occurs among replicas, saving computation time and message delays. This is joint work with Alexey Gotsman (IMDEA Software Institute) and Pierre Sutra (Télécom SudParis).
Alejandro Aguirre, PhD Researcher, Instituto IMDEA Software
Sensitivity properties describe how changes to the input of a program affect the output, typically by upper bounding the distance between the outputs of two runs by a monotone function of the distance between the corresponding inputs. When programs are probabilistic, the distance between outputs is a distance between distributions. The Kantorovich lifting provides a general way of defining a distance between distributions by lifting the distance of the underlying sample space; by choosing an appropriate distance on the base space, one can recover other usual probabilistic distances, such as the Total Variation distance. We develop a relational pre-expectation calculus to upper bound the Kantorovich distance between two executions of a probabilistic program. We illustrate our methods by proving algorithmic stability of a machine learning algorithm, convergence of a reinforcement learning algorithm, and fast mixing for card shuffling algorithms. We also consider some extensions: proving lower bounds on the Total Variation distance and convergence to the uniform distribution. Finally, we describe an asynchronous extension of our calculus to reason about pairs of program executions with different control flow.
Kyveli Doveri, PhD Student, Instituto IMDEA Software
We present a novel algorithmic framework to decide whether inclusion holds between ω-regular languages of infinite words over a finite alphabet. Our approach relies on a least fixpoint characterization of languages based on ultimately periodic infinite words of type uvω, with u finite prefix and v finite period of the word. Our inclusion checking algorithm, called BAInc, is designed as a complete abstract interpretation that performs a least fixpoint computation on a suitable abstraction of sets of finite words. This abstraction is canonically defined through a pair of well-quasiorder relations on finite prefixes and periods of words. We implemented BAInc in Java as a tool called BAIT. We experimentally evaluated BAIT on an extensive suite of benchmarks and performed a comparison with state-of-the-art language inclusion checking tools. The experimental results show that BAIT advances the state-of-the-art of language inclusion tools.