Model Checking Lossy Channels Systems Is Probably Decidable. - Nathalie Bertrand 001; Philippe Schnoebelen (FoSSaCS, 2003)

Identifying and locating-dominating codes on chains and cycles. - Nathalie Bertrand 001; Irène Charon; Olivier Hudry; Antoine Lobstein (Eur. J. Comb., 2004)

1-identifying codes on trees. - Nathalie Bertrand 001; Irène Charon; Olivier Hudry; Antoine Lobstein (Australas. J Comb., 2005)

Verifying nondeterministic probabilistic channel systems against $ omega$-regular linear-time properties - Christel Baier; Nathalie Bertrand 001; Philippe Schnoebelen (CoRR, 2005)

A Short Visit to the STS Hierarchy. - Nathalie Bertrand 001; Philippe Schnoebelen (EXPRESS, 2005)

Verification of probabilistic systems with faulty communication. - Parosh Aziz Abdulla; Nathalie Bertrand 001; Alexander Moshe Rabinovich; Philippe Schnoebelen (Inf. Comput., 2005)

Symbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and Fairness. - Christel Baier; Nathalie Bertrand 001; Philippe Schnoebelen (FORTE, 2006)

On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems. - Christel Baier; Nathalie Bertrand 001; Philippe Schnoebelen (LPAR, 2006)

A note on the attractor-property of infinite-state Markov chains. - Christel Baier; Nathalie Bertrand 001; Philippe Schnoebelen (Inf. Process. Lett., 2006)

Modèles stochastiques pour les pertes de messages dans les protocoles asynchrones, et techniques de vérification automatique. (Stochastic models for Lossy Channel Systems and automated verification techniques). - Nathalie Bertrand 001 (2006)

Probabilistic and Topological Semantics for Timed Automata. - Christel Baier; Nathalie Bertrand 001; Patricia Bouyer; Thomas Brihaye; Marcus Größer (FSTTCS, 2007)

Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties. - Christel Baier; Nathalie Bertrand 001; Philippe Schnoebelen (ACM Trans. Comput. Log., 2007)

On Decision Problems for Probabilistic Büchi Automata. - Christel Baier; Nathalie Bertrand 001; Marcus Größer (FoSSaCS, 2008)

Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata. - Christel Baier; Nathalie Bertrand 001; Patricia Bouyer; Thomas Brihaye; Marcus Größer (LICS, 2008)

Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics. - Nathalie Bertrand 001; Patricia Bouyer; Thomas Brihaye; Nicolas Markey (QEST, 2008)

Determinacy and Decidability of Reachability Games with Partial Observation on Both Sides - Nathalie Bertrand 001; Blaise Genest; Hugo Gimbert (CoRR, 2008)

The Effect of Tossing Coins in Omega-Automata. - Christel Baier; Nathalie Bertrand 001; Marcus Größer (CONCUR, 2009)

When Are Timed Automata Determinizable? - Christel Baier; Nathalie Bertrand 001; Patricia Bouyer; Thomas Brihaye (ICALP (2), 2009)

A Compositional Approach on Modal Specifications for Timed Systems. - Nathalie Bertrand 001; Axel Legay; Sophie Pinchinat; Jean-Baptiste Raclet (ICFEM, 2009)

Refinement and Consistency of Timed Modal Specifications. - Nathalie Bertrand 001; Sophie Pinchinat; Jean-Baptiste Raclet (LATA, 2009)

Probabilistic Acceptors for Languages over Infinite Words. - Christel Baier; Nathalie Bertrand 001; Marcus Größer (SOFSEM, 2009)

Probabilistic Automata over Infinite Words: Expressiveness, Efficiency, and Decidability - Christel Baier; Nathalie Bertrand 001; Marcus Größer (DCFS, 2009)

Probabilistic regular graphs - Nathalie Bertrand 001; Christophe Morvan (INFINITY, 2010)

Minimal Disclosure in Partially Observable Markov Decision Processes. - Nathalie Bertrand 001; Blaise Genest (FSTTCS, 2011)

Emptiness and Universality Problems in Timed Automata with Positive Frequency. - Nathalie Bertrand 001; Patricia Bouyer; Thomas Brihaye; Amélie Stainer (ICALP (2), 2011)

Bounded Satisfiability for PCTL. - Nathalie Bertrand 001; John Fearnley; Sven Schewe (CSL, 2012)

Playing Optimally on Timed Automata with Random Delays. - Nathalie Bertrand 001; Sven Schewe (FORMATS, 2012)

On the Decidability Status of Reachability and Coverability in Graph Transformation Systems. - Nathalie Bertrand 001; Giorgio Delzanno; Barbara König 001; Arnaud Sangnier; Jan Stückrath (RTA, 2012)

Off-line test selection with test purposes for non-deterministic timed automata - Nathalie Bertrand 001; Thierry Jéron; Amélie Stainer; Moez Krichen (Log. Methods Comput. Sci., 2012)

Probabilistic ω-automata. - Christel Baier; Marcus Größer; Nathalie Bertrand 001 (J. ACM, 2012)

Modal event-clock specifications for timed component-based design. - Nathalie Bertrand 001; Axel Legay; Sophie Pinchinat; Jean-Baptiste Raclet (Sci. Comput. Program., 2012)

Parameterized Verification of Many Identical Probabilistic Timed Processes. - Nathalie Bertrand 001; Paulin Fournier (FSTTCS, 2013)

The Steady-State Control Problem for Markov Decision Processes. - S. Akshay 001; Nathalie Bertrand 001; Serge Haddad; Loïc Hélouët (QEST, 2013)

Transient Analysis of Networks of Stochastic Timed Automata Using Stochastic State Classes. - Paolo Ballarini; Nathalie Bertrand 001; András Horváth; Marco Paolieri; Enrico Vicario (QEST, 2013)

Solving Stochastic Büchi Games on Infinite Decisive Arenas. - Nathalie Bertrand 001; Philippe Schnoebelen (QAPL, 2013)

Computable fixpoints in well-structured symbolic model checking. - Nathalie Bertrand 001; Philippe Schnoebelen (Formal Methods Syst. Des., 2013)

Active Diagnosis for Probabilistic Systems. - Nathalie Bertrand 001; Eric Fabre; Stefan Haar; Serge Haddad; Loïc Hélouët (FoSSaCS, 2014)

Playing with Probabilities in Reconfigurable Broadcast Networks. - Nathalie Bertrand 001; Paulin Fournier; Arnaud Sangnier (FoSSaCS, 2014)

Foundation of Diagnosis and Predictability in Probabilistic Systems. - Nathalie Bertrand 001; Serge Haddad; Engel Lefaucheux (FSTTCS, 2014)

Deciding the Value 1 Problem for Reachability in 1-Clock Decision Stochastic Timed Automata. - Nathalie Bertrand 001; Thomas Brihaye; Blaise Genest (QEST, 2014)

Stochastic Timed Automata. - Nathalie Bertrand 001; Patricia Bouyer; Thomas Brihaye; Quentin Menet; Christel Baier; Marcus Größer; Marcin Jurdzinski (Log. Methods Comput. Sci., 2014)

Contributions to the verification and control of timed and probabilistic models : Mémoire d'habilitation à diriger des recherches. - Nathalie Bertrand 001 (2015)

Distributed Local Strategies in Broadcast Networks. - Nathalie Bertrand 001; Paulin Fournier; Arnaud Sangnier (CONCUR, 2015)

A game approach to determinize timed automata. - Nathalie Bertrand 001; Amélie Stainer; Thierry Jéron; Moez Krichen (Formal Methods Syst. Des., 2015)

Diagnosis in Infinite-State Probabilistic Systems. - Nathalie Bertrand 001; Serge Haddad; Engel Lefaucheux (CONCUR, 2016)

Analysing Decisive Stochastic Processes. - Nathalie Bertrand 001; Patricia Bouyer; Thomas Brihaye; Pierre Carlier (ICALP, 2016)

Accurate Approximate Diagnosability of Stochastic Systems. - Nathalie Bertrand 001; Serge Haddad; Engel Lefaucheux (LATA, 2016)

Editorial: Quantitative Aspects of Programming Languages and Systems. - Nathalie Bertrand 001; Luca Bortolussi; Herbert Wiklicky (Theor. Comput. Sci., 2016)

Controlling a Population. - Nathalie Bertrand 001; Miheer Dewaskar; Blaise Genest; Hugo Gimbert (CONCUR, 2017)

Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes. - Aaron Bohy; Véronique Bruyère; Jean-François Raskin; Nathalie Bertrand 001 (Acta Informatica, 2017)

Qualitative Determinacy and Decidability of Stochastic Games with Signals. - Nathalie Bertrand 001; Blaise Genest; Hugo Gimbert (J. ACM, 2017)

Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes. - Christel Baier; Nathalie Bertrand 001; Clemens Dubslaff; Daniel Gburek; Ocan Sankur (LICS, 2018)

Parameterized Verification of Synchronization in Constrained Reconfigurable Broadcast Networks. - A. R. Balasubramanian; Nathalie Bertrand 001; Nicolas Markey (TACAS (2), 2018)

When are stochastic transition systems tameable? - Nathalie Bertrand 001; Patricia Bouyer; Thomas Brihaye; Pierre Carlier (J. Log. Algebraic Methods Program., 2018)

Concurrent Parameterized Games. - Nathalie Bertrand 001; Patricia Bouyer; Anirban Majumdar 002 (FSTTCS, 2019)

Long-run Satisfaction of Path Properties. - Christel Baier; Nathalie Bertrand 001; Jakob Piribauer; Ocan Sankur (LICS, 2019)

Performance Evaluation of Metro Regulations Using Probabilistic Model-Checking. - Nathalie Bertrand 001; Benjamin Bordais; Loïc Hélouët; Thomas Mari; Julie Parreaux; Ocan Sankur (RSSRail, 2019)

A tale of two diagnoses in probabilistic systems. - Nathalie Bertrand 001; Serge Haddad; Engel Lefaucheux (Inf. Comput., 2019)

Controlling a population. - Nathalie Bertrand 001; Miheer Dewaskar; Blaise Genest; Hugo Gimbert; Adwait Amit Godbole (Log. Methods Comput. Sci., 2019)

Introduction to the Special Issue on Qest 2017. - Luca Bortolussi; Nathalie Bertrand 001 (ACM Trans. Model. Comput. Simul., 2019)

Synthesizing Safe Coalition Strategies. - Nathalie Bertrand 001; Patricia Bouyer; Anirban Majumdar 002 (FSTTCS, 2020)

Dynamic Network Congestion Games. - Nathalie Bertrand 001; Nicolas Markey; Suman Sadhukhan; Ocan Sankur (FSTTCS, 2020)

Concurrent Games with Arbitrarily Many Players (Invited Talk). - Nathalie Bertrand 001 (MFCS, 2020)

Taming denumerable Markov decision processes with decisiveness. - Nathalie Bertrand 001; Patricia Bouyer; Thomas Brihaye; Paulin Fournier (CoRR, 2020)

Diagnosis and Degradation Control for Probabilistic Systems. - Nathalie Bertrand 001; Serge Haddad; Engel Lefaucheux (Discret. Event Dyn. Syst., 2020)

Model checking randomized distributed algorithms. - Nathalie Bertrand 001 (ACM SIGLOG News, 2020)

CONCUR Test-Of-Time Award 2021 (Invited Paper). - Nathalie Bertrand 001; Luca de Alfaro; Rob van Glabbeek; Catuscia Palamidessi; Nobuko Yoshida (CONCUR, 2021)

Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms. - Nathalie Bertrand 001; Bastien Thomas; Josef Widder (CONCUR, 2021)

Quantified Linear Temporal Logic over Probabilistic Systems with an Application to Vacuity Checking. - Jakob Piribauer; Christel Baier; Nathalie Bertrand 001; Ocan Sankur (CONCUR, 2021)

Distributed Algorithms: A Challenging Playground for Model Checking (Invited Talk). - Nathalie Bertrand 001 (OPODIS, 2021)

A Reduction Theorem for Randomized Distributed Algorithms Under Weak Adversaries. - Nathalie Bertrand 001; Marijana Lazic; Josef Widder (VMCAI, 2021)

Interviews with the 2021 CONCUR Test-of-Time Award Recipients. - Luca Aceto; Nathalie Bertrand 001; Nobuko Yoshida (Bull. EATCS, 2021)

Reconfiguration and Message Losses in Parameterized Broadcast Networks. - Nathalie Bertrand 001; Patricia Bouyer; Anirban Majumdar 002 (Log. Methods Comput. Sci., 2021)

Verification of randomized consensus algorithms under round-rigid adversaries. - Nathalie Bertrand 001; Igor Konnov 001; Marijana Lazic; Josef Widder (Int. J. Softw. Tools Technol. Transf., 2021)

Correction to: Verification of randomized consensus algorithms under round-rigid adversaries. - Nathalie Bertrand 001; Igor Konnov 001; Marijana Lazic; Josef Widder (Int. J. Softw. Tools Technol. Transf., 2021)

Semilinear Representations for Series-Parallel Atomic Congestion Games. - Nathalie Bertrand 001; Nicolas Markey; Suman Sadhukhan; Ocan Sankur (FSTTCS, 2022)

Parameterized Safety Verification of Round-Based Shared-Memory Systems. - Nathalie Bertrand 001; Nicolas Markey; Ocan Sankur; Nicolas Waldburger (ICALP, 2022)

Brief Announcement: Holistic Verification of Blockchain Consensus. - Nathalie Bertrand 001; Vincent Gramoli; Igor Konnov 001; Marijana Lazic; Pierre Tholoniat; Josef Widder (PODC, 2022)

Holistic Verification of Blockchain Consensus. - Nathalie Bertrand 001; Vincent Gramoli; Igor Konnov 001; Marijana Lazic; Pierre Tholoniat; Josef Widder (DISC, 2022)

Games on Graphs. - Nathanaël Fijalkow; Nathalie Bertrand 001; Patricia Bouyer-Decitre; Romain Brenguier; Arnaud Carayol; John Fearnley; Hugo Gimbert; Florian Horn 001; Rasmus Ibsen-Jensen; Nicolas Markey; Benjamin Monmege; Petr Novotný 001; et al. (CoRR, 2023)

Synchronizing words under LTL constraints. - Nathalie Bertrand 001; Hugo Francon; Nicolas Markey (Inf. Process. Lett., 2023)

Reusable Formal Verification of DAG-Based Consensus Protocols. - Nathalie Bertrand 001; Pranav Ghorpade; Sasha Rubin; Bernhard Scholz; Pavle Subotic (NFM, 2025)

Antichains for Concurrent Parameterized Games. - Nathalie Bertrand 001; Patricia Bouyer; Gaëtan Staquet (CoRR, 2025)