Level: M2

Contact: Philippe Dague (pdague@lmf.cnrs.fr)

Location: Laboratoire Méthodes Formelles, ENS Paris-Saclay

Keywords: Metabolic pathway analysis, models of cellular growth, thermodynamics, kinetics, regulation, convex polyhedral geometry, combinatorial optimization, ASP

Context

In the context of systems biology, the analysis of metabolic pathways is an essential step in studying the behavior of metabolic networks, which has important societal implications for human health (metabolic therapies) and biotechnology (designing cell factories to produce metabolites of interest to the agri-food industry, animal husbandry, energy production, and environmental protection).

In a steady state (i.e., constant concentrations of all molecular species), and when only the stoichiometry of the reactions and the known irreversibility of certain of them are taken into account, metabolic pathways constitute a convex polyhedral cone or, more generally, a convex polyhedron if inhomogeneous linear constraints on fluxes are added [19, 20, 18, 10, 21, 14, 8, 5]. They are thus characterized by those pathways called elementary vectors (EVs), in the sense that they are not decomposable without cancellations: any pathway can actually be broken down into a weighted sum of non-negative coefficients of elementary vectors. In the simplest case of null growth and no inhomogeneous linear constraints, metabolic pathways constitute a subspace cone or flux cone, and EVs are identical to minimal (for the set inclusion of the sets of reactions that compose them) pathways, called elementary flux modes (EFMs). Enumerating EVs or EFMs boils down to enumerating the vertices of a convex polyhedron. The most powerful tools for this are based on the Fourier-Motzkin double description method [3]. However, despite optimized implementations that allow the enumeration of millions of elementary pathways [17, 9], this method cannot handle metabolic models at the genome scale.

Furthermore, most of the pathways produced in this way are not biologically relevant because other biological constraints than only stoichiometry and irreversibility of certain reactions must be taken into account, such as thermodynamics, kinetics, and regulation. Doing so avoids producing pathways that have no biological reality and limits their number with the aim of scaling up to the genome level. Recent international work has begun to incorporate thermodynamic constraints on the one hand [4, 16] and regulatory constraints on the other [7] into the iterative double description algorithm. Other work uses Answer Set Programming (ASP), possibly coupled with Linear Programming, to express and solve the constraints, including thermodynamics constraints [11, 1]. A theoretical study of the structure of the solution space of metabolic pathways in the presence of thermodynamic and kinetic constraints (and, more generally, of sign-monotone constraints) and of Boolean regulatory constraints (and, more generally, of sign-invariant constraints), and of the characterization of the elementary vectors has been conducted in the particular case of null growth [2].

The same author is currently generalizing this work to the case of models of cellular growth, by drawing on the recent articles [6, 13, 15]. In the process of cellular growth, steady-state self-fabrication requires a cell to synthesize all of its components, including metabolites, enzymes, and ribosomes, in proportions that match its own composition. Simultaneously, the concentrations of these components affect the rates of metabolism and biosynthesis, and hence the growth rate. The theory describes all phenotypes that solve this circular problem. Metabolic pathways generalize in growth vectors (GVs) and EVs generalize in elementary growth vectors (EGVs), but the situation is quite different from that in the case of null growth: in the latter case, the concentrations of the molecular species are independent and can be imposed; in case of growth, the concentrations of all species (metabolites, enzymes, ribosome) are fixed by each solution flux (as well as the growth rate). In addition, the kinetic constraints are necessarily taken into account to elaborate the theory, either in the form of complete kinetic models if available, or, most of the time, of (semi-)kinetic models that are constraint-based models [12] where only capacity constraints (bounds on the kinetics) are expressed. Results are obtained concerning growth rate maximization: one can eliminate the fluxes and the concentrations of the enzymes and the ribosome, keeping as variables of the problem the ribosome fractions allocated to the synthesis of each enzyme and the ribosome itself, as well as the metabolite concentrations and growth rate. The solutions in the space of ribosome fractions, for each given metabolite concentration and growth rate, are called growth states (GSs) and constitute a polyhedron whose vertices are called elementary growth states (EGSs) and are also the support- minimal vectors of the polyhedron. One finds that the maximum growth rate is attained at an EGS.

Objectives

The objectives are to design and implement algorithms for enumerating EGVs and EGSs in comprehensive metabolic models of cellular growth, taking thus necessarily kinetic constraints into account (and possibly also regulatory constraints) for large-scale metabolic networks (with the genome level as the ultimate target).

The work will build from one side on the theoretical work [2] and on the software developed during a Master 1 internship in 2015 and during a thesis defended in 2023 for the case of null growth (with thermodynamic or regulatory constraints), and from the other side on the theoretical results obtained in [6, 13, 15] for the case of non-null growth, for which the integration of kinetic constraints will be studied. Methods relying on the double description method by calling on a convex programming solver, or on a constraint solver such as SMT (Satisfiability Modulo Theory) solver or ASP will be implemented, and the effectiveness of the two approaches will be compared. Validation of methods, algorithms, and software will be conducted first on small-scale networks and then on genome-scale networks derived from Bacillus subtilis.

Requirements

Knowledge to acquire about metabolic networks and convex polyhedral geometry, by reading [2], which is self-contained, and [6, 13, 15] for the non-null growth case. Use of a logic-based programming language, such as ASP, and/or of convex programming or combinatorial optimization languages, for experimentation.

Supervision

Philippe Dague, emeritus professor at Université Paris-Saclay (philippe.dague@universite-paris- saclay.fr).

References

[1] Emma Crisci, Maxime Mahout, and Sabine Peres. “Computing Thermodynamically Consistent Elementary Flux Modes with Answer Set Programming”. In: CMSB 2024 - 22nd International Conference on Computational Methods in Systems Biology. Pise, Italy, Sept. 2024, pp. 80–88.

[2] Philippe Dague. “Metabolic Pathway Analysis in the Presence of Biological Constraints”. In: Compu- tation 9(10):111 (2021).

[3] Komei Fukuda and Alain Prodon. “Double Description Method Revisited”. In: Combinatorics and Computer Science. Ed. by M. Deza, R. Euler, and I. Manoussakis. Vol. 1120. Lecture Notes in Computer Science. Springer, 1996, pp. 91–111.

[4] Matthias P. Gerstl, Christian Jungreuthmayer, and Jürgen Zanghellini. “tEFMA: computing thermo- dynamically feasible elementary flux modes in metabolic networks”. In: Bioinformatics 31(13) (2015), pp. 2232–2234.

[5] Matthias P. Gerstl, Stefan Müller, Georg Regensburger, and Jürgen Zanghellini. “Flux tope analysis: studying the coordination of reaction directions in metabolic networks”. In: Bioinformatics 35(2) (2019), pp. 266–273.

[6] Dean H. de Groot, Josephus Hulshof, Bas Teusink, Frank J. Bruggeman, and Robert Planqué. “Elementary Growth Modes provide a molecular description of cellular self-fabrication”. In: PLoS Comput Biol 16(1):e1007559 (2020).

[7] Christian Jungreuthmayer, David E. Ruckerbauer, Matthias P. Gerstl, Michael Hanscho, and Jürgen Zanghellini. “Avoiding the enumeration of infeasible elementary flux modes by including transcriptional regulatory rules in the enumeration process saves computational costs”. In: PLoS ONE 10(6):e0129840 (2015).

[8] Steffen Klamt et al. “From elementary flux modes to elementary flux vectors: metabolic pathway analysis with arbitrary linear flux constraints”. In: PLoS Comput Biol 13:e1005409 (2017).

[9] Jan Bert van Klinken and Ko Willems van Dijk. “FluxModeCalculator: an efficient tool for large-scale flux mode computation”. In: Bioinformatics 32(8) (2016), pp. 1265–1266.

[10] Francisco Llaneras and Jesús Picó. “Which Metabolic Pathways Generate and Characterize the Flux Space? A Comparison among Elementary Modes, Extreme Pathways and Minimal Generators”. In: Journal of Biomedicine and Biotechnology 2010 (2010), pp. 1–13.

[11] Maxime Mahout, Ross P. Carlson, and Sabine Peres. “Answer Set Programming for Computing Constraints-Based Elementary Flux Modes: Application to Escherichia coli Core Metabolism”. In: Processes 8(12) (2020).

[12] Cécile Moulin, Laurent Tournier, and Sabine Peres. “Combining Kinetic and Constraint-Based Modelling to Better Understand Metabolism Dynamics”. In: Processes 9(10) (2021).

[13] Stefan Müller. “Elementary growth modes/vectors and minimal autocatalytic sets for kinetic/constraint- based models of cellular growth”. In: bioRxiv (2021). url: org/content/ early/2021/02/25/2021.02.24.432769.

[14] Stefan Müller and Georg Regensburger. “Elementary Vectors and Conformal Sums in Polyhedral Geometry and their Relevance for Metabolic Pathway Analysis”. In: Frontiers in Genetics 7(90) (2016).

[15] Stefan Müller, Diana Széliová, and Jürgen Zanghellini. “Elementary vectors and autocatalytic sets for resource allocation in next-generation models of cellular growth”. In: PLoS Comput Biol 18(2):e1009843 (2022).

[16] Sabine Peres, Stefan Schuster, and Philippe Dague. “Thermodynamic constraints for identifying the elementary flux modes”. In: Biochemical Society Transactions 46(3) (2018), pp. 641–647.

[17] Marco Terzer and Jörg Stelling. “Large-scale computation of elementary flux modes with bit pattern trees”. In: Bioinformatics 24(19) (2008), pp. 2229–2235.

[18] Cong T. Trinh, Aaron Wlaschin, and Friedrich Srienc. “Elementary mode analysis: a useful metabolic pathway analysis tool for characterizing cellular metabolism”. In: Applied Microbiology and Biotech- nology 81(5) (2009), pp. 813–826.

[19] Robert Urbanczik and Clemens Wagner. “An improved algorithm for stoichiometric network analysis: theory and applications”. In: Bioinformatics 21(7) (2005), pp. 1203–1210.

[20] Clemens Wagner and Robert Urbanczik. “The Geometry of the Flux Cone of a Metabolic Network”. In: Biophysical Journal 89(6) (2005), pp. 3837–3845.

[21] Jürgen Zanghellini, David E. Ruckerbauer, Michael Hanscho, and Christian Jungreuthmayer. “Elementary flux modes in a nutshell: properties, calculation and applications”. In: Biotechnology Journal 8(9) (2013), pp. 1009–1016.

Level: M2

Contact: Philippe Dague (pdague@lmf.cnrs.fr) and Lina Ye (lina.ye@centralesupelec.fr)

Location: Laboratoire Méthodes Formelles, ENS Paris-Saclay

Keywords: Safety analysis, diagnosability, timed automata, hybrid automata, abstraction, approximation

Context

More and more systems are safety-critical, e.g., medical devices, aircraft flight control, nuclear systems, and, more recently, cyber-physical systems. Verifying at the design stage safety properties is consequently crucial for their reliability. We are particularly interested in the diagnosability property [15], i.e., the ability to determine without ambiguity from the observations and within a given time delay that a given fault has occurred, i.e., to disambiguate faulty and normal trajectories from observations. Verifying diagnosability property boils down to proving the unsatisfiability of a logical formula [5, 14] expressing the existence of a so-called critical pair, i.e., a pair of faulty and normal trajectories, with enough long duration after the fault occurrence, sharing the same observations, which would violate diagnosability. For discrete-event systems, checking this formula can be done by using a Satisfiability (SAT) solver or a Satisfiability Modulo Theories [3] (SMT) solver (with Linear Real Arithmetic theory for dealing with time constraints) [8]. The major challenge for modeling and verifying these systems resides in their intrinsic complexity arising from the combination of a continuous part (analog physical processes) and a discrete part (digital computational processes), and the interaction between them. They can be modeled classically by hybrid automata [9], i.e., finite state machines with a finite set of continuous variables whose values are described by a set of ordinary differential equations, associated with the different states (or modes), the discrete transitions between states being in turn determined by the evolution of the continuous variables. Due to the continuous part, almost all problems, even the simplest, such as reachability, are undecidable for general hybrid automata. This shows that the use of approximations is necessary to check the safety properties of hybrid systems.

This is why we resorted to discrete qualitative abstractions (under-approximations) of a hybrid automaton [17], such that verifying the given safety property at their level is decidable, and this property, if satisfied, is then satisfied also at the level of the hybrid automaton [19], providing thus a semi-decision for the property to be checked at its level. Such a qualitative abstraction can be constructed as an automaton or, better still, as a timed automaton [1] (to abstract also the temporal features induced by the continuous dynamics). If there is no decision for the property, the abstraction is refined (by constructing a finer partition into regions of the continuous space), and the process is iterated. Classically, this refinement is guided by a counterexample of the property (here, a critical pair) at the abstract level (deemed fallacious at the concrete level, otherwise it can be concluded that the property is violated at this level), so as to avoid it and similar examples at the finer level: it is the CounterExample-Guided Abstraction Refinement (CEGAR) technique [4, 18], which has been shown to be efficient at solving computationally difficult (e.g., NP or PSPACE) problems. Now, as the diagnosability analysis for timed automata is in itself such a difficult problem (it has been proved to be PSPACE-complete [16]), we have also used approximations and a CEGAR-based approach to solve it [6]. Actually, inspired by a recent extension of the CEGAR framework, called Recursive Explore and Check Abstraction Refinement (RECAR) [10], we alternate the CEGAR technique for over- and for under-approximations of the problem [7]. Applied to over- (resp., under-) approximations, this technique considers more constrained (resp., relaxed) versions of the problem, therefore with fewer (resp., more) solutions. Thus, if the over- (resp., under-) approximate problem is satisfiable (resp., unsatisfiable), so is the initial problem, providing thus sat and unsat shortcuts, respectively. Otherwise, the current approximation must be refined by relaxing (resp., constraining) it. Strategies for switching from one type of approximation to the other are defined based on the execution time of the current instance and its evolution.

Objectives

Depending on the skills and preferences of the candidate, different objectives may be pursued, giving rise to many subjects.

1. Approximation-based Diagnosability Analysis of Timed Automata

Our diagnosability analysis of timed automata with a RECAR-like framework improves the direct analysis in case of a sat answer, i.e., when the system is non-diagnosable, thanks to an efficient over-approximation of the problem, mainly achieved by reducing the length of the critical pair that is searched. But it remains inefficient in case of an unsat answer, i.e., when the system is diagnosable, due to the inefficiency of our under-approximations. So, the objective is to develop more efficient under-approximations of the problem and to test the whole analysis on more benchmarks, automatically generated.

Requirements: Own or acquire skills in timed automata, diagnosability, approximations, and CEGAR, SMT, and use of the SMT solver Z3.

2. Timed Automata Abstractions of Hybrid Automata

The objective is to continue the preliminary work above about the definition and construction of under-approximations of hybrid automata as timed automata and their refinements. The states of such a timed automaton abstracting the given hybrid automaton are obtained by splitting the continuous space into a finite set of areas, each one being an approximation, in a given mode of the hybrid automaton, of the solution space of the differential equations attached to this mode. Its state invariants and transition guards are built from the sojourn duration in each mode. Refinement is achieved by dividing a given area into smaller areas. The automation of the construction of the initial abstraction and its successive refinements (guided by a spurious counter-example, here a critical pair, in a CEGAR framework) will be studied. A general framework will be adopted where an oracle provides lower and upper bounds of the sojourn duration in a mode. Then several methods will be studied for implementing such an oracle: exact computation in the easy case of the existence of a known analytical solution of the set of differential equations; simulation of the hybrid system (flow- pipe calculation); use of neural networks, in particular, Physics-Informed Neural Networks (PINNs) [13]. The arbitrarily close approximation of hybrid systems by recurrent neural net- works was theoretically proved in 1997 [2]. This convinces us that it is worthwhile studying in depth how to approximate hybrid systems with PINNs precisely and efficiently. Testing will be done on the given benchmarks of hybrid systems.

Requirements: Own or acquire skills in timed automata, hybrid automata, and simulation tools, abstractions, and CEGAR, PINNs.

3. Approximation-based Framework for ϵ-Guarantee of Properties on Hybrid Automata

The objective is to define a general RECAR-like framework of over- and under-approximations of hybrid automata and their refinements in order to verify as close as required, i.e., by ϵ for a given positive real number ϵ, given safety properties of these hybrid systems, such as diagnosability. In addition to under-approximations defined as timed automata as above, over- approximations will also have to be defined and implemented. For this, results concerning the over-approximation of attainable states in hybrid systems [11] will be studied. The efficiency of the whole RECAR-like method (with a given timeout) will be tested on the given benchmarks of hybrid systems. Then this RECAR-like procedure will be extended by considering ϵ- approximations [12], without which the termination and thus the correct verdict cannot be guaranteed. In particular, how to best exploit the certificates returned by the solver in each approximation case, when they do not allow a direct conclusion for the considered property of the initial system, will be studied. Precise definitions of an ϵ-approximation of a given hybrid automaton and of an ϵ′-validity of a formal property of such a hybrid automaton will have to be given, and how to transform the validity of a property on an ϵ-approximation of the hybrid system into an ϵ′-validity of the same property on the hybrid system and vice versa will be studied.

Requirements: Own or acquire skills in hybrid automata and simulation tools, approxima- tions, and CEGAR.

Supervision

Philippe Dague, emeritus professor at Université Paris-Saclay (philippe.dague@universite-paris- saclay.fr) and Lina Ye, associate professor at CentraleSup´elec (lina.ye@centralesupelec.fr).

References

[1] Rajeev Alur and David L Dill. “A theory of timed automata”. In: Theoretical computer science 126.2 (1994), pp. 183–235.

[2] Andrew D. Back and Tian-Ping Chen. “Approximation of hybrid systems by neural networks”. In: Proc. of the International Conference on Neural Information Processing, ICONIP 1997, Denver, Colorado, USA. Springer, 1997, pp. 326–329.

[3] Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. “Satisfiability Modulo Theo- ries”. In: Handbook of satisfiability. Ed. by Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh. IOS Press, 2021. Chap. 33, pp. 1267–1329.

[4] Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. “Counterexample- guided abstraction refinement for symbolic model checking”. In: J. ACM 50.5 (2003), pp. 752–794.

[5] Alban Grastien, Anbu Anbulagan, Jussi Rintanen, and Elena Kelareva. “Diagnosis of discrete-event systems using satisfiability algorithms”. In: Proceedings of the 22nd National Conference on Artificial Intelligence AAAI’07. 2007, pp. 305–310.

[6] Lulu He. “Formal verification at design stage of diagnosis related properties for discrete event and real-time systems”. PhD thesis. Université Paris-Saclay, 2022.

[7] Lulu He, Philippe Dague, and Lina Ye. “An approximation-based incremental SMT approach for diagnosability analysis of real-time systems”. In: Discrete Event Dynamic Systems 35.3 (2025), pp. 267– 299.

[8] Lulu He, Lina Ye, and Philippe Dague. “SMT-based Diagnosability Analysis of Real-Time Systems”. In: Proceedings of the 10th Symposium on Fault Detection, Supervision and Safety for Technical Pro- cesses, IFAC SAFEPROCESS 2018. 2018.

[9] Thomas A. Henzinger. “The theory of hybrid automata”. In: Verification of Digital and Hybrid Systems. Springer, 2000, pp. 265–292.

[10] Jean-Marie Lagniez, Daniel Le Berre, Tiago de Lima, and Valentin Montmirail. “A Recursive Shortcut for CEGAR: Application To The Modal Logic K Satisfiability Problem”. In: Proc. of the 26th International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia. Ed. by Carles Sierra. ijcai.org, 2017, pp. 674–680.

[11] Meilun Li, Peter N. Mosaad, Martin Fr¨anzle, Zhikun She, and Bai Xue. “Safe Over- and Under- Approximation of Reachable Sets for Autonomous Dynamical Systems”. In: Formal Modeling and Analysis of Timed Systems. Ed. by David N. Jansen and Pavithra Prabhakar. Springer International Publishing, 2018, pp. 252–270.

[12] Anuj Puri, Vivek Borkar, and Pravin Varaiya. “ϵ-Approximation of differential inclusions”. In: Hybrid Systems III, Verification and Control. Ed. by Rajeev Alur, Thomas A. Henzinger, and Eduardo D. Sontag. Vol. 1066. Lecture Notes in Computer Science. Springer, 1996, pp. 362–376.

[13] Maziar Raissi, Paris Perdikaris, and George Em Karniadakis. “Physics-informed neural networks: A deep learning framework for solving forward and inverse problems involving nonlinear partial differential equations”. In: Journal of Computational Physics 378 (2019), pp. 686–707.

[14] Jussi Rintanen and Alban Grastien. “Diagnosability testing with satisfiability algorithms”. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence IJCAI’07. 2007, pp. 532–537.

[15] Meera Sampath, Raja Sengupta, St´ephane Lafortune, Kasim Sinnamohideen, and Demosthenis Teneket- zis. “Diagnosability of discrete-event systems”. In: IEEE Transactions on automatic control 40.9 (1995), pp. 1555–1575.

[16] Stavros Tripakis. “Fault diagnosis for timed automata”. In: Proceedings of the International symposium on formal techniques in real-time and fault-tolerant systems. Springer. 2002, pp. 205–221.

[17] Hadi Zaatiti, Lina Ye, Philippe Dague, and Jean-Pierre Gallois. “Automating Abstraction Computa- tions of Hybrid Systems”. In: Formal Verification of Physical Systems FVPS 2018, workshop of the 11th Conference on Intelligent Computer Mathematics CICM 2018. Hagenberg, Austria, Aug. 2018.

[18] Hadi Zaatiti, Lina Ye, Philippe Dague, and Jean-Pierre Gallois. “Counterexample-Guided Abstraction- Refinement for Hybrid Systems Diagnosability Analysis”. In: 28th International Workshop on Principles of Diagnosis DX’17. Ed. by Marina Zanella, Ingo Pill, and Alessandro Cimatti. Vol. 4. Kalpa Publications in Computing. EasyChair, 2018, pp. 124–143.

Level: M2

Contact: Philippe Dague (pdague@lmf.cnrs.fr) and Thomas Chatain (chatain@lmf.cnrs.fr)

Location: Laboratoire Méthodes Formelles, ENS Paris-Saclay

Keywords: Boolean Networks, Constraint satisfiability

Context

Since their introduction in the late 1960s [9], logical models, such as Boolean Networks (BNs), have been widely adopted for reasoning about signaling and gene networks as they require few parameters and can easily integrate information from omics datasets and genetic screens. These models represent processes with a high degree of generalization and can offer coarse-grained but robust predictions, which makes them particularly suitable for large biological networks. BNs are formal discrete dynamical systems with notorious applications for modeling cellular differentiation and fate decision processes: the attractors capture the stable behaviors, and the trajectories capture the transient dynamics of the cell. To each BN is attached its interaction graph that references the positive and negative influences between components and hence is a compact and static abstraction of the BN dynamics [6]. Also, methods based on a generalization of the steady state notion, the so- called trap spaces, can be exploited to investigate attractor properties as well as for model reduction techniques [3].

Given a BN, i.e., n local functions from Bn to B, where B = {0, 1} is the Boolean domain, the update mode specifies how to compute the next configuration from the present one. There is a vast zoo of update modes [1, 7], but traditionally, two modes are usually considered in biological modeling: the synchronous (or parallel) deterministic mode, where the next configuration results from the simultaneous application of all n local functions, and the fully asynchronous, where the next configuration results from the application of only one local function, chosen non-deterministically. However, (a)synchronous update modes do not lead to a complete qualitative abstraction of quantitative systems and preclude the prediction of trajectories that are actually feasible when considering time scales or concentration scales. The Most Permissive (MP) [5, 8] is a recently introduced update mode that brings the formal guarantee to capture any trajectory that is feasible by any quantitative system compatible with the Boolean network. In addition, the MP update mode benefits from much better complexity results than the traditional update modes for all current problems, e.g., the problem of reachability between configurations, which is PSPACE-complete for the latter ones, becomes P N P (even P with a local monotonicity assumption) for it.

Despite its good properties, the MP update mode sometimes appears “too permissive”, and it is also the case of the stricter linearly-cuttable update [4]. Allowing spurious, i.e., not feasible in practice, behaviors is quite normal for any abstraction of a given problem; nevertheless, one would want to eliminate the most obvious of them. In particular, those that are not consistent with respect to the “local context, i.e., that differ at two different occurrences of the same context. For example, it may appear legitimate to require that an (unknown but fixed) order is maintained, inside any given component, between the thresholds of activation/inhibition by this component of all the components it influences, or else a fixed time order of the crossing of those thresholds by the variables involved along the trajectory, all else being equal.

The recent work [2] addresses this issue by defining the threshold semantics whose dynamic behaviors are all those given by a single threshold network, a subclass of multivalued networks, for any possible threshold map, and by characterizing it operationally by adding to the MP update mode a system of symbolic constraints, attached to any given trajectory and verifiable by a sat- isfiability solver. The satisfiability of this set of constraints ensures the consistency of the formal threshold conditions associated with the transitions along the trajectory.

Objectives

The objective is to complete the work [2], which in particular contains several conjectures to be proven or disproven by counterexamples. And to implement the satisfiability checking of the system of symbolic constraints associated with any trajectory, and to automate the construction of such consistent trajectories. With the goal of helping in the discovery of counterexamples or of giving insights for establishing proofs, but also of exploring the real complexity of the update mode on realistic examples, and of studying trap spaces

Requirements

Skills in formal methods. Knowledge to acquire about BNs (at least by reading [2], which is self- contained). Use of a logic-based programming language for experimentation, such as ASP (Answer Set Programming).

Supervision

Philippe Dague, emeritus professor at Université Paris-Saclay (philippe.dague@universite-paris- saclay.fr) and Thomas Chatain, associate professor HDR at ENS Paris-Saclay (thomas.chatain@ens- paris-saclay.fr).

References

[1] Thomas Chatain, Stefan Haar, Juraj Kolčák, Lo¨ıc Paulevé, and Aalok Thakkar. “Concurrency in Boolean networks”. In: Natural Computing 19.1 (2020), pp. 91–109.

[2] Philippe Dague. A semantics for Boolean networks consistent with regulatory threshold constraints. Submitted in 2025 to Journal of Theoretical Biology,

[3] Hannes Klarner, Alexander Bockmayr, and Heike Siebert. “Computing maximal and minimal trap spaces of Boolean networks”. In: Natural Computing 14.4 (2015), pp. 535–544.

[4] Aurélien Naldi, Adrien Richard, and Elisa Tonello. “Linear cuts in Boolean network”. In: Natural Computing 22(3) (2023), pp. 431–451.

[5] Loïc Paulevé, Juraj Kolčák, Thomas Chatain, and Stefan Haar. “Reconciling qualitative, abstract, and scalable modeling of biological networks”. In: Nature Communications 11.1 (2020), p. 4256.

[6] Loïc Paulevé and Adrien Richard. “Static analysis of Boolean networks based on interaction graphs: a survey”. In: Electronic Notes in Theoretical Computer Science 284 (2012), pp. 93–104.

[7] Loïc Paulevé and Sylvain Sené. “Boolean networks and their dynamics: the impact of updates”. In: Systems Biology Modelling and Analysis: Formal Bioinformatics Methods and Tools. Wiley, 2022.

[8] Loïc Paulevé and Sylvain Sené. “Non-Deterministic Updates of Boolean Networks”. In: 27th IFIP WG 1.5 International Workshop on Cellular Automata and Discrete Complex Systems (AUTOMATA 2021). Ed. by Alonso Castillo-Ramirez, Pierre Guillon, and Kévin Perrot. Vol. 90. Open Access Series in Informatics (OASIcs). Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021, 10:1–10:16.

[9] René Thomas. “Boolean formalization of genetic control circuits”. In: Journal of theoretical biology 42.3 (1973), pp. 563–585.

Level: M2

Contact: Uli Fahrenberg (uli@lmf.cnrs.fr)

Location: Laboratoire Méthodes Formelles, ENS Paris-Saclay

Keywords: Higher-dimensional automata; concurrency theory; automata theory

Description

Higher-dimensional automata (HDAs) are an extension of automata which allows to model concurrent and parallel executions. Like standard automata they consist of states and transitions, but also of higher-dimensional cells (squares, cubes, etc.) which model parallel execution of several events. This gives HDAs a somewhat geometric flavor.

Read more...

Level: M1 – M2

Contact: Dietmar Berwanger (dwb@lmf.cnrs.fr) and Patricia Bouyer (bouyer@lmf.cnrs.fr)

Location: Laboratoire Méthodes Formelles, ENS Paris-Saclay

Keywords: Distributed synthesis, signalling, automata theory, imperfect information

Description

In distributed systems, control actions are often executed by a single component, but the information needed to make these decisions is dispersed across the system. This internship focuses on the synthesis of signalling strategies, where the objective is not to coordinate multiple control agents but to ensure that information is effectively transmitted within the system.

Read more...

Level: L3 Info-Math, M1

Contact: Burkhart Wolff

Summary.HOL-Bee is a semantic Frontend for Abrial's Event-B Method in Isabelle/HOL. It permits to edit specifications in the Event-B language inside the eco-sytem of Isabelle (IDE, kernel, code-generator, proof-system, libraries) and to generate its semantic representation in form of state-relations.

In this internship, the objective is to extend this functionality by generating the proof-obligations and elementary proof-support. (Read the detailed internship proposal.).

Level: L3, M1

Contact: Burkhart Wolff<burkhart.wolff [at] universite-paris-saclay [dot] fr>, Idir Ait-Sadoune<idir.aitsadoune@centralesupelec.fr>

Location: Laboratoire Méthodes Formelles, Université Paris-Saclay

Keywords: Isabelle/HOL, Isabelle/DOF, Formal Document Generation

More Details: here

Read more...

Level: L3 Info-Math, M1

Contact: Burkhart Wolff

Summary.HOL-Bee is a semantic Frontend for Abrial's Event-B Method in Isabelle/HOL. It permits to edit specifications in the Event-B language inside the eco-sytem of Isabelle (IDE, kernel, code-generator, proof-system, libraries) and to generate its semantic representation in form of state-relations.

 In this internship, the objective is to extend this functionality by  generating the proof-obligations

and elementary proof-support. (Read the detailed internship proposal.).

Level: L3, M1, M2

Contact: Burkhart Wolff

Summary. Isabelle/C is a framework for C code in C11 syntax deeply integrated into the Isabelle/PIDE development environment. Our framework provides an abstract interface for verification back-ends to be plugged-in independently. The purpose of this stage is to develop a translation from C11-AST's generated in Isabelle/C to a semantic backend called Clean, a simple execution model for an imperative target language.

Read the detailed internship proposal.

Modeling and analysis of cyber-physical systems is a challenge for formal methods and an active area of research. Initially developed for the analysis of the safety properties of autonomous vehicles (see [1]), the HOL-Cyberphy framework, based on the Isabelle/HOL proof assistant, has been generalized to model multi-agent cyber-physical systems. . The objective of this internship is to study this framework, notably based on the use of an Isabelle theory of Communicating Sequential Processes (see [2]), and to adapt it to the modeling of cyber-multi-agent systems. communicating physics, in order to analyze and prove their proper functioning properties. We can particularly draw inspiration from the work of André Platzer in this area (see [3]).

Missions:

1. Constitute a state of the art on the formal modeling of communicating cyber-physical multi-agent systems;
2. Take charge of the Isabelle HOL-CyberPhy framework, by creating some models of single and multi-agent cyber-physical systems;
3. Design a generic model of communicating cyber-physical multi-agent systems based on case studies to be identified, and propose an adaptation of the HOL-CyberPhy framework accordingly.

Bibliographic references on the subject:

• [1] Paolo Crisafulli, Safouan Taha, Burkhart Wolff. Modeling and Proving Safety in Autonomous Cars Scenarios in HOL-CSP. Research Report 1, University Paris-Saclay; IRT SystemX, Palaiseau. 2021, pp.81. URL:
• [2] Taha S., Ye L., Wolff B.: HOL-CSP Version 2.0. Archive of Formal Proofs (2019).
• [3] Brieger, Marvin & Mitsch, Stefan & Platzer, André. (2023). Dynamic Logic of Communicating Hybrid Programs

The internship may lead to recruitment for a thesis, on the subject described here

Quatre postes d'enseignant·e·s-chercheur·e·s avec affectation au LMF ouvrent en 2025 :

• Un poste de professeur·e à la Faculté des Sciences, Université Paris-Saclay
• Un poste de professeur·e à l'ENS Paris-Saclay
• Un poste de maître·sse de conférences à la Faculté des Sciences, Université Paris-Saclay
• Un poste de maître·sse de conférences à Polytech, Université Paris-Saclay

Un poste de professeur·e est ouvert dans le DER d'informatique de l'ENS Paris-Saclay, avec affectation au laboratoire LMF. Pour plus d'informations, veuillez s'il-vous-plaît vous référer au profil du poste.

Read more...

Un poste de MCF est ouvert à Polytech, Université Paris-Saclay, avec affectation au laboratoire LMF. Pour plus d'informations, veuillez s'il-vous-plaît vous référer au profil du poste.

Read more...

Un poste de professeur·e est ouvert dans le département d'informatique de la faculté des sciences, Université Paris-Saclay, avec affectation au laboratoire LMF. Pour plus d'informations, veuillez s'il-vous-plaît vous référer au profil du poste.

Read more...

Un poste de MCF est ouvert dans le département d'informatique de la faculté des sciences, Université Paris-Saclay, avec affectation au laboratoire LMF. Pour plus d'informations, veuillez s'il-vous-plaît vous référer au profil du poste.

Read more...