Nathalie Bertrand - INRIA Rennes - Bretagne Atlantique

Nathalie Bertrand
Are you Nathalie Bertrand?

Claim your profile, edit publications, add additional information:

Contact Details

Nathalie Bertrand
INRIA Rennes - Bretagne Atlantique

Pubs By Year

External Links

Pub Categories

Computer 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

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

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

Affiliations: 1INRIA Rennes - Bretagne Atlantique, 2LSV & ENS Cachan, 3Université de Mons, 4Université de Mons, 5Technische Universität Dresden, 6Technische Universität Dresden, 7University 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

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: 1INRIA Rennes - Bretagne Atlantique, 2INRIA Rennes - Bretagne Atlantique, 3University of Rennes 1, 4Institute of Computer Science and Multimedia, Sfax

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

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: 1INRIA Rennes Bretagne Atlantique, 2Université 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: 1Technische Universität Dresden, 2INRIA Rennes, 3Technische Universität Dresden

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

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