ALFA ON SATURDAY, DECEMBER 14TH, 2013

We provide an overview of certain algebraic approaches for the characterization of the expressive power of logics on words and trees.

We introduce a novel approach for synthesis of software models based on identifying deterministic finite state automata. Our approach consists of three important contributions. First, we argue that in order to model software, one should focus mainly on observed executions (positive data), and use the randomly generated failures (negative data) only for testing consistency. We present a new greedy heuristic for this purpose, and show how to integrate it in the state-of-the-art evidence-driven state-merging (EDSM) algorithm. Second, we apply the enhanced EDSM algorithm to iteratively reduce the size of the problem. Yet during each iteration, the evidence is divided over states and hence the effectiveness of this algorithm is decreased. We propose—when EDSM becomes too weak—to tackle the reduced identification problem using satisfiability solvers. Third, in case the amount of positive data is small, we solve the identification problem several times by randomizing the greedy heuristic and combine the solutions using a voting scheme. The interaction between these contributions appeared crucial to solve hard software models synthesis benchmarks. Our implementation, called DFASAT, won the StaMinA competition.

Joint work with Sicco Verwer.

In open systems verification, to formally check for reliability, one needs an appropriate formalism to model the interaction between agents and express the correctness of the system no matter how the environment behaves. Important contributions in this context are given by module checking (a.k.a., module checking of open systems) and modal logics for strategic ability, in the setting of multi-agent games, such as ATL, ATL*, and the like. In this talk, I will first recall and compare these two different approaches. Then, I will introduce Strategy Logic (SL) as a powerful logic framework for reasoning explicitly about strategies in multi-agent concurrent games, which includes both. In particular, I will mainly discuss about the model checking and the satisfiability questions for SL. As a key aspect, SL uses first-order quantifications over strategies, where strategies are not glued to a specific agent, but an explicit binding operator allows to bind an agent to a strategy variable. Notably, this allows agents to share strategies or reuse one previously adopted. ****

The talk is based on papers mainly done with Fabio Mogavero and Moshe Y. Vardi.

For various classes of automata, their reachability problem can be encoded as an unsatisfiability problem in a respective first-order Horn fragment. In this talk I will recapitulate results about this relationship and discuss potential mutual benefits exploiting this relationship.

For the Hecke groups we determine and collect a number of growth functions, their generating series and growth rates: numbers of elements of a given length, numbers of subgroups of a certain index, numbers of normal subgroups, numbers of normal subgroups of genus one and numbers of free subgroups. Depending on the type of these growth functions, we calculate the corresponding generating series or the generating Dirichlet series. A particular emphasis is put on explicit formulas representing these series as rational functions or via Euler product decompositions.

Recently we have proven a new theorem on the convergence speed for Newton's method on commutative semirings (presented at LATA 2013). In this talk I want to discuss the theorem and the techniques used in the proof, in particular the notion of the dimension of a derivation tree (aka. Horton-Strahler number), together with some new recent work: the tree-dimension has nice applications both in graph theory (it is related to the path-width of a tree), as well as in computational linguistics where it can be used for more accurate and faster statistical parsing.

This is joint work with Michael Luttenberger and Javier Esparza.

Fragments of first-order logic over words can often be characterized in terms of finite monoids or finite semigroups. Usually these algebraic descriptions yield decidability of the question whether a given regular language is definable in a particular fragment. An effective algebraic characterization can be obtained from identities of so-called omega-terms. In order to show that a given fragment satisfies some identity of omega-terms, one can use Ehrenfeucht-Fraisse games on word instances of the omega-terms. The resulting proofs often require a significant amount of book-keeping with respect to the constants involved. In this paper we introduce Ehrenfeucht-Fraisse games on omega-terms. To this end we assign a labeled linear order to every omega-term. Our main theorem shows that a given fragment satisfies some identity of omega-terms if and only if Duplicator has a winning strategy for the game on the resulting linear orders. This allows to avoid the book-keeping. As an application of our main result, we show that one can decide in exponential time whether all aperiodic monoids satisfy some given identity of omega-terms, thereby improving a result of McCammond (Int. J. Algebra Comput., 2001).

This is joint work with Martin Huschenbett.