Publications



Probabilities of First Order Sentences on Sparse Random Relational Structures: An Application to Definability on Random CNF Formulas
Alberto Larrauri, Journal of Logic and Computation ( JLC ) 2021.

Summary: We show a convergence law for first order logic in a general model of relational structures. In this model, the probability of a sentence varies smoothly with the density of each predicate. A consequence of this result is that, asymptotically, no certificate for unsatisfiability definable in FO logic succeeds with positive probability on random CNF formulas with linear number of clauses.

Limiting Probabilities of First Order Properties of Random Sparse Graphs and Hypergraphs
Alberto Larrauri, Tobias Müller & Marc Noy, Random Structures and Algorithms ( RSA ) 2022.

Summary: We study the set $L_c$ of limiting probabilities of first order sentences in the binomial random graph $G(n, p)$ in the sparse regime $p \sim c/n$. We show there is a critical value $c_0$ for which $L_c$ is dense in $[0,1]$ if and only if $c \geq c_0$. Moreover, the closure of $L_c$ is always a finite union of closed intervals. The value $c_0$ is precisely the one witnessing $\mathrm{Pr}(G(n, c_0/n) \text{ is acyclic }) = 1/2 + o(1)$. These results are also extended to the binomial $d$-uniform hypergraph.

Industry Paper: Surrogate Models for Testing Analog Designs under Limited Budget – a Bandgap Case Study
Roderick Bloem, Alberto Larrauri, Roland Lengfeldner, Cristinel Mateis, Dejan Ničković & Björn Ziegler Emebedded Systems Week ( ESWEEK ) 2022, to appear.

Summary: Testing analog integrated circuit (IC) designs is notoriously hard. Simulating tens of milliseconds from an accurate transistor level model of a complex analog design can take up to two weeks of computation. Therefore, the number of tests that can be executed during the late development stage of an analog IC can be very limited. We leverage the recent advancements in machine learning (ML) and propose two techniques, artificial neural networks (ANN) and Gaussian processes, to learn a surrogate model from an existing test suite. We then explore the surrogate model with Bayesian optimization to guide the generation of additional tests. We use an industrial bandgap case study to evaluate the two approaches and demonstrate the virtue of Bayesian optimization in efficiently generating complementary tests with constrained effort.

Minimization and Synthesis in Sequential Compositions of Mealy Machines: Revisited
Alberto Larrauri & Roderick Bloem, under submission

Summary: We study two problems on systems that consist of a sequential composition of Mealy machines, called head and tail. In the first problem, the goal is to obtain a smallest replacement for either component without altering the external behavior of the system. We show that minimization of the head and the tail are both NP-complete. However, existing methods proposed for the minimization of the tail have doubly-exponential complexity. The source of this complexity blow-up is identified and an alternative algorithm is proposed. In the second problem, only one component - either the head or the tail - is known, and a desired model for the whole system is given. The goal now is to build the missing component. We show that it takes polynomial time to decide whether a missing tail can be built, but an appropriate model may be of exponential size.

Conformance Testing of Mealy Machines Under Input Restrictions
Alberto Larrauri & Roderick Bloem, under submission

Summary: We introduce a grey-box conformance testing method for networks of interconnected Mealy Machines. This approach addresses the scenario where all interfaces of the component under test are observable, but its inputs are under the control of other white-box components. We prove new conditions for full fault detection that exploit repetitions across branching executions of the composite machine in a novel way. Experimental evaluation of our approach on cascade compositions of up to a thousand states is provided, showing that it notably outperforms existing black-box testing techniques.

Limiting Probabilities of First Order Properties of Sparse Graphs with Given Degree Sequences
Alberto Larrauri, Guillem Perarnau & Marc Noy, in preparation.

Summary: We study the set $L$ of limiting probabilities of first order sentences in the random graph $G_n$ with given degree sequence in the sparse regime. Similarly to our previous work on the binomial random graph $G(n, c/n)$, we show that the closure of $L$ is always a finite union of intervals. Moreover, whether $L$ is dense in $[0,1]$ depends only $\rho$, the ratio between the first and second moment of the limiting degree distribution, which also determines the appearance of a giant component in this random graph. We prove that $L$ is dense in $[0,1]$ if and only if $\rho\geq \rho_0$, where $\rho_0$ is the critical value witnessing $\mathrm{Pr}(G_n \text{ is acyclic }) = 1/2 + o(1)$.

Preservation Theorems on Random Graphs
Alberto Larrauri, in preparation.

Summary: Preservation theorems are results in classical model theory relating semantic classes of first order sentences to syntactic ones. We focus on Lyndon's theorem and Łoś–Tarski's theorem. The first states that a sentence which is monotone in some predicate is equivalent to a sentence which is positive in that predicate, and the second that a sentence closed under embeddings is equivalent to a purely existential one. Famously, both theorems fail when we restrict them to finite structures. This is the case even for finite graphs. We consider probabilistic versions of those theorems on random structures, where equivalence between sentences is substituted for "asymptotically-almost-sure" equivalence. We show that the probabilistic Lyndom theorem holds in multiple regimes of $G(n,p)$ including $p \sim c n^\alpha$ for $\alpha=-1$, or $\alpha= - (k+1)/k$, and close to the connectivity threshold $p \sim c/n + d\log n/n$. Similarly, we also prove the probabilistic Łoś–Tarski's theorem holds for those regimes of $G(n,p)$ as well as in the $n$-vertex uniform random graph chosen from an arbitrary addable minor-closed family.