Gene Regulatory Network (GRN), made of interacting regulators like DNA, RNA, proteins and their complexes, controls the expression levels of mRNA and proteins. GRNs govern several cellular processes such as metabolism, signaling, cell-differentiation, division, cycle arrest in response to DNA damage, and apoptosis.

Understanding dynamics of GRNs by introducing accurate models, then applying efficient mathematical/computational methods for their analysis is useful in identifying the underlying mechanisms of normal and abnormal cell functioning and hence developing drugs against diseases including cancer.

Bistability and oscillations are two crucial nonlinear dynamical behaviors observed in diverse areas of biological systems, in particular, gene regulatory networks. As in many others including electrical systems, bistability and oscillation phenomena appear as consequences of specific patterns of interactions such as positive/negative feedback loops among the components of GRN and have a certain function on the control of gene expression to regulate cellular processes and adaptation to changing environment. Bistability in GRN is a biological switching mechanism accompanied with hysteresis. It appears in a wide variety of GRNs including the lac operon of Escherichia coli, responsible for controlling the lactose metabolism under glucose starvation. Bistable genetic switches with their hysteresis characteristics behave as ON/OFF controllers avoiding unnecessary transitions between induced and uninduced states of the associated operon. Moreover, the oscillations in GRN, like circadian rhythm and 2-phase dynamics of tumor suppressor p53 network, are essentially of relaxation type providing constant amplitude and period, possessing self-sustaining property and ability of synchronization to the environmental inputs and interlinked networks.

The talk will present a series of studies on bifurcation and local stability analysis of some primary examples of bistable switches and relaxation oscillators appearing in GRNs.

In this talk, I will argue that some natural questions on the expressive power of typed λ-calculi (minimalistic functional programming languages) actually pertain not to programming languages, but to automata theory (or “finite-state computation”). After briefly mentioning the results in my PhD thesis on type systems based on linear logic, I will explain how recursion schemes and transducer theory motivate a conjecture on the functions definable in the simply typed λ-calculus (in a certain way that goes back at least to Statman’s work in the 1980s, but about which very little is known).

This is joint work with Pierre Pradic (Swansea University).

Enumeration algorithms are algorithms whose goal is to

output the set of all solutions to a given problem. There exists

different measures for the quality of such algorithm, whose relevance

depends on what the user wants to do with the solutions set.

If the goal of the user is to explore a subset of solutions or to

transform the solutions as they are outputted with a stream-like

algorithm, a relevant measure of the complexity in this case is the

delay, that is, the maximal time between the output of two distinct

solutions. Following this line of thoughts, significant efforts have

been made by the community to design polynomial delay algorithms, that

is, algorithms whose delay between the output of two new solutions is

polynomial in the size of the input.

While this measure is interesting, it is not always completely

necessary to have a bound on the delay and it is enough to ask for a

guarantee that running the algorithm for O(t poly(n)) will produce at

least t solutions. While algorithms having this property can be

transformed into polynomial delay algorithm, the naive transformation

may result in a blow up in the space used by the enumerator.

In this talk, we will present a new technique that allow to transform

such algorithms into polynomial delay algorithm with only a polynomial

overhead on the space.

In this paper we consider two different views of the model checking problems for the Linear Temporal Logic (LTL).

- On the one hand, we consider the
*universal model checking problem for LTL*, where one asks that for a given system and a given formula that all the runs of the system satisfy the formula.
On the other hand, *fair model checking problem for LTL* asks that for a given system and a given formula almost-all the runs of the system satisfy the formula.

It was shown that these two problems have the same theoretical complexity i.e. PSPACE

complete. The question arises whether one can find a fragment of LTL for which the complexity of these two problems differ. One such fragment was identified in a previous work, namely the *Muller fragment*.

We address a similar comparison for the prompt fragment of LTL (pLTL). pLTL extends LTL

with an additional operator, i.e. the *prompt-eventually*. This operator ensures the existence of a bound such that liveness properties are satisfied within this bound.

We show that the corresponding Muller fragment for pLTL does not enjoy the same algorithmic

properties with respect to the comparison considered. We also identify a new expressive fragment for which the fair model checking is faster than the universal one.

The long title : a modest proposal for preventing teacher to think too hard when evaluating student’s programmatic feast.

Therein the speaker, the honourable Benoît Barbot shall enlighten us on the theory and practice of Boltzmann sampling, before reporting on the masterful application in automated evaluation of student’s programming skills in functional programming.

The title is a reference to the excellent essay of Dr J. Swift.

https://en.wikipedia.org/wiki/A_Modest_Proposal

As almost everybody knows, deciding whether a given graph is colourable using 3 colours is an NP-hard problem which means that *finding* a 3-colouring of a graph that is *promised* to be 3-colourable cannot be achieved in polynomial time, unless P = NP.

But how hard is to find a colouring of such a graph using 4, 5, 6, or more colours?

Surprisingly little is known to that account — it has only recently (in 2019) been shown that finding a 5-colouring of a given 3-colourable graph is NP-hard, while the best known polynomial algorithm, due to Kawarabayashi and Thorup, uses a little less than $O(n^{1/5})$ colours where $n$ is the number of vertices of the input graph.

We will present several recent advancements on this problem, and their relevance to a wider scope of *promise constraint satisfaction*.

The promise constraint satisfaction problem is a natural generalisation of both the above promise version of graph colouring and the constraint satisfaction problem (CSP). This generalised, promise variant gained a substantial attention in recent years due to generalisation of algebraic techniques behind the theory of CSP, that lead to the famous CSP dichotomy, to the promise setting.

One important research endeavour at the intersection of circuit complexity theory, algebraic automata theory and logic is the *classification of regular languages according to their localisation within the internal structure* of NC^{1}, the class of languages decided by *Boolean circuits of polynomial size, logarithmic depth and with gates of constant fan-in*. In some sense, the search for such a classification concentrates most of the open questions we have about the relationship between NC^{1} and its well-studied subclasses.

While many questions are still open, one of the greatest successes of this research endeavour has been the characterisation of the regular languages in AC^{0}, the subclass of NC^{1} corresponding to Boolean circuits of polynomial length, constant depth and with gates of unbounded fan-in. This characterisation takes the form of a triple languages-algebra-logic correspondence: a regular language is in AC^{0} if, and only if, its syntactic morphism is quasi-aperiodic if, and only if, it is definable in first-order logic over words with linear order and modular predicates.

It is natural to try to extend such results to classes of formal languages greater than the class of regular languages. A well studied and robust such class is given by visibly pushdown languages (VPLs): languages recognised by pushdown automata where the stack-height-behaviour only depends on the letters read from the input. Over the previous decade, a series of works concentrated on the fine complexity of VPLs, with several achievements: one of those was a characterisation of the class of visibly counter languages (basically VPLs recognised by visibly pushdown automata with only one stack symbol) in AC^{0} by Krebs, Lange and Ludwig. However, the characterisation of the VPLs in AC^{0} still remains open.

In this talk, I shall present a conjectural characterisation of the VPLs in AC^{0} obtained with Stefan Göller at the Universität Kassel. It is inspired by the conjectural characterisation given by Ludwig in his Ph.D. thesis as a generalisation of the characterisation for visibly counter languages, but that is actually false. In fact, we give a more precise general conjectural characterisation that builds upon recognisability by morphisms into Ext-algebras, an extension of recognisability by monoid-morphisms proposed by Czarnetzki, Krebs and Lange to suit the case of VPLs. This characterisation classifies the VPLs into three categories according to precise conditions on the Ext-algebra-morphisms that recognise them:

- those that are TC
^{0}-hard;
- those that are in AC
^{0};
- those that correspond to a well-identified class of “intermediate languages” that we believe to be neither in AC
^{0} nor TC^{0}-hard.

Parity games are well-known infinite two-player games played on finitely colored graphs. We define an extension of parity games, called counter games, where each player can at every move, increment or reset a finite number of counters.

We examine several types of winning conditions that are linked to the boundedness of the counters of the game, and to parity conditions. For every type of winning conditions examined, we give algorithmic complexity results, and results on the size of the memory needed to win. For example, we show that deciding whether Eve can force one of the counters to be bounded can be done in polynomial time, and that, if Eve wins, then Eve has a memoryless winning strategy.

The results in this talk are joint work with Emmanuel Filiot.