Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci, and Philippe
Schnoebelen.
Systems and Software Verification. Model-Checking Techniques
and Tools Springer, 2001.
Philippe Schnoebelen, Béatrice Bérard, Michel Bidoit, François Laroussinie, and Antoine Petit.
Vérification de logiciels : techniques et outils du
model-checking Vuibert, April 1999.
Chapters in Books
Patricia Bouyer and François Laroussinie.
Model checking timed automata.
In Stephan Merz and Nicolas Navet, editors, Modeling and
Verification of Real-Time Systems, pages 111--140. ISTE Ltd. -- John Wiley
& Sons, Ltd., January 2008.
[PDF ]
Patricia Bouyer and François Laroussinie.
Vérification par automates temporisés.
In Nicolas Navet, editor, Systèmes temps-réel 1:
techniques de description et de vérification , pages 121--150.
Hermès, June 2006.
[PDF ]
Journals
Akash Hossain, François Laroussinie.
QCTL model-checking with QBF solvers.
Information and Computation 280:104642 ,
2021.
[ Abstract ,
PDF ]
François Laroussinie, Nicolas Markey.
Augmenting ATL with strategy contexts.
Information and Computation 245:98-123 ,
2015.
[ Abstract ,
PDF ]
François Laroussinie, Nicolas Markey.
Quantified CTL: Expressiveness and Complexity.
Logical Methods in Computer Science 10(4) ,
2014.
[ Abstract ,
PDF ]
François Laroussinie, Antoine Meyer, Eudes Petonnet.
Counting CTL.
Logical Methods in Computer Science 9(1), ,
2012.
[ Abstract ,
PDF ]
Patricia Bouyer, Franck Cassez, and François Laroussinie.
Timed Modal Logics for Real-Time Systems.
Journal of Logic, Language and Information ,
20(2), 2011.
[ Abstract ,
PDF ]
Marcin Jurdzinski, François Laroussinie, and Jeremy Sproston.
Model checking probabilistic timed automata with one or two clocks.
Logical Methods in Computer Science, 4(3:11),
September 2008.
[ Abstract ,
PDF ]
François Laroussinie, Nicolas Markey, and Ghassan Oreiby.
On the expressiveness and complexity of ATL.
Logical Methods in Computer Science, 4(2:7),
May 2008.
[ Abstract ,
PDF ]
François Laroussinie and Jeremy Sproston.
State explosion in almost-sure probabilistic reachability.
Information Processing Letters, 102(6):236--241, June 2007.
[ Abstract ,
PDF ]
Stéphane Demri, François Laroussinie, and Philippe Schnoebelen.
A parametric analysis of the state explosion problem in model checking.
Journal of Computer and System Sciences, 72(4):547--575, June 2006.
[ Abstract ,
PDF ]
François Laroussinie, Nicolas Markey, and Philippe Schnoebelen.
Efficient timed model checking for discrete-time systems.
Theoretical Computer Science, 353(1-3):249--271, March 2006.
[ Abstract ,
PDF ]
François Laroussinie, Philippe Schnoebelen, and Mathieu Turuani.
On the expressivity and complexity of quantitative branching-time
temporal logics.
Theoretical Computer Science, 297(1-3):297--315, March 2003.
[ Abstract ,
PS ]
Luca Aceto and François Laroussinie.
Is your model checker on time? On the complexity of model checking
for timed modal logics.
Journal of Logic and Algebraic Programming, 52-53:7--51, August 2002.
[ Abstract ,
PS ]
François Laroussinie and Philippe Schnoebelen.
Specification in CTL+past for verification in CTL.
Information and Computation, 156(1-2):236--263,
January 2000.
[PS ]
François Laroussinie and Philippe Schnoebelen.
A hierarchy of temporal logics with past.
Theoretical Computer Science, 148(2):303--324,
September 1995.
[PDF ]
François Laroussinie.
About the expressive power of CTL combinators.
Information Processing Letters, 54(6):343--345,
June 1995.
[PS ,
PDF ]
François Laroussinie, Sophie Pinchinat, and Philippe Schnoebelen.
Translations between modal logics of reactive systems.
Theoretical Computer Science, 140(1):53--71,
March 1995.
[PDF ]
Conferences
Akash Hossain and François Laroussinie.
From Quantified CTL to QBF. In
Proceedings of the 26th International Symposium on Temporal Representation and Reasoning, TIME 2019,
[ Abstract ,
PDF ]
Carole Delporte-Gallet, Hugues Fauconnier, Yan Jurski,
François Laroussinie and Arnaud Sangnier.
Towards synthesis of distributed algorithms with SMT solvers. In
Proceedings of the 7th International Conference on NETworked sYStems (NETYS 2019),
[ Abstract ,
PDF ]
Amelie David, François Laroussinie and Nicolas Markey.
On the expressiveness of QCTL. In
Proceedings of the 27th International Conference on Concurrency Theory (CONCUR 2016),
[ Abstract ,
PDF ]
François Laroussinie, Nicolas Markey and Arnaud Sangnier.
ATLsc with partial observation. In
Proceedings of Sixth International Symposium on Games, Automata, Logics
and Formal Verification, GandALF 2015,
[ Abstract ,
PDF ]
François Laroussinie and Nicolas Markey.
Satisfiability of ATL with strategy contexts. In
Proceedings of GandALF'13,
Electronic Proceedings in Theoretical Computer Science, 2013.
To appear.
[ Abstract ,
PDF ]
Arnaud Da Costa, François Laroussinie and Nicolas Markey.
Quantified CTL: expressiveness and model checking. In
Proceedings of the 23rd International Conference on Concurrency Theory (CONCUR 2012),
Newcastle upon Tyne, UK, September 4-7, 2012. Proceedings. Lecture Notes in Computer Science 7454 Springer 2012, pages
177-192
[ Abstract ,
PDF ]
Arnaud Da Costa, François Laroussinie et Nicolas Markey.
Expressiveness and decidability of ATL with strategy contexts. In
Proceedings of the IARCS Annual Conference on
Foundations of Software Technology and Theoretical Computer Science
(FSTTCS'10), Leibniz International Proceedings in Informatics (LIPIcs) 8, page 120-132, 2010.
[ Abstract ,
PDF ]
François Laroussinie, Antoine Meyer, and Eudes Petonnet.
Counting LTL.
In Proceedings
of the
17th International Symposium on
Temporal Representation and Reasoning (TIME'10)
, Paris, France, September 2010. IEEE Computer Society Press.
[ Abstract ,
PDF ]
François Laroussinie, Antoine Meyer, and Eudes Petonnet.
Counting CTL.
In Proceedings
of the 13th
International Conference on Foundations of Software Science and
Computation Structures (FoSSaCS 2010) LNCS 6014,
April 2010.
[ Abstract ,
PDF ]
Thomas Brihaye, Arnaud Da Costa, François Laroussinie, and Nicolas Markey.
ATL with strategy contexts and bounded memory.
In S.N. Artemov and A. Nerode, editors, { Proceedings
of the Symposium on Logical Foundations of Computer Science
(LFCS'09), Deerfield Beach, FL, USA, January 2009, volume 5407 of Lecture
Notes in Computer Science, pages 92--106. Springer.
[ Abstract ,
(long version -- PDF) ]
Thomas Brihaye, François Laroussinie, Nicolas Markey, and Ghassan Oreiby.
Timed concurrent game structures.
In Proceedings of the 18th International Conference on
Concurrency Theory (CONCUR'07), Lisbon, Portugal, September 2007,
volume 4703 of Lecture Notes in Computer Science, pages 445--459.
Springer.
[ Abstract ,
PDF ]
Marcin Jurdzinski, François Laroussinie, and Jeremy Sproston.
Model checking probabilistic timed automata with one or two clocks.
In Proceedings of
the 13th International Conference on Tools and Algorithms for
Construction and Analysis of Systems (TACAS'07), Braga, Portugal,
March 2007, volume 4424 of Lecture Notes in Computer Science,
pages 170--184. Springer.
[ Abstract ,
PDF ]
François Laroussinie, Nicolas Markey, and Ghassan Oreiby.
On the expressiveness and complexity of ATL.
In Proceedings of the 10th
International Conference on Foundations of Software Science and
Computation Structures (FoSSaCS'07), Braga, Portugal, March 2007,
volume 4423 of Lecture Notes in Computer Science, pages 243--257.
Springer.
[ Abstract ,
PDF ]
Houda Belmokadem, Béatrice Bérard, Patricia Bouyer, and François Laroussinie.
Timed temporal logics for abstracting transient states.
In Proceedings of
the 4th International Symposium on Automated Technology for
Verification and Analysis (ATVA'06), Beijing, ROC, October 2006,
volume 4218 of Lecture Notes in Computer Science, pages 337--351.
Springer.
[ Abstract ,
PDF ]
François Laroussinie, Nicolas Markey, and Ghassan Oreiby.
Model checking timed ATL for durational concurrent game structures.
In Proceedings of the 4th International
Conference on Formal Modelling and Analysis of Timed Systems
(FORMATS'06), Paris, France, September 2006, volume 4202 of Lecture
Notes in Computer Science, pages 245--259. Springer.
[ Abstract ,
PDF ]
F. Laroussinie.
Timed modal logics for the verification of real-time systems.
In
Proceedings of the 4th Workshop on Methods for Modalities (M4M-4), Berlin, Germany, December 2005, Informatik Bericht 194, pages 293-305. Humboldt Universität zu Berlin. Invited paper.
[ Abstract ,
PDF ]
Patricia Bouyer, François Laroussinie, and Pierre-Alain Reynier.
Diagonal constraints in timed automata: Forward analysis of timed
systems.
In Proceedings of the
3rd International Conference on Formal Modelling and Analysis of
Timed Systems (FORMATS'05), Uppsala, Sweden, September-October 2005,
volume 3829 of Lecture Notes in Computer Science, pages 112--126.
Springer, November 2005.
[ Abstract ,
PDF ]
Houda Belmokadem, Béatrice Bérard, Patricia Bouyer, and François Laroussinie.
A new modality for almost everywhere properties in timed automata.
In Proceedings of the 16th International Conference on
Concurrency Theory (CONCUR'05), San Francisco, CA, USA, August 2005,
volume 3653 of Lecture Notes in Computer Science, pages 110--124.
Springer.
[ Abstract ,
PDF ,
PDF (long version) ,
]
Patricia Bouyer, Franck Cassez, and François Laroussinie.
Modal logics for timed control.
In Proceedings of the 16th International Conference on
Concurrency Theory (CONCUR'05), San Francisco, CA, USA, August 2005,
volume 3653 of Lecture Notes in Computer Science, pages 81--94.
Springer.
[ Abstract ,
PDF ,
PDF (long version) ]
François Laroussinie and Jeremy Sproston.
Model checking durational probabilistic systems.
In Proceedings of the 8th
International Conference on Foundations of Software Science and
Computation Structures (FoSSaCS'05), Edinburgh, U.K., April 2005,
volume 3441 of >Lecture Notes in Computer Science, pages 140--154.
Springer.
[ Abstract ,
PDF ]
François Laroussinie, Nicolas Markey, and Philippe Schnoebelen.
Model checking timed automata with one or two clocks.
In Proceedings of the 15th International Conference on
Concurrency Theory (CONCUR'04), London, UK, August 2004, volume 3170
of Lecture Notes in Computer Science, pages 387--401.
Springer.
[ Abstract ,
PDF ]
François Laroussinie, Nicolas Markey, and Philippe Schnoebelen.
Temporal logic with forgettable past.
In Proceedings of the 17th Annual IEEE Symposium on
Logic in Computer Science (LICS'02), Copenhagen, Denmark, July
2002, pages 383--392. IEEE Computer Society
Press.
[ Abstract ,
PDF ]
François Laroussinie, Nicolas Markey, and Philippe Schnoebelen.
On model checking durational Kripke structures (extended abstract).
In Proceedings of
the 5th International Conference on Foundations of Software Science
and Computation Structures (FoSSaCS'02), Grenoble, France, April
2002, volume 2303 of Lecture Notes in Computer Science, pages
264--279. Springer.
[ Abstract ,
PDF ]
Stéphane Demri, François Laroussinie, and Philippe Schnoebelen.
A parametric analysis of the state explosion problem in model
checking (extended abstract).
In Proceedings of
the 19th Annual Symposium on Theoretical Aspects of Computer
Science (STACS'02), Antibes Juan-les-Pins, France, March 2002, volume
2285 of Lecture Notes in Computer Science, pages 620--631.
Springer.
[ Abstract ,
PDF ]
François Laroussinie, Nicolas Markey, and Philippe Schnoebelen.
Model checking CTL+ and FCTL is hard.
In Proceedings of the 4th International
Conference on Foundations of Software Science and Computation
Structures (FoSSaCS'01), Genova, Italy, April 2001, volume 2030 of
Lecture Notes in Computer Science, pages 318--331. Springer.
[ Abstract ,
PDF ]
Franck Cassez and François Laroussinie.
Model-checking for hybrid
systems by quotienting and constraints solving.
In Proceedings of the 12th International
Conference on Computer Aided Verification (CAV 2000), Chicago,
Illinois, USA, July 2000, volume 1855 of Lecture Notes in Computer
Science, pages 373--388. Springer.
[PS ]
François Laroussinie, Philippe Schnoebelen, and Mathieu Turuani.
On the expressivity and complexity of quantitative branching-time
temporal logics.
In Proceedings of the 4th Latin American Symposium on
Theoretical Informatics (LATIN 2000), Punta des Este, Uruguay, April
2000, volume 1776 of Lecture Notes in Computer Science, pages
437--446. Springer.
[PS ]
François Laroussinie and Philippe Schnoebelen.
The state-explosion problem from trace to bisimulation equivalence.
In Proceedings of the 3rd
International Conference on Foundations of Software Science and
Computation Structures (FoSSaCS 2000), Berlin, Germany, March 2000,
volume 1784 of Lecture Notes in Computer Science, pages 192--207.
Springer.
[ Abstract ,
PS ]
Luca Aceto and François Laroussinie.
Is your model checker on time?
In Proceedings of the 24th International Symposium on
Mathematical Fundations of Computer Science (MFCS'99), Szklarska
Poreba, Poland, September 1999, volume 1672 of Lecture Notes in
Computer Science, pages 125--136. Springer.
[PS ]
François Laroussinie and Kim G. Larsen.
CMC: A tool for compositional model-checking of real-time systems.
In Proceedings of IFIP TC6 WG6.1 Joint International
Conference on Formal Description Techniques for Distributed
Systems and Communication Protocols (FORTE'XI) and Protocol
Specification, Testing and Verification (PSTV'XVIII), Paris, France,
November 1998, volume 135 of IFIP Conference Proceedings, pages
439--456. Kluwer Academic Publishers.
[PS ]
Kaare J. Kristoffersen, François Laroussinie, Kim G. Larsen, Paul
Pettersson, and Wang Yi.
A compositional proof of a real-time mutual exclusion protocol.
In Proceedings of
the 7th International Joint Conference CAAP/FASE on Theory and
Practice of Software Development (TAPSOFT'97), Lille, France, April
1997, volume 1214 of Lecture Notes in Computer Science, pages
565--579. Springer.
[PS ]
François Laroussinie and Kim G. Larsen.
Compositional model-checking of real time systems.
In Proceedings of
the 6th International Conference on Concurrency Theory (CONCUR'95),
Philadelphia, Pennsylvania, USA, August 1995, volume 962 of Lecture
Notes in Computer Science, pages 27--41.
Springer.
[PS ]
François Laroussinie, Kim G. Larsen, and Carsten Weise.
From timed automata to logic -- and back.
In Proceedings of the 20th International Symposium on
Mathematical Fundations of Computer Science (MFCS'95), Prague,
Czech Republic, August 1995, volume 969 of Lecture Notes in Computer
Science, pages 529--539. Springer.
[PS ]
François Laroussinie, Sophie Pinchinat, and Philippe Schnoebelen.
Translation results for modal logics of reactive systems.
In Proceedings of the 3rd International Conference on
Algebraic Methodology and Software Technology (AMAST'93), Twente,
The Netherlands, June 1993,
Workshops in Computing, pages 299--310.
Springer-Verlag, 1994.
François Laroussinie and Philippe Schnoebelen.
A hierarchy of temporal logics with past.
In Proceedings of the 11th Annual Symposium on Theoretical
Aspects of Computer Science (STACS'94), Caen, France, February
1994, volume 775 of Lecture Notes in Computer Science, pages
47--58. Springer-Verlag.
[PDF ]
Edited Books
Paul Gastin and François Laroussinie (eds.).
Proceedings of the 21st International Conference on Concurrency Theory (CONCUR'10), August-September 2010,
LNCS 6269. Springer.
Franck Cassez and François Laroussinie (eds.).
Contrôle des applications temps- réel: modèles temporisés et hybrides volume 25(3) of Technique et science informatiques. Hermes, Lavoisier, 2006.
Lectures, Tutorials, Surveys
François Laroussinie. Temporal logics for games. In EATCS Bulletin, Number 100, February
2010 [PDF ]
François Laroussinie.
Notes sur les modèles de jeux, leurs logiques temporelles, et leurs extensions temporisées.
Invited lecture, École d'été ETR 2009 (École
Temps Réel), Paris, France,
September 2009
[PDF ]
François Laroussinie.
Automates temporisés et hybrides: Modélisation et vérification.
Invited lecture, École d'été ETR 2003 (École
Temps Réel), Toulouse, France,
September 2003
[PDF ]
Other...
François Laroussinie.
Model checking temporisé -- algorithmes efficaces et
complexité.
Mémoire d'habilitation, Université Paris 7, Paris, France,
December 2005
[PDF ]
François Laroussinie.
Logique temporelle avec passé pour la spécification et la
vérification des systèmes réactifs.
Thèse de doctorat, Institut National Polytechnique de Grenoble,
France, November 1994.
[ PS ]