Publications
You can find below the complete list of my publications.
Journals
 N. Bertrand, B. Genest and H. Gimbert.
Qualitative Determinacy and Decidability of Stochastic Games with Signals.
Journal of the ACM, 64(5): pages 33:133:48, 2017.
Abstract  PdfWe consider twoperson zerosum stochastic games with signals, a standard model of stochastic games with imperfect information. The only source of information for the players consists of the signals they receive; they cannot directly observe the state of the game, nor the actions played by their opponent, nor their own actions.We are interested in the existence of almostsurely winning or positively winning strategies, under reachability, safety, Büchi, or coBüchi winning objectives, and the computation of these strategies when the game has finitely many states and actions. We prove two qualitative determinacy results. First, in a reachability game, either player 1 can achieve almost surely the reachability objective, or player 2 can achieve surely the dual safety objective, or both players have positively winning strategies. Second, in a Büchi game, if player 1 cannot achieve almost surely the Büchi objective, then player 2 can ensure positively the dual coBüchi objective. We prove that players only need strategies with finite memory. The number of memory states needed to win with finitememory strategies ranges from one (corresponding to memoryless strategies) to doubly exponential, with matching upper and lower bounds. Together with the qualitative determinacy results, we also provide fixpoint algorithms for deciding which player has an almostsurely winning or a positively winning strategy and for computing an associated finitememory strategy. Complexity ranges from EXPTIME to 2EXPTIME, with matching lower bounds. Our fixpoint algorithms also enjoy a better complexity in the cases where one of the players is better informed than their opponent.
Our results hold even when players do not necessarily observe their own actions. The adequate class of strategies, in this case, is mixed or general strategies (they are equivalent). Behavioral strategies are too restrictive to guarantee determinacy: it may happen that one of the players has a winning general strategy but none of them has a winning behavioral strategy. On the other hand, if a player can observe their actions, then general, mixed, and behavioral strategies are equivalent. Finitememory strategies are sufficient for determinacy to hold, provided that randomized memory updates are allowed.
 A. Bohy,
V. Bruyère,
JF Raskin, and
N. Bertrand.
Symblicit algorithms for meanpayoff and shortest path in monotonic Markov decision processes
Acta Informatica, 54(6), pages 545587, 2017.
Abstract  PdfWhen treating Markov decision processes (MDPs) with large state spaces, using explicit representations quickly becomes unfeasible. Lately, Wimmer et al. have proposed a socalled symblicit algorithm for the synthesis of optimal strategies in MDPs, in the quantitative setting of expected meanpayoff. This algorithm, based on the strategy iteration algorithm of Howard and Veinott, efficiently combines symbolic and explicit data structures, and uses binary decision diagrams as symbolic representation. The aim of this paper is to show that the new data structure of pseudoantichains (an extension of antichains) provides another interesting alternative, especially for the class of monotonic MDPs. We design efficient pseudoantichain based symblicit algorithms (with open source implementations) for two quantitative settings: the expected meanpayoff and the stochastic shortest path. For two practical applications coming from automated planning and 𝖫𝖳𝖫 synthesis, we report promising experimental results w.r.t. both the run time and the memory consumption. We also show that a variant of pseudoantichains allows to handle the infinite state spaces underlying the qualitative verification of probabilistic lossy channel systems. 
N. Bertrand, A. Stainer, T. Jéron and M. Krichen.
A game approach to determinize timed automata.
Formal methods in System Design 46(1), pages 4280, 2015.
Abstract  PdfTimed automata are frequently used to model realtime systems. Their determinization is a key issue for several validation problems. However, not all timed automata can be determinized, and determinizability itself is undecidable. In this paper, we propose a gamebased algorithm which, given a timed automaton, tries to produce a languageequivalent deterministic timed automaton, otherwise a deterministic overapproximation. Our method generalizes two recent contributions: the determinization procedure of [BBBBicalp09] and the approximation algorithm of [KTfmsd09]. Moreover, we extend it to apply to timed automata with invariants and εtransitions, and also consider other useful approximations: underapproximation, and combination of under and overapproximations.  N. Bertrand, P. Bouyer, T. Brihaye, Q. Menet, C. Baier,
M. Groesser and M. Jurdzinski.
Stochastic timed automata.
Logical Methods in Computer Science 10(4), December 2014.
Abstract  PdfA 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 almostsure modelchecking 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 almostsure modelchecking problem. Correctness of the abstraction holds when automata are almostsurely fair, which we show, is the case for two large classes of systems, singleclock automata and socalled weakreactive automata. Techniques employed in this article gather tools from realtime verification and probabilistic verification, as well as topological games played on timed automata.  N. Bertrand and Ph. Schnoebelen.
Computable fixpoints in wellstructured symbolic model checking.
Formal Methods in System Design 43(2), pages 233267, October 2013.
Abstract  PdfWe prove a general finitetime convergence theorem for fixpoint expressions over a wellquasiordered set. This has immediate applications for the verification of wellstructured systems, where a main issue is the computability of fixpoint expressions, and in particular for gametheoretical properties and probabilistic systems where nesting and alternation of least and greatest fixpoints are common.  C. Baier,
N. Bertrand and M. Groesser.
Probabilistic ωautomata.
Journal of the ACM 59(1), 2012.
Abstract  PdfProbabilistic ωautomata are variants of nondeterministic automata over infinite words where all choices are resolved by probabilistic distributions. Acceptance of a run for an infinite input word can be defined using traditional acceptance criteria for ωautomata, such as Büchi, Rabin or Streett conditions. The accepted language of a probabilistic ωautomata is then defined by imposing a constraint on the probability measure of the accepting runs. In this paper, we study a series of fundamental properties of probabilistic ωautomata with three different languagesemantics: (1) the probable semantics that requires positive acceptance probability, (2) the almostsure semantics that requires acceptance with probability 1, and (3) the threshold semantics that relies on an additional parameter λ in ]0,1[ that specifies a lower probability bound for the acceptance probability. We provide a comparison of probabilistic ωautomata under these three semantics and nondeterministic ωautomata concerning expressiveness and efficiency. Furthermore, we address closure properties under the Boolean operators union, intersection and complementation and algorithmic aspects, such as checking emptiness or language containment. 
N. Bertrand, T. Jéron, A. Stainer and M. Krichen.
Offline test selection with test purposes for nondeterministic timed automata.
Logical methods in Computer Science 8(4), 2012.
Abstract  PdfThis article proposes novel offline test generation techniques from nondeterministic 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 ioabstraction 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 coreachability 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.  N. Bertrand, A. Legay, S. Pinchinat
and J.B. Raclet.
Modal eventclock specifications for timed componentbased design.
Science of Computer Programming 77 (12), pages 12121234, Elsevier, 2012.
Abstract  PdfModal specifications are classic, convenient, and expressive mathematical objects to represent interfaces of componentbased systems. However, time is a crucial aspect of systems for practical applications, e.g. in the area of embedded systems. And yet, only few results exist on the design of timed componentbased systems. In this paper, we propose a timed extension of modal specifications, together with fundamental operations (conjunction, product, and quotient) that enable reasoning in a compositional way about timed system. The specifications are given as modal eventclock automata, where clock resets are easy to handle. We develop an entire theory that promotes efficient incremental design techniques.  C. Baier,
N. Bertrand and Ph. Schnoebelen.
Verifying nondeterministic probabilistic channel systems against omegaregular lineartime properties.
ACM Transactions on Computational Logic 9(1), 2007.
Abstract  PdfLossy channel systems (LCS’s) are systems of finite state processes that communicate via unreliable unbounded fifo channels. We introduce NPLCS’s, a variant of LCS’s where message losses have a probabilistic behavior while the component processes behave nondeterministically, and study the decidability of qualitative verification problems for omegaregular lineartime properties. We show that – in contrast to finitestate Markov decision processes – the satisfaction relation for lineartime formulas depends on the type of schedulers that resolve the nondeterminism. While the qualitative model checking problems for the full class of historydependent schedulers is undecidable, the same questions for finitememory schedulers can be solved algorithmically. Additionally, some special kinds of reachability, or recurrent reachability, qualitative properties yield decidable verification problems for the full class of schedulers, which – for this restricted class of problems – are as powerful as finitememory schedulers, or even a subclass of them.  C. Baier,
N. Bertrand and Ph. Schnoebelen.
A note on the attractorproperty of infinitestate Markov chains.
Information Processing Letters 97(2), pages 5863, 2006.
Abstract  PdfIn the past 5 years, a series of verification algorithms has been proposed for infinite Markov chains that have a finite attractor, i.e., a set that will be visited infinitely often almost surely starting from any state. In this paper, we establish a sufficient criterion for the existence of an attractor. We show that if the states of a Markov chain can be given levels (positive integers) such that the expected next level for states at some level n>0 is less than n&Delta for some positive &Delta, then the states at level 0 constitute an attractor for the chain. As an application, we obtain a direct proof that some probabilistic channel systems combining message losses with duplication and insertion errors have a finite attractor.  P. A. Abdulla, N. Bertrand, A. Rabinovich and Ph. Schnoebelen.
Verification of Probabilistic Systems with Faulty Communication.
Information and Computation 202(2), pages 141165, 2005.
Abstract  PdfMany protocols are designed to operate correctly even in the case where the underlying communication medium is faulty. To capture the behavior of such protocols, Lossy Channel Systems (LCS's) have been proposed. In an LCS the communication channels are modeled as unbounded FIFO buffers which are unreliable in the sense that they can nondeterministically lose messages. Recently, several attempts have been made to study Probabilistic Lossy Channel Systems (PLCS's) in which the probability of losing messages is taken into account. In this article, we consider a variant of PLCS's which is more realistic than those studied previously. More precisely, we assume that during each step in the execution of the system, each message may be lost with a certain predefined probability. We show that for such systems the following modelchecking problem is decidable: to verify whether a lineartime property definable by a finitestate omegaautomaton holds with probability one. We also consider other types of faulty behavior, such as corruption and duplication of messages, and insertion of new messages, and show that the decidability results extend to these models.  N. Bertrand, I. Charon,
O. Hudry and A. Lobstein.
1Identifying Codes on Trees.
Australasian Journal of Combinatorics 31, pages 2135, 2005.  N. Bertrand, I. Charon,
O. Hudry and
A. Lobstein.
Identifying and LocatingDominating Codes on Chains and Cycles.
European Journal of Combinatorics 25(7), pages 969987, 2004.
Conferences
 Balasubramanian A.R., N. Bertrand, N. Markey.
Parameterized verification of synchronization in constrained reconfigurable broadcast networks
In Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18), Thessaloniki, Greece, April 2018. To appear.
AbstractReconfigurable 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, synchronization becomes undecidable. We complete the classification by showing that synchronization is decidable whenever the number of reconfigurations grows with the number of agents. We also explore restrictions on the network topologies to regain decidability while bounding the number of reconfigurations.

N. Bertrand, S. Haddad and E. Lefaucheux.
Diagnostic et contrôle de la dégradation des systèmes probabilistes
Actes de la conférence Modélisation des Systèmes Réactifs (MSR'17), Marseille, France, Novembre 2017.
AbstractLe diagnostic actif est opéré par un contrôleur en vue de rendre un système diagnosticable. Afin d'éviter que le contrôleur ne dégrade trop fortement le système, on lui affecte généralement un second objectif en termes de qualité de service. Dans le cadre des systèmes probabilistes, une spécification possible consiste à assurer une probabilité positive qu'une exécution infinie soit correcte, ce qu'on appelle le diagnostic actif sûr. Nous introduisons ici deux spécifications alternatives. La gammacorrection du système affecte à une exécution une valeur de correction dépendant d'un facteur de décote gamma et le contrôleur doit assurer une valeur moyenne supérieure à un seuil fixé. La alphadégradation requiert qu'asymptotiquement, à chaque unité de temps une proportion supérieure à alpha des exécutions jusqu'alors correctes le demeure. D'un point de vue sémantique, nous explicitons des liens significatifs entre les différentes notions. Algorithmiquement, nous établissons la frontière entre décidabilité et indécidabilité des problèmes et dans le cas positif nous exhibons leur complexité précise ainsi qu'une synthèse, potentiellement à mémoire infinie. 
N. Bertrand, M. Dewaskar, B. Genest and H. Gimbert.
Controlling a population
In proceedings of the 28th International Conference on Concurrency Theory (Concur'17), Berlin, Germany, September 2017, LIPIcs 85, pages 12:112:16, Schloss Dagstuhl  LeibnizZentrum fuer Informatik.
Abstract  PdfWe introduce a new setting where a population of agents, each modelled by a finitestate 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 con troller, the controller aims at driving all agents synchronously to a target state. The agents are naturally represented by a nondeterministic finite state automaton (NFA), the same for every agent, and the whole system is encoded as a 2player game. The first player (Controller) chooses actions, and the second player (Agents) resolves nondeterminism 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 2player games), namely the population control problem: can Controller control the mpopulation game for all m ∈ N whatever Agents does?
In this paper, we prove that the population control problem is decidable, and it is a EXPTIMEcomplete 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 mpopulation game if and only if m ≤ M . Surprisingly, M can be doubly exponential in the number of states of the NFA, with tight upper and lower bounds. 
N. Bertrand, S. Haddad and E. Lefaucheux.
Diagnosis in InfiniteState Probabilistic Systems
In proceedings of the 27th International Conference on Concurrency Theory (Concur'16), Québec City, Canada, August 2016. LIPIcs 59, pages 37:137:15, Schloss Dagstuhl  LeibnizZentrum fuer Informatik.
Abstract  PdfIn a recent work, we introduced four variants of diagnosability (FA, IA, FF, IF) in (finite) probabilistic systems (pLTS) depending whether one considers (1) finite or infinite runs and (2) faulty or all runs. We studied their relationship and established that the corresponding decision problems are PSPACEcomplete. A key ingredient of the decision procedures was a characterisation of diagnosability by the fact that a random run almost surely lies in an open set whose specification only depends on the qualitative behaviour of the pLTS. Here we investigate similar issues for infinite pLTS. We first show that this characterisation still holds for FFdiagnosability but with a Gδ set instead of an open set and also for IF and IAdiagnosability when pLTS are finitely branching. We also prove that surprisingly FAdiagnosability cannot be characterised in this way even in the finitely branching case. Then we apply our characterisations for a partially ob servable probabilistic extension of visibly pushdown automata (POpVPA), yielding EXPSPACE procedures for solving diagnosability problems. In addition, we establish some computational lower bounds and show that slight extensions of POpVPA lead to undecidability. 
N. Bertrand, P. Bouyer, T. Brihaye
and P. Carlier.
Analysing decisive stochastic processes
In proceedings of the 43rd International Colloquium on Automata, Languages and Programming (ICALP'16), Roma, Italy, July 2016. LIPIcs 43, pages 101:1101:14, Schloss Dagstuhl  LeibnizZentrum fuer Informatik.
Abstract  PdfIn 2007, Abdulla et al. introduced the elegant concept of decisive Markov chain. Intuitively, decisiveness allows one to lift the good properties of finite Markov chains to infinite Markov chains. For instance, the approximate quantitative reachability problem can be solved for decisive Markov chains (enjoying reasonable effectiveness assumptions) including probabilistic lossy channel systems and probabilistic vector addition systems with states. In this paper, we extend the concept of decisiveness to more general stochastic processes. This extension is non trivial as we consider stochastic processes with a potentially continuous set of states and uncountable branching (common features of realtime stochastic processes). This allows us to obtain decidability results for both qualitative and quantitative verification problems on some classes of realtime stochastic processes, including generalized semiMarkov processes and stochastic timed automata. 
N. Bertrand, S. Haddad and E. Lefaucheux.
Accurate Approximate Diagnosability of Stochastic Systems
In proceedings of the 10th International Conference on Language and Automata Theory and Applications (LATA'16), Prag, Czech Republic, March 2016. LNCS 9618, pages 549561.
Abstract  PdfDiagnosis of partially observable stochastic systems prone to faults was introduced in the late nineties. Diagnosability, i.e. the existence of a diagnoser, may be specified in different ways: (1) exact diagnosability (called Adiagnosability) requires that almost surely a fault is detected and that no fault is erroneously claimed while (2) approximate diagnosability (called εdiagnosability) allows a small probability of error when claiming a fault and (3) accurate approximate diagnosability (called AAdiagnosability) requires that this error threshold may be chosen arbitrarily small. Here we mainly focus on approximate diagnoses. We first refine the almost sure requirement about finite delay introducing a uniform version and showing that while it does not discriminate between the two versions of exact diagnosability this is no more the case in approximate diagnosis. Then we establish a complete picture for the decidability status of the diagnosability problems: (uniform) εdiagnosability and uniform AAdiagnosability are undecidable while AAdiagnosability is decidable in PTIME, answering a longstanding open question. 
N. Bertrand, P. Fournier and
A. Sangnier.
Distributed Local Strategies in Broadcast Networks
In Proceedings of the 26th International Conference on Concurrency Theory (Concur'15), Madrid, Spain, September 2015. LIPIcs 42, pages 4457. Schloss Dagstuhl  LeibnizZentrum fuer Informatik.
Abstract  PdfWe study the problems of reaching a specific control state, or converging to a set of target states, in networks with a parameterized number of identical processes communicating via broadcast. To reflect the distributed aspect of such networks, we restrict our attention to executions in which all the processes must follow the same local strategy that, given their past performed actions and received messages, provides the next action to be performed. We show that the reachability and target problem under such local strategies are NPcomplete, assuming that the set of receivers is chosen nondeterministically at each step. On the other hand, these problems become undecidable when the communication topology is a clique. However, decidability can be regained with the additional assumption that all processes are bound to receive the broadcast messages. 
N. Bertrand, S. Haddad and E. Lefaucheux.
Foundation of Diagnosis and Predictability in Probabilistic Systems
In proceedings of the 34th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'14), New Delhi, India, December 2014. LIPIcs 29, pages 417429. Schloss Dagstuhl  LeibnizZentrum fuer Informatik.
Abstract  PdfIn discrete event systems prone to unobservable faults, a diagnoser must eventually detect fault occurrences. The diagnosability problem consists in deciding whether such a diagnoser exists. Here we investigate diagnosisfor probabilistic systems modelled by partially observed Markov chains also called probabilistic labeled transition systems (pLTS). First we study different specifications of diagnosability and establish their relations both in finite and infinite pLTS. Then we analyze the complexity of the diagnosability problem for finite pLTS: we show that the polynomial time procedure earlier proposed is erroneous and that in fact for all considered specifications, the problem is PSPACEcomplete. We also establish tight bounds for the size of diagnosers. Afterwards we consider the dual notion of predictability which consists in predicting that in a safe run, a fault will eventually occur. Predictability is an easier problem than diagnosability: it is NLOGSPACEcomplete. Yet the predictor synthesis is as hard as the diagnoser synthesis. Finally we introduce and study the more flexible notion of prediagnosability that generalizes predictability and diagnosability. 
N. Bertrand, Th. Brihaye and B. Genest.
Deciding the value 1 problem for reachability in 1clock decision stochastic timed automata.
In proceedings of the 11th International Conference on Quantitative Evaluation of Systems (QEST'14), Firenze, Italy, September 2014. LNCS 8657, pages 313328. Springer.
Abstract  PdfWe consider reachability objectives on an extension of stochastic timed automata (STA) with nondeterminism. Decision stochastic timed automata (DSTA) are Markov decision processes based on timed automata where delays are chosen randomly and choices between enabled edges are nondeterministic. Given a reachability objective, the value 1 problem asks whether a target can be reached with probability arbitrary close to 1. Simple examples show that the value can be 1 and yet no strategy ensures reaching the target with probability 1. In this paper, we prove that, the value 1 problem is decidable for single clock DSTA by nontrivial reduction to a simple almostsure reachability problem on a finite Markov decision process. The εoptimal strategies are involved: the precise probability distributions, even if they do not change the winning nature of a state, impact the timings at which εoptimal strategies must change their decisions, and more surprisingly these timings cannot be chosen uniformly over the set of regions. 
N. Bertrand, P. Fournier and
A. Sangnier.
Playing with probabilities in reconfigurable broadcast networks
In Proceedings of the 17th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'14), Grenoble, France, April 2014. LNCS 8412, pages 134148. Springer.
Abstract  PdfWe study verification problems for a model of network with the following characteristics: the number of entities is parametric, communication is performed through broadcast with adjacent neighbors, entities can change their internal state probabilistically and reconfiguration of the communication topology can happen at any time. The semantics of such a model is given in term of an infinite state system with both non deterministic and probabilistic choices. We are interested in qualitative problems like whether there exists an initial topology and a resolution of the non determinism such that a configuration exhibiting an error state is almost surely reached. We show that all the qualitative reachability problems are decidable and some proofs are based on solving a 2 player game played on the graphs of a reconfigurable network with broadcast with parity and safety objectives. 
N. Bertrand, E. Fabre, S. Haar, S. Haddad and L. Hélouët.
Active diagnosis for probabilistic systems
In Proceedings of the 17th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'14), Grenoble, France, April 2014. LNCS 8412, pages 2942. Springer.
Abstract  PdfThe diagnosis problem amounts to deciding whether some specific "fault" event occurred or not in a system, given the observations collected on a run of this system. This system is then diagnosable if the fault can always be detected, and the active diagnosis problem consists in controlling the system in order to ensure its diagnosability. We consider here a stochastic framework for this problem: once a control is selected, the system becomes a stochastic process. In this setting, the active diagnosis problem consists in deciding whether there exists some observationbased strategy that makes the system diagnosable with probability one. We prove that this problem is EXPTIMEcomplete, and that the active diagnosis strategies are beliefbased. The safe active diagnosis problem is similar, but aims at enforcing diagnosability while preserving a positive probability to non faulty runs, i.e. without enforcing the occurrence of a fault. We prove that this problem requires non beliefbased strategies, and that it is undecidable. However, it belongs to NEXPTIME when restricted to beliefbased strategies. Our work also refines the decidability/undecidability frontier for verification problems on partially observed Markov decision processes.  N. Bertrand and P. Fournier.
Parameterized verification of many identical probabilistic timed processes
In proceedings of the 33rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'13), Guwahati, India, December 2013. LIPIcs 24, pages 501513. Schloss Dagstuhl  LeibnizZentrum fuer Informatik.
Abstract  PdfParameterized verification aims at validating a system's model irrespective of the value of a parameter. We introduce a model for networks of identical probabilistic timed processes, where the number of processes is a parameter. Each process is a probabilistic singleclock timed automaton and communicates with the others by broadcasting. The number of processes either is constant (static case), or evolves over time through random disappearances and creations (dynamic case). An example of relevant parameterized verification problem for these systems is whether, independently of the number of processes, a configuration where one process is in an error state is reached almostsurely under all scheduling policies. On the one hand, most parameterized verification problems turn out to be undecidable in the static case (even for untimed processes). On the other hand, we prove their decidability in the dynamic case.  S. Akshay,
N. Bertrand, S. Haddad and L. Hélouët.
The steadystate control problem for Markov decision processes
In proceedings of the 10th International Conference on Quantitative Evaluation of Systems (QEST'13), Buenos Aires, Argentina, August 2013. LNCS 8054, pages 390304. Springer.
Abstract  PdfThis paper addresses a control problem for probabilistic models in the setting of Markov decision processes (MDP). We are interested in the steadystate control problem which asks, given an ergodic MDP M and a distribution \delta, whether there exists a (historydependent randomized) policy \pi ensuring that the steadystate distribution of M under \pi is exactly \delta. We first show that stationary randomized policies suffice to achieve a given steadystate distribution. Then we infer that the steadystate control problem is decidable for MDP, and can be represented as a linear program which is solvable in PTIME. This decidability result extends to labeled MDP (LMDP) where the objective is a steadystate distribution on labels carried by the states, and we provide a PSPACE algorithm. We also show that a related steadystate language inclusion problem is decidable in EXPTIME for LMDP. Finally, we prove that if we consider MDP under partial observation (POMDP), the steadystate control problem becomes undecidable.  P. Ballarini,
N. Bertrand, A. Horváth, M. Paolieri, and E. Vicario.
Transient Analysis of Networks of Stochastic Timed Automata using Stochastic State Classes
In proceedings of the 10th International Conference on Quantitative Evaluation of Systems (QEST'13), Buenos Aires, Argentina, August 2013. LNCS 8054, pages 355371. Springer.
Abstract  PdfStochastic Timed Automata (STA) associate logical locations with continuous generally distributed sojourn times. In this paper, we introduce Networks of Stochastic Timed Automata (NSTA), where the components interact with each other by message broadcasts. This results in an underlying stochastic process whose state is made of the vector of logical locations, of their remaining sojourn times, and of the value of clocks. We characterize this general state space Markov chain through transient stochastic state classes that sample the state and the absolute age after each event. This provides an algorithmic approach to transient analysis of NSTA models, with fairly general termination conditions which we characterize with respect to structural properties of individual components.  N. Bertrand and Ph. Schnoebelen.
Solving Stochastic Büchi Games on Infinite Arenas with a Finite Attractor.
In proceedings of the 11th International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL'13), Roma, Italia, March 2013.
Abstract  PdfWe 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 finiteattractor property. From this we directly deduce the decidability of these games on probabilistic lossy channel systems.  N. Bertrand and S. Schewe.
Playing Optimally on Timed Automata with Random Delays.
In proceedings of the 10th International Conference on Formal Modeling and Analysis of Timed Systems (Formats'12), London, UK, September 2012. LNCS 7595, pages 4358. Springer.
Abstract  Pdf
We marry continuous time Markov decision processes (CTMDPs) with stochastic timed automata into a model with joint expressive power. This extension is very natural, as the two original models already share exponentially distributed sojourn times in locations. It enriches CTMDPs with timing constraints, or symmetrically, stochastic timed automata with one conscious player. Our model maintains the existence of optimal control known for CTMDPs. This also holds for a richer model with two players, which extends continuous time Markov games. But we have to sacrifice the existence of simple schedulers: polyhedral regions are insufficient to obtain optimal control even in the singleplayer case.
 N. Bertrand, J. Fearnley and S. Schewe.
Bounded Satisfiability for PCTL.
In proceedings of the 21st EACSL Annual Conferences on Computer Science Logic (CSL'12), Fontainebleau, France, September 2012. LIPIcs 16, pages 92106. Schloss Dagstuhl  LeibnizZentrum fuer Informatik.
Abstract  Pdf
While model checking PCTL for Markov chains is decidable in polynomialtime, 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.
 N. Bertrand, G. Delzanno, B. König, A. Sangnier and J. Stückrath.
On the Decidability Status of Reachability and Coverability in Graph Transformation Systems.
In proceedings of 23rd International Conference on Rewriting Techniques and Applications (RTA'12), Nagoya, Japan, MayJune 2012. LIPIcs 15, pages 101116. Schloss Dagstuhl  LeibnizZentrum fuer Informatik.
Abstract  Pdf
We study decidability issues for reachability problems in graph transformation systems, a powerful infinitestate model. For a fixed initial configuration, we consider reachability of an entirely specified configuration and of a configuration that satisfies a given pattern (coverability). The former is a fundamental problem for any computational model, the latter is strictly related to verification of safety properties in which the pattern specifies an infinite set of bad configurations. In this paper we reformulate results obtained, e.g., for contextfree graph grammars and concurrency models, such as Petri nets, in the more general setting of graph transformation systems and study new results for classes of models obtained by adding constraints on the form of reduction rules.
 N. Bertrand and B. Genest.
Minimal Disclosure in Partially Observable Markov Decision Processes.
In proceedings of the 31st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'11), Mumbai, India, December 2011. LIPIcs 13, pages 411422. Schloss Dagstuhl  LeibnizZentrum fuer Informatik.
Abstract  Pdf
For security and efficiency reasons, most systems do not give the users a full access to their information. One key specification formalism for these systems are the so called Partially Observable Markov Decision Processes (POMDP for short), which have been extensively studied in several research communities, among which AI and modelchecking. In this paper we tackle the problem of the minimal information a user needs at runtime to achieve a simple goal, modeled as reaching an objective with probability one. More precisely, to achieve her goal, the user can at each step either choose to use the partial information, or pay a fixed cost and receive the full information. The natural question is then to minimize the cost the user needs to fulfill her objective. This optimization question gives rise to two different problems, whether we consider to minimize the worst case cost, or the average cost. On the one hand, concerning the worst case cost, we show that efficient techniques from the model checking community can be adapted to compute the optimal worst case cost and give optimal strategies for the users. On the other hand, we show that the optimal average price (a question typically considered in the AI community) cannot be computed in general, nor can it be approximated in polynomial time even up to a large approximation factor.  N. Bertrand, P. Bouyer, Th. Brihaye and A. Stainer.
Emptiness and Universality Problems in Timed Automata with Positive Frequency.
In Proceedings of the 38th International Colloquium on Automata, Languages and Programming (ICALP'11), Zürich, Switzerland, July 2011. LNCS 6756, pages 246257. Springer.
Abstract  PdfThe languages of infinite timed words accepted by timed automata are traditionally defined using Büchilike 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 socalled frequency, which measures the proportion of time spent in the accepting states. We study various properties of timed languages accepted with positive frequency, and in particular the emptiness and universality problems.  N. Bertrand, A. Stainer, T. Jéron and M. Krichen.
A Game Approach to Determinize Timed Automata.
In Proceedings of the 14th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'11), Saarbrücken, Germany, April 2011. LNCS 6604, pages 245259. Springer.
Abstract  Pdf  Long versionTimed automata are frequently used to model realtime systems. Their determinization is a key issue for several validation problems. However, not all timed automata can be determinized, and determinizability itself is undecidable. In this paper, we propose a gamebased algorithm which, given a timed automaton with εtransitions and invariants, tries to produce a languageequivalent deterministic timed automaton, otherwise a deterministic overapproximation. Our method subsumes two recent contributions: it is at once more general than the determinization procedure of [BBBB09] and more precise than the approximation algorithm of [KT09]  N. Bertrand, T. Jéron, A. Stainer and M. Krichen.
Offline Test Selection with Test Purposes for NonDeterministic Timed Automata.
In Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'11), Saarbrücken, Germany, April 2011. LNCS 6605, pages 96111. Springer.
Abstract  Pdf  Long versionThis paper proposes novel offline test generation techniques for nondeterministic 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, but is in general impossible. This problem is solved here thanks to an approximate determinization using a game approach, which preserves tioco and guarantees the soundness of generated test cases. A second problem is test selection for which a precise description of timed behaviors to be tested is carried out by expressive test purposes modeled by a generalization of TAIOs. Finally, using a symbolic coreachability analysis guided by the test purpose, test cases are generated in the form of TAIOs equipped with verdicts.  N. Bertrand and C. Morvan.
Probabilistic Regular Graphs.
In Proceedings of the 12th International Workshop on Verification of InfiniteState Systems (INFINITY'10), Singapore, September 2010. EPTCS 39, page 7790.
Abstract  PdfDeterministic 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 modelchecking problem for PCTL on probabilistic regular graphs is undecidable, unless restricting to qualitative properties.Our results generalise those of Esparza et al., on probabilistic pushdown automata, using similar methods combined with graph grammars techniques.
 N. Bertrand, A. Legay, S. Pinchinat
and J.B. Raclet.
A Compositional Approach on Modal Specifications for Timed Systems.
In Proceedings of the 11th International Conference on Formal Engineering Methods (ICFEM'09), Rio de Janeiro, Brazil, December 2009. LNCS 5585, pages 679697. Springer.
Abstract  Pdf  Long versionOn the one hand, modal specifications are classic, convenient, and expressive mathematical objects to represent interfaces of componentbased systems. On the other hand, time is a crucial aspect of systems for practical applications, e.g. in the area of embedded systems. And yet, only few results exist on the design of timed componentbased systems. In this paper, we propose a timed extension of modal specifications, together with fundamental operations (conjunction, product, and quotient) that enable to reason in a compositional way about timed system. The specifications are given as modal eventclock automata, where clock resets are easy to handle. We develop an entire theory that promotes efficient incremental design techniques.  C. Baier,
N. Bertrand, P. Bouyer, and Th. Brihaye.
When are timed automata determinizable?
In Proceedings of the 36th International Colloquium on Automata, Languages and Programming (ICALP'09), Rhodes, Greece, July 2009, LNCS 5556, pages 4354. Springer.
Abstract  PdfIn this paper, we propose an abstract procedure which, given a timed automaton, produces a languageequivalent deterministic infinite timed tree. We prove that under a certain boundedness condition, the infinite timed tree can be reduced into a classical deterministic timed automaton. The boundedness condition is satisfied by several subclasses of timed automata, some of them were known to be determinizable (eventclock timed automata, automata with integer resets), but some others were not. We prove for instance that strongly nonZeno timed automata can be determinized. As a corollary of those constructions, we get for those classes the decidability of the universality and of the inclusion problems, and compute their complexities (the inclusion problem is for instance EXPSPACEcomplete for strongly nonZeno timed automata).  N. Bertrand, B. Genest and H. Gimbert.
Qualitative Determinacy and Decidability of Stochastic Games with Signals.
In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science (LICS'09), Los Angeles, CA, USA, August 2009, pages 319328. IEEE Computer Society Press.
Abstract  PdfWe consider twoplayers stochastic zerosum games with partial observation on both sides and finitely many states, signals and actions. We are interested in the existence of almostsurely winning or positively winning strategies, under reachability or Büchi winning conditions. It turns out that for reachability games, if neither player 1 nor player 2 can win almostsurely, then both players have positively winning strategies. For Büchi games, if player 1 cannot win almostsurely, then player 2 has a positively winning strategy. Together with these qualitative determinacy results, we provide fixpoint algorithms to decide which player has an almost surely winning or positive winning strategy. Complexity ranges from EXPTIME to 2EXPTIME (depending on the relation between observation of the players), with matching lower bounds. We prove that players only need finitememory strategies, computed by the fixpoint algorithm, ranging from no memory to doublyexponential, which we prove necessary to achieve a safety condition with positive probability.  N. Bertrand, S. Pinchinat
and J.B. Raclet.
Refinement and Consistency of Timed Modal Specifications.
In Proceedings of the 3rd International Conference on Language and Automata Theory and Applications (LATA'09), Tarragona, Spain, April 2009, LNCS 5457, pages 152163. Springer.
Abstract  PdfIn the application domain of componentbased system design, developing theories which support compositional reasoning is notoriously challenging. We define timed modal specifications, an automatabased formalism combining modal and timed aspects. As a stepping stone to compositional approaches of timed systems, we define the notions of refinement and consistency, and establish their decidability.  N. Bertrand, P. Bouyer, Th. Brihaye and N. Markey.
Quantitative ModelChecking of OneClock Timed Automata under Probabilistic Semantics.
In Proceedings of the 5th International Conference on the Quantitative Evaluation of Systems (QEST'08), Saint Malo, France, September 2008, pages 5564. IEEE Computer Society Press.
Abstract  PdfIn [BBBBGlics08] a probabilistic semantics for timed automata has been defined in order to rule out unlikely (sequences of) events. The qualitative modelchecking problem for LTL properties has been investigated, where the aim is to check whether a given LTL property holds with probability 1 in a timed automaton, and solved for the class of singleclock timed automata. In this paper, we consider the quantitative modelchecking problem for omegaregular properties: we aim at computing the exact probability that a given timed automaton satisfies an omegaregular property. We develop a framework in which we can compute a closedform expression for this probability; we furthermore give an approximation algorithm, and finally prove that we can decide the threshold problem in that framework.  C. Baier,
N. Bertrand, P. Bouyer, Th. Brihaye and M. Groesser.
AlmostSure Model Checking of Infinite Paths in OneClock Timed Automata.
In Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science (LICS'08), Pittsburgh, PA, USA, June 2008, pages 217226. IEEE Computer Society Press.
Abstract  Pdf  Long versionIn this paper, we define two relaxed semantics (one based on probabilities and the other one based on the topological notion of largeness) for LTL over infinite runs of timed automata which rule out unlikely sequences of events. We prove that these two semantics match in the framework of singleclock timed automata (and only in that framework), and prove that the corresponding relaxed modelchecking problems are PSPACEComplete. Moreover, we prove that the probabilistic nonZenoness can be decided for singleclock timed automata in NLOGSPACE.  C. Baier,
N. Bertrand and M. Groesser.
On Decision Problems for Probabilistic Büchi Automata.
In Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'08), Budapest, Hungary, MarchApril 2008, LNCS 4962, pages 287301. Springer.
EATCS best theory paper at ETAPS.
Abstract  PdfProbabilistic Büchi automata (PBA) are finitestate acceptors for infinite words where all choices are resolved by fixed distributions and where the accepted language is defined by the requirement that the measure of the accepting runs is positive. The main contribution of this paper is a complementation operator for PBA and a discussion on several algorithmic problems for PBA. All interesting problems, such as checking emptiness or equivalence for PBA or checking whether a finite transition system satisfies a PBAspecification, turn out to be undecidable. An important consequence of these results are several undecidability results for stochastic games with incomplete information, modelled by partiallyobservable Markov decision processes and omegaregular winning objectives. Furthermore, we discuss an alternative semantics for PBA where it is required that almost all runs for an accepted word are accepting, which turns out to be less powerful, but has a decidable emptiness problem.  C. Baier,
N. Bertrand, P. Bouyer, Th. Brihaye and M. Groesser.
Probabilistic and Topological Semantics for Timed Automata.
In Proceedings of the 27th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07), New Delhi, India, December 2007, LNCS 4855, pages 179191. Springer.
Abstract  PdfLike most models used in modelchecking, timed automata are an idealized mathematical model used for representing systems with strong timing requirements. In such mathematical models, properties can be violated, due to unlikely (sequences of) events. We propose two new semantics for the satisfaction of LTL formulas, one based on probabilities, and the other one based on topology, to rule out these sequences. We prove that the two semantics are equivalent and lead to a PSPACEComplete modelchecking problem for LTL over finite executions.  C. Baier,
N. Bertrand and Ph. Schnoebelen.
On Computing Fixpoints in WellStructured Regular Model Checking, with Applications to Lossy Channel Systems.
In Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'06), Phnom Penh, Cambodia, November 2006, LNAI 4246, pages 347361. Springer.
Abstract  PdfWe prove a general finite convergence theorem for “upwardguarded” fixpoint expressions over a wellquasiordered set. This has immediate applications in regular model checking of wellstructured 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.  C. Baier,
N. Bertrand and Ph. Schnoebelen.
Symbolic verification of communicating systems with probabilistic message losses: liveness and fairness.
In Proceedings of 26th IFIP WG6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'06), Paris, France, September 2006, LNCS 4229, pages 212227. Springer.
Abstract  PdfNPLCS’s are a new model for nondeterministic channel systems where unreliable communication is modeled by probabilistic message losses. We show that, for omegaregular lineartime properties and finitememory schedulers, qualitative modelchecking is decidable. The techniques extend smoothly to questions where fairness restrictions are imposed on the schedulers. The symbolic procedure underlying our decidability proofs has been implemented and used to study a simple protocol handling twoway transfers in an unreliable setting.  N. Bertrand and Ph. Schnoebelen.
A short visit to the STS hierarchy.
In Proceedings of the 12th International Workshop on Expressiveness in Concurrency (EXPRESS'05), San Francisco, CA, USA, August 2005, ENTCS 154(3), pages 5969. Elsevier Science Publishers, 2006.
Abstract  PdfThe hierarchy of Symbolic Transition Systems, introduced by Henzinger, Majumdar and Raskin, is an elegant classification tool for some families of infinitestate operational models that support some variants of a symbolic "backward closure" verification algorithm. It was first used and illustrated with families of hybrid systems. In this paper we investigate whether the STS hierarchy can account for classical families of infinitestate systems outside of timed or hybrid systems.  N. Bertrand and Ph. Schnoebelen.
Model Checking Lossy Channels Systems Is Probably Decidable.
In Proceedings of the 6th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'03), Warsaw, Poland, April 2003, LNCS 2620, pages 120135. Springer.
Abstract  PdfLossy channel systems (LCS's) are systems of finite state automata that communicate via unreliable unbounded fifo channels. We propose a new probabilistic model for these systems, where losses of messages are seen as faults occurring with some given probability, and where the internal behavior of the system remains nondeterministic, giving rise to a reactive Markov chains semantics. We then investigate the verification of lineartime properties on this new model.
Theses
 N. Bertrand.
Contributions to the verification and control of timed and probabilistic models
HDR, IRISA, Université Rennes 1 , France, November 2015.
Pdf  N. Bertrand.
Modèles stochastiques pour les pertes de messages dans les protocoles asynchrones et techniques de vérification automatique.
Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, October 2006.
Abstract  PdfAsynchronous communication protocols are naturally seen as communicating finite automata over unbounded FIFO channels. In this thesis, we consider variants of LCS (Lossy Channel Systems) for which message losses are probabilistic. More precisely, we introduce the models of Probabilistic LCS (PLCS), and Nondeterministic and Probabilistic LCS (NPLCS) whose semantics are respectively Markov chains and Markov decision processes. A general criterion on convergence of fixed points expressions in Well Structured Transition Systems allows to prove a number a decidability results with respect to verification of lineartime properties for both models. We also prove undecidability results to show the limits of these models. A prototype tool in OCaml implements the algorithms of this thesis. Despite the high complexity of the problems, this tool allows to prove liveness properties of commmunication protocols such as the Alternating Bit Protocol and Pachl's protocol.
Other publications
 N. Bertrand, B. Genest and H. Gimbert.
Qualitative Determinacy and Decidability of Stochastic Games with Signals.
Preliminary version of the LICS'09 paper. HAL preprint.  N. Bertrand and Ph. Schnoebelen.
Verifying Nondeterministic Channel Systems With Probabilistic Message Losses.
In Proceedings of the 3rd International Workshop on Automated Verification of InfiniteState Systems (AVIS'04), Barcelona, Spain, April 2004.
Abstract  PdfLossy channel systems (LCS's) are systems of finite state automata that communicate via unreliable unbounded fifo channels. In order to circumvent the undecidability of model checking for nondeterministic LCS's, probabilistic models have been introduced, where it can be decided whether a lineartime property holds almost surely. However, such fully probabilistic systems are not a faithful model of nondeterministic protocols. We study a hybrid model for LCS's 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 infinitestate reactive Markov chains (equivalently, Markovian decision processes). A similar model was introduced in the second part of our FOSSACS'03 article: we continue this work and give a complete picture of the decidability of qualitative model checking for MSOdefinable properties and some relevant subcases.  N. Bertrand, I. Charon, O. Hudry and A. Lobstein.
Identifying or LocatingDominating Codes for some Families of Graphs.
Research report, ENST Télécom Paris, France, February 2003. 48 pages.  N. Bertrand.
Vérification de canaux à pertes stochastiques.
Rapport de DEA, DEA Algorithmique, Paris, France, September 2002.
Ps.gz