In recent years a wealth of logic-based languages have been introduced to reason about the strategic abilities of autonomous agents in multi-agent systems. This talk presents some of these important logical formalisms, namely, the Alternating-time Temporal Logic and Strategy Logic. We discuss recent extensions of those formalisms to capture different degrees of satisfaction, as well as to handle uncertainty caused by the partial observability of agents and the intrinsic randomness of MAS. Finally, we describe the recent application of those formalisms for Mechanism Design and explain how they can be used either to automatically check that a given mechanism satisfies some desirable property, or to produce a mechanism that does it.

It is widely known that the precision of a program analyzer is closely related to intensional program properties, namely, properties concerning how the program is written. This explains, for instance, the interest in code obfuscation techniques, namely, tools explicitly designed to degrade the results of program analysis by operating syntactic program transformations. Less is known about a possible relation between what the program extensionally computes, namely, its input-output relation, and the precision of a program analyzer. In this paper we explore this potential connection in an effort to isolate program fragments that can be precisely analyzed by abstract interpretation, namely, programs for which there exists a complete abstract interpretation. In the field of static inference of numeric invariants, this happens for programs, or parts of programs, that manifest a monotone (either non-decreasing or non-increasing) behavior. We first formalize the notion of program monotonicity with respect to a given input and a set of numerical variables of interest. A sound proof system is then introduced with judgments specifying whether a program is monotone relatively to a set of variables and a set of inputs. The interest in monotonicity is justified because we prove that the family of monotone programs admit a complete abstract interpretation over a specific class of non-trivial numerical abstractions and inputs. This class includes all non-relational abstract domains that refine interval analysis (i.e., at least as precise as the intervals abstraction) and that satisfy a topological convexity hypothesis.

Cyber-Physical Systems (CPS) provide the foundation for our critical infrastructure systems, such as energy, transportation, and manufacturing, to name a few. Although CPS are already ubiquitous in our society, their security aspects were only recently incorporated into their design process, mainly in response to catastrophic incidents caused by cyber-attacks. One common class of attacks on CPS is called data-deception attacks, which involve an attacker hijacking the CPS sensors. In this talk, we focus on two questions: (1) How can we model and analyze CPS under data-deception attacks? (2) Can we automatically find vulnerabilities of a given CPS to data-deception attacks? We present a general control framework to help engineers detect and address data-deception vulnerabilities in CPS. This framework can answer the following types of questions: Does the attacker go undetected by an intrusion monitor? What is the likelihood of a safety violation? What information does the attacker need to be successful? We demonstrate that this control framework can analyze realistic case studies by detecting several vulnerabilities in a water treatment testbed and an aircraft power distribution testbed. We discuss how our formal approach can improve the security of the next generation of critical infrastructure systems by reducing vulnerabilities to data-deception of attacks.

Timed languages contain sequences of discrete events (“letters”) separated by real-valued delays, they can be recognized by timed automata, and represent behaviors of various real-time systems. The notion of bandwidth of a timed language defined in a previous paper characterizes the amount of information per time unit, encoded in words of the language observed with some precision ε.

In this paper, we identify three classes of timed automata according to the asymptotics of the bandwidth of their languages with respect to this precision ε: automata are either meager, with an O(1) bandwidth, normal, with a Θ(log (1/ε)) bandwidth, or obese, with Θ(1/ε) bandwidth. We define two structural criteria and prove that they partition timed automata into these 3 classes of bandwidth, implying that there are no intermediate asymptotic classes.

Both criteria are formulated using morphisms from paths of the timed automaton to some finite monoids extending Puri's orbit graphs, and the proofs are based on Simon's factorization forest theorem.

Joint work with E. Asarin, A.Degorre, C.Dima

We consider networks of processes that all execute the same finite-state protocol and communicate via a rendez-vous mechanism. When a process requests a rendez-vous, another process can respond to it and they both change their control states accordingly. We focus here on a specific semantics, called non-blocking, where the process requesting a rendez-vous can change its state even if no process can respond to it. We study the parameterised coverability problem of a configuration in this context, which consists in determining whether there is an initial number of processes and an execution allowing to reach a configuration bigger than a given one. We show that this problem is EXPSPACE-complete and can be solved in polynomial time if the protocol is partitioned into two sets of states, the states from which a process can request a rendez-vous and the ones from which it can answer one. We also prove that the problem of the existence of an execution bringing all the processes in a final state is undecidable in our context. These two problems can be solved in polynomial time with the classical rendez-vous semantics.

We present a layered method to solve a multi-agent state problem, involving Timed Automata, SMT and Reinforcement Learning. The first layer of our method, based on Timed Automata, efficiently models the systems and gives us a high-level plan. Then, in a second step, we refine our model and solve it with SMT. We combining these steps and call it the SWA-SMT solver. A main issue is that it cannot be executed in real time. To overcome this, we use SWA-SMT solutions as the initial training dataset for our final step, which aims to obtain a neural network control policy. We use reinforcement learning to train the policy. We develop and show an example where the use of this initial dataset is crucial for the overall success of the method.

We present an algorithm to learn a deterministic timed automaton (DTA) via membership and equivalence queries. Our algorithm is an extension of the L* algorithm with a Myhill-Nerode style characterization of recognizable timed languages, which is the class of timed languages recognizable by DTAs. We first characterize the recognizable timed languages with a Nerode-style congruence. Using it, we give an algorithm with a smart teacher answering symbolic membership queries in addition to membership and equivalence queries. With a symbolic membership query, one can ask the membership of a certain set of timed words at one time. We prove that for any recognizable timed language, our learning algorithm returns a DTA recognizing it. We show how to answer a symbolic membership query with finitely many membership queries. We also show that our learning algorithm requires a polynomial number of queries with a smart teacher and an exponential number of queries with a normal teacher. We applied our algorithm to various benchmarks and confirmed its effectiveness with a normal teacher.

In this talk I will discuss recent work on investigating the increase in observational capabilities of monitors that analyse systems over multiple runs. I will illustrate how this augmented monitoring setup can affect the class of properties that can be verified at runtime focussing, in particular, on branching-time properties expressed in the modal mu-calculus. Although branching-time properties are considered to be preserve of static verification techniques such as model-checking, our preliminary results show that the extended monitoring setup can be used to systematically extend previously established monitorability limits. If time permits, I will also discuss bounds that capture the correspondence between the syntactic structure of a branching-time property and the number of system runs required to conduct adequate runtime verification. This is joint work with Antonis Achilleos and Jasmine Xuereb.

In an embedded real-time system (ERTS), real-time tasks (software) are typically executed on a multicore shared-memory platform (hardware). The number of cores is usually small, contrasted with a larger number of complex tasks that share data to collaborate. Since most ERTSs are safety-critical, it is crucial to rigorously verify their software against various real-time requirements under the actual hardware constraints (concurrent access to data, number of cores). Both the real-time systems and the formal methods communities provide elegant techniques to realize such verification, which nevertheless face major challenges. For instance, model checking (formal methods) suffers from the state- space explosion problem, whereas schedulability analysis (real-time systems) is pessimistic and restricted to simple task models and schedulability properties. In this paper, we propose a scalable and generic approach to formally verify ERTSs. The core contribution is enabling, through joining the forces of both communities, compositional verification to tame the state-space size. To that end, we formalize a realistic ERTS model where tasks are complex with an arbitrary number of jobs and job segments, then show that compositional verification of such model is possible, using a hybrid approach (from both communities), under the state-of-the-art partitioned fixed-priority (P-FP) with limited preemption scheduling algorithm. The approach consists of the following steps, given the above ERTS model and scheduling algorithm. First, we compute fine-grained data sharing overheads for each job segment that reads or writes some data from the shared memory. Second, we generalize an algorithm that, aware of the data sharing overheads, computes an affinity (task-core allocation) guaranteeing the schedulability of hard-real-time (HRT) tasks. Third, we devise a timed automata (TA) model of the ERTS, that takes into account the affinity, the data sharing overheads and the scheduling algorithm, on which we demonstrate that various properties can be verified compositionally, i.e., on a subset of cores instead of the whole ERTS, therefore reducing the state-space size. In particular, we enable the scalable computation of tight worst-case response times (WCRTs) and other tight bounds separating events on different cores, thus overcoming the pessimism of schedulability analysis techniques. We fully automate our approach and show its benefits on three real-world complex ERTSs, namely two autonomous robots and an automotive case study from the WATERS 2017 industrial challenge.

We study the computational complexity of finding a solution in straight-cut and square-cut pizza sharing, where the objective is to fairly divide 2-dimensional resources. We show that, for both the discrete and continuous versions of the problems, finding an approximate solution is PPA-complete even for very large constant additive approximation, while finding an exact solution for the square-cut problem is FIXP-hard and in BU. We also study the corresponding decision variants of the problems and their complexity. All our hardness results for the continuous versions apply even when the input is very simple, namely, a union of unweighted squares or triangles.

Joint work with Argyrios Deligkas and John Fearnley.

Robots are facilitating new business models from food delivery to healthcare. Current engineering practice cannot yet provide the formal guarantees needed to allay the safety concerns of regulators. Simulation, a technique favoured by practitioners, provides an avenue for experimenting with different scenarios before committing to expensive tests and proofs. In this talk, I will discuss how different models may be brought together for the (co-)verification of system properties, with simulation complementing formal verification. This will be explored in the context of the model-driven RoboStar framework, that clearly identifies models of the software, hardware, and scenario, and has heterogeneous formal semantics amenable to verification using model-checkers and theorem provers.

The main obstacle in learning distributed systems is the absence of a canonical distributed device for a given behavior. This is why deterministic negotiations without deadlock are interesting in this context. We present an Angluin style active learning algorithm for this model.

Deterministic negotiations are models of distributed systems, a kind of Petri nets or Zielonka automata with additional structure. We show that this additional structure together with the assumption of deadlock freedom allows minimizing such negotiations.

Angluin's L* algorithm can learn a regular language with polynomialy many queries to Teacher. Active learning algorithms have been designed for many extensions of deterministic finite automata. The challenge in adapting this approach to negotiations is in extracting relevant information from a Teacher's answer: if a teacher says that an execution should not be accepted, it is not clear which parallel component in a negotiation should be modified.

We present a learning algorithm whose complexity, measured in the number of queries to the Teacher, is practically the same as the standard algorithm for finite automata. This is interesting, as a finite automaton representing a negotiation can be exponentially bigger than the negotiation.

In order to master the complexity of a system at the design stage, several models have to be defined and combined together. However, when heterogeneous and independent DSLs are used to define these models, there is a need to explicitly compose their semantics. While the composition of static semantics of DSLs is straightforward, the coordination of their execution semantics is still challenging. This issue is generally called inter-DSL collaboration. In this paper, we propose a formal Model Driven Engineering (MDE) framework built on the Meeduse language workbench that we extend with the Business Process Model and Notation (BPMN). Meeduse allows to instrument DSLs with formal semantics using the B method. BPMN provides an easy-to-use notation to define the coordination of execution semantics of these DSLs. A transformation of BPMN models into Communication Sequential Process (CSP) formal language enables the possibility for animation and verification. Our approach is successfully demonstrated by modeling the collaboration of two DSLs from a real case study.

We develop value iteration-based algorithms to solve in a unified manner different classes of combinatorial zero-sum games with mean-payoff type rewards. These algorithms rely on an oracle, evaluating the dynamic programming operator up to a given precision. We provide a basic bound, showing in essence that the number of calls to the oracle needed to determine exact optimal (positional) strategies is, up to a factor polynomial in the dimension, of order R/sep, where the “separation” sep is defined as the minimal difference between distinct values arising from strategies, and R is a metric estimate, involving the norm of approximate sub and super-eigenvectors of the dynamic programming operator. We illustrate this method by two applications. The first one is a new proof, leading to improved complexity estimates, of a theorem of Boros, Elbassioni, Gurvich and Makino, showing that turn-based mean-payoff games with a fixed number of random positions can be solved in pseudo-polynomial time. The second one concerns entropy games, a model introduced by Asarin, Cervelle, Degorre, Dima, Horn and Kozyakin. The rank of an entropy game is defined as the maximal rank among all the ambiguity matrices determined by strategies of the two players. We show that entropy games with a fixed rank, in their original formulation, can be solved in polynomial time, and that an extension of entropy games incorporating weights can be solved in pseudo-polynomial time under the same fixed rank condition. We shall also discuss a more recent, alternative approach, combining the ideas of relative value iteration and of Krasnoselskii-Mann damping. This leads to improved parameterized bounds for concurrent mean-payoff games, under an irreducibility assumption. The proofs are based on an operator approach, exploiting tools from non-linear Perron-Frobenius theory and variational analysis. The talk will include an introductive survey of this operator approach. This is based on a series of works, with Akian, Grand-Clément, Guillaud, Allamigeon, Katz, Skomra, and more recently Naepels and Terver.

*Real-time systems* are computing systems subject to stringent timing constraints and found in many safety-critical domains (e.g., avionics, automotive, robotics). An essential step in the safety certification of such systems is *schedulability analysis*: a category of formal methods that assess the system's temporal correctness (i.e., compliance with the stated timing constraints).

However, how much *trust* should we place in the results of a schedulability analysis, and more generally, results obtained with formal methods, in the certification of critical systems? Using schedulability analysis as a specific example, I will examine several ways in which analysis results might be unsound or otherwise unsatisfying and argue that there is ample room for reasonable doubt. However, that begs the question: why should industry practitioners adopt methods conceived to increase confidence in a system's (temporal) correctness if these methods are not so confidence-inspiring after all?

Formal verification offers a path out of this conundrum. While the implied effort and learning curve may initially seem off-putting, I will argue that it is, in fact, both viable and desirable to verify schedulability analyses formally. As a proof of concept, I will present PROSA, a Coq framework for machine-checked schedulability analysis, which we have been developing since 2015. Out of the box, PROSA provides machine-checked and hence *trustworthy* schedulability analyses suitable for use in critical systems. Additionally, PROSA has enabled us to find more general results and derive explainable analyses, as I will explain in my talk.

Finally, I will report on two ongoing projects, one seeking to close the “model gap” between PROSA and a system's codebase and one aiming to enable mathematically sound below-worst-case provisioning.

Reaching consensus in a distributed system is one of the most fundamental problems studied in distributed computing. It is non-trivial due to uncertainties related to unsuccessful communication and process faults. In particular, the celebrated FLP impossibility result shows why scheduling an event via an asynchronous communication medium such as email is difficult. In this talk, I will present our recent results on exact and approximate consensus in hostile environments such as dynamic networks (e.g., due to mobility of agents) and synthetic bacterial cultures

Event logs are often one of the main sources of information to understand the behavior of a system. While numerous approaches have extracted partial information from event logs, we aim at inferring a global model of a system from its event logs.

We consider real-time systems, which can be modeled with Timed Automata: our approach is thus a Timed Automata learner. There is a handful of related work, however, they might require a lot of parameters or produce Timed Automata that either are undeterministic or lack precision. In contrast, we propose an approach, called TAG, that requires only one parameter and learns, without any a-priori knowledge, a deterministic Timed Automaton having a good tradeoff between accuracy and automata complexity. This allows getting an interpretable and accurate global model of the considered real-time system. Experiments compare our approach to related work and demonstrate its merits.

In this talk we look at the strategy complexity of a lim sup objective in countable MDPs equipped with transition based rewards. This lim sup objective generalises the Buchi objective which is a well studied objective in verification. We will sketch three upper bound results, one epsilon-optimal and two different optimal upper bounds. We will take special care to highlight the techniques common to each proof which will hopefully convey the essence of what characterises lim sup.

Despite its great success, reinforcement learning struggles when the reward signal is sparse and temporally extended (e.g., in cases where the agent has to perform a complex series of tasks in a specific order). To expedite the learning process in such situations, a particular form of finite-state machines, called reward machines, has recently been shown to help immensely. However, designing a proper reward machine for the task at hand is challenging and remains a tedious and error-prone manual task.

In this presentation, we will survey recent approaches that intertwine reinforcement learning and the inference of reward machines, thereby eliminating the need to craft a reward machine by hand. At their heart, these methods transform the inference task into a series of constraint satisfaction problems that can be solved using off-the-shelf SAT and SMT solvers. We will see how this idea can be used to integrate user-provided advice into the learning process and how it deals with stochastic reward signals. Moreover, we will briefly discuss theoretical properties and hint at empirical evidence demonstrating that reinforcement learning with reward machines outperforms existing methods, such as hierarchical and deep reinforcement learning.

Conformance checking techniques asses the suitability of a process model in representing an underlying process, observed through a collection of real executions. An important problem for conformance checking is to align a log trace with a model, that is, to find the minimal changes necessary to correct a new observation to conform to a process model.

The subject of this work is to study conformance checking for timed models, that is, process models that consider both the sequence of events in a process as well as the timestamps at which each event is recorded. We set our problem of timed alignment and solve two cases, each corresponding to a different metric over timed traces.

In this talk, we show how queueing theory limit theorems can be used to define the domain of feasibility of probabilistic real-time systems and provide sufficient conditions of their schedulability on a single processor under a static-priority policy. We will see how we can approximate response times with the first-passage time of a Brownian motion, and build a scheduling test from this approximation. We will also discuss a possible application in an example.

The problem of solving parity games, or equivalently model-checking for mu-calculus, is known to be both in NP and co-NP: hence, it is widely believed that they are not NP-complete (nor coNP-complete). Yet, for 30 years, we failed to find a polynomial-time algorithm solving them, despite active research on the topic.

The first quasi-polynomial algorithm was found in 2017. Soon after, McNaughton-Zielonka algorithm (an exponential-time recursive algorithm, which is arguably one of the simplest algorithm for solving parity games, and the most effective in practice) was tweaked, first by Parys and then by Lehtinen, Schewe and Wojtczak, to run in quasipolynomial time. In some sense, these algorithms forces McNaughton-Zielonka algorithm to skip enough recursive calls as to run in quasipolynomial time, but not too much so that the output remains correct. We introduce a meta-algorithm that solves parity games, parametrized by trees, which will precisely guide the recursive call made by the algorithm, and show that the output is correct when the trees satisfy some combinatorial property called universality, introduced by Fijalkow and co-authors. McNaughton-Zielonka algorithm and variations can all three be seen as an instantiation of this meta-algorithm on particular classes of universal trees.

I will also emphasize and reformulate these ideas in the slightly more general context of nested fixpoints over finite lattices, and show that these algorithms can be turned into symbolic algorithm that only uses logarithmic symbolic space. The talk is mainly based on a joint work with Marcin Jurdziński and K. S. Thejaswini. The results were proven independently by André Arnold, Damian Niwiński and Paweł Parys, for nested fixpoints.

The performance and reliability of Cyber-Physical Systems are increasingly aided through the use of digital twins, which mirror the static and dynamic behaviour of a Cyber-Physical System (CPS) in software. Digital twins enable the development of self-adaptive CPSs which reconfigure their behaviour in response to novel environments. It is crucial that these self-adaptations are formally verified at runtime, to avoid expensive re-certification of the reconfigured CPS. In this talk, I discuss formally verified self-adaptation in a digital twinning system, by constructing a non-deterministic model which captures the uncertainties in the system behaviour after a self-adaptation. We use Signal Temporal Logic to specify the safety requirements the system must satisfy after reconfiguration and employ formal methods based on verified monitoring over Flow* flowpipes to check these properties at runtime. This gives us a framework to predictively detect and mitigate unsafe self-adaptations before they can lead to unsafe states in the physical system.

Joint work with O. Carton

Normality has been introduced by É. Borel more than one hundred years ago. A real number is normal to an integer base if, in its infinite expansion expressed in that base, all blocks of digits of the same length have the same limiting frequency. Normality can also be characterized by non-compressibility by finite state machines. In this talk, we will present a new result showing that pushdown machines, even deterministic, can compress some normal sequences. This solves positively a question left open by V. Becher, P. A. Heiber and O. Carton.

Given two finite automata A1, A2, recognising languages L1, L2, respectively, the state complexity of union (or intersection, or complement, etc.) is how many states (in terms of the number of states in A1, A2) may be needed in the worst case for an automaton that recognises L1 union L2 (or L1 intersect L2, or the complement of L1, etc.). The state complexity of complementing unambiguous finite automata has long been open, and as late as 2015 Colcombet asked whether unambiguous automata can be complemented with a polynomial blowup. I will report on progress on this question in recent years, both in terms of lower and upper bounds. For the currently best lower bound, techniques from communication complexity play an essential role.

In a two-player win/lose concurrent graph game, two players at a given state concurrently (i.e. simultaneously) choose an action (among a finite set of available actions) which leads to another state. The process is repeated indefinitely thus forming an infinite sequence of states. The winnor of the game is determined by an objective (i.e. a subset of infinite sequences of states).

Concurrent games are more general than their turn-based counterparts in which, at each state, only one player chooses the next state to visit. However, this comes at the cost of not enjoying the desirable properties that turn-based games do. (For instance, in turn-based games with the parity objective, there are always optimal strategies that are pure and positional whereas optimal strategies do not exist in general in concurrent games.) In this talk, I will illustrate the turn-based and concurrent formalisms and show on specific examples why concurrent games behave more poorly than turn-based games. Then I will present how to build concurrent games that are more general than turn-based games but still enjoy similar properties that turn-based game do for specific objectives, namely reachability, Büchi and co-Büchi. This is a joint work with my PhD supervisors Patricia Bouyer and Stéphane Le Roux.

In this talk, we will survey recent advances towards safe and risk-aware probabilistic decision-making. We will study the problem of controlling an agent, represented by a Markov decision process (MDP), so as to maximize the agent’s expected utility while ensuring that the agent’s policy does not violate a given safety constraint. Problems of this form are routinely studied in verification and operations research literature (e.g. in the context of constrained MDPs). However, our focus will be on solving MDPs too large or otherwise complex (e.g. due to the presence of partial observability) to be handled by exact algorithms. To this end, we will present a framework combining Monte carlo tree search, an efficient heuristic algorithm capable of solving very large models (and staying at the core of, e.g. AlphaZero and related algorithms), with techniques inspired by probabilistic verification. The resulting algorithms are capable of solving models beyond the scope of exact algorithms while providing practical (and sometimes even theoretically guaranteed) assurances about satisfaction of the safety constraint. We will examine the presented framework in several contexts, touching topics such as 2-player graph games (discounted-payoff/energy/consumption objectives, multiobjective games), constrained MDPs, risk measures, permissive controller synthesis, shielding, and reinforcement learning.