6 views
   owned this note
# Scilex-2 Continuous versus discrete systems Contacts: * Alexandre Chapoutot (ENSTA Paris) * Franck Delaplace (IBISC, UEVE) ## Description of the theme Cyber-physical systems or biological systems are made of different kinds of components which are of different natures. Usually they can be modelled by hybrid systems mixing continuous-time parts and discrete-time parts which communicate and influence each other. Automatically analyzing, verifying, or synthetizing (part of) such systems is required to deal with the complexity. Mathematical modelling of cyber-physical systems or biological systems involves different classes of mathematical models going from finite state automata to differential equations which may also involve distributed computations. The coupling of these classes of models requires a great care. All these elements make the application of formal methods challenging. Formal methods as used in software verification (model checking, abstract interpretation, interactive proof) have to be adapted, extended to deal with continuous-time dynamical systems and the interaction with discrete-time parts. ## Some hot research topics of the theme ### 1 - Data driven modeling of dynamical systems *Possible contributor:* **TBD** (contacted by **TDB**) #### Summary Mathematical modelling of systems in order to apply formal methods may involve an important amount of knowledge on the physical or biologicial process. Nowadays an important amount of data exists (coming from sensors or experiments) which can be used to define mathematical models. This represents a new challenge to apply formal methods as mathematical models coming from data do not assume particular properties. *Keywords:* dynamical systems, mathematical models, data #### Researchers involved or interested * [Antoine Girard](https://sites.google.com/site/antoinesgirard/), L2S, Antoine.Girard@l2s.centralesupelec.fr * [Laurent Fribourg](http://www.lsv.fr/~fribourg/), LSV, fribourg@lsv.ens-cachan.fr * [Goran Frehse](https://sites.google.com/site/frehseg/), ENSTA Paris, goran.frehse@ensta-paris.fr * [Julien Alexandre dit Sandretto](), ENSTA Paris, julien.alexandre-dit-sandretto@ensta-paris.fr * [Eric Goubault](http://www.lix.polytechnique.fr/Labo/Eric.Goubault/), Ecole polytechnique, goubault@lix.polytechnique.fr * [Sylvie Putot](http://www.lix.polytechnique.fr/Labo/Sylvie.Putot/), Ecole polytechnique, Sylvie.Putot@polytechnique.edu #### A few references * Interpretable classification of time-series data using efficient enumerative techniques by Sara Mohammadinejad, Jyotirmoy V. Deshmukh, Aniruddh G. Puranic, Marcell Vazquez-Chanlatte, and Alexandre Donzé. HSCC 2020. * Conformance verification for neural network models of glucose-insulin dynamics by Taisa Kushner, Sriram Sankaranarayanan and Marc Breton. HSCC 2020. * Neural Predictive Monitoring by Luca Bortolussi, Francesca Cairoli, Nicola Paoletti, Scott Smolka and Scott Stoller. RV 2019. ### 2 - Formal methods for neural network-based systems *Possible contributor:* **TBD** (contacted by **TDB**) #### Summary Neural networks are an important class of algorithms used in autonomous systems or robots for perception or control. The size and the complexity of such neural networks represent a new challenge to apply formal methods on closed-loop systems. As a side effect, an new research direction is to build safe-by-construction controller based neural networks. Dealing with neural networks component involve also the design of formal specification which is a new challenge. *Keywords:* formal methods, neural networks, closed-loop systems, controller #### Researchers involved or interested * [Eric Goubault](http://www.lix.polytechnique.fr/Labo/Eric.Goubault/), Ecole polytechnique, goubault@lix.polytechnique.fr * [Sylvie Putot](http://www.lix.polytechnique.fr/Labo/Sylvie.Putot/), Ecole polytechnique, Sylvie.Putot@polytechnique.edu * [Sergio Mover](http://www.sergiomover.eu), Ecole polytechnique, sergio.mover@lix.polytechnique.fr * [Sao Mai Nguyen](http://nguyensmai.free.fr/Home.html), ENSTA Paris, sao-mai.nguyen@ensta-paris.fr * [Goran Frehse](https://sites.google.com/site/frehseg/), ENSTA Paris, goran.frehse@ensta-paris.fr * [Zakaria Hichem Chihani](https://sites.google.com/site/zakchihani/), CEA, zakaria.chihani@cea.fr * [Marc Schoenauer](https://www.lri.fr/~marc/), INRIA, marc.schoenauer@inria.fr * [Guillaume Charpiat](https://www.lri.fr/~gcharpia/), INRIA, guillaume.charpiat@inria.fr * [Serge Haddad](http://www.lsv.fr/~haddad/), LSV, haddad@lsv.fr #### A few references * Reachability Analysis for Neural Feedback Systems using Regressive Polynomial Rule Inference by Souradeep Dutta, Xin Chen and Sriram Sankaranarayanan. HSCC 2019. * Verisig: verifying safety properties of hybrid systems with neural network controllers by Radoslav Ivanov, James Weimer, Rajeev Alur, George Pappas and Insup Lee. HSCC 2019. * Probabilistic Guarantees for Safe Deep Reinforcement Learning by Edoardo Bacci, David Parker. FORMATS 2020. #### Related Digicosme project * ColeSlAW: Continuously Learning Complex Tasks via Symbolic Analysis ### 3 - Network medicine *Possible contributor:* **TBD** (contacted by **TDB**) #### Summary Network medicine is an emerging domain of precision medicine analysing disease through the lens of network science. Biological networks provide a systems-level understanding of molecular processes based on molecular interaction study. The objective is to provide a comprehensive holistic understanding of the perturbations entailed by diseases where the causes of diseases are assimilated to disturbances affecting the molecular interactions. Hence, cells are envisioned as complex webs of macromolecular interactions forming the interactome where the nodes are metabolites, proteins, genes and their RNA transcripts while the edges are the biochemical interactions. Fundamentally, network medicine constitutes a novel paradigm for linking phenotypes to the underlying molecular processes (genotypes) through the study of their interactions. The network framework then allows to integrate large scale multi-omics and phenotypic data, in order to gain insights into disease mechanisms, and to support drug design and tailoring treatments to patients. This approach enables to sustain discovery of novel clinically actionable knowledge for diagnosis, prognosis, treatment and prediction. More generally, the integrative view provided by networks constitutes a tool for multi-scale analysis in health sciences, from molecules to ecosystems. The challenges are: - Reappraisal of disease taxonomy based on interactome analysis; - functional modules (groups of nodes) identification based on static analysis; - dynamical network analysis for deciphering both the disease mechanisms, and the effect of drug administration; - network controllability study to investigate induced cell fate deviations for purposefully reaching some expected outcomes regarded as healthy state; - Network-based ecosystem study. *Keywords:* network medicine, biological networks, diagnosis, prediction #### Researchers involved or interested * [Franck Delaplace](https://www.ibisc.univ-evry.fr/~delapla/), IBISC, franck.delaplace@univ-evry.fr * [Alain Denise](http://www.lri.fr/~denise/), LRI, alain.denise@lri.fr (et son équipe) * [François Fage](https://lifeware.inria.fr/wiki/Fages/HomePage), INRIA, francois.fages@inria.fr (et son équipe) * [Stephan Haar](http://www.lsv.fr/~haar/), LSV, stefan.haar@inria.fr * [Sabine Peres](https://www.lri.fr/~speres/), LISN, Sabine.Peres@lri.fr * [Franck Pommereau](https://www.ibisc.univ-evry.fr/~fpommereau/), IBISC, franck.pommereau@univ-evry.fr #### A few references * Albert-László Barabási, Natali Gulbahce, and Joseph Loscalzo. “Network medicine: a network-based approach to human disease”. In: Nature reviews genetics 12.1 (2011), pp. 56–68. * Laurel Yong Hwa Lee and Joseph Loscalzo. “Network Medicine in Pathobiology”. In: American Journal of Pathology 189.7 (2019), pp. 1311–1326. ISSN: 1525219 * Network Medicine. N.p., Harvard University Press, 2017. #### Related Digicosme project * ACTONET: Controllability of Biological Network Fate. * ESCAPE: EcoSystem Causal Analysis Using PEtri net unfoldings. ### 4 - Distributed microbiological systems *Possible contributor:* **TBD** (contacted by **TDB**) #### Summary In the past few decades, synthetic biology has laid considerable focus on the re-programming of cells as computing machines. They have been engineered to sense a range of inputs (metabolites, light, oxygen, pH) and process them to produce desired outputs according to defined processing codes (primarily digital, but occasionally analog). Some potential applications of the cellular machines include production of metabolic compounds of interest, bio-remediation of toxic environments, sensing of disease bio-markers, and therapeutic intervention by targeted effector delivery. Yet, the ability of single cells to reliably process multiple inputs is acutely constrained by their limited resources. Adding too many processes into one cell leads to resource-stress and eventually the code is lost due to mutation, a baseline error mechanism present in all living systems. This has, in part, encouraged the notion of distributing the computational tasks across multiple cells, to reduce resource-stress and improve robustness. The value of the idea is corroborated by the success of the division of labor seen in multi-cellular organisms that have naturally evolved from their unicellular ancestors. While task-distribution in cell populations solves some problems, it immediately leads to other challenges that must be tackled for the successful implementation of any complex distributed program. Some of these challenges include: the orthogonality/specificity of communication signals, the rate and bandwidth of communication channels, cellular growth and its effect on signal amplification or dissipation, and effect of cross-talk between different signals. *Keywords:* microbiological circuits, distributed computing, chemical reaction networks #### Researchers involved or interested * [Matthias Függer](http://www.lsv.fr/~mfuegger/), LMF, mfuegger@lsv.fr * [Thomas Nowak](https://www.lri.fr/~nowak/), LISN, thomas.nowak@lri.fr * [Patrick Amar](https://www.lri.fr/~pa/), LISN, pa@lri.fr * Joffroy Beauquier, LISN, jb@lri.fr * Janna Burman, LISN, burman@lri.fr * [Laurent Fribourg](http://www.lsv.fr/~fribourg/), LMF, fribourg@lsv.ens-cachan.fr #### A few references * Sergi Regot, Javier Macia, Nuria Conde, Kentaro Furukawa, Jimmy Kjellen, Tom Peeters, Stefan Hohmann,Eulàlia de Nadal, Francesc Posas, Ricard Sole. [Distributed biological computation with multicellular engineered networks](https://www.nature.com/articles/nature09679). Nature, 469(7329):207–211, 2010 * Michael J. Liao, M. Omar Din, Lev Tsimring, Jeff Hasty. [Rock-paper-scissors: Engineered population dynamics increase genetic stability](https://science.sciencemag.org/content/365/6457/1045.abstract). Science 365(6457):1045-1049. 2019. * Da-Jung Cho, Matthias Függer, Corbin Hopper, Manish Kushwaha, Thomas Nowak, Quentin Soubeyran. [Distributed computation with continual population growth](https://doi.org/10.4230/LIPIcs.DISC.2020.7). Proceedings of the 34th International Symposium on Distributed Computing (DISC). 2020. #### Related Digicosme project * HicDiesMeus: Highly Constrained Discrete Agents for Modeling Natural Systems * DIGIT: Distributed Pulse Generation in Bacterial Colonies ## Write your name if you are interested / want to participate in this theme | Nom | Prénom | E-mail | Affiliation | | ---- | ------ | ------ | ----------- | | Nowak | Thomas | thomas.nowak@lri.fr | LISN | | | | | | | | | | | | | | | |