Showing 1–29 of 29 results for author: Bertrand, N

Reusable Formal Verification of DAG-based Consensus Protocols

Authors: Nathalie Bertrand, Pranav Ghorpade, Sasha Rubin, Bernhard Scholz, Pavle Subotic

Abstract: DAG-based consensus protocols are being adoption by blockchain companies to decrease energy footprints and improve security. A DAG-based consensus protocol collaboratively constructs a partial order of blocks of transactions and produces linearly ordered blocks. The ubiquity and strategic importance of blockchains call for formal proof of the correctness of key components, namely, consensus protoc… ▽ More DAG-based consensus protocols are being adoption by blockchain companies to decrease energy footprints and improve security. A DAG-based consensus protocol collaboratively constructs a partial order of blocks of transactions and produces linearly ordered blocks. The ubiquity and strategic importance of blockchains call for formal proof of the correctness of key components, namely, consensus protocols. This paper presents a safety-proven formal specification of two DAG-based protocols. Our specification highlights several dissemination, DAG construction, and ordering variations that can be combined to express the two protocols. The formalization requires a refinement approach for modeling the consensus. In an abstract model, we first show the safety of DAG-based consensus on leader blocks and then further refine the specification to encompass all blocks for all processes. The TLA+ specification for a given protocol consists of 492-732 lines, and the proof system TLAPS verifies 2025-2294 obligations in 6-8 minutes. △ Less

Submitted 2 July, 2024; originally announced July 2024.

Games on Graphs

Authors: Nathanaël Fijalkow, Nathalie Bertrand, Patricia Bouyer-Decitre, Romain Brenguier, Arnaud Carayol, John Fearnley, Hugo Gimbert, Florian Horn, Rasmus Ibsen-Jensen, Nicolas Markey, Benjamin Monmege, Petr Novotný, Mickael Randour, Ocan Sankur, Sylvain Schmitz, Olivier Serre, Mateusz Skomra

Abstract: The objective of this collaborative textbook is to present the state of the art on games on graphs, which is part of a larger research topic called game theory. Games on graphs is the field concerned with games whose rules and evolution are represented by a graph. The objective of this collaborative textbook is to present the state of the art on games on graphs, which is part of a larger research topic called game theory. Games on graphs is the field concerned with games whose rules and evolution are represented by a graph. △ Less

Submitted 17 May, 2023; originally announced May 2023.

Comments: 490 pages. Coordinator: Nathanaël Fijalkow

Holistic Verification of Blockchain Consensus

Authors: Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Marijana Lazić, Pierre Tholoniat, Josef Widder

Abstract: Blockchain has recently attracted the attention of the industry due, in part, to its ability to automate asset transfers. It requires distributed participants to reach a consensus on a block despite the presence of malicious (a.k.a. Byzantine) participants. Malicious participants exploit regularly weaknesses of these blockchain consensus algorithms, with sometimes devastating consequences. In fact… ▽ More Blockchain has recently attracted the attention of the industry due, in part, to its ability to automate asset transfers. It requires distributed participants to reach a consensus on a block despite the presence of malicious (a.k.a. Byzantine) participants. Malicious participants exploit regularly weaknesses of these blockchain consensus algorithms, with sometimes devastating consequences. In fact, these weaknesses are quite common and are well illustrated by the flaws in the hand-written proofs of existing blockchain consensus protocols [63]. Paradoxically, until now, no blockchain consensus has been holistically verified using model checking. In this paper, we remedy this paradox by model checking for the first time a blockchain consensus used in industry. We propose a holistic approach to verify the consensus algorithm of the Red Belly Blockchain [20], for any number $n$ of processes and any number $f<n/3$ of Byzantine processes. We decompose directly the algorithm pseudocode in two parts -- an inner broadcast algorithm and an outer decision algorithm -- each modelled as a threshold automaton [36], and we formalize their expected properties in linear-time temporal logic. We then automatically check the inner broadcasting algorithm, under a carefully identified fairness assumption. For the verification of the outer algorithm, we simplify the model of the inner algorithm by relying on its checked properties. Doing so, we formally verify not only the safety properties of the Red Belly Blockchain consensus but also its liveness in about 70 seconds. △ Less

Submitted 9 June, 2022; originally announced June 2022.

Parameterized safety verification of round-based shared-memory systems

Authors: Nathalie Bertrand, Nicolas Markey, Ocan Sankur, Nicolas Waldburger

Abstract: We consider the parameterized verification problem for distributed algorithms where the goal is to develop techniques to prove the correctness of a given algorithm regardless of the number of participating processes. Motivated by an asynchronous binary consensus algorithm [J. Aspnes, Fast deterministic consensus in a noisy environment. Journal of Algorithms, 2002], we consider round-based distribu… ▽ More We consider the parameterized verification problem for distributed algorithms where the goal is to develop techniques to prove the correctness of a given algorithm regardless of the number of participating processes. Motivated by an asynchronous binary consensus algorithm [J. Aspnes, Fast deterministic consensus in a noisy environment. Journal of Algorithms, 2002], we consider round-based distributed algorithms communicating with shared memory. A particular challenge in these systems is that 1) the number of processes is unbounded, and, more importantly, 2) there is a fresh set of registers at each round. A~verification algorithm thus needs to manage both sources of infinity. In this setting, we prove that the safety verification problem, which consists in deciding whether all possible executions avoid a given error state, is PSPACE-complete. For~negative instances of the safety verification problem, we~also provide exponential lower and upper bounds on the minimal number of processes needed for an error execution and on the minimal round on which the error state can be covered. △ Less

Submitted 25 April, 2022; originally announced April 2022.

Finding the Gap: Neuromorphic Motion Vision in Cluttered Environments

Authors: Thorben Schoepe, Ella Janotte, Moritz B. Milde, Olivier J. N. Bertrand, Martin Egelhaaf, Elisabetta Chicca

Abstract: Many animals meander in environments and avoid collisions. How the underlying neuronal machinery can yield robust behaviour in a variety of environments remains unclear. In the fly brain, motion-sensitive neurons indicate the presence of nearby objects and directional cues are integrated within an area known as the central complex. Such neuronal machinery, in contrast with the traditional stream-b… ▽ More Many animals meander in environments and avoid collisions. How the underlying neuronal machinery can yield robust behaviour in a variety of environments remains unclear. In the fly brain, motion-sensitive neurons indicate the presence of nearby objects and directional cues are integrated within an area known as the central complex. Such neuronal machinery, in contrast with the traditional stream-based approach to signal processing, uses an event-based approach, with events occurring when changes are sensed by the animal. Contrary to von Neumann computing architectures, event-based neuromorphic hardware is designed to process information in an asynchronous and distributed manner. Inspired by the fly brain, we model, for the first time, a neuromorphic closed-loop system mimicking essential behaviours observed in flying insects, such as meandering in clutter and gap crossing, which are highly relevant for autonomous vehicles. We implemented our system both in software and on neuromorphic hardware. While moving through an environment, our agent perceives changes in its surroundings and uses this information for collision avoidance. The agent's manoeuvres result from a closed action-perception loop implementing probabilistic decision-making processes. This loop-closure is thought to have driven the development of neural circuitry in biological agents since the Cambrian explosion. In the fundamental quest to understand neural computation in artificial agents, we come closer to understanding and modelling biological intelligence by closing the loop also in neuromorphic systems. As a closed-loop system, our system deepens our understanding of processing in neural networks and computations in biological and artificial systems. With these investigations, we aim to set the foundations for neuromorphic intelligence in the future, moving towards leveraging the full potential of neuromorphic systems. △ Less

Submitted 16 February, 2021; originally announced February 2021.

Comments: 7 main pages with two figures, including appendix 26 pages with 14 figures

Dynamic network congestion games

Authors: Nathalie Bertrand, Nicolas Markey, Suman Sadhukhan, Ocan Sankur

Abstract: Congestion games are a classical type of games studied in game theory, in which n players choose a resource, and their individual cost increases with the number of other players choosing the same resource. In network congestion games (NCGs), the resources correspond to simple paths in a graph, e.g. representing routing options from a source to a target. In this paper, we introduce a variant of NCG… ▽ More Congestion games are a classical type of games studied in game theory, in which n players choose a resource, and their individual cost increases with the number of other players choosing the same resource. In network congestion games (NCGs), the resources correspond to simple paths in a graph, e.g. representing routing options from a source to a target. In this paper, we introduce a variant of NCGs, referred to as dynamic NCGs: in this setting, players take transitions synchronously, they select their next transitions dynamically, and they are charged a cost that depends on the number of players simultaneously using the same transition. We study, from a complexity perspective, standard concepts of game theory in dynamic NCGs: social optima, Nash equilibria, and subgame perfect equilibria. Our contributions are the following: the existence of a strategy profile with social cost bounded by a constant is in PSPACE and NP-hard. (Pure) Nash equilibria always exist in dynamic NCGs; the existence of a Nash equilibrium with bounded cost can be decided in EXPSPACE, and computing a witnessing strategy profile can be done in doubly-exponential time. The existence of a subgame perfect equilibrium with bounded cost can be decided in 2EXPSPACE, and a witnessing strategy profile can be computed in triply-exponential time. △ Less

Submitted 28 September, 2020; originally announced September 2020.

Comments: Full version of a paper to appear at FSTTCS 2020

Taming denumerable Markov decision processes with decisiveness

Authors: Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Paulin Fournier

Abstract: Decisiveness has proven to be an elegant concept for denumerable Markov chains: it is general enough to encompass several natural classes of denumerable Markov chains, and is a sufficient condition for simple qualitative and approximate quantitative model checking algorithms to exist. In this paper, we explore how to extend the notion of decisiveness to Markov decision processes. Compared to Marko… ▽ More Decisiveness has proven to be an elegant concept for denumerable Markov chains: it is general enough to encompass several natural classes of denumerable Markov chains, and is a sufficient condition for simple qualitative and approximate quantitative model checking algorithms to exist. In this paper, we explore how to extend the notion of decisiveness to Markov decision processes. Compared to Markov chains, the extra non-determinism can be resolved in an adversarial or cooperative way, yielding two natural notions of decisiveness. We then explore whether these notions yield model checking procedures concerning the infimum and supremum probabilities of reachability properties. △ Less

Submitted 24 August, 2020; originally announced August 2020.

Synthesizing safe coalition strategies

Authors: Nathalie Bertrand, Patricia Bouyer, Anirban Majumdar

Abstract: Concurrent games with a fixed number of agents have been thoroughly studied, with various solution concepts and objectives for the agents. In this paper, we consider concurrent games with an arbitrary number of agents, and study the problem of synthesizing a coalition strategy to achieve a global safety objective. The problem is non-trivial since the agents do not know a priori how many they are w… ▽ More Concurrent games with a fixed number of agents have been thoroughly studied, with various solution concepts and objectives for the agents. In this paper, we consider concurrent games with an arbitrary number of agents, and study the problem of synthesizing a coalition strategy to achieve a global safety objective. The problem is non-trivial since the agents do not know a priori how many they are when they start the game. We prove that the existence of a safe arbitrary-large coalition strategy for safety objectives is a PSPACE-hard problem that can be decided in exponential space. △ Less

Submitted 30 September, 2020; v1 submitted 9 August, 2020; originally announced August 2020.

Reconfiguration and Message Losses in Parameterized Broadcast Networks

Authors: Nathalie Bertrand, Patricia Bouyer, Anirban Majumdar

Abstract: Broadcast networks allow one to model networks of identical nodes communicating through message broadcasts. Their parameterized verification aims at proving a property holds for any number of nodes, under any communication topology, and on all possible executions. We focus on the coverability problem which dually asks whether there exists an execution that visits a configuration exhibiting some gi… ▽ More Broadcast networks allow one to model networks of identical nodes communicating through message broadcasts. Their parameterized verification aims at proving a property holds for any number of nodes, under any communication topology, and on all possible executions. We focus on the coverability problem which dually asks whether there exists an execution that visits a configuration exhibiting some given state of the broadcast protocol. Coverability is known to be undecidable for static networks, i.e. when the number of nodes and communication topology is fixed along executions. In contrast, it is decidable in PTIME when the communication topology may change arbitrarily along executions, that is for reconfigurable networks. Surprisingly, no lower nor upper bounds on the minimal number of nodes, or the minimal length of covering execution in reconfigurable networks, appear in the literature. In this paper we show tight bounds for cutoff and length, which happen to be linear and quadratic, respectively, in the number of states of the protocol. We also introduce an intermediary model with static communication topology and non-deterministic message losses upon sending. We show that the same tight bounds apply to lossy networks, although, reconfigurable executions may be linearly more succinct than lossy executions. Finally, we show NP-completeness for the natural optimisation problem associated with the cutoff. △ Less

Submitted 17 March, 2021; v1 submitted 15 December, 2019; originally announced December 2019.

Journal ref: Logical Methods in Computer Science, Volume 17, Issue 1 (March 18, 2021) lmcs:5981

Controlling a population

Authors: Nathalie Bertrand, Miheer Dewaskar, Blaise Genest, Hugo Gimbert, Adwait Amit Godbole

Abstract: We introduce a new setting where a population of agents, each modelled by a finite-state system, are controlled uniformly: the controller applies the same action to every agent. The framework is largely inspired by the control of a biological system, namely a population of yeasts, where the controller may only change the environment common to all cells. We study a synchronisation problem for such… ▽ More We introduce a new setting where a population of agents, each modelled by a finite-state system, are controlled uniformly: the controller applies the same action to every agent. The framework is largely inspired by the control of a biological system, namely a population of yeasts, where the controller may only change the environment common to all cells. We study a synchronisation problem for such populations: no matter how individual agents react to the actions of the controller, the controller aims at driving all agents synchronously to a target state. The agents are naturally represented by a non-deterministic finite state automaton (NFA), the same for every agent, and the whole system is encoded as a 2-player game. The first player (Controller) chooses actions, and the second player (Agents) resolves non-determinism for each agent. The game with m agents is called the m -population game. This gives rise to a parameterized control problem (where control refers to 2 player games), namely the population control problem: can Controller control the m-population game for all m in N whatever Agents does? △ Less

Submitted 26 July, 2019; v1 submitted 2 July, 2018; originally announced July 2018.

Comments: This is a journal version of the extended abstract arXiv:1707.02058 which appeared in Concur 2017, together with proofs

Journal ref: Logical Methods in Computer Science, Volume 15, Issue 3 (July 29, 2019) lmcs:4662

Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes

Authors: Christel Baier, Nathalie Bertrand, Clemens Dubslaff, Daniel Gburek, Ocan Sankur

Abstract: The paper deals with finite-state Markov decision processes (MDPs) with integer weights assigned to each state-action pair. New algorithms are presented to classify end components according to their limiting behavior with respect to the accumulated weights. These algorithms are used to provide solutions for two types of fundamental problems for integer-weighted MDPs. First, a polynomial-time algor… ▽ More The paper deals with finite-state Markov decision processes (MDPs) with integer weights assigned to each state-action pair. New algorithms are presented to classify end components according to their limiting behavior with respect to the accumulated weights. These algorithms are used to provide solutions for two types of fundamental problems for integer-weighted MDPs. First, a polynomial-time algorithm for the classical stochastic shortest path problem is presented, generalizing known results for special classes of weighted MDPs. Second, qualitative probability constraints for weight-bounded (repeated) reachability conditions are addressed. Among others, it is shown that the problem to decide whether a disjunction of weight-bounded reachability conditions holds almost surely under some scheduler belongs to $\textrm{NP}\cap \textrm{coNP}$, is solvable in pseudo-polynomial time and is at least as hard as solving two-player mean-payoff games, while the corresponding problem for universal quantification over schedulers is solvable in polynomial time. △ Less

Submitted 30 April, 2018; originally announced April 2018.

MSC Class: 68Q87 ACM Class: G.3; F.4.1; D.2.4

Parameterized verification of synchronization in constrained reconfigurable broadcast networks

Authors: A. R. Balasubramanian, Nathalie Bertrand, Nicolas Markey

Abstract: Reconfigurable broadcast networks provide a convenient formalism for modelling and reasoning about networks of mobile agents broadcasting messages to other agents following some (evolving) communication topology. The parameterized verification of such models aims at checking whether a given property holds irrespective of the initial configuration (number of agents, initial states and initial commu… ▽ More Reconfigurable broadcast networks provide a convenient formalism for modelling and reasoning about networks of mobile agents broadcasting messages to other agents following some (evolving) communication topology. The parameterized verification of such models aims at checking whether a given property holds irrespective of the initial configuration (number of agents, initial states and initial communication topology). We focus here on the synchronization property, asking whether all agents converge to a set of target states after some execution. This problem is known to be decidable in polynomial time when no constraints are imposed on the evolution of the communication topology (while it is undecidable for static broadcast networks). In this paper we investigate how various constraints on reconfigurations affect the decidability and complexity of the synchronization problem. In particular, we show that when bounding the number of reconfigured links between two communications steps by a constant, synchronization becomes undecidable; on the other hand, synchronization remains decidable in PTIME when the bound grows with the number of agents. △ Less

Submitted 23 February, 2018; originally announced February 2018.

Comments: Accepted for publication in TACAS 2018

Controlling a Population

Authors: Nathalie Bertrand, Miheer Dewaskar, Blaise Genest, Hugo Gimbert

Abstract: We introduce a new setting where a population of agents, each modelled by a finite-state system, are controlled uniformly: the controller applies the same action to every agent. The framework is largely inspired by the control of a biological system, namely a population of yeasts, where the controller may only change the environment common to all cells. We study a synchronisation problem for such… ▽ More We introduce a new setting where a population of agents, each modelled by a finite-state system, are controlled uniformly: the controller applies the same action to every agent. The framework is largely inspired by the control of a biological system, namely a population of yeasts, where the controller may only change the environment common to all cells. We study a synchronisation problem for such populations: no matter how individual agents react to the actions of the controller , the controller aims at driving all agents synchronously to a target state. The agents are naturally represented by a non-deterministic finite state automaton (NFA), the same for every agent, and the whole system is encoded as a 2-player game. The first player (Controller) chooses actions, and the second player (Agents) resolves non-determinism for each agent. The game with m agents is called the m-population game. This gives rise to a parameterized control problem (where control refers to 2 player games), namely the population control problem: can Controller control the m-population game for all $m $\in$ N$ whatever Agents does? In this paper, we prove that the population control problem is decidable, and it is a EXPTIME-complete problem. As far as we know, this is one of the first results on parameterized control. Our algorithm, not based on cutoff techniques, produces winning strategies which are symbolic, that is, they do not need to count precisely how the population is spread between states. We also show that if there is no winning strategy, then there is a population size M such that Controller wins the m-population game if and only if $m $\le$ M$. Surprisingly, M can be doubly exponential in the number of states of the NFA, with tight upper and lower bounds. △ Less

Submitted 7 July, 2017; originally announced July 2017.

When are Stochastic Transition Systems Tameable?

Authors: Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Pierre Carlier

Abstract: A decade ago, Abdulla, Ben Henda and Mayr introduced the elegant concept of decisiveness for denumerable Markov chains [1]. Roughly speaking, decisiveness allows one to lift most good properties from finite Markov chains to denumerable ones, and therefore to adapt existing verification algorithms to infinite-state models. Decisive Markov chains however do not encompass stochastic real-time systems… ▽ More A decade ago, Abdulla, Ben Henda and Mayr introduced the elegant concept of decisiveness for denumerable Markov chains [1]. Roughly speaking, decisiveness allows one to lift most good properties from finite Markov chains to denumerable ones, and therefore to adapt existing verification algorithms to infinite-state models. Decisive Markov chains however do not encompass stochastic real-time systems, and general stochastic transition systems (STSs for short) are needed. In this article, we provide a framework to perform both the qualitative and the quantitative analysis of STSs. First, we define various notions of decisiveness (inherited from [1]), notions of fairness and of attractors for STSs, and make explicit the relationships between them. Then, we define a notion of abstraction, together with natural concepts of soundness and completeness, and we give general transfer properties, which will be central to several verification algorithms on STSs. We further design a generic construction which will be useful for the analysis of ω-regular properties, when a finite attractor exists, either in the system (if it is denumerable), or in a sound denumerable abstraction of the system. We next provide algorithms for qualitative model-checking, and generic approximation procedures for quantitative model-checking. Finally, we instantiate our framework with stochastic timed automata (STA), generalized semi-Markov processes (GSMPs) and stochastic time Petri nets (STPNs), three models combining dense-time and probabilities. This allows us to derive decidability and approximability results for the verification of these models. Some of these results were known from the literature, but our generic approach permits to view them in a unified framework, and to obtain them with less effort. We also derive interesting new approximability results for STA, GSMPs and STPNs. △ Less

Submitted 4 April, 2018; v1 submitted 14 March, 2017; originally announced March 2017.

Comments: 77 pages

Global Sensitivity Analysis with 2D Hydraulic Codes: Application on Uncertainties Related to High-Resolution Topographic Data

Authors: M Abily, O Delestre, P Gourbesville, N Bertrand, C. -M Duluc, Y Richet

Abstract: Technologies such as aerial photogrammetry allow production of 3D topographic data including complex environments such as urban areas. Therefore, it is possible to create High Resolution (HR) Digital Elevation Models (DEM) incorporating thin above ground elements influencing overland flow paths. Even though this category of big data has a high level of accuracy, there are still errors in measureme… ▽ More Technologies such as aerial photogrammetry allow production of 3D topographic data including complex environments such as urban areas. Therefore, it is possible to create High Resolution (HR) Digital Elevation Models (DEM) incorporating thin above ground elements influencing overland flow paths. Even though this category of big data has a high level of accuracy, there are still errors in measurements and hypothesis under DEM elaboration. Moreover, operators look for optimizing spatial discretization resolution in order to improve flood models computation time. Errors in measurement, errors in DEM generation, and operator choices for inclusion of this data within 2D hydraulic model, might influence results of flood models simulations. These errors and hypothesis may influence significantly flood modelling results variability. The purpose of this study is to investigate uncertainties related to (i) the own error of high resolution topographic data, and (ii) the modeller choices when including topographic data in hydraulic codes. The aim is to perform a Global Sensitivity Analysis (GSA) which goes through a Monte-Carlo uncertainty propagation, to quantify impact of uncertainties, followed by a Sobol' indices computation, to rank influence of identified parameters on result variability. A process using a coupling of an environment for parametric computation (Prom{é}th{é}e) and a code relying on 2D shallow water equations (FullSWOF 2D) has been developed (P-FS tool). The study has been performed over the lower part of the Var river valley using the estimated hydrograph of 1994 flood event. HR topographic data has been made available for the study area, which is 17.5 km 2 , by Nice municipality. Three uncertain parameters were studied: the measurement error (var. E), the level of details of above-ground element representation in DEM (buildings, sidewalks, etc.) (var. S), and the spatial discretization resolution (grid cell size for regular mesh) (var. R). Parameter var. E follows a probability density function, whereas parameters var. S and var. R. are discrete operator choices. Combining these parameters, a database of 2, 000 simulations has been produced using P-FS tool implemented on a high performance computing structure. In our study case, the output of interest is the maximal △ Less

Submitted 24 March, 2016; originally announced April 2016.

Journal ref: 2014, Jun 2014, Sophia Antipolis - Nice, France. Springer Singapore, Advances in Hydroinformatics - Simhydro 2014, pp.301-315, 2015, Advances in Hydroinformatics - Simhydro 2014

Global sensitivity analysis with 2d hydraulic codes: applied protocol and practical tool

Authors: M Abily, N Bertrand, O Delestre, P Gourbesville, Y Richet, C. -M Duluc

Abstract: Global Sensitivity Analysis (GSA) methods are useful tools to rank input parameters uncertainties regarding their impact on result variability. In practice, such type of approach is still at an exploratory level for studies relying on 2D Shallow Water Equations (SWE) codes as GSA requires specific tools and deals with important computational capacity. The aim of this paper is to provide both a pro… ▽ More Global Sensitivity Analysis (GSA) methods are useful tools to rank input parameters uncertainties regarding their impact on result variability. In practice, such type of approach is still at an exploratory level for studies relying on 2D Shallow Water Equations (SWE) codes as GSA requires specific tools and deals with important computational capacity. The aim of this paper is to provide both a protocol and a tool to carry out a GSA for 2D hydraulic modelling applications. A coupled tool between Prom{é}th{é}e (a parametric computation environment) and FullSWOF 2D (a code relying on 2D SWE) has been set up: Prom{é}th{é}e-FullSWOF 2D (P-FS). The main steps of our protocol are: i) to identify the 2D hydraulic code input parameters of interest and to assign them a probability density function, ii) to propagate uncertainties within the model, and iii) to rank the effects of each input parameter on the output of interest. For our study case, simulations of a river flood event were run with uncertainties introduced through three parameters using P-FS tool. Tests were performed on regular computational mesh, spatially discretizing an urban area, using up to 17.9 million of computational points. P-FS tool has been installed on a cluster for computation. Method and P-FS tool successfully allow the computation of Sobol indices maps. Keywords Uncertainty, flood hazard modelling, global sensitivity analysis, 2D shallow water equation, Sobol index. Analyse globale de sensibilit{é} en mod{é}lisation hydrauliqu{è} a surface libre 2D : application d'un protocole et d{é}veloppement d'outils op{é}rationnels -- Les m{é}thodes d'analyse de sensibilit{é} permettent de contr{ô}ler la robustesse des r{é}sultats de mod{é}lisation ainsi que d'identifier le degr{é} d'influence des param etres d' entr{é}e sur le r{é}sultat en sortie d'un mod ele. Le processus complet constitue une analyse globale de sensibilit{é} (GSA). Ce type d'approche pr{é}sente un grand int{é}r{ê}t pour analyser les incer-titudes de r{é}sultats de mod{é}lisation , mais est toujours a un stade exploratoire dans les etudes appliqu{é}es mettant en jeu des codes bas{é}s sur la r{é}solution bidimensionnelle des equations de Saint-Venant. En effet, l' impl{é}mentation d'une GSA est d{é}licate car elle △ Less

Submitted 24 March, 2016; originally announced March 2016.

Journal ref: La Houille Blanche - Revue internationale de l'eau, EDP Sciences, 2015, 5, pp.16-22

Use of 3D classified topographic data with FullSWOF for high resolution simulation of a river flood event over a dense urban area

Authors: Morgan Abily, Olivier Delestre, Laura Amossé, Nathalie Bertrand, Christian Laguerre, Claire-Marie Duluc, Philippe Gourbesville

Abstract: High resolution (infra-metric) topographic data, including photogram-metric born 3D classified data, are becoming commonly available at large range of spatial extend, such as municipality or industrial site scale. This category of dataset is promising for high resolution (HR) Digital Surface Model (DSM) generation, allowing inclusion of fine above-ground structures which might influence overland f… ▽ More High resolution (infra-metric) topographic data, including photogram-metric born 3D classified data, are becoming commonly available at large range of spatial extend, such as municipality or industrial site scale. This category of dataset is promising for high resolution (HR) Digital Surface Model (DSM) generation, allowing inclusion of fine above-ground structures which might influence overland flow hydrodynamic in urban environment. Nonetheless several categories of technical and numerical challenges arise from this type of data use with standard 2D Shallow Water Equations (SWE) based numerical codes. FullSWOF (Full Shallow Water equations for Overland Flow) is a code based on 2D SWE under conservative form. This code relies on a well-balanced finite volume method over a regular grid using numerical method based on hydrostatic reconstruction scheme. When compared to existing industrial codes used for urban flooding simulations, numerical approach implemented in FullSWOF allows to handle properly flow regime changes, preservation of water depth positivity at wet/dry cells transitions and steady state preservation. FullSWOF has already been tested on analytical solution library (SWASHES) and has been used to simulate runoff and dam-breaks. FullSWOFs above mentioned properties are of good interest for urban overland flow. Objectives of this study are (i) to assess the feasibility and added values of using HR 3D classified topographic data to model river overland flow and (ii) to take advantage of FullSWOF code properties for overland flow simulation in urban environment. △ Less

Submitted 24 March, 2016; originally announced March 2016.

Comments: 3rd IAHR Europe Congress, 14-16 April 2014, Porto, Portugal, Apr 2014, Porto, Portugal. 2016

Proceedings Thirteenth Workshop on Quantitative Aspects of Programming Languages and Systems

Authors: Nathalie Bertrand, Mirco Tribastone

Abstract: This volume contains the proceedings of the Thirteenth Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2015), held in London, UK, on 11 and 12 April, 2015. QAPL 2015 was a satellite event of the European Joint Conferences on Theory and Practice of Software (ETAPS) focussing on quantitative aspects of computation. The Program Committee of QAPL 2015 selected 8 regular pap… ▽ More This volume contains the proceedings of the Thirteenth Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2015), held in London, UK, on 11 and 12 April, 2015. QAPL 2015 was a satellite event of the European Joint Conferences on Theory and Practice of Software (ETAPS) focussing on quantitative aspects of computation. The Program Committee of QAPL 2015 selected 8 regular papers and 2 presentation-only papers. The workshop programme included two QAPL keynote presentations by Catuscia Palamidessi (Inria/LIX, France) on "Quantitative Aspects of Privacy and Information Flow," and Holger Hermanns (Saarland University, Germany) on "Optimal Continuous Time Markov Decisions." △ Less

Submitted 27 September, 2015; originally announced September 2015.

Journal ref: EPTCS 194, 2015

Stochastic Timed Automata

Authors: Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Quentin Menet, Christel Baier, Marcus Groesser, Marcin Jurdzinski

Abstract: A stochastic timed automaton is a purely stochastic process defined on a timed automaton, in which both delays and discrete choices are made randomly. We study the almost-sure model-checking problem for this model, that is, given a stochastic timed automaton A and a property $Φ$, we want to decide whether A satisfies $Φ$ with probability 1. In this paper, we identify several classes of automata a… ▽ More A stochastic timed automaton is a purely stochastic process defined on a timed automaton, in which both delays and discrete choices are made randomly. We study the almost-sure model-checking problem for this model, that is, given a stochastic timed automaton A and a property $Φ$, we want to decide whether A satisfies $Φ$ with probability 1. In this paper, we identify several classes of automata and of properties for which this can be decided. The proof relies on the construction of a finite abstraction, called the thick graph, that we interpret as a finite Markov chain, and for which we can decide the almost-sure model-checking problem. Correctness of the abstraction holds when automata are almost-surely fair, which we show, is the case for two large classes of systems, single- clock automata and so-called weak-reactive automata. Techniques employed in this article gather tools from real-time verification and probabilistic verification, as well as topological games played on timed automata. △ Less

Submitted 7 December, 2014; v1 submitted 8 October, 2014; originally announced October 2014.

Comments: 40 pages + appendix

Journal ref: Logical Methods in Computer Science, Volume 10, Issue 4 (December 9, 2014) lmcs:1092

Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems

Authors: Nathalie Bertrand, Luca Bortolussi

Abstract: This volume contains the proceedings of the Twelfth Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2014), held in Grenoble, France, on 12 and 13 April, 2014. QAPL 2014 was a satellite event of the European Joint Conferences on Theory and Practice of Software (ETAPS). The central theme of the workshop is that of quantitative aspects of computation. These aspects are re… ▽ More This volume contains the proceedings of the Twelfth Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2014), held in Grenoble, France, on 12 and 13 April, 2014. QAPL 2014 was a satellite event of the European Joint Conferences on Theory and Practice of Software (ETAPS). The central theme of the workshop is that of quantitative aspects of computation. These aspects are related to the use of physical quantities (storage space, time, bandwidth, etc.) as well as mathematical quantities (e.g. probability and measures for reliability, security and trust), and play an important (sometimes essential) role in characterising the behaviour and determining the properties of systems. Such quantities are central to the definition of both the model of systems (architecture, language design, semantics) and the methodologies and tools for the analysis and verification of the systems properties. The aim of this workshop is to discuss the explicit use of quantitative information such as time and probabilities either directly in the model or as a tool for the analysis of systems. △ Less

Submitted 5 June, 2014; originally announced June 2014.

Journal ref: EPTCS 154, 2014

Emptiness and Universality Problems in Timed Automata with Positive Frequency

Authors: Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Amelie Stainer

Abstract: The languages of infinite timed words accepted by timed automata are traditionally defined using Buchi-like conditions. These acceptance conditions focus on the set of locations visited infinitely often along a run, but completely ignore quantitative timing aspects. In this paper we propose a natural quantitative semantics for timed automata based on the so-called frequency, which measures the pro… ▽ More The languages of infinite timed words accepted by timed automata are traditionally defined using Buchi-like conditions. These acceptance conditions focus on the set of locations visited infinitely often along a run, but completely ignore quantitative timing aspects. In this paper we propose a natural quantitative semantics for timed automata based on the so-called frequency, which measures the proportion of time spent in the accepting locations. We study various properties of timed languages accepted with positive frequency, and in particular the emptiness and universality problems. △ Less

Submitted 11 September, 2013; originally announced September 2013.

Off-line test selection with test purposes for non-deterministic timed automata

Authors: Nathalie Bertrand, Thierry Jéron, Amélie Stainer, Moez Krichen

Abstract: This article proposes novel off-line test generation techniques from non-deterministic timed automata with inputs and outputs (TAIOs) in the formal framework of the tioco conformance theory. In this context, a first problem is the determinization of TAIOs, which is necessary to foresee next enabled actions after an observable trace, but is in general impossible because not all timed automata are d… ▽ More This article proposes novel off-line test generation techniques from non-deterministic timed automata with inputs and outputs (TAIOs) in the formal framework of the tioco conformance theory. In this context, a first problem is the determinization of TAIOs, which is necessary to foresee next enabled actions after an observable trace, but is in general impossible because not all timed automata are determinizable. This problem is solved thanks to an approximate determinization using a game approach. The algorithm performs an io-abstraction which preserves the tioco conformance relation and thus guarantees the soundness of generated test cases. A second problem is the selection of test cases from a TAIO specification. The selection here relies on a precise description of timed behaviors to be tested which is carried out by expressive test purposes modeled by a generalization of TAIOs. Finally, an algorithm is described which generates test cases in the form of TAIOs equipped with verdicts, using a symbolic co-reachability analysis guided by the test purpose. Properties of test cases are then analyzed with respect to the precision of the approximate determinization: when determinization is exact, which is the case on known determinizable classes, in addition to soundness, properties characterizing the adequacy of test cases verdicts are also guaranteed. △ Less

Submitted 16 October, 2012; v1 submitted 26 July, 2012; originally announced July 2012.

Comments: 33 pages; Logical Methods in Computer Science 2002; 10.2168/LMCS-???

ACM Class: D.2.4; D.2.5; D.4.7; F.1.1

Journal ref: Logical Methods in Computer Science, Volume 8, Issue 4 (October 17, 2012) lmcs:1037

Solving Stochastic Büchi Games on Infinite Arenas with a Finite Attractor

Authors: Nathalie Bertrand, Philippe Schnoebelen

Abstract: We consider games played on an infinite probabilistic arena where the first player aims at satisfying generalized Büchi objectives almost surely, i.e., with probability one. We provide a fixpoint characterization of the winning sets and associated winning strategies in the case where the arena satisfies the finite-attractor property. From this we directly deduce the decidability of these games on… ▽ More We consider games played on an infinite probabilistic arena where the first player aims at satisfying generalized Büchi objectives almost surely, i.e., with probability one. We provide a fixpoint characterization of the winning sets and associated winning strategies in the case where the arena satisfies the finite-attractor property. From this we directly deduce the decidability of these games on probabilistic lossy channel systems. △ Less

Submitted 11 June, 2013; v1 submitted 19 July, 2012; originally announced July 2012.

Comments: In Proceedings QAPL 2013, arXiv:1306.2413

ACM Class: D.2.4; G.3; C.2.2

Journal ref: EPTCS 117, 2013, pp. 116-131

Bounded Satisfiability for PCTL

Authors: Nathalie Bertrand, John Fearnley, Sven Schewe

Abstract: While model checking PCTL for Markov chains is decidable in polynomial-time, the decidability of PCTL satisfiability, as well as its finite model property, are long standing open problems. While general satisfiability is an intriguing challenge from a purely theoretical point of view, we argue that general solutions would not be of interest to practitioners: such solutions could be too big to be i… ▽ More While model checking PCTL for Markov chains is decidable in polynomial-time, the decidability of PCTL satisfiability, as well as its finite model property, are long standing open problems. While general satisfiability is an intriguing challenge from a purely theoretical point of view, we argue that general solutions would not be of interest to practitioners: such solutions could be too big to be implementable or even infinite. Inspired by bounded synthesis techniques, we turn to the more applied problem of seeking models of a bounded size: we restrict our search to implementable -- and therefore reasonably simple -- models. We propose a procedure to decide whether or not a given PCTL formula has an implementable model by reducing it to an SMT problem. We have implemented our techniques and found that they can be applied to the practical problem of sanity checking -- a procedure that allows a system designer to check whether their formula has an unexpectedly small model. △ Less

Submitted 30 March, 2012; originally announced April 2012.

Probabilistic regular graphs

Authors: Nathalie Bertrand, Christophe Morvan

Abstract: Deterministic graph grammars generate regular graphs, that form a structural extension of configuration graphs of pushdown systems. In this paper, we study a probabilistic extension of regular graphs obtained by labelling the terminal arcs of the graph grammars by probabilities. Stochastic properties of these graphs are expressed using PCTL, a probabilistic extension of computation tree logic. We… ▽ More Deterministic graph grammars generate regular graphs, that form a structural extension of configuration graphs of pushdown systems. In this paper, we study a probabilistic extension of regular graphs obtained by labelling the terminal arcs of the graph grammars by probabilities. Stochastic properties of these graphs are expressed using PCTL, a probabilistic extension of computation tree logic. We present here an algorithm to perform approximate verification of PCTL formulae. Moreover, we prove that the exact model-checking problem for PCTL on probabilistic regular graphs is undecidable, unless restricting to qualitative properties. Our results generalise those of EKM06, on probabilistic pushdown automata, using similar methods combined with graph grammars techniques. △ Less

Submitted 31 October, 2010; originally announced November 2010.

Comments: In Proceedings INFINITY 2010, arXiv:1010.6112

Journal ref: EPTCS 39, 2010, pp. 77-90

Probabilistic Automata over Infinite Words: Expressiveness, Efficiency, and Decidability

Authors: Christel Baier, Nathalie Bertrand, Marcus Größer

Abstract: Probabilistic omega-automata are variants of nondeterministic automata for infinite words where all choices are resolved by probabilistic distributions. Acceptance of an infinite input word can be defined in different ways: by requiring that (i) the probability for the accepting runs is positive (probable semantics), or (ii) almost all runs are accepting (almost-sure semantics), or (iii) the pro… ▽ More Probabilistic omega-automata are variants of nondeterministic automata for infinite words where all choices are resolved by probabilistic distributions. Acceptance of an infinite input word can be defined in different ways: by requiring that (i) the probability for the accepting runs is positive (probable semantics), or (ii) almost all runs are accepting (almost-sure semantics), or (iii) the probability measure of the accepting runs is greater than a certain threshold (threshold semantics). The underlying notion of an accepting run can be defined as for standard omega-automata by means of a Buechi condition or other acceptance conditions, e.g., Rabin or Streett conditions. In this paper, we put the main focus on the probable semantics and provide a summary of the fundamental properties of probabilistic omega-automata concerning expressiveness, efficiency, and decision problems. △ Less

Submitted 27 July, 2009; originally announced July 2009.

ACM Class: F.4.3

Journal ref: EPTCS 3, 2009, pp. 3-16

Determinacy and Decidability of Reachability Games with Partial Observation on Both Sides

Authors: Nathalie Bertrand, Blaise Genest, Hugo Gimbert

Abstract: We prove two determinacy and decidability results about two-players stochastic reachability games with partial observation on both sides and finitely many states, signals and actions. We prove two determinacy and decidability results about two-players stochastic reachability games with partial observation on both sides and finitely many states, signals and actions. △ Less

Submitted 24 November, 2008; originally announced November 2008.

On computing fixpoints in well-structured regular model checking, with applications to lossy channel systems

Authors: C. Baier, N. Bertrand, Ph. Schnoebelen

Abstract: We prove a general finite convergence theorem for "upward-guarded" fixpoint expressions over a well-quasi-ordered set. This has immediate applications in regular model checking of well-structured systems, where a main issue is the eventual convergence of fixpoint computations. In particular, we are able to directly obtain several new decidability results on lossy channel systems. We prove a general finite convergence theorem for "upward-guarded" fixpoint expressions over a well-quasi-ordered set. This has immediate applications in regular model checking of well-structured systems, where a main issue is the eventual convergence of fixpoint computations. In particular, we are able to directly obtain several new decidability results on lossy channel systems. △ Less

Submitted 21 June, 2006; originally announced June 2006.

Comments: 16 pages

Journal ref: Proc. LPAR 2006, LNCS 4246, pp. 347-361, Springer 2006

Verifying nondeterministic probabilistic channel systems against $ω$-regular linear-time properties

Authors: Christel Baier, Nathalie Bertrand, Philippe Schnoebelen

Abstract: Lossy channel systems (LCSs) are systems of finite state automata that communicate via unreliable unbounded fifo channels. In order to circumvent the undecidability of model checking for nondeterministic LCSs, probabilistic models have been introduced, where it can be decided whether a linear-time property holds almost surely. However, such fully probabilistic systems are not a faithful model o… ▽ More Lossy channel systems (LCSs) are systems of finite state automata that communicate via unreliable unbounded fifo channels. In order to circumvent the undecidability of model checking for nondeterministic LCSs, probabilistic models have been introduced, where it can be decided whether a linear-time property holds almost surely. However, such fully probabilistic systems are not a faithful model of nondeterministic protocols. We study a hybrid model for LCSs where losses of messages are seen as faults occurring with some given probability, and where the internal behavior of the system remains nondeterministic. Thus the semantics is in terms of infinite-state Markov decision processes. The purpose of this article is to discuss the decidability of linear-time properties formalized by formulas of linear temporal logic (LTL). Our focus is on the qualitative setting where one asks, e.g., whether a LTL-formula holds almost surely or with zero probability (in case the formula describes the bad behaviors). Surprisingly, it turns out that -- in contrast to finite-state Markov decision processes -- the satisfaction relation for LTL formulas depends on the chosen type of schedulers that resolve the nondeterminism. While all variants of the qualitative LTL model checking problem for the full class of history-dependent schedulers are undecidable, the same questions for finite-memory scheduler can be solved algorithmically. However, the restriction to reachability properties and special kinds of recurrent reachability properties yields decidable verification problems for the full class of schedulers, which -- for this restricted class of properties -- are as powerful as finite-memory schedulers, or even a subclass of them. △ Less

Submitted 11 April, 2006; v1 submitted 4 November, 2005; originally announced November 2005.

Comments: 39 pages

Journal ref: ACM Trans. Computational Logic 9(1), 2007