# Nathalie Bertrand - INRIA Rennes - Bretagne Atlantique

## Contact Details

NameNathalie Bertrand |
||

AffiliationINRIA Rennes - Bretagne Atlantique |
||

CityRennes |
||

CountryFrance |
||

## Pubs By Year |
||

## External Links |
||

## Pub CategoriesComputer Science - Logic in Computer Science (8) Computer Science - Performance (2) Computer Science - Computational Engineering; Finance; and Science (2) Computer Science - Computer Science and Game Theory (2) Computer Science - Programming Languages (1) Mathematics - Analysis of PDEs (1) Mathematics - Numerical Analysis (1) |

## Publications Authored By Nathalie Bertrand

A decade ago, Abdulla et al introduced the elegant concept of decisiveness for denumerable Markov chains [1]. Roughly 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. Denumerable Markov chains however do not encompass stochastic real-time systems, and general stochastic transition systems (STSs) are needed. Read More

**Authors:**Morgan Abily

^{1}, Olivier Delestre

^{2}, Laura Amossé

^{3}, Nathalie Bertrand

^{4}, Christian Laguerre

^{5}, Claire-Marie Duluc

^{6}, Philippe Gourbesville

^{7}

**Affiliations:**

^{1}I-CiTy,

^{2}JAD,

^{3}IRSN,

^{4}IRSN,

^{5}MAPMO,

^{6}IRSN,

^{7}I-CiTy

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. Read More

**Affiliations:**

^{1}Inria Rennes, France,

^{2}IMT - Institute for Advanced Studies Lucca, Italy

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. Read More

**Authors:**Nathalie Bertrand

^{1}, Patricia Bouyer

^{2}, Thomas Brihaye

^{3}, Quentin Menet

^{4}, Christel Baier

^{5}, Marcus Groesser

^{6}, Marcin Jurdzinski

^{7}

**Affiliations:**

^{1}INRIA Rennes - Bretagne Atlantique,

^{2}LSV & ENS Cachan,

^{3}Université de Mons,

^{4}Université de Mons,

^{5}Technische Universität Dresden,

^{6}Technische Universität Dresden,

^{7}University of Warwick

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 $\Phi$, we want to decide whether A satisfies $\Phi$ with probability 1. In this paper, we identify several classes of automata and of properties for which this can be decided. Read More

**Affiliations:**

^{1}INRIA, Rennes,

^{2}University of Trieste

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. Read 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. Read More

**Affiliations:**

^{1}INRIA Rennes - Bretagne Atlantique,

^{2}INRIA Rennes - Bretagne Atlantique,

^{3}University of Rennes 1,

^{4}Institute of Computer Science and Multimedia, Sfax

**Category:**

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. Read More

**Affiliations:**

^{1}Inria Rennes Bretagne Atlantique,

^{2}LSV, CNRS and ENS Cachan

We consider games played on an infinite probabilistic arena where the first player aims at satisfying generalized B\"uchi objectives almost surely, i.e., with probability one. Read 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. Read More

**Affiliations:**

^{1}INRIA Rennes Bretagne Atlantique,

^{2}Université Paris-Est and INRIA Rennes Bretagne Atlantique

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. Read More

**Affiliations:**

^{1}Technische Universität Dresden,

^{2}INRIA Rennes,

^{3}Technische Universität Dresden

**Category:**

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. Read More

**Affiliations:**

^{1}LaBRI,

^{2}LaBRI,

^{3}LaBRI

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. Read 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. Read More