Selected publications by Nicolas Markey

BBMU12

Patricia Bouyer, Romain Brenguier, Nicolas Markey and Michael Ummels. Concurrent games with ordered objectives. In Lars Birkedal (ed.), FoSSaCS'12, Lecture Notes in Computer Science 7213, pages 301-315. Springer, 2012. To appear.

PDF | PDF (long version) | BibTeX + Abstract

DLM12

Arnaud Da Costa, François Laroussinie and Nicolas Markey. Quantified CTL: expressiveness and model checking. Research Report LSV-12-02, Laboratoire Spécification et Vérification, ENS Cachan, France, January 2012. 16 pages.

PDF | BibTeX + Abstract

BBMU11

Patricia Bouyer, Romain Brenguier, Nicolas Markey and Michael Ummels. Nash Equilibria in Concurrent Games with Büchi Objectives. In Supratik Chakraborty and Amit Kumar (eds.), FSTTCS'11, Leibniz International Proceedings in Informatics, pages 375-386. Leibniz-Zentrum für Informatik, 2011.

PDF | BibTeX + Abstract

doi: 10.4230/LIPIcs.FSTTCS.2011.375

SBM11

Ocan Sankur, Patricia Bouyer and Nicolas Markey. Shrinking Timed Automata. In Supratik Chakraborty and Amit Kumar (eds.), FSTTCS'11, Leibniz International Proceedings in Informatics, pages 90-102. Leibniz-Zentrum für Informatik, 2011.

PDF | BibTeX + Abstract

doi: 10.4230/LIPIcs.FSTTCS.2011.90

BMOU11

Patricia Bouyer, Nicolas Markey, Jörg Olschewski and Michael Ummels. Measuring Permissiveness in Parity Games: Mean-Payoff Parity Games Revisited. In Tevfik Bultan and Pao-Ann Hsiung (eds.), ATVA'11, Lecture Notes in Computer Science 6996, pages 135-149. Springer, 2011.

PDF | PDF (long version) | BibTeX + Abstract

doi: 10.1007/978-3-642-24372-1_11

BFLM11

Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen and Nicolas Markey. Quantitative analysis of real-time systems using priced timed automata. Communications of the ACM 54(9), pages 78-87, 2011.

PDF | BibTeX + Abstract

doi: 10.1145/1995376.1995396

BLM⁺11

Patricia Bouyer, Kim G. Larsen, Nicolas Markey, Ocan Sankur and Claus Thrane. Timed automata can always be made implementable. In Joost-Pieter Katoen and Barbara König (eds.), CONCUR'11, Lecture Notes in Computer Science 6901, pages 76-91. Springer, 2011.

PDF | BibTeX + Abstract

doi: 10.1007/978-3-642-23217-6_6

BMS11

Patricia Bouyer, Nicolas Markey and Ocan Sankur. Robust Model-Checking of Timed Automata via Pumping in Channel Machines. In Uli Fahrenberg and Stavros Tripakis (eds.), FORMATS'11, Lecture Notes in Computer Science 6919, pages 97-112. Springer, 2011.

PDF | PDF (long version) | BibTeX + Abstract

doi: 10.1007/978-3-642-24310-3_8

Mar11a

Nicolas Markey. Robustness in Real-time Systems. In SIES'11, pages 28-34. IEEE Computer Society Press, 2011.

PDF | Slides | BibTeX + Abstract

doi: 10.1109/SIES.2011.5953652

Mar11b

Nicolas Markey. Verification of Embedded Systems - Algorithms and Complexity. Mémoire d'habilitation, École Normale Supérieure de Cachan, France, April 2011.

PDF | Slides | BibTeX

Mar10

Nicolas Markey. Timed and Hybrid Automata. Course notes, Master Parisien de Recherche en Informatique, Paris, France. 2010.

PDF | BibTeX

DLM10

Arnaud Da Costa, François Laroussinie and Nicolas Markey. ATL with strategy contexts: Expressiveness and Model Checking. In Kamal Lodaya and Meena Mahajan (eds.), FSTTCS'10, Leibniz International Proceedings in Informatics 8, pages 120-132. Leibniz-Zentrum für Informatik, 2010.

PDF | PDF (long version) | BibTeX + Abstract

doi: 10.4230/LIPIcs.FSTTCS.2010.120

HBM⁺10

Paul Hunter, Patricia Bouyer, Nicolas Markey, Joël Ouaknine and James Worrell. Computing rational radical sums in uniform TC⁰. In Kamal Lodaya and Meena Mahajan (eds.), FSTTCS'10, Leibniz International Proceedings in Informatics 8, pages 308-316. Leibniz-Zentrum für Informatik, 2010.

PDF | BibTeX + Abstract

doi: 10.4230/LIPIcs.FSTTCS.2010.308

BBM10a

Patricia Bouyer, Romain Brenguier and Nicolas Markey. Computing Equilibria in Two-Player Timed Games via Turn-Based Finite Games. In Krishnendu Chatterjee and Thomas A. Henziner (eds.), FORMATS'10, Lecture Notes in Computer Science 6246, pages 62-76. Springer, 2010.

PDF | PDF (long version) | BibTeX + Abstract

doi: 10.1007/978-3-642-15297-9_7

MW10

Nicolas Markey and Jef Wijsen (eds.). Proceedings of the 17th International Symposium on Temporal Representation and Reasoning (TIME'10), Paris, France, September 2010. IEEE Computer Society Press.

Web page | BibTeX

BBM10b

Patricia Bouyer, Romain Brenguier and Nicolas Markey. Nash Equilibria for Reachability Objectives in Multi-player Timed Games. In Paul Gastin and François Laroussinie (eds.), CONCUR'10, Lecture Notes in Computer Science 6269, pages 192-206. Springer, 2010.

PDF | PDF (long version) | BibTeX + Abstract

doi: 10.1007/978-3-642-15375-4_14

BJL⁺10

Thomas Brihaye, Marc Jungers, Samson Lasaulce, Nicolas Markey and Ghassan Oreiby. Using Model Checking for Analyzing Distributed Power Control Problems. EURASIP Journal on Wireless Communications and Networking 2010(861472), 2010.

PDF | BibTeX + Abstract

doi: 10.1155/2010/861472

BFLM10

Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen and Nicolas Markey. Timed Automata with Observers under Energy Constraints. In Karl Henrik Johansson and Wang Yi (eds.), HSCC'10, pages 61-70. ACM Press, 2010.

PDF | PDF (long version) | BibTeX + Abstract

doi: 10.1145/1755952.1755963

BCM10

Patricia Bouyer, Fabrice Chevalier and Nicolas Markey. On the Expressiveness of TPTL and MTL. Information and Computation 208(2), pages 97-116, 2010.

PDF | BibTeX + Abstract

doi: 10.1016/j.ic.2009.10.004

CM09

Franck Cassez and Nicolas Markey. Control of Timed Systems. In Claude Jard and Olivier H. Roux (eds.), Communicating Embedded Systems - Software and Design, chapter 3, pages 83-120. Wiley-ISTE, 2009.

Web page | BibTeX

BDMR09

Patricia Bouyer, Marie Duflot, Nicolas Markey and Gabriel Renault. Measuring Permissivity in Finite Games. In Mario Bravetti and Gianluigi Zavattaro (eds.), CONCUR'09, Lecture Notes in Computer Science 5710, pages 196-210. Springer, 2009.

PDF | PDF (long version) | BibTeX + Abstract

doi: 10.1007/978-3-642-04081-8_14

BDLM09

Thomas Brihaye, Arnaud Da Costa, François Laroussinie and Nicolas Markey. ATL with Strategy Contexts and Bounded Memory. In Sergei N. Artemov and Anil Nerode (eds.), LFCS'09, Lecture Notes in Computer Science 5407, pages 92-106. Springer, 2009.

PDF | PDF (long version) | BibTeX + Abstract

doi: 10.1007/978-3-540-92687-0_7

Mar08a

Nicolas Markey. Weighted automata: Model checking and games. Course notes, Master Parisien de Recherche en Informatique, Paris, France. 2008.

PDF | BibTeX

DDMR08

Martin De Wulf, Laurent Doyen, Nicolas Markey and Jean-François Raskin. Robust Safety of Timed Automata. Formal Methods in System Design 33(1-3), pages 45-84, 2008.

PDF | BibTeX + Abstract

doi: 10.1007/s10703-008-0056-7

CM08

Franck Cassez and Nicolas Markey. Contrôle des systèmes temporisés. In Olivier H. Roux and Claude Jard (eds.), Approches formelles des systèmes embarqués communicants, chapter 4, pages 105-144. Hermès, 2008.

Web page | BibTeX

BBBM08

Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye and Nicolas Markey. Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics. In QEST'08, pages 55-64. IEEE Computer Society Press, 2008.

PDF | BibTeX + Abstract

doi: 10.1109/QEST.2008.19

BFL⁺08

Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey and Jiří Srba. Infinite Runs in Weighted Timed Automata with Energy Constraints. In Franck Cassez and Claude Jard (eds.), FORMATS'08, Lecture Notes in Computer Science 5215, pages 33-47. Springer, 2008.

PDF | PDF (long version) | BibTeX + Abstract

doi: 10.1007/978-3-540-85778-5_4

BMOW08

Patricia Bouyer, Nicolas Markey, Joël Ouaknine and James Worrell. On Expressiveness and Complexity in Real-time Model Checking. In Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir and Igor Walukiewicz (eds.), ICALP'08, Lecture Notes in Computer Science 5126, pages 124-135. Springer, 2008.

PDF | BibTeX + Abstract

doi: 10.1007/978-3-540-70583-3_11

BLM08

Patricia Bouyer, Kim G. Larsen and Nicolas Markey. Model Checking One-clock Priced Timed Automata. Logical Methods in Computer Science 4(2:9), 2008.

PDF | BibTeX + Abstract

doi: 10.2168/LMCS-4(2:9)2008

BGMR08

Thomas Brihaye, Mohamed Ghannem, Nicolas Markey and Lionel Rieg. Good friends are hard to find! In TIME'08, pages 32-40. IEEE Computer Society Press, 2008.

PDF | BibTeX + Abstract

doi: 10.1109/TIME.2008.10

Mar08b

Nicolas Markey. Timed Systems - Model Checking and Games, Invited tutorial, 8th School on Modelling and Verifying Parallel Processes (MOVEP'08), Nouan-le-Fuzelier, France, 2008.

Web page | Slides | BibTeX

LMO08

François Laroussinie, Nicolas Markey and Ghassan Oreiby. On the Expressiveness and Complexity of ATL. Logical Methods in Computer Science 4(2:7), 2008.

PDF | BibTeX + Abstract

doi: 10.2168/LMCS-4(2:7)2008

BMR08

Patricia Bouyer, Nicolas Markey and Pierre-Alain Reynier. Robust Analysis of Timed Automata via Channel Machines. In Roberto Amadio (ed.), FoSSaCS'08, Lecture Notes in Computer Science 4962, pages 157-171. Springer, 2008.

PDF | PS | PS.GZ | PDF (long version) | BibTeX + Abstract

doi: 10.1007/978-3-540-78499-9_12

BMO⁺08

Patricia Bouyer, Nicolas Markey, Joël Ouaknine, Philippe Schnoebelen and James Worrell. On Termination for Faulty Channel Machines. In Susanne Albers and Pascal Weil (eds.), STACS'08, Leibniz International Proceedings in Informatics 1, pages 121-132. Leibniz-Zentrum für Informatik, 2008.

PDF | PS | PS.GZ | BibTeX + Abstract

BM07

Patricia Bouyer and Nicolas Markey. Costs are Expensive! In Jean-François Raskin and P. S. Thiagarajan (eds.), FORMATS'07, Lecture Notes in Computer Science 4763, pages 53-68. Springer, 2007.

PDF | PS | PS.GZ | Slides | BibTeX + Abstract

doi: 10.1007/978-3-540-75454-1_6

BLMO07

Thomas Brihaye, François Laroussinie, Nicolas Markey and Ghassan Oreiby. Timed Concurrent Game Structures. In Luís Caires and Vasco T. Vasconcelos (eds.), CONCUR'07, Lecture Notes in Computer Science 4703, pages 445-459. Springer, 2007.

PDF | PS | PS.GZ | BibTeX + Abstract

doi: 10.1007/978-3-540-74407-8_30

CM07

Franck Cassez and Nicolas Markey. Contrôle et implémentation des systèmes temporisés. In ETR'07, pages 111-123. 2007.

PDF | Slides | BibTeX

BMOW07

Patricia Bouyer, Nicolas Markey, Joël Ouaknine and James Worrell. The Cost of Punctuality. In LICS'07, pages 109-118. IEEE Computer Society Press, 2007.

PDF | PS | PS.GZ | PDF (long version) | BibTeX + Abstract

doi: 10.1109/LICS.2007.49

BLM07

Patricia Bouyer, Kim G. Larsen and Nicolas Markey. Model-Checking One-Clock Priced Timed Automata. In Helmut Seidl (ed.), FoSSaCS'07, Lecture Notes in Computer Science 4423, pages 108-122. Springer, 2007.

PDF | PS | PS.GZ | BibTeX + Abstract

doi: 10.1007/978-3-540-71389-0_9

LMO07

François Laroussinie, Nicolas Markey and Ghassan Oreiby. On the Expressiveness and Complexity of ATL. In Helmut Seidl (ed.), FoSSaCS'07, Lecture Notes in Computer Science 4423, pages 243-257. Springer, 2007.

PDF | PS | PS.GZ | Slides | BibTeX + Abstract

doi: 10.1007/978-3-540-71389-0_18

Mar06

Nicolas Markey. Temporal logics. Course notes, Master Parisien de Recherche en Informatique, Paris, France. 2006.

PDF | BibTeX

BLMR06

Patricia Bouyer, Kim G. Larsen, Nicolas Markey and Jacob Illum Rasmussen. Almost Optimal Strategies in One-Clock Priced Timed Automata. In Naveen Garg and S. Arun-Kumar (eds.), FSTTCS'06, Lecture Notes in Computer Science 4337, pages 345-356. Springer, 2006.

doi: 10.1007/11944836_32

LMO06

François Laroussinie, Nicolas Markey and Ghassan Oreiby. Model Checking Timed ATL for Durational Concurrent Game Structures. In Eugène Asarin and Patricia Bouyer (eds.), FORMATS'06, Lecture Notes in Computer Science 4202, pages 245-259. Springer, 2006.

PDF | PS | PS.GZ | BibTeX + Abstract

doi: 10.1007/11867340_18

MR06

Nicolas Markey and Jean-François Raskin. Model Checking Restricted Sets of Timed Paths. Theoretical Computer Science 358(2-3), pages 273-292, 2006.

PDF | PS | PS.GZ | BibTeX + Abstract

doi: 10.1016/j.tcs.2006.01.019

LM06

François Laroussinie and Nicolas 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

BBM06

Patricia Bouyer, Thomas Brihaye and Nicolas Markey. Improved Undecidability Results on Weighted Timed Automata. Information Processing Letters 98(5), pages 188-194, 2006.

PDF | PS | PS.GZ | BibTeX + Abstract

doi: 10.1016/j.ipl.2006.01.012

BMR06

Patricia Bouyer, Nicolas Markey and Pierre-Alain Reynier. Robust Model-Checking of Linear-Time Properties in Timed Automata. In Jose R. Correa, Alejandro Hevia and Marcos Kiwi (eds.), LATIN'06, Lecture Notes in Computer Science 3887, pages 238-249. Springer, 2006.

doi: 10.1007/11682462_25

LMS06

François Laroussinie, Nicolas Markey and Philippe 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

doi: 10.1016/j.tcs.2005.11.020

MS06

Nicolas Markey and Philippe Schnoebelen. Mu-Calculus Path Checking. Information Processing Letters 97(6), pages 225-230, 2006.

PDF | PS | PS.GZ | BibTeX + Abstract

doi: 10.1016/j.ipl.2005.11.010

BCM05

Patricia Bouyer, Fabrice Chevalier and Nicolas Markey. On the Expressiveness of TPTL and MTL. In R. Ramanujam and Sandeep Sen (eds.), FSTTCS'05, Lecture Notes in Computer Science 3821, pages 432-443. Springer, 2005.

doi: 10.1007/11590156_35

AMRT05

Karine Altisen, Nicolas Markey, Pierre-Alain Reynier and Stavros Tripakis. Implémentabilité des automates temporisés. In Hassane Alla and Éric Rutten (eds.), MSR'05, pages 395-406. Hermès, 2005. Invited paper.

PDF | PS | PS.GZ | BibTeX + Abstract

DDMR04

Martin De Wulf, Laurent Doyen, Nicolas Markey and Jean-François Raskin. Robustness and Implementability of Timed Automata. In Yassine Lakhnech and Sergio Yovine (eds.), FORMATS'04/FTRTFT'04, Lecture Notes in Computer Science 3253, pages 118-133. Springer, 2004.

PDF | PS | PS.GZ | Slides | BibTeX + Abstract

MS04a

Nicolas Markey and Philippe Schnoebelen. Symbolic Model Checking for Simply-Timed Systems. In Yassine Lakhnech and Sergio Yovine (eds.), FORMATS'04/FTRTFT'04, Lecture Notes in Computer Science 3253, pages 102-117. Springer, 2004.

PDF | PS | PS.GZ | Slides | BibTeX + Abstract

MS04b

Nicolas Markey and Philippe Schnoebelen. TSMV: A Symbolic Model Checker for Quantitative Analysis of Systems. In QEST'04, pages 330-331. IEEE Computer Society Press, 2004.

PDF | PS | PS.GZ | Slides | BibTeX + Abstract

doi: 10.1109/QEST.2004.10028

LMS04

François Laroussinie, Nicolas Markey and Philippe Schnoebelen. Model Checking Timed Automata with One or Two Clocks. In Philippa Gardner and Nobuko Yoshida (eds.), CONCUR'04, Lecture Notes in Computer Science 3170, pages 387-401. Springer, 2004.

PDF | PS | PS.GZ | BibTeX + Abstract

doi: 10.1007/978-3-540-28644-8_25

MR04

Nicolas Markey and Jean-François Raskin. Model Checking Restricted Sets of Timed Paths. In Philippa Gardner and Nobuko Yoshida (eds.), CONCUR'04, Lecture Notes in Computer Science 3170, pages 432-447. Springer, 2004.

PDF | PS | PS.GZ | Slides | BibTeX + Abstract

doi: 10.1007/978-3-540-28644-8_28

Mar04a

Nicolas Markey. TSMV: model-checking symbolique de systèmes simplement temporisés. In Jacques Julliand (ed.), AFADL'04, pages 349-352. 2004.

PDF | PS | PS.GZ | BibTeX

Mar04b

Nicolas Markey. Past is for Free: On the Complexity of Verifying Linear Temporal Properties with Past. Acta Informatica 40(6-7), pages 431-458, 2004.

PDF | PS | PS.GZ | BibTeX + Abstract

doi: 10.1007/s00236-003-0136-5

DCMM04

Jennifer M. Davoren, Vaughan Coulthard, Nicolas Markey and Thomas Moor. Non-deterministic Temporal Logics for General Flow Systems. In Rajeev Alur and George J. Pappas (eds.), HSCC'04, Lecture Notes in Computer Science 2993, pages 280-295. Springer, 2004.

PDF | PS | PS.GZ | BibTeX + Abstract

MS04c

Nicolas Markey and Philippe Schnoebelen. A PTIME-Complete Matching Problem for SLP-Compressed Words. Information Processing Letters 90(1), pages 3-6, 2004.

PDF | PS | PS.GZ | BibTeX + Abstract

doi: 10.1016/j.ipl.2004.01.002

MS03

Nicolas Markey and Philippe Schnoebelen. Model Checking a Path (Preliminary Report). In Roberto M. Amadio and Denis Lugiez (eds.), CONCUR'03, Lecture Notes in Computer Science 2761, pages 251-265. Springer, 2003.

PDF | PS | PS.GZ | Slides | BibTeX + Abstract

doi: 10.1007/b11938

Mar03a

Nicolas Markey. Logiques temporelles pour la vérification: expressivité, complexité, algorithmes. Thèse de doctorat, Laboratoire d'Informatique Fondamentale d'Orléans, France, April 2003.

PDF | PS | PS.GZ | Slides | BibTeX

Mar03b

Nicolas Markey. Temporal Logic with Past is Exponentially More Succinct. EATCS Bulletin 79, pages 122-128, 2003.

PDF | PS | PS.GZ | BibTeX + Abstract

Mar02

Nicolas Markey. Past is for Free: On the Complexity of Verifying Linear Temporal Properties with Past. In Uwe Nestmann and Prakash Panagaden (eds.), EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 87-104. Elsevier Science Publishers, 2002.

PDF | PS | PS.GZ | Slides | BibTeX + Abstract

doi: 10.1016/S1571-0661(05)80366-4

LMS02a

François Laroussinie, Nicolas Markey and Philippe Schnoebelen. Temporal Logic with Forgettable Past. In LICS'02, pages 383-392. IEEE Computer Society Press, 2002.

PDF | PS | PS.GZ | Slides | BibTeX + Abstract

doi: 10.1109/LICS.2002.1029846

LMS02b

François Laroussinie, Nicolas Markey and Philippe Schnoebelen. On Model Checking Durational Kripke Structures (Extended Abstract). In Mogens Nielsen and Uffe Engberg (eds.), FoSSaCS'02, Lecture Notes in Computer Science 2303, pages 264-279. Springer, 2002.

PDF | PS | PS.GZ | Slides | BibTeX + Abstract

LMS01

François Laroussinie, Nicolas Markey and Philippe Schnoebelen. Model checking CTL⁺ and FCTL is hard. In Furio Honsell and Marino Miculan (eds.), FoSSaCS'01, Lecture Notes in Computer Science 2030, pages 318-331. Springer, 2001.

PDF | PS | PS.GZ | Slides | BibTeX + Abstract

Mar00

Nicolas Markey. Complexité de la logique temporelle avec passé. Rapport de DEA, DEA Algorithmique, Paris, France, June 2000.

BibTeX

Selected publications by Nicolas Markey

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

2000

About LSV

Search this list

List of coauthors