## Le LMF recherche un·e administrateur·trice systèmes et réseaux

Localisation :

École Normale Supérieure de Paris-Saclay &
Université Paris-Saclay
Plateau du Moulon, Gif-sur-Yvette (91)

Mode de recrutement : Un concours externe du CNRS conférant le statut d'Ingénieur·e d'Études (fonctionnaire)

Mission rattachée au poste : L'ingénieur·e d'études recruté·e sera responsable du service informatique du Laboratoire Méthodes Formelles (LMF), sa mission sera de concevoir et déployer les infrastructures matérielles et logicielles du laboratoire, en veillant à leur cohérence, qualité et sécurité. Il/elle sera garant·e du bon fonctionnement du service informatique de l’unité et du soutien apporté aux utilisateurs.

Contexte : Le Laboratoire Méthodes Formelles (LMF) est né le 1er janvier 2021 de la volonté politique de ses tutelles - Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria et CentraleSupélec - de créer un pôle ciblé sur les méthodes formelles. Le LMF est formé du Laboratoire Spécification et Vérification (LSV) et de l’équipe Vals du Laboratoire de Recherche en Informatique (LRI) soit une centaine de personnes.

Le LMF est un laboratoire de recherche en informatique, Read more...

## Deciding the Logic of Subsequences

Contact: Philippe Schnoebelen

The logic of subsequences is the logic of the structure {$(X^*;\leq_*,..)$} where the universe {$X^*$} contains all finite sequences over some base set {$X$}, and where {$\leq_*$} is the subsequence relation (as in Higman's Lemma).

For example, this logic allows writing constraints like {$$\tag{\phi} {aa}\leq_* x \land {bb}\leq_* x \land {ab}\not\leq_* x$$} where {$a,b$} are letters and {$x$} is a variable standing for an unknown word. Over {$X=\{a,b\}$}, the two-letter alphabet, the solution set of the above constraint is the language {$L_\phi={bbb}^*{aaa}^*$}.

The logic allows more complex formulae, like

\begin{equation*} \tag{$\psi$} \forall x,y: \exists z: \bigl( x\leq_* z\land y\leq_* z \land \forall u: x\leq_* u\land y\leq_* u\implies z\leq_* u \bigr) \end{equation*} that states that {$(X^*,\leq_*)$} is an upper semilattice. Whether {$\psi$} is true or false depends on {$X$}.

The goal of this Master Internship is to develop the computational theory of the logic of subsequences, especially by identifying decidable fragments of the logic and assessing their algorithmic complexity.

Until recently, not much was known about the decidability of the logic of subsequences and its fragment [Kus06]. It was then shown that the {$\Sigma_2$} fragment is undecidable (as expected) [KS15], that the {$\mathrm{FO}^2$} fragment is decidable, even elementary [KS16], and that the {$\Sigma_1$}, or existential, fragment is undecidable [HSZ17]. That last result was completely unexpected and has potential far-reaching consequences for existential logics on graphs.

Regarding the {$\mathrm{FO}^2$} fragment, the initial decidability result raised many new questions. In particular there are several interesting directions in which to try to extend the decidability. Among these, the following seem to be good starting points for the M2R internship:

• Extending the decidability of the {$\mathrm{FO}^2$} fragment by allowing combination with other (simple) predicates like {$\leq_{*,1}$} defined via "{$x\leq_{*,1} y$} iff {$x\leq_* y\land |y|=|x|+1$}".
• Extending the logic of subsequences with numerical predicates and (fragments of) Presburger arithmetic.

Another important aspect of [KS16] is that it introduced a new theory of piecewise-complexity as a fundamental tool for establishing elementary upper bounds. This theory need developing and there are many open problems to investigate:

• Algorithmic questions for the piecewise-complexity of words and languages, see e.g. [HS18].
• Extending the theory to trees and other ordered structures.

This research project should suit a theoretically-minded student with some taste for abstract algorithmic constructions like what is encountered in basic courses on recursion theory and computational complexity. It is an ideal opportunity for starting a PhD thesis.

### Literature

[HS18]
S. Halfon and Ph. Schnoebelen. On shuffle products, acyclic automata and piecewise-testable languages. Information Processing Letters, 145:68-73, 2019.
[HSZ17]
S. Halfon, Ph. Schnoebelen, and G. Zetzsche. Decidability, complexity, and expressiveness of first-order logic over the subword ordering. In Proc. LICS 2017, pages 1–12. IEEE Comp. Soc. Press, 2017.
[KS15]
P. Karandikar and Ph. Schnoebelen. Decidability in the logic of subsequences and supersequences. In Proc. FST&TCS 2015, volume 45 of LIPICS, pages 84–97. Leibniz-Zentrum für Informatik, 2015.
[KS16]
P. Karandikar and Ph. Schnoebelen. The height of piecewise-testable languages with applications in logical complexity. In Proc. CSL 2016, volume 62 of LIPICS, pages 37 :1–37 :22. Leibniz-Zentrum für Informatik, 2016.
[Kus06]
D. Kuske. Theories of orders on the set of words. RAIRO Theoretical Informatics and Applications, 40(1) :53–74, 2006.

## Specification and Verification of Properties of Neural Networks

Context. With the development of machine learning and its daily applications, gaining confidence in the systems produced by such techniques has become a critical issue. A first problem consists in formalizing what is expected from the systems. Such requirements may be either generic or specific to the task to be achieved. For instance, adversarial robustness is a generic property . It measures howmuch information is needed by an attacker to “falsify” the answer of a classifying system. On the other hand, assume the system proposes actions to be performed in the presence of an intruder, a specific property would be that there is no actionto be proposed when no intruder is detected.

In the internship, we will focus on neural networks since this is the most widely used and moreover it presents similar features to hybrid systems letting the possibility to adapt efficient techniques from this domain. Let us illustrate an example of specification formula:

{$\forall \mathbf{x}, y \, \mathrm{Pre}(x) \wedge \mathrm{InOut}( x, y) \implies \mathrm{Post}(y )$}

where {$x$} (resp.{$y$}) is the input (resp. output) vector of the system, {$Pre$} is a precondition on the inputs and {$Post$} is a postcondition on the outputs. Thus checking the negation of a formula consists in solving some existential first-ordertheory .

The design of verification for neural networks is a challenging issue sincethe number of neurons generally is between few hundreds and millions (see for a comparative study for piecewise linear neural networks). The techniquesare either sound and complete  or can proceed via astraction  thus rising the issue of incompleteness and how to tackle with it. There are now softwareframework dedicated to the verification of deep neural networks .

Goals. Thus the goals of this internship are twofold:

• Specifying a language or a logic that can express the main properties ex-pected to be satisfied by neural networks;
• Identifying specificities of formula related to these properties in order to de-sign new exact and/or approximate algorithms for verifying these properties.

References

1. Bastani, O., Ioannou, Y., Lampropoulos, L., Vytiniotis, D., Nori, A.V.,Criminisi, A.: Measuring neural net robustness with constraints. In: Lee,D.D., Sugiyama, M., von Luxburg, U., Guyon, I., Garnett, R. (eds.)Advances in Neural Information Processing Systems 29: Annual Confer-ence on Neural Information Processing Systems 2016, December 5-10,2016, Barcelona, Spain. pp. 2613–2621 (2016),http://papers.nips.cc/paper/6339-measuring-neural-net-robustness-with-constraints
2. Bunel, R., Turkaslan, I., Torr, P.H.S., Kohli, P., Kumar, M.P.: Piecewise linearneural network verification: A comparative study. CoRRabs/1711.00455(2017),http://arxiv.org/abs/1711.00455
3. Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: Anefficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kuncak,V. (eds.) Computer Aided Verification - 29th International Conference, CAV 2017,Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. Lecture Notes in Com-puter Science, vol. 10426, pp. 97–117. Springer (2017). https://doi.org/10.1007/978-3-319-63387-95,https://doi.org/10.1007/978-3-319-63387-9_5
4. Katz, G., Huang, D.A., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P.,Thakoor, S., Wu, H., Zeljic, A., Dill, D.L., Kochenderfer, M.J., Barrett, C.W.:The marabou framework for verification and analysis of deep neural networks.In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st InternationalConference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I. Lecture Notes in Computer Science, vol. 11561, pp. 443–452. Springer(2019). https://doi.org/10.1007/978-3-030-25540-426,https://doi.org/10.1007/978-3-030-25540-4_26
5. Mirman, M., Gehr, T., Vechev, M.T.: Differentiable abstract interpretation for provably robust neural networks. In: Dy, J.G., Krause, A. (eds.) Proceedingsof the 35th International Conference on Machine Learning, ICML 2018, Stockholm, Sweden, July 10-15, 2018. Proceedings of Machine Learn-ing Research, vol. 80, pp. 3575–3583. PMLR (2018),http://proceedings.mlr.press/v80/mirman18b.html
6. Tjeng, V., Tedrake, R.: Verifying neural networks with mixed integer programming.CoRRabs/1711.07356(2017),http://arxiv.org/abs/1711.07356

## Observe locally, control globally

Contact: Stefan Schwoon, Stefan Haar

Supervisory control of partially observable Petri nets has been studied int he literature mostly under a sequential and centralized perspective. With new application challenges from systems biology, it is time to to create a frameworkfor supervisory control of partially observable Petri nets, under the constraints of concurrency of the supervised processes (which are intrinsically non-sequential)and decentralization of observation and intervention.

The objectives targeted by the control must include reachability objectives in safe Petri nets; ideally, the results exceed this domain, to include reprogrammingof long-term behaviors of models arising in cell regulation. In this setting, thestakes are to steer the cell fate into a desired attractor or phenotype, whilestaying clear of fatal pathways (cancerous mutation, etc.)

The strengths of the well-known unfolding technique for safe Petri nets are expected to be instrumental in this work. The controller’s knowledge is a decentralized and asynchronous observation coming from a distributed set of observers. The tasks include:

• establish the semantics of supervisory control under these circumstances;
• determine an adequate game theoretic setting, and
• develop efficient techniques for synthezing controllers.

::