Books |
|
• |
B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci and Ph. Schnoebelen. Systems and Software Verification. Model-Checking Techniques and
Tools. Springer, 2001. ( Web page | BibTeX )
|
|
• |
Ph. Schnoebelen, B. Bérard, M. Bidoit, F. Laroussinie and A. Petit. Vérification de logiciels : techniques et outils du
model-checking. Vuibert, 1999. ( Web page | BibTeX )
|
Chapters in Books |
|
• |
P. Bouyer and F. Laroussinie. Model Checking Timed Automata. In Modeling and Verification of Real-Time Systems, pages 111-140. ISTE Ltd. - John Wiley & Sons, Ltd., 2008. ( PDF | BibTeX )
|
|
• |
P. Bouyer and F. Laroussinie. Vérification par automates temporisés. In Systèmes temps-réel 1 : techniques de description et de
vérification, pages 121-150. Hermès, 2006. ( Web page | PDF | PS | PS.GZ | BibTeX )
|
Edited Books |
|
• |
F. Cassez and F. Laroussinie (eds.). Contrôle des applications temps-réel : modèles
temporisés et hybrides. Technique et Science Informatiques 25(3), 2006. ( Web page | BibTeX )
|
Journals |
|
• |
M. Jurdzinski, F. Laroussinie and J. Sproston. Model Checking Probabilistic Timed Automata with One or Two Clocks. Logical Methods in Computer Science 4(3:12), 2008. ( BibTeX + Abstract )
|
|
• |
F. Laroussinie, N. Markey and G. Oreiby. On the Expressiveness and Complexity of ATL. Logical Methods in Computer Science 4(2:7), 2008. ( PDF | BibTeX + Abstract )
|
|
• |
F. Laroussinie and J. Sproston. State Explosion in Almost-Sure Probabilistic Reachability. Information Processing Letters 102(6), pages 236-241, 2007. ( PDF | BibTeX + Abstract )
|
|
• |
S. Demri, F. Laroussinie and Ph. Schnoebelen. A Parametric Analysis of the State Explosion Problem in Model
Checking. Journal of Computer and System Sciences 72(4), pages 547-575, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract )
|
|
• |
F. Laroussinie, N. Markey and Ph. Schnoebelen. Efficient Timed Model Checking for Discrete-Time Systems. Theoretical Computer Science 353(1-3), pages 249-271, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract )
|
|
• |
F. Laroussinie, Ph. Schnoebelen and M. Turuani. On the Expressivity and Complexity of Quantitative Branching-Time
Temporal Logics. Theoretical Computer Science 297(1-3), pages 297-315, 2003. ( PS | PS.GZ | BibTeX + Abstract )
|
|
• |
L. Aceto and F. 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, pages 7-51, 2002. ( PS | PS.GZ | BibTeX )
|
|
• |
F. Laroussinie and Ph. Schnoebelen. Specification in CTL+Past for verification in CTL. Information and Computation 156(1-2), pages 236-263, 2000. ( PS | PS.GZ | BibTeX )
|
|
• |
F. Laroussinie and Ph. Schnoebelen. A Hierarchy of Temporal Logics with Past. Theoretical Computer Science 148(2), pages 303-324, 1995. ( PS | PS.GZ | BibTeX )
|
|
• |
F. Laroussinie. About the Expressive Power of CTL Combinators. Information Processing Letters 54(6), pages 343-345, 1995. ( PS | PS.GZ | BibTeX )
|
|
• |
F. Laroussinie, S. Pinchinat and Ph. Schnoebelen. Translations between Modal Logics of Reactive Systems. Theoretical Computer Science 140(1), pages 53-71, 1995. ( PS | PS.GZ | BibTeX )
|
Conferences |
|
• |
Th. Brihaye, A. Da Costa, F. Laroussinie and N. Markey. ATL with Strategy Contexts and Bounded Memory. In LFCS'09, LNCS 5407, pages 92-106. Springer, 2009. ( PDF | PDF (long version) | BibTeX + Abstract )
|
|
• |
Th. Brihaye, F. Laroussinie, N. Markey and G. Oreiby. Timed Concurrent Game Structures. In CONCUR'07, LNCS 4703, pages 445-459. Springer, 2007. ( PDF | PS | PS.GZ | BibTeX + Abstract )
|
|
• |
M. Jurdzinski, F. Laroussinie and J. Sproston. Model Checking Probabilistic Timed Automata with One or Two Clocks. In TACAS'07, LNCS 4424, pages 170-184. Springer, 2007. ( PDF | BibTeX + Abstract )
|
|
• |
F. Laroussinie, N. Markey and G. Oreiby. On the Expressiveness and Complexity of ATL. In FoSSaCS'07, LNCS 4423, pages 243-257. Springer, 2007. ( PDF | PS | PS.GZ | BibTeX + Abstract )
|
|
• |
H. Bel mokadem, B. Bérard, P. Bouyer and F. Laroussinie. Timed temporal logics for abstracting transient states. In ATVA'06, LNCS 4218, pages 337-351. Springer, 2006. ( PDF | BibTeX + Abstract )
|
|
• |
F. Laroussinie, N. Markey and G. Oreiby. Model Checking Timed ATL for Durational Concurrent Game Structures. In FORMATS'06, LNCS 4202, pages 245-259. Springer, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract )
|
|
• |
F. Laroussinie. Timed modal logics for the verification of real-time systems. In M4M-4, Informatik Bericht 194, pages 293-305. Humboldt Universität zu Berlin, 2005. Invited paper. ( PDF | PS | PS.GZ | BibTeX + Abstract )
|
|
• |
P. Bouyer, F. Laroussinie and P.-A. Reynier. Diagonal Constraints in Timed Automata: Forward Analysis of Timed
Systems. In FORMATS'05, LNCS 3829, pages 112-126. Springer, 2005. ( PDF | PS | PS.GZ | PDF (long version) | PS (long version) | PS.GZ (long version) | BibTeX + Abstract )
|
|
• |
H. Bel mokadem, B. Bérard, P. Bouyer and F. Laroussinie. A New Modality for Almost Everywhere Properties in Timed Automata. In CONCUR'05, LNCS 3653, pages 110-124. Springer, 2005. ( PDF | PS | PS.GZ | PDF (long version) | PS (long version) | PS.GZ (long version) | BibTeX + Abstract )
|
|
• |
P. Bouyer, F. Cassez and F. Laroussinie. Modal Logics for Timed Control. In CONCUR'05, LNCS 3653, pages 81-94. Springer, 2005. ( PDF | PS | PS.GZ | PDF (long version) | PS (long version) | PS.GZ (long version) | BibTeX + Abstract )
|
|
• |
F. Laroussinie and J. Sproston. Model Checking Durational Probabilistic Systems. In FoSSaCS'05, LNCS 3441, pages 140-154. Springer, 2005. ( PDF | PS | PS.GZ | BibTeX + Abstract )
|
|
• |
F. Laroussinie, N. Markey and Ph. Schnoebelen. Model Checking Timed Automata with One or Two Clocks. In CONCUR'04, LNCS 3170, pages 387-401. Springer, 2004. ( PDF | PS | PS.GZ | BibTeX + Abstract )
|
|
• |
F. Laroussinie, N. Markey and Ph. Schnoebelen. Temporal Logic with Forgettable Past. In LICS'02, pages 383-392. IEEE Computer Society Press, 2002. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract )
|
|
• |
F. Laroussinie, N. Markey and Ph. Schnoebelen. On Model Checking Durational Kripke Structures (Extended Abstract). In FoSSaCS'02, LNCS 2303, pages 264-279. Springer, 2002. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract )
|
|
• |
S. Demri, F. Laroussinie and Ph. Schnoebelen. A Parametric Analysis of the State Explosion Problem in Model Checking
(Extended Abstract). In STACS'02, LNCS 2285, pages 620-631. Springer, 2002. ( PDF | PS | PS.GZ | BibTeX + Abstract )
|
|
• |
F. Laroussinie, N. Markey and Ph. Schnoebelen. Model checking CTL+ and FCTL is hard. In FoSSaCS'01, LNCS 2030, pages 318-331. Springer, 2001. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract )
|
|
• |
F. Cassez and F. Laroussinie. Model-Checking for Hybrid Systems by Quotienting and Constraints
Solving. In CAV 2000, LNCS 1855, pages 373-388. Springer, 2000. ( PS | PS.GZ | BibTeX )
|
|
• |
F. Laroussinie and Ph. Schnoebelen. The State-Explosion Problem from Trace to Bisimulation Equivalence. In FoSSaCS 2000, LNCS 1784, pages 192-207. Springer, 2000. ( PS | PS.GZ | BibTeX )
|
|
• |
L. Aceto and F. Laroussinie. Is your Model Checker on Time? In MFCS'99, LNCS 1672, pages 125-136. Springer, 1999. ( PS | PS.GZ | BibTeX )
|
|
• |
F. Laroussinie and K. G. Larsen. CMC: A Tool for Compositional Model-Checking of Real-Time Systems. In FORTE'XI/PSTV'XVIII, IFIP Conference Proceedings 135, pages 439-456. Kluwer Academic Publishers, 1998. ( PS | PS.GZ | BibTeX )
|
|
• |
K. J. Kristoffersen, F. Laroussinie, K. G. Larsen, P. Pettersson and W. Yi. A Compositional Proof of a Real-Time Mutual Exclusion Protocol. In TAPSOFT'97, LNCS 1214, pages 565-579. Springer, 1997. ( PS | PS.GZ | BibTeX )
|
|
• |
F. Laroussinie and K. G. Larsen. Compositional Model-Checking of Real Time Systems. In CONCUR'95, LNCS 962, pages 27-41. Springer, 1995. ( PS | PS.GZ | BibTeX )
|
|
• |
F. Laroussinie, K. G. Larsen and C. Weise. From Timed Automata to Logic - and Back. In MFCS'95, LNCS 969, pages 529-539. Springer, 1995. ( PS | PS.GZ | BibTeX )
|
|
• |
F. Laroussinie, S. Pinchinat and Ph. Schnoebelen. Translation Results for Modal Logics of Reactive Systems. In AMAST'93, Workshops in Computing, pages 299-310. Springer-Verlag, 1994. ( BibTeX )
|
|
• |
F. Laroussinie and Ph. Schnoebelen. A Hierarchy of Temporal Logics with Past. In STACS'94, LNCS 775, pages 47-58. Springer-Verlag, 1994. ( BibTeX )
|
Theses |
|
• |
F. Laroussinie. Model checking temporisé - Algorithmes efficaces et
complexité. Mémoire d'habilitation, Université Paris 7, Paris, France, December 2005. ( PDF | BibTeX )
|
|
• |
F. 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. ( BibTeX )
|
Other Publications |
|
• |
F. Laroussinie and N. Markey. Expressiveness of Temporal Logics, Introductory course, 18th European Summer School in Logic,
Language and Information (ESSLLI'06), Málaga, Spain, 2006. ( PDF | Slides | BibTeX )
|
|
• |
S. Pinchinat, F. Laroussinie and Ph. Schnoebelen. Logical Characterizations of Truly Concurrent Bisimulation. Technical Report 114, Laboratoire d'Informatique Fondamentale et d'Intelligence
Artificielle, Grenoble, France, March 1994. ( PS | PS.GZ | BibTeX )
|