Selected publications by Nicolas Markey
2012
- 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.
- 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.
2011
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- Mar11a
-
Nicolas Markey. Robustness in Real-time Systems. In SIES'11, pages 28-34. IEEE Computer Society Press, 2011.
- Mar11b
-
Nicolas Markey. Verification of Embedded Systems - Algorithms and Complexity. Mémoire d'habilitation, École Normale Supérieure de Cachan, France, April 2011.
2010
- Mar10
-
Nicolas Markey. Timed and Hybrid Automata. Course notes, Master Parisien de Recherche en Informatique,
Paris, France. 2010.
- 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.
- HBM+10
-
Paul Hunter, Patricia Bouyer, Nicolas Markey, Joël Ouaknine and James Worrell. Computing rational radical sums in uniform TC0. In Kamal Lodaya and Meena Mahajan (eds.), FSTTCS'10, Leibniz International Proceedings in Informatics 8, pages 308-316. Leibniz-Zentrum für Informatik, 2010.
- 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.
- 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.
- 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.
- 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.
- 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.
- BCM10
-
Patricia Bouyer, Fabrice Chevalier and Nicolas Markey. On the Expressiveness of TPTL and MTL. Information and Computation 208(2), pages 97-116, 2010.
2009
- 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.
- 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.
- 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.
2008
- Mar08a
-
Nicolas Markey. Weighted automata: Model checking and games. Course notes, Master Parisien de Recherche en Informatique,
Paris, France. 2008.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
2007
- 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.
- 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.
- CM07
-
Franck Cassez and Nicolas Markey. Contrôle et implémentation des systèmes temporisés. In ETR'07, pages 111-123. 2007.
- 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.
- 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.
- 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.
2006
- Mar06
-
Nicolas Markey. Temporal logics. Course notes, Master Parisien de Recherche en Informatique,
Paris, France. 2006.
- 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.
- 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.
- 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.
- 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.
- BBM06
-
Patricia Bouyer, Thomas Brihaye and Nicolas Markey. Improved Undecidability Results on Weighted Timed Automata. Information Processing Letters 98(5), pages 188-194, 2006.
- 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.
- 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.
- MS06
-
Nicolas Markey and Philippe Schnoebelen. Mu-Calculus Path Checking. Information Processing Letters 97(6), pages 225-230, 2006.
2005
- 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.
- 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.
2004
- 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.
- 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.
- 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.
- 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.
- 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.
- Mar04a
-
Nicolas Markey. TSMV: model-checking symbolique de systèmes simplement
temporisés. In Jacques Julliand (ed.), AFADL'04, pages 349-352. 2004.
- 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.
- 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.
- MS04c
-
Nicolas Markey and Philippe Schnoebelen. A PTIME-Complete Matching Problem for SLP-Compressed Words. Information Processing Letters 90(1), pages 3-6, 2004.
2003
- 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.
- 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.
- Mar03b
-
Nicolas Markey. Temporal Logic with Past is Exponentially More Succinct. EATCS Bulletin 79, pages 122-128, 2003.
2002
- 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.
- 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.
- 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.
2001
- 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.
2000
- Mar00
-
Nicolas Markey. Complexité de la logique temporelle avec passé. Rapport de DEA, DEA Algorithmique, Paris, France, June 2000.