19TH INTERNATIONAL CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING

ALFA Accepted Papers with Abstracts

Gerhard Rosenberger (University Passau)
Growth in Hecke groups

ABSTRACT. 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.

Zoltan Esik (University of Szeged)
Some algebraic means for characterizing logics

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

Christoph Weidenbach (Max-Planck-Institut für Informatik)
Automata Reasoning via First-Order Superposition

ABSTRACT. 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.

Manfred Kufleitner (University of Stuttgart)
Ehrenfeucht-Fraisse Games on Omega-Terms

ABSTRACT. 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.

Maximilian Schlund (Technische Universität München)
Newton's Method on Commutative Semirings, Tree Dimension, and Applications

ABSTRACT. 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.

Andreas Krebs (Universitat Tübingen)
Algebraic Characterization of the Alternation Hierarchy in FO2[<] on Finite Words

ABSTRACT. We characterize the languages in the individual levels of the quantifier alternation hierarchy of first-order logic with two variables in terms of two-sided semidirect products, and by identities. This implies decidability of the individual levels. More generally we show that the two-sided semidirect products with J as the right-hand factor preserves decidability.

Martin Leucker (University of Lübeck)
Runtime Verification with Data

ABSTRACT. Several approaches for verifying properties involving data at runtime are reviewed. Starting with a typical, mainly academic account to runtime verification based on linear temporal logic (LTL) we present existing extensions such as LTL with parameterized propositions and first-order LTL. Moreover, we compare these approaches with further frameworks such as LOLA, RuleR and Eagle. The goal is to give a comprehensive picture of runtime verification in the light of data values.

Aniello Murano (Università degli Studi di Napoli Federico II)
Strategic Reasoning in Formal Verification

ABSTRACT. 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.

Marijn Heule (University of Texas at Austin)
Software model synthesis using satisfiability solvers

ABSTRACT. 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.