Translation Results for Modal Logics of Reactive Systems. - François Laroussinie; Sophie Pinchinat; Philippe Schnoebelen (AMAST, 1993)

A Hierarchy of Temporal Logics with Past (Extended Abstract). - François Laroussinie; Philippe Schnoebelen (STACS, 1994)

Compositional Model Checking of Real Time Systems. - François Laroussinie; Kim Guldstrand Larsen (CONCUR, 1995)

From Timed Automata to Logic - and Back. - François Laroussinie; Kim Guldstrand Larsen; Carsten Weise (MFCS, 1995)

About the Expressive Power of CTL Combinators. - François Laroussinie (Inf. Process. Lett., 1995)

Translations Between Modal Logics of Reactive Systems. - François Laroussinie; Sophie Pinchinat; Philippe Schnoebelen (Theor. Comput. Sci., 1995)

A Hierarchy of Temporal Logics with Past. - François Laroussinie; Philippe Schnoebelen (Theor. Comput. Sci., 1995)

A Compositional Proof of a Real-Time Mutual Exclusion Protocol. - Kåre J. Kristoffersen; François Laroussinie; Kim Guldstrand Larsen; Paul Pettersson; Wang Yi 001 (TAPSOFT, 1997)

Specification in CTL+Past, verification in CTL. - François Laroussinie; Philippe Schnoebelen (EXPRESS, 1997)

CMC: A Tool for Compositional Model-Checking of Real-Time Systems. - François Laroussinie; Kim Guldstrand Larsen (FORTE, 1998)

Model-Checking for Hybrid Systems by Quotienting and Constraints Solving. - Franck Cassez; François Laroussinie (CAV, 2000)

The State Explosion Problem from Trace to Bisimulation Equivalence. - François Laroussinie; Philippe Schnoebelen (FoSSaCS, 2000)

Systems and Software Verification, Model-Checking Techniques and Tools. - Béatrice Bérard; Michel Bidoit; Alain Finkel; François Laroussinie; Antoine Petit 001; Laure Petrucci; Philippe Schnoebelen; Pierre McKenzie (Springer, 2001)

Model Checking CTL+ and FCTL is Hard. - François Laroussinie; Nicolas Markey; Philippe Schnoebelen (FoSSaCS, 2001)

On Model Checking Durational Kripke Structures. - François Laroussinie; Nicolas Markey; Philippe Schnoebelen (FoSSaCS, 2002)

Temporal Logic with Forgettable Past. - François Laroussinie; Nicolas Markey; Philippe Schnoebelen (LICS, 2002)

Is your model checker on time? On the complexity of model checking for timed modal logics. - Luca Aceto; François Laroussinie (J. Log. Algebraic Methods Program., 2002)

On the expressivity and complexity of quantitative branching-time temporal logics. - François Laroussinie; Philippe Schnoebelen; Mathieu Turuani (Theor. Comput. Sci., 2003)

Model Checking Timed Automata with One or Two Clocks. - François Laroussinie; Nicolas Markey; Philippe Schnoebelen (CONCUR, 2004)

Modal Logics for Timed Control. - Patricia Bouyer; Franck Cassez; François Laroussinie (CONCUR, 2005)

A New Modality for Almost Everywhere Properties in Timed Automata. - Houda Bel Mokadem; Béatrice Bérard; Patricia Bouyer; François Laroussinie (CONCUR, 2005)

Diagonal Constraints in Timed Automata: Forward Analysis of Timed Systems. - Patricia Bouyer; François Laroussinie; Pierre-Alain Reynier (FORMATS, 2005)

Model Checking Durational Probabilistic Systems. - François Laroussinie; Jeremy Sproston (FoSSaCS, 2005)

Guidelines for a graduate curriculum on embedded software and systems. - Paul Caspi; Alberto L. Sangiovanni-Vincentelli; Luís Almeida 001; Albert Benveniste; Bruno Bouyssounouse; Giorgio C. Buttazzo; Ivica Crnkovic; Werner Damm; Jakob Engblom; Gerhard Fohler; Marisol García-Valls; Hermann Kopetz; et al. (ACM Trans. Embed. Comput. Syst., 2005)

Timed Temporal Logics for Abstracting Transient States. - Houda Bel Mokadem; Béatrice Bérard; Patricia Bouyer; François Laroussinie (ATVA, 2006)

Model-Checking Timed. - François Laroussinie; Nicolas Markey; Ghassan Oreiby (FORMATS, 2006)

A parametric analysis of the state-explosion problem in model checking. - Stéphane Demri; François Laroussinie; Philippe Schnoebelen (J. Comput. Syst. Sci., 2006)

Efficient timed model checking for discrete-time systems. - François Laroussinie; Nicolas Markey; Philippe Schnoebelen (Theor. Comput. Sci., 2006)

Timed Concurrent Game Structures. - Thomas Brihaye; François Laroussinie; Nicolas Markey; Ghassan Oreiby (CONCUR, 2007)

State explosion in almost-sure probabilistic reachability. - François Laroussinie; Jeremy Sproston (Inf. Process. Lett., 2007)

Model Checking Probabilistic Timed Automata with One or Two Clocks. - Marcin Jurdzinski; Jeremy Sproston; François Laroussinie (Log. Methods Comput. Sci., 2008)

On the Expressiveness and Complexity of ATL. - François Laroussinie; Nicolas Markey; Ghassan Oreiby (Log. Methods Comput. Sci., 2008)

ATL with Strategy Contexts and Bounded Memory. - Thomas Brihaye; Arnaud Da Costa Lopes; François Laroussinie; Nicolas Markey (LFCS, 2009)

ATL with Strategy Contexts: Expressiveness and Model Checking. - Arnaud Da Costa Lopes; François Laroussinie; Nicolas Markey (FSTTCS, 2010)

Counting LTL. - François Laroussinie; Antoine Meyer; Eudes Petonnet (TIME, 2010)

Christel Baier and Joost-Pieter KatoenPrinciples of Model Checking. MIT Press (May 2008).ISBN: 978-0-262-02649-9, 975 pp. Hardcover. - François Laroussinie (Comput. J., 2010)

Temporal Logics for Games. - François Laroussinie (Bull. EATCS, 2010)

Timed Modal Logics for Real-Time Systems - Specification, Verification and Control. - Patricia Bouyer; Franck Cassez; François Laroussinie (J. Log. Lang. Inf., 2011)

Quantified CTL: Expressiveness and Model Checking - (Extended Abstract). - Arnaud Da Costa Lopes; François Laroussinie; Nicolas Markey (CONCUR, 2012)

Counting CTL - François Laroussinie; Antoine Meyer; Eudes Petonnet (Log. Methods Comput. Sci., 2012)

Satisfiability of ATL with strategy contexts. - François Laroussinie; Nicolas Markey (GandALF, 2013)

Quantified CTL: Expressiveness and Complexity. - François Laroussinie; Nicolas Markey (Log. Methods Comput. Sci., 2014)

ATLsc with partial observation. - François Laroussinie; Nicolas Markey; Arnaud Sangnier (GandALF, 2015)

Augmenting ATL with strategy contexts. - François Laroussinie; Nicolas Markey (Inf. Comput., 2015)

On the Expressiveness of QCTL. - Amélie David 001; François Laroussinie; Nicolas Markey (CONCUR, 2016)

Timed Temporal Logics. - Patricia Bouyer; François Laroussinie; Nicolas Markey; Joël Ouaknine; James Worrell 001 (Models, Algorithms, Logics and Tools, 2017)

Towards Synthesis of Distributed Algorithms with SMT Solvers. - Carole Delporte-Gallet; Hugues Fauconnier; Yan Jurski; François Laroussinie; Arnaud Sangnier (NETYS, 2019)

From Quantified CTL to QBF. - Akash Hossain; François Laroussinie (TIME, 2019)

QCTL model-checking with QBF solvers. - Akash Hossain; François Laroussinie (Inf. Comput., 2021)

QLTL Model-Checking. - François Laroussinie; Loriane Leclercq; Arnaud Sangnier (CSL, 2024)

Arbitrary-arity Tree Automata and QCTL. - François Laroussinie; Nicolas Markey (CoRR, 2024)

Arbitrary-Arity Tree Automata for QCTL. - François Laroussinie; Nicolas Markey (CONCUR, 2025)