Loïc Paulevé

AAAI Conference 2024 Conference Paper

CEGAR-Based Approach for Solving Combinatorial Optimization Modulo Quantified Linear Arithmetics Problems

• Kerian Thuillier
• Anne Siegel
• Loïc Paulevé

Bioinformatics has always been a prolific domain for generating complex satisfiability and optimization problems. For instance, the synthesis of multi-scale models of biological networks has recently been associated with the resolution of optimization problems mixing Boolean logic and universally quantified linear constraints (OPT+qLP), which can be benchmarked on real-world models. In this paper, we introduce a Counter-Example-Guided Abstraction Refinement (CEGAR) to solve such problems efficiently. Our CEGAR exploits monotone properties inherent to linear optimization in order to generalize counter-examples of Boolean relaxations. We implemented our approach by extending Answer Set Programming (ASP) solver Clingo with a quantified linear constraints propagator. Our prototype enables exploiting independence of sub-formulas to further exploit the generalization of counter-examples. We evaluate the impact of refinement and partitioning on two sets of OPT+qLP problems inspired by system biology. Additionally, we conducted a comparison with the state-of-the-art ASP solver Clingo[lpx] that handles non-quantified linear constraints, showing the advantage of our CEGAR approach for solving large problems.

GandALF Workshop 2022 Workshop Paper

Avoid One's Doom: Finding Cliff-Edge Configurations in Petri Nets

• Giann Karlo Aguirre-Samboní
• Stefan Haar
• Loïc Paulevé
• Stefan Schwoon
• Nick Würdemann

A crucial question in analyzing a concurrent system is to determine its long-run behaviour, and in particular, whether there are irreversible choices in its evolution, leading into parts of the reachability space from which there is no return to other parts. Casting this problem in the unifying framework of safe Petri nets, our previous work has provided techniques for identifying attractors, i. e. terminal strongly connected components of the reachability space, whose attraction basins we wish to determine. Here, we provide a solution for the case of safe Petri nets. Our algorithm uses net unfoldings and provides a map of all of the system's configurations (concurrent executions) that act as cliff-edges, i. e. any maximal extension for those configurations lies in some basin that is considered fatal. The computation turns out to require only a relatively small prefix of the unfolding, just twice the depth of Esparza's complete prefix.

SAT Conference 2020 Conference Paper

SAT Heritage: A Community-Driven Effort for Archiving, Building and Running More Than Thousand SAT Solvers

• Gilles Audemard
• Loïc Paulevé
• Laurent Simon 0001

Abstract SAT research has a long history of source code and binary releases, thanks to competitions organized every year. However, since every cycle of competitions has its own set of rules and an adhoc way of publishing source code and binaries, compiling or even running any solver may be harder than what it seems. Moreover, there has been more than a thousand solvers published so far, some of them released in the early 90’s. If the SAT community wants to archive and be able to keep track of all the solvers that made its history, it urgently needs to deploy an important effort. We propose to initiate a community-driven effort to archive and to allow easy compilation and running of all SAT solvers that have been released so far. We rely on the best tools for archiving and building binaries (thanks to Docker, GitHub and Zenodo) and provide a consistent and easy way for this. Thanks to our tool, building (or running) a solver from its source (or from its binary) can be done in one line.

TCS Journal 2019 Journal Article

Parameter space abstraction and unfolding semantics of discrete regulatory networks

• Juri Kolčák
• David Šafránek
• Stefan Haar
• Loïc Paulevé

The modelling of discrete regulatory networks combines a graph specifying the pairwise influences between the variables of the system, and a parametrisation from which can be derived a discrete transition system. Given the influence graph only, the exploration of admissible parametrisations and the behaviours they enable is computationally demanding due to the combinatorial explosions of both parametrisation and reachable state space. This article introduces an abstraction of the parametrisation space and its refinement to account for the existence of given transitions, and for constraints on the sign and observability of influences. The abstraction uses a convex sublattice containing the concrete parametrisation space specified by its infimum and supremum parametrisations. It is shown that the computed abstractions are optimal, i. e. , no smaller convex sublattice exists. Although the abstraction may introduce over-approximation, it has been proven to be conservative with respect to reachability of states. Then, an unfolding semantics for Parametric Regulatory Networks is defined, taking advantage of concurrency between transitions to provide a compact representation of reachable transitions. A prototype implementation is provided: it has been applied to several examples of Boolean and multi-valued networks, showing its tractability for networks with numerous components.

TCS Journal 2019 Journal Article

Preface

• Jérôme Feret
• Loïc Paulevé
• David Šafránek

TCS Journal 2015 Journal Article

Identification of biological regulatory networks from Process Hitting models

• Maxime Folschette
• Loïc Paulevé
• Katsumi Inoue
• Morgan Magnin
• Olivier Roux

Qualitative formalisms offer a well-established alternative to the more traditionally used differential equation models of Biological Regulatory Networks (BRNs). These formalisms led to numerous theoretical works and practical tools to understand emerging behaviors. The analysis of the dynamics of very large models is however a rather hard problem, which led us to previously introduce the Process Hitting framework (PH), which is a particular class of nondeterministic asynchronous automata network (or safe Petri nets). Its major advantage lies in the efficiency of several static analyses recently designed to assess dynamical properties, making it possible to tackle very large models. In this paper, we address the formal identification of qualitative models of BRNs from PH models. First, the inference of the Interaction Graph from a PH model summarizes the signed influences between the components that are effective for the dynamics. Second, we provide the inference of all René Thomas models of BRNs that are compatible with a given PH. As the PH allows the specification of nondeterministic interactions between components, our inference emphasizes the ability of PH to deal with large BRNs with incomplete knowledge on interactions, where Thomas' approach fails because of the combinatorics of parameters. The inference of corresponding Thomas models is implemented using Answer Set Programming, which allows in particular an efficient enumeration of (possibly numerous) compatible parameterizations.

TCS Journal 2015 Journal Article

Sufficient conditions for reachability in automata networks with priorities

• Maxime Folschette
• Loïc Paulevé
• Morgan Magnin
• Olivier Roux

In this paper, we develop a framework for an efficient under-approximation of the dynamics of Asynchronous Automata Networks (AANs). An AAN is an Automata Network with synchronised transitions between automata, where each transition changes the local state of exactly one automaton (but any number of synchronising local states are allowed). The work we propose here is based on static analysis by abstract interpretation, which allows to prove that reaching a state with a given property is possible, without the same computational cost of usual model checkers: the complexity is polynomial with the total number of local states and exponential with the number of local states within a single automaton. Furthermore, we address AANs with classes of priorities, and give an encoding into AANs without priorities, thus extending the application range of our under-approximation. Finally, we illustrate our method for the model checking of large-scale biological networks.

TCS Journal 2012 Journal Article

Stochastic simulation of multiple process calculi for biology

• Matthew R. Lakin
• Loïc Paulevé
• Andrew Phillips

Numerous programming languages based on process calculi have been developed for biological modelling, many of which can generate potentially unbounded numbers of molecular species and reactions. As a result, such languages cannot rely on standard reaction-based simulation methods, and are generally implemented using custom stochastic simulation algorithms. As an alternative, this paper proposes a generic abstract machine that can be instantiated to simulate a range of process calculi using a range of simulation methods. The abstract machine functions as a just-in-time compiler, which dynamically updates the set of possible reactions and chooses the next reaction in an iterative cycle. We instantiate the generic abstract machine with two Markovian simulation methods and provide encodings for four process calculi: the agent-based pi-calculus, the compartment-based bioambient calculus, the rule-based kappa calculus and the domain-specific DNA strand displacement calculus. We present a generic method for proving that the encoding of an arbitrary process calculus into the abstract machine is correct, and we use this method to prove the correctness of all four calculus encodings. Finally, we demonstrate how the generic abstract machine can be used to simulate heterogeneous models in which discrete communicating sub-models are written using different domain-specific languages and then simulated together. Our approach forms the basis of a multi-language environment for the simulation of heterogeneous biological models.