Nicolas Markey

@phdthesis{phd-jaziri,
  author =              {Jaziri, Samy},
  title =               {Automata on timed structures},
  year =                {2019},
  month =               sep,
  school =              {{\'E}cole Normale Sup{\'e}rieure de Cachan, France},
}

@article{sttt19(3)-JBBEHKPRRSSTW,
  author =              {Jacobs, Swen and Bloem, Roderick and Brenguier,
                         Romain and Ehlers, R{\"u}diger and Hell, Timotheus
                         and K{\"o}nighofer, Robert and P{\'e}rez, Guillermo
                         A. and Raskin, Jean-Fran{\c c}ois and Ryzhyk, Leonid
                         and Sankur, Ocan and Seidl, Martin and Tentrup,
                         Leander and Walker, Adam},
  title =               {The first reactive synthesis competition
                         ({SYNTCOMP}~2014)},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {19},
  number =              {3},
  pages =               {367-390},
  year =                {2017},
  month =               jun,
  doi =                 {10.1007/s10009-016-0416-3},
}

@article{jlap78(5)-JBCS,
  author =              {Jaghoori, Mohammad Mahdi and de~Boer, Frank S. and
                         Chothia, Tom and Sirjani, Marjan},
  title =               {Schedulability of asynchronous real-time concurrent
                         objects},
  publisher =           {Elsevier},
  journal =             {Journal of Logic and Algebraic Programming},
  volume =              {78},
  number =              {5},
  pages =               {402-416},
  year =                {2009},
  month =               may,
}

@inproceedings{ceemas2005-JD,
  author =              {Jamroga, Wojciech and Dix, J{\"u}rgen},
  title =               {Do Agents Make Model Checking Explode
                         (Computationally)?},
  editor =              {P{\v e}chouc{\v e}k, Michal and Petta, Paolo and
                         Varga, L{\'a}szl{\'o} Zsolt},
  booktitle =           {{P}roceedings of the 4th {I}nternational {C}entral
                         and {E}astern {E}uropean {C}onference on
                         {M}ulti-{A}gent {S}ystems ({CEEMAS}'05)},
  acronym =             {{CEEMAS}'05},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Artificial Intelligence},
  volume =              {23690},
  pages =               {398-407},
  year =                {2005},
  month =               sep,
}

@techreport{IfI-06-02-JD,
  author =              {Jamroga, Wojciech and Dix, J{\"u}rgen},
  title =               {Model Checking Abilities of Agents: A Closer Look},
  number =              {IfI-06-02},
  year =                {2006},
  institution =         {Institut f{\'u}r Informatik, Technische
                         Universit{\"a}t Clausthal, Germany},
  type =                {Technical Report},
}

@article{tocsys42(3)-JD,
  author =              {Jamroga, Wojciech and Dix, J{\"u}rgen},
  title =               {Model Checking Abilities of Agents: A Closer Look},
  publisher =           {Springer-Verlag},
  journal =             {Theory of Computing Systems},
  volume =              {42},
  number =              {3},
  pages =               {366-410},
  year =                {2008},
  month =               apr,
  doi =                 {10.1007/s00224-007-9080-z},
}

@techreport{AR-VerTeCs-2003,
  author =              {J{\'e}ron, Thierry},
  title =               {Project-Team {VerTeCs}},
  year =                {2003},
  institution =         {IRISA, Rennes, France},
  type =                {Annual Reviews Inc.},
}

@phdthesis{hab-jeron,
  author =              {J{\'e}ron, Thierry},
  title =               {Contribution {\`a} la g{\'e}n{\'e}ration automatique
                         de tests pour les syst{\`e}mes r{\'e}actifs},
  year =                {2004},
  month =               feb,
  school =              {Universit{\'e} Rennes~1, France},
  type =                {M\'emoire d'habilitation},
}

@inproceedings{lira1997-JGB,
  author =              {Jani{\v c}i{\'c}, Predrag and Green, Ian and Bundy,
                         Alan},
  title =               {A Comparison of Decision Procedures in {P}resburger
                         Arithmetic},
  editor =              {To{\v s}i{\'c}, Ratko and Budimac, Zoran},
  booktitle =           {{P}roceedings of the 8th {I}nternational
                         {C}onference on {L}ogic and {C}omputer {S}cience
                         ({LIRA}'97)},
  acronym =             {{LIRA}'97},
  pages =               {91-101},
  year =                {1997},
  month =               sep,
}

@article{fundi63(2-3)-JH,
  author =              {Jamroga, Wojciech and van der Hoek, Wiebe},
  title =               {Agents that Know How to Play},
  publisher =           {IOS Press},
  journal =             {Fundamenta Informaticae},
  volume =              {63},
  number =              {2-3},
  pages =               {185-219},
  year =                {2004},
}

@inproceedings{epia2005-JHW,
  author =              {Jamroga, Wojciech and van der Hoek, Wiebe and
                         Wooldridge, Michael},
  title =               {Intentions and Strategies in Game-Like Scenarios},
  editor =              {Bento, Carlos and Cardoso, Am{\'\i}lcar and Dias,
                         Ga{\"e}l},
  booktitle =           {{P}roceedings of the 12th {P}ortuguese {C}onference
                         on {A}rtificial {I}ntelligence ({EPIA}'05)},
  acronym =             {{EPIA}'05},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Artificial Intelligence},
  volume =              {3808},
  pages =               {512-523},
  year =                {2005},
  month =               dec,
}

@inproceedings{aamas2016-JKP,
  author =              {Jamroga, Wojciech and Konikowska, Beata and Penczek,
                         Wojciech},
  title =               {Multi-Valued Verification of Strategic Ability},
  editor =              {Jonker, Catholijn M. and Marsella, Stacy and
                         Thangarajah, John and Tuyls, Karl},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {A}utonomous {A}gents and
                         {M}ultiagent {S}ystems ({AAMAS}'16)},
  acronym =             {{AAMAS}'16},
  publisher =           {International Foundation for Autonomous Agents and
                         Multiagent Systems},
  pages =               {1180-1189},
  year =                {2016},
  month =               may,
}

@inproceedings{icalp2003-JL,
  author =              {Johannsen, Jan and Lange, Martin},
  title =               {{CTL{\(^+\)}} is Complete for Double Exponential
                         Time},
  editor =              {Baeten, Jos C. M. and Lenstra, Jan Karel and Parrow,
                         Joachim and Woeginger, Gerhard J.},
  booktitle =           {{P}roceedings of the 30th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'03)},
  acronym =             {{ICALP}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2719},
  pages =               {767-775},
  year =                {2003},
  month =               jun,
}

@article{fundi61(3-4)-JL,
  author =              {Janin, David and Lenzi, Giacommo},
  title =               {On the Relationship Between Monadic and Weak Monadic
                         Second Order Logic on Arbitrary Trees},
  publisher =           {IOS Press},
  journal =             {Fundamenta Informaticae},
  volume =              {61},
  number =              {3-4},
  pages =               {247-265},
  year =                {2004},
}

@techreport{diro1-59-JLM,
  author =              {Jenner, Birgit and Lange, Klaus-J{\"o}rn and
                         McKenzie, Pierre},
  title =               {Tree Isomorphism and Some Other Complete Problems
                         for Deterministic Logspace},
  number =              {1059},
  year =                {1997},
  month =               mar,
  institution =         {DIRO, Universit{\'e} de Montr{\'e}al, Canada},
  type =                {Technical Report},
}

@inproceedings{tpfm2013-JLR,
  author =              {Juhl, Line and Larsen, Kim Guldstrand and Raskin,
                         Jean-Fran{\c c}ois},
  title =               {Optimal Bounds for Multiweighted and Parametrised
                         Energy Games},
  editor =              {Liu, Zhiming and Woodcock, Jim and Zhu, Yunshan},
  booktitle =           {Theories of Programming and Formal Methods~-- Essays
                         Dedicated to Jifeng He on the Occasion of His 70th
                         Birthday},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8051},
  pages =               {244-255},
  year =                {2013},
  doi =                 {10.1007/978-3-642-39698-4_15},
}

@article{tse41(5)-JLR,
  author =              {Jovanovi{\'c}, Aleksandra and Lime, Didier and Roux,
                         Olivier H.},
  title =               {Integer Parameter Synthesis for Timed Automata},
  publisher =           {IEEE Comp. Soc. Press},
  journal =             {IEEE Transactions on Software Engineering},
  volume =              {41},
  number =              {5},
  pages =               {445-461},
  year =                {2015},
  month =               may,
  doi =                 {10.1109/TSE.2014.2357445},
}

@inproceedings{tacas2007-JLS,
  author =              {Jurdzi{\'n}ski, Marcin and Laroussinie, Fran{\c
                         c}ois and Sproston, Jeremy},
  title =               {Model Checking Probabilistic Timed Automata with One
                         or Two Clocks},
  editor =              {Grumberg, Orna and Huth, Michael},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'07)},
  acronym =             {{TACAS}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4424},
  pages =               {170-184},
  year =                {2007},
  month =               mar,
  doi =                 {10.1007/978-3-540-71209-1_15},
}

@inproceedings{ssv2012-JLS,
  author =              {J{\o}rgensen, Kenneth Yrke and Larsen, Kim
                         Guldstrand and Srba, Ji{\v r}{\'\i}},
  title =               {Time-Darts: A~Data Structure for Verification of
                         Closed Timed Automata},
  booktitle =           {{P}roceedings of the 7th {C}onference on {S}ystems
                         {S}oftware {V}erification ({SSV}'12)},
  acronym =             {{SSV}'12},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {102},
  pages =               {141-155},
  year =                {2012},
  month =               nov,
  doi =                 {10.4204/EPTCS.102.13},
}

@inproceedings{icalp2015-JLS,
  author =              {Jurdzi{\'n}ski, Marcin and Lazi{\'c}, Ranko and
                         Schmitz, Sylvain},
  title =               {Fixed-Dimensional Energy Games are in
                         Pseudo-Polynomial Time},
  editor =              {Halld{\'o}rsson, Magn{\'u}s M. and Iwana, Kazuo and
                         Kobayashi, Naoki and Speckmann, Bettina},
  booktitle =           {{P}roceedings of the 42nd {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'15)~-- Part~{II}},
  acronym =             {{ICALP}'15},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9135},
  pages =               {260-272},
  year =                {2015},
  month =               jul,
  doi =                 {10.1007/978-3-662-47666-6_21},
}

@inproceedings{spin2013-JLSO,
  author =              {Jensen, Jonas Finnemann and Larsen, Kim Guldstrand
                         and Srba, Ji{\v r}{\'\i} and {\O}stergaard, Lars
                         K{\ae}rlund},
  title =               {Local Model Checking of Weighted {CTL} with
                         Upper-Bound Constraints},
  editor =              {Bartocci, Ezio and Ramakrishnan, C. R.},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {S}ymposium on {M}odel-{C}herking {S}oftware
                         ({SPIN}'13)},
  acronym =             {{SPIN}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7976},
  pages =               {178-195},
  year =                {2013},
  month =               jul,
  doi =                 {10.1007/978-3-642-39176-7_12},
}

@inproceedings{nasaFM2014-JLSST,
  author =              {Jensen, Peter Gj{\o}l and Larsen, Kim Guldstrand and
                         Srba, Ji{\v r}{\'\i} and S{\o}rensen, Mathias Grund
                         and Taankvist, Jakob Haar},
  title =               {Memory Efficient Data Structures for Explicit
                         Verification of Timed Systems},
  editor =              {Badger, Julia M. and Rozier, Kristin Yvonne},
  booktitle =           {{P}roceedings of the 6th {NASA} {F}ormal {M}ethods
                         {S}ymposium ({NFM}'14)},
  acronym =             {{NFM}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8430},
  pages =               {307-312},
  year =                {2014},
  month =               apr,
  doi =                 {10.1007/978-3-319-06200-6_26},
}

Résumé

Requirements engineering is a key phase in the development process. Ensuring that requirements are consistent is essential so that they do not conflict and admit implementations. We consider the formal verification of rt-consistency, which imposes that the inevitability of definitive errors of a requirement should be anticipated, and that of partial consistency, which was recently introduced as a more effective check. We generalize and formalize both notions for discrete-time timed automata, develop three incremental algorithms, and present experimental results.

@inproceedings{formats2020-JMMNS,
  author =              {J{\'e}ron, Thierry and Markey, Nicolas and
                         Mentr{\'e}, David and Noguchi, Reiya and Sankur,
                         Ocan},
  title =               {Incremental methods for checking real-time
                         consistency},
  editor =              {Bertrand, Nathalie and Jansen, Nils},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'20)},
  acronym =             {{FORMATS}'20},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {12288},
  pages =               {249-264},
  year =                {2020},
  month =               sep,
  doi =                 {10.1007/978-3-030-57628-8_15},
  abstract =            {Requirements engineering is a key phase in the
                         development process. Ensuring that requirements are
                         consistent is essential so that they do not conflict
                         and admit implementations. We~consider the formal
                         verification of rt-consistency, which imposes that
                         the inevitability of definitive errors of a
                         requirement should be anticipated, and that of
                         partial consistency, which was recently introduced
                         as a more effective check. We~generalize and
                         formalize both notions for discrete-time timed
                         automata, develop three incremental algorithms, and
                         present experimental results.},
}

@inproceedings{icfem2007-JMO,
  author =              {Julliand, Jacques and Mountassir, Hassan and Oudot,
                         {\'E}milie},
  title =               {{V}e{STA}: A~Tool to Verify the Correct Integration
                         of a Component in a Composite Timed System},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {F}ormal {E}ngineering {M}ethods
                         ({ICFEM}'07)},
  acronym =             {{ICFEM}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4789},
  pages =               {116-135},
  year =                {2007},
  month =               nov,
  doi =                 {10.1007/978-3-540-76650-6_8},
}

@inproceedings{cdc2003-JMRT,
  author =              {J{\'e}ron, Thierry and Marchand, Herv{\'e} and Rusu,
                         Vlad and Tschaen, Val{\'e}ry},
  title =               {Ensuring the Conformance of Reactive Discrete-Event
                         Systems using Supervisory Control},
  booktitle =           {{P}roceedings of the 42nd {IEEE} {C}onference on
                         {D}ecision and {C}ontrol ({CDC}'03)},
  acronym =             {{CDC}'03},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {2692- 2697},
  year =                {2003},
  month =               dec,
}

@article{ja4(4)-joh,
  author =              {Johnson, David S.},
  title =               {The{NP}-Completeness Column: An Ongoing Guide},
  publisher =           {Elsevier},
  journal =             {Journal of Algorithms},
  volume =              {4},
  number =              {4},
  pages =               {397-411},
  year =                {1983},
  month =               dec,
}

@incollection{HTCSa1990-Joh,
  author =              {Johnson, David S.},
  title =               {A Catalog of Complexity Classes},
  editor =              {van Leeuwen, Jan},
  booktitle =           {Handbook of Theoretical Computer Science},
  publisher =           {Elsevier},
  volume =              {A},
  pages =               {67-161},
  chapter =             {2},
  year =                {1990},
}

@inproceedings{stacs2004-Joh,
  author =              {Johannsen, Jan},
  title =               {Satisfiability Problems Complete for Deterministic
                         Logarithmic Space},
  editor =              {Diekert, Volker and Habib, Michel},
  booktitle =           {{P}roceedings of the 21st {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'04)},
  acronym =             {{STACS}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2996},
  pages =               {317-325},
  year =                {2003},
  month =               mar,
}

@inproceedings{fossacs2011-JR,
  author =              {Jaubert, R{\'e}mi and Reynier, Pierre-Alain},
  title =               {Quantitative Robustness Analysis of Flat Timed
                         Automata},
  editor =              {Hofmann, Martin},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'11)},
  acronym =             {{FoSSaCS}'11},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6604},
  pages =               {229-244},
  year =                {2011},
  month =               mar,
}

@inproceedings{formats2007-JRLD,
  author =              {Jensen, Jan J. and Rasmussen, Jacob Illum and
                         Larsen, Kim Guldstrand and David, Alexandre},
  title =               {Guided Controller Synthesis for Climate Controller
                         Using {UPPAAL} {T}iga},
  editor =              {Raskin, Jean-Fran{\c c}ois and Thiagarajan, P. S.},
  booktitle =           {{P}roceedings of the 5th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'07)},
  acronym =             {{FORMATS}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4763},
  pages =               {227-240},
  year =                {2007},
  month =               oct,
}

@article{ipl104(5)-JS,
  author =              {Jan{\v c}ar, Petr and Sawa, Zden{\v{e}}k},
  title =               {A note on Emptiness for Alternating Finite Automata
                         with a One-letter Alphabet},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {104},
  number =              {5},
  pages =               {164-167},
  year =                {2007},
  month =               nov,
}

@incollection{ctr2-JT,
  author =              {Jenner, Birgit and Tor{\'a}n, Jacobo},
  title =               {The Complexity of Obtaining Solutions for Problems
                         in {NP} and {NL}},
  editor =              {Hemaspaandra, Lane A. and Selman, Alan L.},
  booktitle =           {Complexity Theory Retrospective~II},
  publisher =           {Springer-Verlag},
  pages =               {155-178},
  year =                {1998},
}

@article{ipl68(3)-Jur,
  author =              {Jurdzi{\'n}ski, Marcin},
  title =               {Deciding the Winner in Parity Games is in
                         {UP}{\(\cap\)}co-{UP}},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {68},
  number =              {3},
  pages =               {119-124},
  year =                {1998},
  month =               nov,
}

@inproceedings{stacs2000-Jur,
  author =              {Jurdzi{\'n}ski, Marcin},
  title =               {Small Progress Measures for Solving Parity Games},
  editor =              {Reichel, Horst and Tison, Sophie},
  booktitle =           {{P}roceedings of the 17th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'00)},
  acronym =             {{STACS}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1770},
  pages =               {290-301},
  year =                {2000},
  month =               mar,
}

@inproceedings{mfcs1995-JW,
  author =              {Janin, David and Walukiewicz, Igor},
  title =               {Automata for the Modal {\(\mu\)}-Calculus and
                         Related Results},
  editor =              {Wiedermann, Jir{\'\i} and H{\'a}jek, Petr},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {S}ymposium on {M}athematical {F}oundations of
                         {C}omputer {S}cience ({MFCS}'95)},
  acronym =             {{MFCS}'95},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {969},
  pages =               {552-562},
  year =                {1995},
  month =               aug,
}

@inproceedings{concur1996-JW,
  author =              {Janin, David and Walukiewicz, Igor},
  title =               {On the Expressive Completeness of the Propositional
                         Mu-Calculus With Respect to Monadic Second Order
                         Logic},
  editor =              {Montanari, Ugo and Sassone, Vladimiro},
  booktitle =           {{P}roceedings of the 7th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'96)},
  acronym =             {{CONCUR}'96},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1119},
  pages =               {263-277},
  year =                {1996},
  month =               aug,
}

@inproceedings{cdc2018-JW,
  author =              {Jacquot, Paulin and Wan, Cheng},
  title =               {Routing game on parallel networks: the~convergence
                         of atomic to nonatomic},
  booktitle =           {{P}roceedings of the 57th {IEEE} {C}onference on
                         {D}ecision and {C}ontrol ({CDC}'18)},
  acronym =             {{CDC}'18},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {6951-6956},
  year =                {2018},
  month =               dec,
  doi =                 {10.1109/CDC.2018.8619369},
}