Schedule of the meeting[.ics]

This meeting is supported by the ANR projects AMIS and FREC

Program

Thursday January the 24th, 2013

13:30 - 14:00Coffee break
14:00 - 15:00Matthew Hague, C-SHORe: A Collapsible Approach to Higher-Order Model-Checking

We study the model-checking problem for models of higher-order programs. In particular, via higher-order recursion schemes and their connection to collapsible pushdown systems. We present a saturation method for global backwards reachability analysis of these models. Beginning with an automaton representing a set of configurations, we build an automaton accepting all configurations that can reach this set. We have implemented this technique, and will comment on some of our optimisation techniques and preliminary results.

This is joint work with C. Broadbent, A. Carayol and O. Serre in Paris.

15:00 - 15:15Coffee break
15:15 - 16:15Axel Haddad, Revisiting Gobal Model Checking and Logical Selection

We study two problems that generalise model-checking of higher order recursion schemes: logical reflection and logical selection. The two problems ask to transform a scheme so that the generated tree is marked by a set of nodes satisfying a given logical formula. The only known decidability results for those problems were obtained using collapsible pushdown automata. The drawback of going back and forth between collapsible pushdown automata and schemes is that the resulting scheme has no structural similarities with the original one. We circumvent this drawback by providing new proofs of the decidability of logical reflection and logical selection without appealing to collapsible pushdown automata presenting a scheme-shape-preserving solution. As a side result we also give a denotational semantics for the μ-calculus on recursion schemes.

16:15 - 16:30Coffee break
16:30 - 17:30Géraud Sénizergues, lAlBlC: a program testing the equivalence of dpda's.

We present a preliminar version of the program "lAlBlC" (i.e. lA=lB? let us Compute).

The equivalence problem for dpda consists in deciding, for two given deterministic pushdown automata A,B, whether they recognize the same language. It was proved in [TCS 2001, G.S.] that this problem is decidable by means of some complete proof systems.

The program lAlBlC gives, in some sense, life to the above completeness proof: on an input A,B, the program computes either a proof of their equivalence (w.r.t. to the system D5 of the above reference) or it computes a witness of their non-equivalence (i.e. a word that belongs to the symmetric difference of the two languages).

We shall outline the main mathematical objects that are manipulated as well as the main functions performed over these objects and, finally, describe some experimental results.

The talk is based on an ongoing, joint, work with P. Henry.

20:00Meeting dinner

Friday January the 25th, 2013

09:30 - 10:30Paul-André Melliès, tba
10:30 - 11:00Coffee break
11:00 - 12:00Antoine Meyer, Higher-order automatic graphs

Families of trees and graphs generated by various classes of higher-order pushdown automata have recently received a lot of attention. Important results include their equi-expressivity with higher-order program schemes as generators of infinite trees, and the characterization of the winning regions of parity games played over their transition graphs using natural notions of regular sets of higher-order stacks.

In a 2007 paper, Colcombet and Löding proposed a higher-order generalization of tree-automatic graphs using weak monadic second-order finite sets interpretations. Just as any (order 1) tree-automatic graph may be obtained by finite sets interpretation from the full binary tree (or equivalently from the graph of an order 1 pushdown automaton), order n tree-automatic graphs are those obtained via the same operation applied to an order n pushdown graph.

In this work, relying on the above-mentioned results on higher-order pushdown graphs and trees, we propose a direct automata-theoretic characterization of Colcombet and Löding's tree-automatic-like hierarchy. This characterization coincides at order 1 with the usual definition of tree-automatic graphs. As an application, we characterize the languages of order n tree-automatic graphs seen as infinite automata.

This is joint (ongoing) work with Arnaud Carayol.

12:00 - 14:00Lunch break
14:00 - 15:00Igor Walukiewicz, Evaluation is MSOL compatible

We consider simply-typed lambda calculus with fixpoint operators. Evaluation of a term gives as a result the Bohm tree of the term. We show that evaluation is compatible with monadic second-order logic (MSOL). This means that for a fixed finite vocabulary of terms, the MSOL properties of Bohm trees of terms are effectively MSOL properties of terms themselves. Theorems of this kind have been known for some graph operations: unfolding, and Muchnik iteration. Similarly to those results, our main theorem has diverse applications. It can be used to show decidability results, to construct classes of graphs with decidable MSOL theory, or to obtain MSOL formulas expressing properties of terms. Another application is decidability of a control-flow synthesis problem.

Joint work with S. Salvati

15:00 - 15:30Coffee break
15:30 - 16:30Sylvain Salvati, Finite models and properties of simply typed λY-calculus

Simply typed lambda Y-calculus is a very simple programming language that can be seen as a subset of PCF. It is nevertheless presenting some practical interest for at least two scientific communities: formal language theory and program verification. A natural way of approaching the properties of λY-terms in those two contexts is by using finite models. This approach presents several advantages, it gives very simple decision procedures and simple ways of transforming grammars/programs.

In this talk, we are going to present finite monotonous models of λY-calculus. We show their interest and limitations in the context of formal language theory and program verification. We then give some direction so as to overcome some of their limitations.

This work is partially joint with G. Kobele and I. Walukiewicz

16:30 - 17:00Discussion

Participants

Venue

The meeting is taking place in the seminar room LIGM (University of Paris-Est) which is at the fourth floor of the Copernic Building (file with direction to LIGM [.pdf]). You can reach LIGM from Paris by taking RER A and leave the train at the station Noisy-champs (check the train is stopping at Noisy-champs before taking it). If you arrive with TGV at Marne-la-Vallée-Chessy, you can also reach LIGM using RER A. The following map gives the direction to reach LIGM from RER A Noisy-champs station.


Enlarge the map

Contact