• Home
• Publications
• Talks
• Teaching
• Misc

Journals

• N. Bertrand.
  Model checking randomized distributed algorithms.
  SIGLOG News 7(1): 35-45, 2020. Abstract | Pdf | doi
  Randomization is a powerful paradigm to solve hard problems, especially in distributed computing. Proving the correctness, and assessing the performances, of randomized distributed algorithms, is a very challenging research objective, that the verification community has started to address. In this article, we review existing model checking approaches to the verification of randomized distributed algorithms and identify further research directions.


• N. Bertrand, M. Dewaskar, B. Genest, H. Gimbert, A. A. Godbole.
  Controlling a population.
  Logical Methods in Computer Science 15(3), 2019.
  Abstract | Pdf | doi
  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?


• N. Bertrand, S. Haddad and E. Lefaucheux.
  Tale of Two Diagnoses in Probabilistic Systems.
  Information and Computation 269, 2019.
  Abstract | Pdf | doi
  Diagnosis of partially observable stochastic systems prone to faults was introduced in the late nineties. Diagnosability, \emph{i.e.} the existence of a diagnoser, may be specified in different ways: exact diagnosability requires that almost surely a fault is detected and that no fault is erroneously claimed; approximate diagnosability tolerates a small error probability when claiming a fault; last, accurate approximate diagnosability guarantees that the error probability can be chosen arbitrarily small. In this article, we first refine the specification of diagnosability by identifying three criteria: (1) detecting faulty runs or providing information for all runs (2) considering finite or infinite runs, and (3) requiring or not a uniform detection delay. We then give a complete picture of relations between the different diagnosability specifications for probabilistic systems and establish characterisations for most of them in the finite-state case. Based on these characterisations, we develop decision procedures, study their complexity and prove their optimality. We also design synthesis algorithms to construct diagnosers and we analyse their memory requirements. Finally we establish undecidability of the diagnosability problems for which we provided no characterisation.


• N. Bertrand, P. Bouyer, T. Brihaye, and Pierre Carlier.
  When are stochastic transition systems tameable?
  Journal of Logic and Algebraic Methods in Programming, 99: pages 41-96, 2018.
  Abstract | Pdf
  A decade ago, Abdulla, Ben Henda and Mayr introduced the elegant concept of decisiveness for denumerable Markov chains [ABM07]. 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. Our first contribution is to define various notions of decisiveness (inherited from [ABM07]), notions of fairness and of attractors for STSs, and explicit the relationships between them. As a second contribution, 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. Our third contribution focuses on qualitative model-checking. Beyond (repeated) reachability properties for which our technics are strongly inspired by [ABM07], we use abstractions to design algorithms for the qualitative model-checking problem of arbitrary ω-regular properties, when the STS admits a denumerable (sound and complete) abstraction with a finite attractor. Our fourth contribution is the design of generic approximation procedures for quantitative model-checking; in addition to extensions of [ABM07] for general STSs, we design approximation algorithms for ω-regular properties (once again by means of specific abstractions). Last, our fifth contribution consists in instantiating our framework with stochastic timed automata (STA) and generalized semi-Markov processes (GSMP), two models combining dense-time and probabilities. This allows us to derive decidability and approximability results for the verification of these two 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 and GSMPs.


• N. Bertrand, B. Genest and H. Gimbert.
  Qualitative Determinacy and Decidability of Stochastic Games with Signals.
  Journal of the ACM, 64(5): pages 33:1-33:48, 2017.
  Abstract | Pdf
  We consider two-person zero-sum 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 almost-surely winning or positively winning strategies, under reachability, safety, Büchi, or co-Bü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 co-Büchi objective. We prove that players only need strategies with finite memory. The number of memory states needed to win with finite-memory 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 fix-point algorithms for deciding which player has an almost-surely winning or a positively winning strategy and for computing an associated finite-memory strategy. Complexity ranges from EXPTIME to 2EXPTIME, with matching lower bounds. Our fix-point 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. Finite-memory strategies are sufficient for determinacy to hold, provided that randomized memory updates are allowed.



• A. Bohy, V. Bruyère, J-F Raskin, and N. Bertrand.
  Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes
  Acta Informatica, 54(6), pages 545-587, 2017.
  Abstract | Pdf
  When treating Markov decision processes (MDPs) with large state spaces, using explicit representations quickly becomes unfeasible. Lately, Wimmer et al. have proposed a so-called symblicit algorithm for the synthesis of optimal strategies in MDPs, in the quantitative setting of expected mean-payoff. 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 pseudo-antichains (an extension of antichains) provides another interesting alternative, especially for the class of monotonic MDPs. We design efficient pseudo-antichain based symblicit algorithms (with open source implementations) for two quantitative settings: the expected mean-payoff 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 pseudo-antichains 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 42-80, 2015.
  Abstract | Pdf
  Timed automata are frequently used to model real-time 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 game-based algorithm which, given a timed automaton, tries to produce a language-equivalent deterministic timed automaton, otherwise a deterministic over-approximation. Our method generalizes two recent contributions: the determinization procedure of [BBBB-icalp09] and the approximation algorithm of [KT-fmsd09]. Moreover, we extend it to apply to timed automata with invariants and ε-transitions, and also consider other useful approximations: under-approximation, and combination of under- and over-approximations.


• 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 | Pdf
  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.


• N. Bertrand and Ph. Schnoebelen.
  Computable fixpoints in well-structured symbolic model checking.
  Formal Methods in System Design 43(2), pages 233-267, October 2013.
  Abstract | Pdf
  We prove a general finite-time convergence theorem for fixpoint expressions over a well-quasi-ordered set. This has immediate applications for the verification of well-structured systems, where a main issue is the computability of fixpoint expressions, and in particular for game-theoretical 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 | Pdf
  Probabilistic ω-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 language-semantics: (1) the probable semantics that requires positive acceptance probability, (2) the almost-sure 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.
  Off-line test selection with test purposes for non-deterministic timed automata.
  Logical methods in Computer Science 8(4), 2012.
  Abstract | Pdf
  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.


• N. Bertrand, A. Legay, S. Pinchinat and J.-B. Raclet.
  Modal event-clock specifications for timed component-based design.
  Science of Computer Programming 77 (12), pages 1212-1234, Elsevier, 2012.
  Abstract | Pdf
  Modal specifications are classic, convenient, and expressive mathematical objects to represent interfaces of component-based 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 component-based 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 event-clock 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 omega-regular linear-time properties.
  ACM Transactions on Computational Logic 9(1), 2007.
  Abstract | Pdf
  Lossy 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 omega-regular linear-time properties. We show that – in contrast to finite-state 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 history-dependent 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 finite-memory schedulers, or even a subclass of them.


• C. Baier, N. Bertrand and Ph. Schnoebelen.
  A note on the attractor-property of infinite-state Markov chains.
  Information Processing Letters 97(2), pages 58-63, 2006.
  Abstract | Pdf
  In 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 141-165, 2005.
  Abstract | Pdf
  Many 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 model-checking problem is decidable: to verify whether a linear-time property definable by a finite-state omega-automaton 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.
  1-Identifying Codes on Trees.
  Australasian Journal of Combinatorics 31, pages 21-35, 2005.


• N. Bertrand, I. Charon, O. Hudry and A. Lobstein.
  Identifying and Locating-Dominating Codes on Chains and Cycles.
  European Journal of Combinatorics 25(7), pages 969-987, 2004.

Conferences

• N. Bertrand, P. Bouyer and A. Majumdar.
  Concurrent Parameterized Games
  In proceedings of the 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'19), Bombay, India, December 2019. LIPIcs 150, pages 31:1-31:15, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
  Abstract | Pdf
  Traditional concurrent games on graphs involve a fixed number of players, who take decisions simultaneously, determining the next state of the game. In this paper, we introduce a parameterized variant of concurrent games on graphs, where the parameter is precisely the number of players. Parameterized concurrent games are described by finite graphs, in which the transitions bear regular languages to describe the possible move combinations that lead from one vertex to another.

  We consider the problem of determining whether the first player, say Eve, has a strategy to ensure a reachability objective against any strategy profile of her opponents as a coalition. In particular Eve's strategy should be independent of the number of opponents she actually has. Technically, this paper focuses on an a priori simpler setting where the languages labeling transitions only constrain the number of opponents (but not their precise action choices). These constraints are described as semilinear sets, finite unions of intervals, or intervals.

  We establish the precise complexities of the parameterized reachability game problem, ranging from PTIME-complete to PSPACE-complete, in a variety of situations depending on the contraints (semilinear predicates, unions of intervals, or intervals) and on the presence or not of non-determinism.



• N. Bertrand, Igor Konnov, Marijana Lazic and Josef Widder.
  Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries
  In proceedings of the 30th International Conference on Concurrency Theory (CONCUR'19) Amsterdam, the Netherlands, August 2019. LIPIcs 140, pages 32:1-32:15, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
  Abstract | Pdf
  Randomized fault-tolerant distributed algorithms pose a number of challenges for automated verification: (i) parameterization in the number of processes and faults, (ii) randomized choices and probabilistic properties, and (iii) an unbounded number of asynchronous rounds. This combination makes verification hard. Challenge (i) was recently addressed in the framework of threshold automata.

  We extend threshold automata to model randomized algorithms that perform an unbounded number of asynchronous rounds. For non-probabilistic properties, we show that it is necessary and sufficient to verify these properties under round-rigid schedules, that is, schedules where processes enter round r only after all processes finished round r-1. For almost-sure termination, we analyze these algorithms under round-rigid adversaries, that is, fair adversaries that only generate round-rigid schedules. This allows us to do compositional and inductive reasoning that reduces verification of the asynchronous multi-round algorithms to model checking of a one-round threshold automaton. We apply this framework and automatically verify the following classic algorithms: Ben-Or's and Bracha's seminal consensus algorithms for crashes and Byzantine faults, 2-set agreement for crash faults, and RS-Bosco for the Byzantine case.



• N. Bertrand, P. Bouyer and A. Majumdar.
  Reconfiguration and Message Losses in Parameterized Broadcast Networks
  In proceedings of the 30th International Conference on Concurrency Theory (CONCUR'19) Amsterdam, the Netherlands, August 2019. LIPIcs 140, pages 32:1-32:15, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
  Abstract | Pdf
  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.



• C. Baier, N. Bertrand, J. Piribauer and O. Sankur.
  Long-run Satisfaction of Path Properties
  In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'19), Vancouver, CA, July 2019, ACM, pages 1-14.
  Abstract | Pdf
  The paper introduces the concepts of long-run frequency of path properties for paths in Kripke structures, and their generalization to long-run probabilities for schedulers in Markov decision processes. We then study the natural optimization problem of computing the optimal values of these measures, when ranging over all paths or all schedulers, and the corresponding decision problem when given a threshold. The main results are as follows. For (repeated) reachability and other simple properties, optimal long-run probabilities and corresponding optimal memoryless schedulers are computable in polynomial time. When it comes to constrained reachability properties, memoryless schedulers are no longer sufficient, even in the non-probabilistic setting. Nevertheless, optimal long-run probabilities for constrained reachability are computable in pseudo-polynomial time in the probabilistic setting and in polynomial time for Kripke structures. Finally for co-safety properties expressed by NFA, we give an exponential-time algorithm to compute the optimal long-run frequency, and prove the PSPACE-completeness of the threshold problem.


• C. Baier, N. Bertrand, C. Dubslaff, D. Gburek and O. Sankur.
  Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes
  In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'18), Oxford, UK, July 2018, ACM, pages 86-94.
  Abstract | Pdf
  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 NP and 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.


• 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. LNCS 10806, pages 38-54.
  Abstract | Pdf
  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, 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.
  Abstract
  Le 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 gamma-correction 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 alpha-dé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:1-12:16, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
  Abstract | Pdf
  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 con- troller, 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 ∈ 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 cut-off 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 ≤ 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 Infinite-State Probabilistic Systems
  In proceedings of the 27th International Conference on Concurrency Theory (Concur'16), Québec City, Canada, August 2016. LIPIcs 59, pages 37:1-37:15, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
  Abstract | Pdf
  In 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 PSPACE-complete. 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 FF-diagnosability but with a Gδ set instead of an open set and also for IF- and IA-diagnosability when pLTS are finitely branching. We also prove that surprisingly FA-diagnosability 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:1-101:14, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
  Abstract | Pdf
  In 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 real-time stochastic processes). This allows us to obtain decidability results for both qualitative and quantitative verification problems on some classes of real-time stochastic processes, including generalized semi-Markov 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 549-561.
  Abstract | Pdf
  Diagnosis 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 A-diagnosability) 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 AA-diagnosability) 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 AA-diagnosability are undecidable while AA-diagnosability 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 44-57. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
  Abstract | Pdf
  We 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 NP-complete, assuming that the set of receivers is chosen non-deterministically 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 417-429. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
  Abstract | Pdf
  In 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 PSPACE-complete. 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 NLOGSPACE-complete. 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 1-clock 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 313-328. Springer.
  Abstract | Pdf
  We 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 non-trivial reduction to a simple almost-sure 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 134-148. Springer.
  Abstract | Pdf
  We 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 29-42. Springer.
  Abstract | Pdf
  The 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 observation-based strategy that makes the system diagnosable with probability one. We prove that this problem is EXPTIME-complete, and that the active diagnosis strategies are belief-based. 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 belief-based strategies, and that it is undecidable. However, it belongs to NEXPTIME when restricted to belief-based 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 501-513. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
  Abstract | Pdf
  Parameterized 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 single-clock 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 almost-surely 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 steady-state 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 390-304. Springer.
  Abstract | Pdf
  This paper addresses a control problem for probabilistic models in the setting of Markov decision processes (MDP). We are interested in the steady-state control problem which asks, given an ergodic MDP M and a distribution \delta, whether there exists a (history-dependent randomized) policy \pi ensuring that the steady-state distribution of M under \pi is exactly \delta. We first show that stationary randomized policies suffice to achieve a given steady-state distribution. Then we infer that the steady-state 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 steady-state distribution on labels carried by the states, and we provide a PSPACE algorithm. We also show that a related steady-state language inclusion problem is decidable in EXPTIME for LMDP. Finally, we prove that if we consider MDP under partial observation (POMDP), the steady-state 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 355-371. Springer.
  Abstract | Pdf
  Stochastic 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 | Pdf
  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.


• 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 43-58. 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 single-player 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 92-106. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
  Abstract | Pdf
  
  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.
  
  
• 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, May-June 2012. LIPIcs 15, pages 101-116. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
  Abstract | Pdf
  
  We study decidability issues for reachability problems in graph transformation systems, a powerful infinite-state 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 context-free 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 411-422. Schloss Dagstuhl - Leibniz-Zentrum 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 model-checking. 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 246-257. Springer.
  Abstract | Pdf
  The languages of infinite timed words accepted by timed automata are traditionally defined using Büchi-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 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 245-259. Springer.
  Abstract | Pdf | Long version
  Timed automata are frequently used to model real-time 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 game-based algorithm which, given a timed automaton with ε-transitions and invariants, tries to produce a language-equivalent deterministic timed automaton, otherwise a deterministic over-approximation. 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.
  Off-line Test Selection with Test Purposes for Non-Deterministic 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 96-111. Springer.
  Abstract | Pdf | Long version
  This paper proposes novel off-line test generation techniques for 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, 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 co-reachability 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 Infinite-State Systems (INFINITY'10), Singapore, September 2010. EPTCS 39, page 77-90.
  Abstract | Pdf
  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 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 679-697. Springer.
  Abstract | Pdf | Long version
  On the one hand, modal specifications are classic, convenient, and expressive mathematical objects to represent interfaces of component-based 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 component-based 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 event-clock 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 43-54. Springer.
  Abstract | Pdf
  In this paper, we propose an abstract procedure which, given a timed automaton, produces a language-equivalent 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 (event-clock timed automata, automata with integer resets), but some others were not. We prove for instance that strongly non-Zeno 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 EXPSPACE-complete for strongly non-Zeno 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 319-328. IEEE Computer Society Press.
  Abstract | Pdf
  We consider two-players stochastic zero-sum games with partial observation on both sides and finitely many states, signals and actions. We are interested in the existence of almost-surely 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 almost-surely, then both players have positively winning strategies. For Büchi games, if player 1 cannot win almost-surely, then player 2 has a positively winning strategy. Together with these qualitative determinacy results, we provide fix-point 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 finite-memory strategies, computed by the fix-point algorithm, ranging from no memory to doubly-exponential, 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 152-163. Springer.
  Abstract | Pdf
  In the application domain of component-based system design, developing theories which support compositional reasoning is notoriously challenging. We define timed modal specifications, an automata-based 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 Model-Checking of One-Clock 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 55-64. IEEE Computer Society Press.
  Abstract | Pdf
  In [BBBBG-lics08] a probabilistic semantics for timed automata has been defined in order to rule out unlikely (sequences of) events. The qualitative model-checking 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 single-clock timed automata. In this paper, we consider the quantitative model-checking problem for omega-regular properties: we aim at computing the exact probability that a given timed automaton satisfies an omega-regular property. We develop a framework in which we can compute a closed-form 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.
  Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata.
  In Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science (LICS'08), Pittsburgh, PA, USA, June 2008, pages 217-226. IEEE Computer Society Press.
  Abstract | Pdf | Long version
  In 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 single-clock timed automata (and only in that framework), and prove that the corresponding relaxed model-checking problems are PSPACE-Complete. Moreover, we prove that the probabilistic non-Zenoness can be decided for single-clock 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, March-April 2008, LNCS 4962, pages 287-301. Springer.
  EATCS best theory paper at ETAPS.
  Abstract | Pdf
  Probabilistic Büchi automata (PBA) are finite-state 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 PBA-specification, turn out to be undecidable. An important consequence of these results are several undecidability results for stochastic games with incomplete information, modelled by partially-observable Markov decision processes and omega-regular 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 179-191. Springer.
  Abstract | Pdf
  Like most models used in model-checking, 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 PSPACE-Complete model-checking problem for LTL over finite executions.


• C. Baier, N. Bertrand and Ph. Schnoebelen.
  On Computing Fixpoints in Well-Structured 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 347-361. Springer.
  Abstract | Pdf
  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.


• 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 212-227. Springer.
  Abstract | Pdf
  NPLCS’s are a new model for nondeterministic channel systems where unreliable communication is modeled by probabilistic message losses. We show that, for omega-regular linear-time properties and finite-memory schedulers, qualitative model-checking 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 two-way 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 59-69. Elsevier Science Publishers, 2006.
  Abstract | Pdf
  The hierarchy of Symbolic Transition Systems, introduced by Henzinger, Majumdar and Raskin, is an elegant classification tool for some families of infinite-state 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 infinite-state 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 120-135. Springer.
  Abstract | Pdf
  Lossy 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 linear-time 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 | Pdf
  Asynchronous 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 linear-time 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 Infinite-State Systems (AVIS'04), Barcelona, Spain, April 2004.
  Abstract | Pdf
  Lossy 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 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 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 infinite-state 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 MSO-definable properties and some relevant subcases.


• N. Bertrand, I. Charon, O. Hudry and A. Lobstein.
  Identifying or Locating-Dominating 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