Logo IRISA logo Inria

Exposés de la saison 2021-2022

July 19th, 10.30AM (Paris/France). Salle Markov. (in French)

Aurélie Hurault (INP Toulouse, IRIT)

Vérification de systèmes distribués asynchrone : exploration de la diversité des modèles asynchrones et du modèle Heard-Of

La présentation abordera deux séries de travaux autour de la vérification de systèmes distribués asynchrone.
Dans un premier temps, nous nous intéresserons à la formalisation des interactions asynchrones. Lors d’une preuve d’algorithme distribué, les propriétés sur la communication sont prouvées suffisantes pour la correction de l’algorithme. Cependant, il est souvent peu clair quelles sont ces propriétés de communication car elles sont généralement noyées au sein de l’algorithme. Il est notamment difficile de remplacer un modèle de communication par un autre sans avoir à refaire complètement la preuve ou le développement. Nous avons défini un cadre générique pour spécifier la diversité des modèles de communication asynchrone. Ce cadre permet de comprendre et comparer les différents modèles ainsi que de prouver la correction et la complétude de différentes définitions des modèles. Des modèles formels spécifiques de communications asynchrones ont été défini à l’aide d’Event-B et de TLA+ . Basé sur ces modèles, nous avons proposé un framework de vérification de compatibilité de systèmes distribués communiquant par messages asynchrones, en point à point ou en multicast. Il est mis à disposition en ligne : http://vacs.enseeiht.fr/
Dans un second temps, nous nous intéresserons aux défaillances. Plutôt que de formaliser chaque structure d’algorithme et chaque type de défaillance, nous nous restreignons aux algorithmes fonctionnant par tours et nous utilisons le modèle Heard-Of qui abstrait les défaillances en représentant par un prédicat l’ensemble des pairs pour lesquels un pair donné reçoit un message à un tour donné. Nous avons apporté des réponses à deux questions alors ouvertes : comment trouver le prédicat heard-of qui correspond à un modèle classique donné ? quelles pertes surviennent lors de cette conversion ? Une formalisation de la dérivation d’un prédicat heard-of correspondant à un certain modèle, avec une méthodologie pour dériver un modèle à partir de modèles plus simples, permet de répondre à la première question. La seconde question a été résolue grâce à une équivalence entre des prédicats heard-of et les modèles à messages asynchrones avec détecteurs de défaillances.

June 30th, 3PM (Paris/France). Salle Markov

Helge Spieker (Simula Research Laboratory in Oslo, Norway)

The interplay of AI and software testing for resilient software systems.

AI-based software are of increasing relevance but also add additional challenges for the software testing process, such as the oracle problem of uncertainty in the precise expected outcome of the software or gigantic numbers of potential test scenarios. At the same time, AI techniques, both data-driven machine learning and logic-driven constraint solving, can aid testing techniques to be more cost-effective and focus on finding faults early. In this talk I will discuss a selection of applications at this intersection, involving metamorphic testing, reinforcement learning, and constraint optimization.

June 9th, 3PM (Paris/France). Replay

Damien Busatto-Gaston (Université Libre de Bruxelles)

On the strategy synthesis problem in MDPs: probabilistic CTL and rolling windows. (Slides)

In this talk I will present recent work on Markov decision processes. Given an MDP and a formula phi, the strategy synthesis problem asks if there exists a strategy for the MDP such that the resulting Markov chain satisfies phi. This challenging problem is known to be undecidable for the probabilistic temporal logic PCTL. We study a class of formulae that can be seen as a fragment of PCTL where a local, bounded horizon property is enforced globally. Moreover, we allow for linear expressions in the probabilistic inequalities. We show that this class of formulae is at the frontier of decidability, depending on the type of strategies considered. In particular, strategy synthesis becomes decidable when strategies are either deterministic or memoryless, while the general problem remains undecidable. We compare with results on the entire PCTL logic and consider applications to the PCTL satisfiability problem.

June 2nd, 10AM (Paris/France). Playback

Xiong Xu (Institute of Software, Chinese Academy of Sciences, China)

Semantics Foundation for Cyber-Physical Systems Using Higher-Order UTP

Model-based design has become the predominant approach to the design of hybrid and cyber-physical systems (CPSs). It advocates the use of mathematically founded models to capture heterogeneous digital and analog behaviours from domain-specific formalisms, allowing all engineering tasks of verification, code synthesis and validation to be performed within a single semantic body. Guaranteeing the consistency among the different views and heterogeneous models of a system at different levels of abstraction however poses significant challenges. To address these issues, Hoare and He’s Unifying Theories of Programming (UTP) proposes a calculus to capture domain-specific programming and modelling paradigms into a unified semantic framework. Our goal is to extend UTP to form a semantic foundation for CPS design. Higher-Order UTP (HUTP) is a conservative extension to Hoare and He’s theory which supports the specification of discrete, real-time and continuous dynamics, concurrency and communication, and higher-order quantification. Within HUTP, we define a calculus of normal hybrid designs to model, analyse, compose, refine and verify heterogeneous hybrid system models. In addition, we define respective formal semantics for HCSP (Hybrid Communicating Sequential Processes) and Simulink using HUTP.

May 19th, 3PM (Paris/France). Salle Markov

Pierre Le Scornet (LogicA, IRISA, France)

Deciding attacker penetration capabilities in dynamic virtual networks.

Virtualization is a new development of Cloud technologies, that comes with new kinds of security breaches. For administrators of these complex systems, it is essential to assess risks on their infrastructure to be able to apply appropriate countermeasures. Among the various risks such infrastructures may face, analyzing which pieces of hardware or software an attacker has access to and which vulnerabilities he may exploit to improve his privileges is a challenging question, all the more if such analyses are expected to be automated. We propose a mathematical setting that relies on a host-based attack graph model and that is amenable to deciding the attacker's penetration capabilities in a dynamic virtual networks. As we can specify networks with an unbounded number of configurations, the overall machinery we develop to establish our decidability results is non-trivial. In particular, it makes use of the powerful theory of well-structured transition systems. Regarding the specification of penetration risks, we allow to use a well-tuned first-order logic language.

May 12th, 3PM (Paris/France). Salle Petri-Turing

Christine Tasson (Sorbonne Université, France)

Denotational Semantics of Probabilistic Programming (Slides).

In this talk, I will first introduce probabilistic programming with examples of programs and of algorithms used for inference in probabilistic programming languages. The second part of the talk will be dedicated to denotational semantics of functional probabilistic programming, the difficulties to design higher order models, the existing solutions and the interpretation of programs.

May 5th, 3PM (Paris/France). Playback

Johan Commelin (University of Freiburg, Germany)

Reflection on the Liquid Tensor Experiment (Slides)

In this talk I will present a medley of reflections on the Liquid Tensor Experiment. What worked well? What can we learn for future projects? The talk will be an informal mix of maths and computer science.

April 14th, 3PM (Paris/France). Salle Petri-Turing

Frédéric MARIS (Université Toulouse III - Paul Sabatier, France)

A Simple Framework for Cognitive Planning.

Cognitive planning is a generalization of epistemic planning: the goal is to achieve cognitive states of target agents which could involve not only beliefs, but also intentions. We encode the cognitive planning problem in an epistemic logic with a semantics of explicit and implicit beliefs exploiting belief bases. We study a NP-fragment of the logic whose satisfiability problem is reduced to SAT. Indeed, we focus on a simple version for which only a special agent, called the machine, has implicit beliefs. We introduce a formalization of simple cognitive planning as a quantified boolean formula (QBF) with an optimal number of quantifiers in the prefix. Indeed, we show that the simple cognitive planning problem is on the second level of the polynomial hierarchy. Moreover, we illustrate the potential of simple cognitive planning for applications in human-machine interaction in which an artificial agent is expected to interact with a human agent through dialogue and to persuade the human to behave in a certain way.
Joint work with Jorge Fernandez, Emiliano Lorini and Dominique Longin.

April 7th, 3PM (Paris/France). (Playback)

Eric Goubault (Ecole Polytechnique, France)

Cyber-Physical Systems, Artificial Intelligence, Control and Validation (slides)

Autonomous cars, drones and swarms of drones, smart grid, industry 4.0...these are all examples of automated control systems of physical processes, possibly distributed and on a large scale, called cyber-physical systems. Artificial Intelligence (AI) has profoundly renewed the problem of control and verification of the correct behaviour of these systems, which is essential for their social acceptability. However, it will be shown in this talk that some theories (abstract interpretation, assembly methods...) successfully applied to help debug and certify critical embedded systems, for example for the aerospace and nuclear industry, allow to develop efficient verification strategies.

February 17th, 3PM (Paris/France). Webinar

Inigo Incer (University of California, Berkeley)

The Algebra of Contracts

Contract-based design has been proposed as a formal design methodology to support compositional design in industry. Assume-guarantee (AG) contracts are formal specifications consisting of two trace properties: (i) assumptions made on the environment and (ii) responsibilities imposed on the object under specification when the environment behaves according to the contract's assumptions. In this talk, we will first discuss all algebraic operations known on AG contracts, and the applications of these operations in engineering design. As there are many formal design attributes, such as secure information flow, that cannot be expressed with trace properties or AG contracts, we will then discuss the theory of hypercontracts, which enables us to carry out assume-guarantee reasoning in complex systems using arbitrary hyperproperties.

January 20th, 11AM. Webinar

Hugo Gimbert (CNRS, LaBRI, France)

Distributed Asynchronous Games With Causal Memory are Undecidable

The distributed version of the Ramadge and Wonham control problem asks for the existence of a correct controller of a plant modeled as an asynchronous transition system. The controllable plant is distributed on several finite-state processes which interact asynchronously using shared actions. The controller is distributed as well, and decomposes as one local controller on every process. Each local controller can choose to block some of the actions, called controllable actions, but it cannot block the uncontrollable actions from the environment. A controller is correct if it guarantees that every possible execution of the plant satisfies some specification. The controller synthesis problem is the decision problem which, given a plant as input, asks whether the system admits a correct controller. In case such a controller exists, the algorithm should compute one as well. The difficulty of the controller synthesis depends on several factors, including the architecture of the information flow between processes (pipeline, ring, ...), the information available to the controllers, and the specification. The choices of the local controllers can be based on several sources of information. A minima, a local controller monitors the sequence of states and actions of the local process. This information is called the *local view* of the controller. Pnueli and Rosner proved that the distributed controller synthesis problem is undecidable when local controllers are restricted to use their local view for taking decisions, even for very simple architectures. Gastin, Lerman and Zeitoun have proposed in 2004 a variant of the distributed controller synthesis problem where local controllers are allowed to base their decisions on their *causal past*. When a shared action is played by several processes then all the controllers of these processes are allowed to exchange as much information as they want, and in particular together they can compute their mutual view of the global execution: their causal past. In this setting, Gastin et al. established the decidability of the synthesis for series-parallel architectures, and left open the decidability in the general case. In this talk, we provide a negative answer to their open question: the distributed controller synthesis problem with causal memory is undecidable. We also review several architectures which where proved decidable or for which the decidability is still open.

Friday December 17th, 10AM Paris/France. Salle Markov.

Valeria Vignudelli (Ecole normale supérieure de Lyon, France)

Equational reasoning, metrics, and monads for nondeterministic and probabilistic systems

Programs combining nondeterministic and probabilistic features allow us to account for both the presence of concurrency, where scheduling choices may be unpredictable, and the presence of quantitative or uncertain information. In recent contributions, we have studied methods to reason about the equivalence of systems combining nondeterminism and probability. The quantitative information brought by probabilities moreover allows us to encompass program equivalence and to reason about the finer notion of program distance. This does not only tell us whether two systems are equivalent or not, but also how much they differ. As main reasoning tool, we use equational theories and their analogues for distances, in order to obtain axiomatizations of the systems and properties of interest. By modelling nondeterminism and probabilities via monads, we are able to show our results in the abstract setting of category theory and coalgebra. In this talk I will present our framework and show applications to proving equivalences and distances, e.g. bisimulation-based, of nondeterministic and probabilistic transition systems.

Thursday December 16th, 3PM Paris/France.

Yvo Meeres (University of Leipzig, Germany)

Accepting Directed Acyclic Graphs with the Help of Finite State Automata. (Slides)

Analogously to regular string and tree languages, regular directed graph (DAG) languages had been defined in literature. Although called regular, those DAG-languages are way more powerful and, consequently, standard problems have a higher complexity than in the string case. Top-down as well as bottom-up deterministic DAG languages are subclasses of the regular DAG languages. We refine this hierarchy by providing a weaker subclass of the deterministic DAG languages. Obviously, this weaker class exhibits beneficial algorithmic properties.For a DAG-automaton accepting a language in this new DAG language class, a classical finite state automaton (FSA) can be constructed which states enumerate the dangling edges throughout an appropriate run of the DAG-automaton. An edge is called dangling if not yet all of its vertices have been read in the run. This means that an FSA can be used for deciding membership of such DAGs.The motivation behind this joint work with Johannes Blum and Frank Drewes is the transfer of results about regular string languages to graphs. Furthermore, we provide a characterization of the class via the DAG-automaton’s rules.

Thursday December 9th, 4:15PM Paris/France. (Playback)

Fabio Mogavero (Università degli Studi di Napoli Federico II, Italy)

Herbrand Property, Finite Quasi-Herbrand Models, and a Chandra-Merlin Theorem for Quantified Conjunctive Queries. (Slides)

A structure enjoys the Herbrand property if, whenever it satisfies an equality between some terms, these terms are unifiable. On such structures the expressive power of equalities becomes trivial, as their semantic satisfiability is reduced to a purely syntactic check. In this work, we introduce the notion of Herbrand property and develop it in a finite model-theoretic perspective. We provide, indeed, a canonical realization of the new concept by what we call quasi-Herbrand models and observe that, in stark contrast with the naive implementation of the property via standard Herbrand models, their universe can be finite even in presence of functions in the vocabulary. We exploit this feature to decide and collapse the general and finite version of the satisfiability and entailment problems for previously unsettled fragments of first-order logic. We take advantage of the Herbrand property also to establish novel and tight complexity results for the aforementioned decision questions. In particular, we show that the finite containment problem for quantified conjunctive queries is NPTIME-complete, tightening along two dimensions the known 3EXPTIME upper bound for the general version of the problem (Chen, Madelaine, and Martin, LICS'08). We finally present an alternative view on this result by generalizing to such queries the classic characterization of conjunctive query containment via polynomial-time verifiable homomorphisms (Chandra and Merlin, STOC'77).

Thursday December 2nd, 2:30PM Paris/France.

Dietrich Kuske (Technische Universität Ilmenau, Germany)

Complexity of counting first-order logic for the subword order

This paper considers the structure consisting of the set of all words over a given alphabet together with the subword relation, regular predicates, and constants for every word. We are interested in the counting extension of first-order logic by threshold counting quantifiers. The main result shows that the two-variable fragment of this logic can be decided in two-fold exponential space provided the regular predicates are restricted to piecewise testable ones. This result improves prior insights by Karandikar and Schnoebelen by extending the logic and saving one exponent. Its proof consists of two main parts: First, we provide a quantifier elimination procedure that results in a formula with constants of bounded length (this generalizes the procedure by Karandikar and Schnoebelen for first-order logic). From this, it follows that quantification in formulas can be restricted to words of bounded length, i.e., the second part of the proof is an adaptation of the method by Ferrante and Rackoff to counting logic and deviates significantly from the path of reasoning by Karandikar and Schnoebelen.

Tuesday November 16th, 3PM Paris/France. Salle Markov (Inria Rennes)

Uli Fahrenberg (EPITA, Rennes, France)

Posets with Interfaces as a Model for Concurrency

We introduce posets with interfaces (iposets) and generalise the standard serial composition of posets to a new gluing composition. In the non-interleaving, event-based semantics of concurrency, interfaces and gluing allow modelling events that continue their execution across components. Alternatively, taking a decompositional view on concurrent systems, it allows cutting through events, while serial composition may cut through precedence or causality edges only.
We show that iposets under gluing composition form a category, generalising the monoid of posets under serial composition, and a 2-category when a suitable subsumption order and a lax tensor in the form of a non-commutative parallel composition are added. This generalises the interchange monoids used in concurrent Kleene algebra.
We also consider the hierarchy of iposets generated from singleton iposets by finitary gluing and parallel compositions. We show that it includes the series-parallel posets and the interval orders, which are also well studied in concurrency theory. Finally, we show that not all posets are gluing-parallel, exposing several forbidden substructures.

Wednesday November 10th, 3PM Paris/France.(Replay)

Katherine Cordwell (CMU, Pittsburgh, USA)

Towards Practical Provably Correct Algorithms for Real Quantifier Elimination (Slides)

Real arithmetic questions involving the “there exists” and “for all” quantifiers arise in various fields, including formalized mathematics, rigorous engineering domains, and life sciences. Although Tarski proved that real quantified statements can always be reduced to logically equivalent quantifier-free statements through quantifier elimination (QE), QE algorithms are notoriously complicated. This makes QE algorithms difficult to formally verify---formally verified algorithms require accompanying proofs of correctness (typically developed in theorem provers) that rely only on a set of trusted logical axioms---and so in practice, QE problems must be solved with unverified software. This is undesirable given the subtlety of QE algorithms and the safety-critical nature of their applications. In recent work, my collaborators and I found that some of the existing unverified QE tools are self-contradictory on (in total) 137 benchmarks, which underscores the need for more support for practical formally verified QE.
My proposed approach is twofold: First, verify the Ben-Or, Kozen, and Reif (BKR) decision procedure---and Renegar's variation of BKR---which fits in a potential “sweet spot” in between practicality and ease of verification. Second, augment BKR with strong auxiliary methods and preprocessing methods, including virtual substitution (an extremely practical QE method for QE problems that involve low-degree polynomials). This talk discusses progress towards this goal, which includes verifying univariate BKR and linear and quadratic virtual substitution (in joint work).