Publications

Summary: We give a complete complexity classification for the problem of finding a solution to a given system of equations over a fixed finite monoid, given that a solution over a more restricted monoid exists. As a corollary, we obtain a complexity classification for the same problem over groups.

Summary: Feed-forward controllers compute control outputs to adapt to changes in environmental parameters in a cyber-physical system. When synthesizing control functions it can be difficult to give an analytical description of the controlled plant or to decide the expected control output ahead of time. These systems must, however, adhere to strict safety requirements, which makes it hard to write correct controllers. In this paper, we propose a novel blackbox synthesis approach to construct a continuous control function while dynamically sampling a limited number of test cases. The controller is guaranteed to be correct for a given Lipschitz bound. It can be adapted to work for increasingly conservative estimates of the bound based on observed behavior, iteratively providing increasing confidence in its correctness. Our algorithm employs a linear interpolation model, based on a Delaunay triangulation, to identify candidate control functions. It then generates additional test cases to either confirm a candidate or to improve the model. We evaluate our approach on random benchmarks and CPS examples to show its effectiveness.

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.

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.

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.

Summary: A celebrated result of Håstad established that, for any constant $\varepsilon>0$, it is NP-hard to find an assignment satisfying a $(1/|G|+\varepsilon)$-fraction of the constraints of a given $3$-Lin instance over an Abelian group $G$ even if one is promised that an assignment satisfying a $(1-\varepsilon)$-fraction of the constraints exists. Engebretsen, Holmerin, and Russell showed the same result for $3$-Lin instances over any finite (not necessarily Abelian) group. In other words, for almost-satisfiable instances of $3$-Lin the random assignment achieves an optimal approximation guarantee. % We prove that the random assignment algorithm is still best possible under a stronger promise that the $3$-Lin instance is almost satisfiable over an arbitrarily more restrictive group.

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)$.

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.

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.

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.