• Home
• Publications
• Talks
• Misc

Journals

• 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, 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. Springer, to appear.
  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.

Thesis

• 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