Search

Grove is a concurrent separation logic library for verifying distributed systems. Grove is the first to handle time-based leases, including their interaction with reconfiguration, crash recovery, thread-level concurrency, and unreliable networks. This paper uses Grove to verify several distributed system components written in Go, including GroveKV, a realistic distributed multi-threaded key-value store. GroveKV supports reconfiguration, primary/backup replication, and crash recovery, and uses leases to execute read-only requests on any replica. GroveKV achieves high performance (67-73% of Redis on a single core), scales with more cores and more backup replicas (achieving about 2x the throughput when going from 1 to 3 servers), and can safely execute reads while reconfiguring., Comment: Extended version of paper appearing at SOSP 2023

Inspired by the paper of Groenewald, Kaashoek and Ran (Wiener-Hopf indices of unitary functions on the unit circle in terms of realizations and related results on Toeplitz operators. \emph{Indag. Math.} 28, (2017), 649-710), we present an operator-theoretic approach to provide further insight and simpler computational formulas for the Wiener-Hopf indices of a rational matrix valued function taking unimodular values on the unit circle.

As in the paper [G. Groenewald, M.A. Kaashoek, A.C.M. Ran, Wiener-Hopf indices of unitary functions on the unit circle in terms of realizations and related results on Toeplitz operators. \emph{Indag. Math.} 28 (2017) 694--710] our aim is to obtain explicitly the Wiener-Hopf indices of a rational $m\times m$ matrix function $R(z)$ that has no poles and no zeros on the unit circle $\mathbb{T}$ but, in contrast with that paper, the function $R(z)$ is not required to be unitary on the unit circle. On the other hand, using a Douglas-Shapiro-Shields type of factorization, we show that $R(z)$ factors as $R(z)=\Xi(z)\Psi(z)$, where $\Xi(z)$ and $\Psi(z)$ are rational $m\times m$ matrix functions, $\Xi(z)$ is unitary on the unit circle and $\Psi(z)$ is an invertible outer function. Furthermore, the fact that $\Xi(z)$ is unitary on the unit circle allows us to factor as $\Xi(z) =V(z)W^*(z)$ where $V(z)$ and $W(z)$ are rational bi-inner $m\times m$ matrix functions. The latter allows us to solve the Wiener-Hopf indices problem. To derive explicit formulas for the functions $V(z)$ and $W(z)$ requires additional realization properties of the function $\Xi(z)$ which are given in the last two sections.

Large, human-annotated datasets are central to the development of natural language processing models. Collecting these datasets can be the most challenging part of the development process. We address this problem by introducing a general purpose technique for ``simulation-to-real'' transfer in language understanding problems with a delimited set of target behaviors, making it possible to develop models that can interpret natural utterances without natural training data. We begin with a synthetic data generation procedure, and train a model that can accurately interpret utterances produced by the data generator. To generalize to natural utterances, we automatically find projections of natural language utterances onto the support of the synthetic language, using learned sentence embeddings to define a distance metric. With only synthetic training data, our approach matches or outperforms state-of-the-art models trained on natural language data in several domains. These results suggest that simulation-to-real transfer is a practical framework for developing NLP applications, and that improved models for transfer might provide wide-ranging improvements in downstream tasks.

This paper explains a flaw in the published proof of the Scalable Commutativity Rule (SCR), presents a revised and formally verified proof of the SCR in the Coq proof assistant, and discusses the insights and open questions raised from our experience proving the SCR., Comment: 9 pages, 4 figures

In this paper a twofold inverse problem for orthogonal matrix functions in the Wiener class is considered. The scalar-valued version of this problem was solved by Ellis and Gohberg in 1992. Under reasonable conditions, the problem is reduced to an invertibility condition on an operator that is defined using the Hankel and Toeplitz operators associated to the Wiener class functions that comprise the data set of the inverse problem. It is also shown that in this case the solution is unique. Special attention is given to the case that the Hankel operator of the solution is a strict contraction and the case where the functions are matrix polynomials., Comment: 15 pages

The matrix-valued {Bezout-corona} problem $G(z)X(z)=I_m$, $|z|<1$, is studied in a Wiener space setting, that is, the given function $G$ is an analytic matrix function on the unit {disc} whose Taylor coefficients are absolutely summable and the same is required for the solutions $X$. It turns out that all Wiener solutions can be described explicitly in terms of two matrices and a square analytic Wiener function $Y$ satisfying $\det Y(z)\not =0$ for all $|z|\leq 1$. It is also shown that some of the results hold in the $H^\infty$ {setting, but} not all. In fact, if $G$ is an $H^\infty$ function, then $Y$ is just an $H^2$ function. Nevertheless, in this case, using the two matrices and the function $Y$, all $H^2$ solutions to the Bezout-corona problem can be described explicitly in a form analogous to the one appearing in the Wiener setting., Comment: 21 pages

The main results presented in this paper provide a complete and explicit description of all solutions to the left tangential operator Nevanlinna- Pick interpolation problem assuming the associated Pick operator is strictly positive. The complexity of the solutions is similar to that found in descriptions of the sub-optimal Nehari problem and variation on the Nevanlinna-Pick interpolation problem in the Wiener class that have been obtained through the band method. The main techniques used to derive the formulas are based on the theory of co-isometric realizations, and use the Douglas factorization lemma and state space calculations. A new feature is that we do not assume an additional stability assumption on our data, which allows us to view the Leech problem and a large class of commutant lifting problems as special cases. Although the paper has partly the character of a survey article, all results are proved in detail and some background material has been added to make the paper accessible to a large audience including engineers., Comment: 72 pages

In this paper we consider a twofold Ellis-Gohberg type inverse problem in an abstract *-algebraic setting. Under natural assumptions, necessary and sufficient conditions for the existence of a solution are obtained, and it is shown that in case a solution exists, it is unique. The main result relies strongly on an inversion formula for a $2\times 2$ block operator matrix whose off diagonal entries are Hankel operators while the diagonal entries are identity operators. Various special cases are presented, including the cases of matrix-valued $L^1$-functions on the real line and matrix-valued Wiener functions on the unit circle of the complex plane. For the latter case, it is shown how the results obtained in an earlier publication by the authors can be recovered., Comment: 52 pages

This paper deals with the Bezout equation $G(s)X(s)=I_m$, $\Re s \geq 0$, in the Wiener space of analytic matrix-valued functions on the right half plane. In particular, $G$ is an $m\times p$ matrix-valued analytic Wiener function, where $p\geq m$, and the solution $X$ is required to be an analytic Wiener function of size $p\times m$. The set of all solutions is described explicitly in terms of a $p\times p$ matrix-valued analytic Wiener function $Y$, which has an inverse in the analytic Wiener space, and an associated inner function $\Theta$ defined by $Y$ and the value of $G$ at infinity. Among the solutions, one is identified that minimizes the $H^2$-norm. A Wiener space version of Tolokonnikov's lemma plays an important role in the proofs. The results presented are natural analogs of those obtained for the discrete case in [11]., Comment: 15 pages

The Riccati inequality and equality are studied for infinite dimensional linear discrete time stationary systems with respect to the scattering supply rate. The results obtained are an addition to and based on our earlier work on the Kalman-Yakubovich-Popov inequality in [6]. The main theorems are closely related to the results of Yu. M. Arlinski\u{\i} in [3]. The main difference is that we do not assume the original system to be a passive scattering system, and we allow the solutions of the Riccati inequality and equality to satisfy weaker conditions., Comment: Published in Methods of Functional Analysis and Topology (MFAT), available at http://mfat.imath.kiev.ua/article/?id=840

In this paper we study direct and inverse problems for discrete and continuous time skew-selfadjoint Dirac systems with rectangular (possibly non-square) pseudo-exponential potentials. For such a system the Weyl function is a strictly proper rational rectangular matrix function and any strictly proper rational matrix function appears in this way. In fact, extending earlier results, given a strictly proper rational matrix function we present an explicit procedure to recover the corresponding potential using techniques from mathematical system and control theory. We also introduce and study a nonlinear generalized discrete Heisenberg magnet model, extending earlier results for the isotropic case. A large part of the paper is devoted to the related discrete time systems of which the pseudo-exponential potential depends on an additional continuous time parameter. Our techniques allows us to obtain explicit solutions for the generalized discrete Heisenberg magnet model and evolution of the Weyl functions.

For the strictly positive case (the suboptimal case), given stable rational matrix functions $G$ and $K$, the set of all $H^\infty$ solutions $X$ to the Leech problem associated with $G$ and $K$, that is, $G(z)X(z)=K(z)$ and $\sup_{|z|\leq 1}\|X(z)\|\leq 1$, is presented as the range of a linear fractional representation of which the coefficients are presented in state space form. The matrices involved in the realizations are computed from state space realizations of the data functions $G$ and $K$. On the one hand the results are based on the commutant lifting theorem and on the other hand on stabilizing solutions of algebraic Riccati equations related to spectral factorizations., Comment: 28 pages

For the strictly positive case (the suboptimal case) the maximum entropy solution $X$ to the Leech problem $G(z)X(z)=K(z)$ and $\|X\|_\infty=\sup_{|z|\leq 1}\|X(z)\|\leq 1$, with $G$ and $K$ stable rational matrix functions, is proved to be a stable rational matrix function. An explicit state space realization for $X$ is given, and $\|X\|_\infty$ turns out to be strictly less than one. The matrices involved in this realization are computed from the matrices appearing in a state space realization of the data functions $G$ and $K$. A formula for the entropy of $X$ is also given., Comment: 19 pages

Given stable rational matrix functions $G$ and $K$, a procedure is presented to compute a stable rational matrix solution $X$ to the Leech problem associated with $G$ and $K$, that is, $G(z)X(z)=K(z)$ and $\sup_{|z|\leq 1}\|X(z)\|\leq 1$. The solution is given in the form of a state space realization, where the matrices involved in this realization are computed from state space realizations of the data functions $G$ and $K$., Comment: 25 pages

A Redheffer type description of the set of all contractive solutions to the relaxed commutant lifting problem is given. The description involves a set of Schur class functions which is obtained by combining the method of isometric coupling with results on isometric realizations. For a number of special cases, including the case of the classical commutant lifting theorem, the description yields a proper parameterization of the set of all contractive solutions, but examples show that, in general, the Schur class function determining the contractive lifting does not have to be unique. Also some sufficient conditions are given guaranteeing that the corresponding relaxed commutant lifting problem has only one solution., Comment: Integral Equations Operator Theory 54 (2006), 33--67

In a 1990 paper Helton and Young showed that under certain conditions the optimal solution of the Nehari problem corresponding to a finite rank Hankel operator with scalar entries can be efficiently approximated by certain functions defined in terms of finite dimensional restrictions of the Hankel operator. In this paper it is shown that these approximants appear as optimal solutions to restricted Nehari problems. The latter problems can be solved using relaxed commutant lifting theory. This observation is used to extent the Helton and Young approximation result to a matrix-valued setting. As in the Helton and Young paper the rate of convergence depends on the choice of the initial space in the approximation scheme., Comment: 22 pages

This paper is devoted to connections between accelerants and potentials of Krein systems and of canonical systems of Dirac type, both on a finite interval. It is shown that a continuous potential is always generated by an accelerant, provided the latter is continuous with a possible jump discontinuity at the origin. Moreover, the generating accelerant is uniquely determined by the potential. The results are illustrated on pseudo-exponential potentials. The paper is a continuation of the earlier paper of the authors [1] dealing with the direct problem for Krein systems.

In the present paper we extend results of M.G. Krein associated to the spectral problem for Krein systems to systems with matrix valued accelerants with a possible jump discontinuity at the origin. Explicit formulas for the accelerant are given in terms of the matrizant of the system in question. Recent developments in the theory of continuous analogs of the resultant operator play an essential role.

A time-variant analogue of an interpolation problem equivalent to the relaxed commutant lifting problem is introduced and studied. In a somewhat less general form the problem already appears in the analysis of the set of all solutions to the three chain completion problem. The interpolants are upper triangular operator matrices of which the columns induce contractive operators. The set of all solutions of the problem is described explicitly. The results presented are time-variant analogues of the main theorems in [A.E. Frazho, S. ter Horst, and M.A. Kaashoek, All solutions to the relaxed commutant lifting problem, Acta Sci. Math. (Szeged) 72 (2006), 299--318]., Comment: 25 pages

This paper presents a few additions to commutant lifting theory. An operator interpolation problem is introduced and shown to be equivalent to the relaxed commutant lifting problem. Using this connection a description of all solutions of the former problem is given. Also a new application, involving bounded operators induced by $H^2$ operator-valued functions, is presented., Comment: 14 pages

A new description is given of all solutions to the relaxed commutant lifting problem. The method of proof is also different from earlier ones, and uses only an operator-valued version of a classical lemma on harmonic majorants., Comment: 15 pages

A discrete analog of a skew selfadjoint canonical (Zakharov-Shabat or AKNS) system with a pseudo-exponential potential is introduced. For the corresponding Weyl function the direct and inverse problem are solved explicitly in terms of three parameter matrices. As an application explicit solutions are obtained for the discrete integrable nonlinear equation corresponding to the isotropic Heisenberg magnet model. State space techniques from mathematical system theory play an important role in the proofs.