Strix is a new tool for reactive LTL synthesis combining a direct translation of LTL formulas into deterministic parity automata (DPA) and an efficient, multi-threaded explicit state solver for parity games. In brief, Strix (1) decomposes the given formula into simpler formulas, (2) translates these on-the-fly into DPAs based on the queries of the parity game solver, (3) composes the DPAs into a parity game, and at the same time already solves the intermediate games using strategy iteration, and (4) finally translates the winning strategy, if it exists, into a Mealy machine or an AIGER circuit with optional minimization using external tools. We experimentally demonstrate the applicability of our approach by a comparison with Party, BoSy, and ltlsynt using the syntcomp2017 benchmarks. In these experiments, our prototype can compete with BoSy and ltlsynt with only Party performing slightly better. In particular, our prototype successfully synthesizes the full and unmodified LTL specification of the AMBA protocol for $$n=2$$ masters.

We present two structural results concerning longest common prefixes of non-empty languages. First, we show that the longest common prefix of the language generated by a context-free grammar of size $N$ equals the longest common prefix of the same grammar where the heights of the derivation trees are bounded by $4N$. Second, we show that each nonempty language $L$ has a representative subset of at most three elements which behaves like $L$ w.r.t. the longest common prefix as well as w.r.t. longest common prefixes of $L$ after unions or concatenations with arbitrary other languages. From that, we conclude that the longest common prefix, and thus the longest common suffix, of a context-free language can be computed in polynomial time.

We suggest a new annotation scheme for unlexicalized PCFGs that is inspired by formal language theory and only depends on the structure of the parse trees. We evaluate this scheme on the TüBa-D/Z treebank w.r.t. several metrics and show that it improves both parsing accuracy and parsing speed considerably. We also show that our strategy can be fruitfully com-bined with known ones like parent annota-tion to achieve accuracies of over 90 % la-beled F1 and leaf-ancestor score. Despite increasing the size of the grammar, our annotation allows for parsing more than twice as fast as the PCFG baseline. 1

This article presents a novel generic technique for solving dataflow equations in interprocedural dataflow analysis. The technique is obtained by generalizing Newton's method for computing a zero of a differentiable function to ω-continuous semirings. Complete semilattices, the common program analysis framework, are a special class of ω-continuous semirings. We show that our generalized method always converges to the solution, and requires at most as many iterations as current methods based on Kleene's fixed-point theorem. We also show that, contrary to Kleene's method, Newton's method always terminates for arbitrary idempotent and commutative semirings. More precisely, in the latter setting the number of iterations required to solve a system of n equations is at most n .

We consider equation systems of the form $X_1=f_1(X_1,\dots,X_n)$, $\dots$, $X_n = f_n(X_1,\dots,X_n)$, where $f_1,\dots,f_n$ are polynomials with positive real coefficients. In vector form we denote such an equation system by ${\bf X}={\bf f}({\bf X})$ and call ${\bf f}$ a system of positive polynomials (SPP). Equation systems of this kind appear naturally in the analysis of stochastic models like stochastic context-free grammars (with numerous applications to natural language processing and computational biology), probabilistic programs with procedures, web-surfing models with back buttons, and branching processes. The least nonnegative solution $\mu{\bf f}$ of an SPP equation ${\bf X}={\bf f}({\bf X})$ is of central interest for these models. Etessami and Yannakakis [J. ACM, 56 (2009), pp. 1–66] have suggested a particular version of Newton's method to approximate $\mu{\bf f}$. We extend a result of Etessami and Yannakakis and show that Newton's method starting at ${\bf 0}$ always converges to $\mu{\bf f}$. We obtain lower bounds on the convergence speed of the method. For so-called strongly connected SPPs we prove the existence of a threshold $k_{{\bf f}}\in\mathbb{N}$ such that for every $i\geq0$ the $(k_{{\bf f}}+i)$th iteration of Newton's method has at least i valid bits of $\mu{\bf f}$. The proof yields an explicit bound for $k_{{\bf f}}$ depending only on syntactic parameters of ${\bf f}$. We further show that for arbitrary SPP equations, Newton's method still converges linearly: there exists a threshold $k_{{\bf f}}$ and an $\alpha_{{\bf f}}>0$ such that for every $i\geq0$ the $(k_{{\bf f}}+\alpha_{{\bf f}}\cdot i)$th iteration of Newton's method has at least i valid bits of $\mu{\bf f}$. The proof yields an explicit bound for $\alpha_{{\bf f}}$; the bound is exponential in the number of equations in ${\bf X}={\bf f}({\bf X})$, but we also show that it is essentially optimal. The proof does not yield any bound for $k_{{\bf f}}$, but only proves its existence. Constructing a bound for $k_{{\bf f}}$ is still an open problem. Finally, we also provide a geometric interpretation of Newton's method for SPPs.

Monotone systems of polynomial equations (MSPEs) are systems of fixed-point equations $X_1 = f_1(X_1, ..., X_n),$ $..., X_n = f_n(X_1, ..., X_n)$ where each $f_i$ is a polynomial with positive real coefficients. The question of computing the least non-negative solution of a given MSPE $\vec X = \vec f(\vec X)$ arises naturally in the analysis of stochastic models such as stochastic context-free grammars, probabilistic pushdown automata, and back-button processes. Etessami and Yannakakis have recently adapted Newton's iterative method to MSPEs. In a previous paper we have proved the existence of a threshold $k_{\vec f}$ for strongly connected MSPEs, such that after $k_{\vec f}$ iterations of Newton's method each new iteration computes at least 1 new bit of the solution. However, the proof was purely existential. In this paper we give an upper bound for $k_{\vec f}$ as a function of the minimal component of the least fixed-point $μ\vec f$ of $\vec f(\vec X)$. Using this result we show that $k_{\vec f}$ is at most single exponential resp. linear for strongly connected MSPEs derived from probabilistic pushdown automata resp. from back-button processes. Further, we prove the existence of a threshold for arbitrary MSPEs after which each new iteration computes at least $1/w2^h$ new bits of the solution, where $w$ and $h$ are the width and height of the DAG of strongly connected components.

Monotone systems of polynomial equations (MSPEs) are systems of fixed-point equations X1 = f1(X1, ..., Xn), ..., Xn = fn(X1, ..., Xn) where each fi is a polynomial with positive real coefficients. The question of computing the least non-negative solution of a given MSPE X = f(X) arises naturally in the analysis of stochastic context-free grammars, recursive Markov chains, and probabilistic pushdown automata. While the Kleene sequence f(0), f(f(0)), ... always converges to the least solution mu.f, if it exists, the number of iterations needed to compute the first i bits of mu.f may grow exponentially in i.Etessami and Yannakakis have recently adapted Newton's iterative method to MSPEs and proved that the Newton sequence converges at least as fast as the Kleene sequence and exponentially faster in many cases.They conjecture that, given an MSPE of size m, the number of Newton iterations needed to obtain i accurate bits of mu.f grows polynomially in i and m. In this paper we show that the number of iterations grows linearly in i for strongly connected MSPEs and may grow exponentially in m for general MSPEs.