CSL 2017: 26TH EACSL ANNUAL CONFERENCE ON COMPUTER SCIENCE LOGIC
PROGRAM FOR WEDNESDAY, AUGUST 23RD
Days:
previous day
next day
all days

View: session overviewtalk overview

09:00-10:00 Session 16: Invited Talk
Chair:
Location: De Geer Salen
09:00
Arithmetic Circuits: An Overview
SPEAKER: Meena Mahajan

ABSTRACT. This talk reviews recent developments in algebraic complexity theory. It outlines some major results concerning structure, completeness, closure, and lower bounds. It describes some techniques that have been central to obtaining these results, including extreme depth reduction, partial derivatives, and padding.

10:30-12:30 Session 17: Automata
Location: De Geer Salen
10:30
On the (In)Succinctness of Muller Automata
SPEAKER: Udi Boker

ABSTRACT. There are several types of finite automata on infinite words, differing in their acceptance conditions. As each type has its own advantages, there is an extensive research on the size blowup involved in translating one automaton type to another.

Of special interest is the Muller type, providing the most detailed acceptance condition. It turns out that there is inconsistency and incompleteness among the literature results regarding the translations to and from Muller automata. Considering the automaton size, some results take into account, in addition to the number of states, the alphabet length and the number of transitions while ignoring the length of the acceptance condition, whereas other results consider the length of the acceptance condition while ignoring the two other parameters.

We establish a full picture of the translations to and from Muller automata, enhancing known results and adding new ones. Overall, Muller automata can be considered less succinct than parity, Rabin, and Streett automata: translating nondeterministic Muller automata to the other nondeterministic types involves a polynomial size blowup, while the other way round is exponential; translating between the deterministic versions is exponential in both directions; and translating nondeterministic automata of all types to deterministic Muller automata is doubly exponential, as opposed to a single exponent in the translations to the other deterministic types.

11:00
Query Learning of Derived Omega-Tree Languages in Polynomial Time
SPEAKER: Dana Fisman

ABSTRACT. We present the first polynomial time algorithm to learn nontrivial classes of languages of infinite trees.

Specifically, our algorithm uses membership and equivalence queries to learn classes of omega-tree languages derived from weak regular omega-word languages in polynomial time. The method is a general polynomial time reduction of learning a class of derived omega-tree languages to learning the underlying class of omega-word languages, for any class of omega-word languages recognized by a deterministic Büchi acceptor. Our reduction, combined with the polynomial time learning algorithm of Maler and Pnueli [15] for the class of weak regular omega-word languages yields the main result.

We also show that subset queries that return counterexamples can be implemented in polynomial time using subset queries that return no counterexamples for deterministic or nondeterministic finite word acceptors, and deterministic or non-deterministic Büchi omega-word acceptors.

A previous claim of an algorithm to learn regular omega-trees due to Jayasrirani, Begam and Thomas [11] is unfortunately incorrect, as shown in [4].

11:30
Advice Automatic Structures and Uniformly Automatic Classes

ABSTRACT. We study structures that are automatic with advice. These are structures that admit a presentation by finite automata (over finite or infinite words or trees) with access to an additional input,called an advice. Over finite words, a standard example of a structure that is automatic with advice, but not automatic in the classical sense, is the additive group of rational numbers (Q,+). By using a set of advices rather than a single advice, this leads to the new concept of a parameterised automatic presentation as a means to uniformly represent a whole class of structures. The decidability of the first-order theory of such a uniformly automatic class reduces to the decidability of the monadic second-order theory of the set of advices that are used in the presentation. Such decidability results also hold for extensions of first-order logic by regularity preserving quantifiers, such as cardinality quantifiers and Ramsey quantifiers. To investigate the power of this concept, we present examples of structures and classes of structures that are automatic with advice but not without advice, and we prove classification theorems for the structures with an advice automatic presentation for several algebraic domains. In particular, we prove that the class of all torsion-free Abelian groups of rank one is uniformly omega-automatic and that there is a uniform omega-tree-automatic presentation of the class of all Abelian groups up to elementary equivalence and of the class of all countable divisible Abelian groups. On the other hand we show that every uniformly omega-automatic class of Abelian groups must have bounded rank. While for certain domains, such as trees and Abelian groups, it turns out that automatic presentations with advice are capable of presenting significantly more complex structures than ordinary automatic presentations, there are other domains, such as Boolean algebras, where this is provably not the case. Further, advice seems to not be of much help for representing some particularly relevant examples of structures with decidable theories, most notably the field of reals. Finally we study closure properties for several kinds of uniformly automatic classes, and decision problems concerning the number of non-isomorphic models in uniformly automatic classes with the unique representation property.

12:00
CALF: Categorical Automata Learning Framework

ABSTRACT. Automata learning is a technique that has successfully been applied in verification, with the automaton type varying depending on the application domain. Adaptations of automata learning algorithms for increasingly complex types of automata have to be developed from scratch because there was no abstract theory offering guidelines. This makes it hard to devise such algorithms, and it obscures their correctness proofs. We introduce a simple category-theoretic formalism that provides an appropriately abstract foundation for studying automata learning. Furthermore, our framework establishes formal relations between algorithms for learning, testing, and minimization. We illustrate its generality with two examples: deterministic and weighted automata.

14:00-15:00 Session 18: Process Algebra and Concurrency
Location: De Geer Salen
14:00
Precongruence Formats with Lookahead through Modal Decomposition
SPEAKER: Wan Fokkink

ABSTRACT. Bloom, Fokkink & van Glabbeek (2004) presented a method to decompose formulas from Hennessy-Milner logic with regard to a structural operational semantics specification. A term in the corresponding process algebra satisfies a Hennessy-Milner formula if and only if its subterms satisfy certain formulas, obtained by decomposing the original formula. They used this decomposition method to derive congruence formats in the realm of structural operational semantics. In this paper it is shown how this framework can be extended to specifications that include bounded lookahead in their premises. This extension is used in the derivation of a congruence format for the partial trace preorder.

14:30
Strategies with Parallel Causes
SPEAKER: unknown

ABSTRACT. In a distributed game we imagine a team Player engaging a team Opponent in a distributed fashion. Such games and their strategies have been formalised within event structures. However there are limitations in founding strategies on traditional event structures. Sometimes a probabilistic distributed strategy relies on certain benign races where, intuitively, several members of team Player may race each other to make a common move. Although there are event structures which support such parallel causes, in which an event is enabled in several compatible ways, they do not support an operation of hiding central to the composition of strategies; nor do they support probability adequately. An extension of traditional event structures is devised which supports parallel causes and hiding, as well as the mix of probability and nondeterminism needed to account for probabilistic distributed strategies. The extension is located within existing models for concurrency and tested in the construction of a bicategory of probabilistic distributed strategies with parallel causes. The bicategory is rich in operations relevant to probabilistic as well as deterministic parallel programming.