12th CSPSAT Seminar

Prof. Daniel Le Berre got his Ph.d. degree from IRIT, Toulouse in 2000, on using SAT solvers to perform non monotonic reasoning. That thesis was about designing truth maintenance systems mechanisms using SAT engines. After working in Australia under the direction of Mary-Anne Williams, he has started his work at Artois University/CRIL since September 2001 as Associate professor, and has become full professor since 2013. His interests are: SAT, MAXSAT, Pseudo-Boolean Optimization, QBF, Nonmonotonic Reasoning, Modal Logics. He initiated the SAT competition in 2002, and also he is the original creator of Sat4j, a free Java-based library of SAT technologies. He has been awarded CNRS Innovation Medal on 2018 for the development of the Sat4j open source library and its integration in the open platform Eclipse.

20 years ago, Bounded Model Checking was proposed as an alternative to Model Checking using binary decision diagrams. While the initial finding was that SAT solvers could be an alternative when BDD-based system failed, such new application of SAT solvers triggered the design of the disruptive SAT solver Chaff, a huge interest for practical SAT solving in the academic community and the adoption of SAT technology in formal verification companies. This talk will review the principles behind SAT-based Model Checking, from it’s roots in Planning as Satisfiability to recent implementations which do not require unrolling.

Prof. Morgan Magnin got his Ph.d. degree from École centrale de Nantes, France, for the work entitled “Stopwatch Petri nets with dense-time and discrete-time semantics”. Since his Ph.d., he have been working in École centrale de Nantes, and he becomes Professor as well as the leader of the research team MeForBio in École centrale de Nantes. He is also a visiting Professor at National Institute of Informatics in Japan. His research interests are: Logic Programming, Machine Learning, Model-checking, Systems Biology, Constraint Programming.

Understanding the mechanisms involved in biological regulation is a fundamental issue to analyze living systems. Time delays play a major role in the sustainability and control of oscillations, as shown for example in phenomena related to the mammal circadian clock. Our work focuses on synchronous/asynchronous Automata Networks (AN). In Automata Networks, the evolution of a component is determined by the state of at most one other component that does not evolve. This is modelled by actions of the form X+Y-> X+Y’, where X behaves like a catalyst molecule that “hits” another molecule Y and changes it into Y’, without being changed itself. Assuming catalysts are always available, this can represent any biochemical system made of monomolecular reactions, and can also represent catalytic networks such as metabolic networks. Our motivation behind this framework was to design a model and analysis techniques adapted to biological modelling. These analyses avoid building the whole state space, which allows to tackle very large systems (that would have led to a huge number of states, hopelessly too huge to be analysed). Our work aims at checking reachability properties that, for a given initial state s and the discrete expression level n of a given component x, have the form: “Starting from state s, is it possible to reach a state in which x is at level n?”. The particular form of Automata Networks makes it possible to partially overcome combinatorial explosion problems by approaching the dynamics of the models. In this talk, we will discuss the merits and limits of such approaches, and draw comparisons with more classical bounded model checking approaches. In particular, we will emphasize the new results that may be brought by a combination between these methodologies.