Satellite Event: INFINIS Meeting

As a satellite event of WoLLIC 2012 a meeting of INFINIS French-Argentinean Laboratory will be hosted on Friday, September 7th. INFINIS is a French-Argentinean Laboratory (Laboratoire Internationale Associé) between Centre National de la Recherche Scientifique (CNRS) and Université Paris Diderot, on the one hand, and Consejo Nacional de Investigaciones Científicas y Técnicas (CONICET) and the Universidad de Buenos Aires, on the other. It is devoted to research in Computer Science. Specific focus is placed on formal methods, for modeling, verification and development of complex software artifacts.

Time and Place

The meeting will take place at Aula 7 of the Departamanto de Computación (Pabellón I, Ciudad Universidaria), of the Facultad de Ciencias Exactas y Naturales, de la Universidad de Buenos Aires, from 9am to 14am on September 7th.

Program

09:00 to 09:30 Anca Muscholl
09:30 to 10:00 Lorijn van Rooijen
10:00 to 10:30 Gabriel Senno
10:30 to 11:00 Carlos Lombardi
11:00 to 11:30 Coffee Break
11:30 to 12:00 Pablo Heiber
12:00 to 12:30 Veronica Becher
12:30 to 13:00 Ezequiel Orbe
13:00 to 13:30 Guillaume Hoffmann

Speaker: Anca Muscholl
Title: On distributed control and monitoring
Abstract: In this survey we discuss verification issues in the setting of distributed finite-state systems. Verifying the correctness of such systems is known to be a very challenging task, for which current techniques are much less advanced than for sequential systems. First we will consider the control problem for finite-state processes synchronizing via shared variables, a particular instance of distributed synthesis. Its decidability status is one the main open problems in this area. Then we consider the monitoring problem, where we are interested in properties that can be monitored locally on such systems. We propose a distributed framework for monitoring issued from topological considerations.

Speaker: Lorijn van Rooijen
Title: The separation problem for group languages
Abstract: In this talk, we regard regular languages from an algebraic point of view, via recognition by finite monoids. Pseudovarieties of finite monoids correspond to classes of regular languages. A question related to the expressiveness of these classes is the so-called separation problem: For which pairs of disjoint regular languages L and L', does a language K in the considered class exist, such that L ⊆ K and L' ∩ K = ∅?
We will explain the algebraic point of view and we will focus on the class of languages recognized by finite groups. It is known that two languages are separable by a group language if and only if their closures in the free group, with respect to the Hall topology, are disjoint.
We exploit this in order to obtain a separating group language in an algorithmic fashion. In [Aui05], a proof is given for the Ribes and Zaleski product theorem. We show that this proof can be converted into a construction giving such a separating group language.
References: [Aui05] B. Auinger, K. Steinberg. A constructive version of the Ribes-Zalesski product theorem. Mathematische Zeitschrift, 250(2):287–297, 2005.

Speaker: Gabriel Senno
Title: Linearizing Bad Sequences: Upper Bounds for the Product and Majoring Well Quasi-orders
Abstract: Well quasi-orders (wqo’s) are an important mathematical tool for proving termination of many algorithms. Under some assump- tions upper bounds for the computational complexity of such algorithms can be extracted by analyzing the length of controlled bad sequences. We develop a new, self-contained study of the length of bad sequences over the product ordering of Nn , which leads to known results but with a much simpler argument.
We also give a new tight upper bound for the length of the longest con- trolled descending sequence of multisets of Nn , and use it to give an upper bound for the length of controlled bad sequences in the majoring order- ing of sets of tuples. We apply this upper bound to obtain complexity upper bounds for decision procedures of automata over data trees. In both cases the idea is to linearize bad sequences, i.e. transform them into a descending one over a well-order for which upper bounds can be more easily handled.

Speaker: Carlos Lombardi
Title: Normalisation for Dynamic Pattern Calculi
Abstract: The Pure Pattern Calculus (PPC) extends the Lambda Calculus, as well as the family of algebraic pattern calculi with first-class patterns, i.e. patterns can be passed as arguments, evaluated and returned as results. The notion of *matching failure* of PPC not only provides a mechanism to define functions by pattern matching on cases but also supplies it with parallel-or-like, non-sequential behaviour. Therefore, devising normalising strategies for PPC to obtain well-behaved implementations turns out to be challenging.
This talk focuses on normalising reduction strategies for PPC. We define a (multistep) strategy and show that it is normalising. The strategy generalises the leftmost-outermost strategy for Lambda Calculus and is strictly finer than parallel-outermost. The normalisation proof is based on the notion of *necessary set of redexes*, a generalisation of the notion of needed redex encompassing non-sequential reduction systems.
This is joint work with with Eduardo Bonelli, Delia Kesner and Alejandro Ríos and was presented at RTA 2012.

Speaker: Pablo Heiber
Title: Normality and Finite Automata
Abstract: We generalize known results about compression of normal sequences with finite automata. We investigate the question of how much computational power is needed to compress a normal sequence. We prove that the following automata cannot compress normal sequences, even under relaxed conditions:

• Non-deterministic finite automata
• k-counter real time non-deterministic finite automata
• Two-way deterministic finite automata

This is joint work with Verónica Becher and Olivier Carton.

Speaker: Verónica Becher
Title: On the descriptive complexity of defining the set of normal numbers
Abstract: A fairly new result proves that the set of normal numbers in a given base is complete for the class of real numbers definable with two alternations of quantifiers. We will discuss our new results and conjectures in this direction.
This is joint work with Pablo Heiber and Theodore Slaman.

Speaker: Ezequiel Orbe
Title: Symmetries in Modal Logic
Abstract: In this talk, I will introduce the notion of symmetries in modal logics. I will present a brief introduction of the topic of symmetries in other logics and how we can take advantage of them in automated deduction. Finally I will present some theoretical results concerning symmetries in modal logics using coinductive modal models and discuss our current research work.

Speaker: Guillaume Hoffmann
Title: Complexity results for the Model Checking problems of four Frame-Changing Modal Logics
Abstract: Modal Logics are traditionally interpreted on Kripke models, constituted of a graph (called "frame") and a valuation function that decorates the graphs with sets of true propositional symbols. Usually, evaluating a modal formula in a model only requires moving from one point to another, without changing anything. One well-studied exception to that tradition is the down-arrow binder of hybrid logics, that can dynamically modify the valuation of certain propositional symbols.
We study dynamic modal operators that can change the frame of the model during the evaluation of a formula. In particular, we extend the basic modal language with modalities that are able to swap, delete or add pairs of related elements of the domain, while traversing an edge of the accessibility relation. We study these languages together with the sabotage modal logic, which can arbitrarily delete edges of the model.
We show that the complexity of their model checking problems is PSpace-complete. We also consider versions of the model checking problems where the model is fixed (formula complexity), and when the formula is fixed (program complexity).