# Publications

You can find below the complete list of my publications.

## Journals

- 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 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 | PdfThis 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.

AbstractModal 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 | 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 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 | 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 141-165, 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 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 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 | PdfThe 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 versionTimed 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 versionThis 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 | 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 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 versionOn 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 | PdfIn 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 | PdfWe 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 | PdfIn 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 | PdfIn [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 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 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 | PdfProbabilistic 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 | PdfLike 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 | PdfWe 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 | PdfNPLCS’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 | PdfThe 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 | 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 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 | 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 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 | 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 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