Nicolas Markey

@article{acta24(2)-Den,
  author =              {de Nicola, Rocco},
  title =               {Extensional Equivalences for Transitions Systems},
  publisher =           {Springer-Verlag},
  journal =             {Acta Informatica},
  volume =              {24},
  number =              {2},
  pages =               {211-237},
  year =                {1986},
}

@article{pnas36(1)-Nash,
  author =              {Nash, Jr., John F.},
  title =               {Equilibrium Points in {\(n\)}-Person Games},
  publisher =           {National Academy of Sciences of the United States of
                         America},
  journal =             {Proceedings of the National Academy of Sciences},
  volume =              {36},
  number =              {1},
  pages =               {48-49},
  year =                {1950},
  month =               jan,
}

@article{am54(2)-Nash,
  author =              {Nash, Jr., John F.},
  title =               {Non-cooperative Games},
  publisher =           {Princeton University Press},
  journal =             {Annals of Mathematics},
  volume =              {54},
  number =              {2},
  pages =               {286-295},
  year =                {1951},
  month =               sep,
}

@article{tsmcA37(3)-NB,
  author =              {Narasimhan, Sriram and Biswas, Gautam},
  title =               {Model-Based Diagnosis of Hybrid Systems},
  publisher =           {IEEE},
  journal =             {IEEE Transactions on Systems, Man, and
                         Cybernetics~-- Part~A: Systems and Humans},
  volume =              {37},
  number =              {3},
  pages =               {348-361},
  year =                {2007},
  month =               may,
  doi =                 {10.1109/TSMCA.2007.893487},
}

@article{tcs34()-DH,
  author =              {de Nicola, Rocco and Hennessy, Matthew C. B.},
  title =               {Testing Equivalence for Processes},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {34},
  pages =               {83-133},
  year =                {1984},
}

@phdthesis{phd-nickovic,
  author =              {Nickovic, Dejan},
  title =               {Checking Timed and Hybrid Properties: Theory and
                         Applications},
  year =                {2008},
  month =               oct,
  school =              {Lab. VERIMAG, Grenoble, France},
}

@article{jalc24(2-4)-Nic,
  author =              {Nicaud, Cyril},
  title =               {The {{\v{C}}}ern{\'y} conjecture holds with high
                         probability},
  journal =             {Journal of Automata, Languages and Combinatorics},
  volume =              {24},
  number =              {2-4},
  pages =               {343-365},
  year =                {2019},
  doi =                 {10.25596/jalc-2019-343},
}

@incollection{lncs2500-niessner,
  author =              {Nie{\ss}ner, Frank},
  title =               {Non-deterministic tree automata},
  editor =              {Gr{\"a}del, Erich and Thomas, Wolfgang and Wilke,
                         Thomas},
  booktitle =           {Automata, Logics, and Infinite Games},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2500},
  pages =               {227-232},
  year =                {2002},
}

@article{cc4()-Nis,
  author =              {Nisan, Noam},
  title =               {\(RL \subseteq SC\)},
  publisher =           {Birkh{\"a}user},
  journal =             {Computational Complexity},
  volume =              {4},
  pages =               {1-11},
  year =                {1994},
}

@article{tcs189(1-2)-Niw,
  author =              {Niwi{\'n}ski, Damian},
  title =               {Fixed point characterization of infinite behavior of
                         finite-state systems},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {189},
  number =              {1-2},
  pages =               {1-69},
  year =                {1997},
  month =               dec,
  doi =                 {10.1016/S0304-3975(97)00039-X},
}

@inproceedings{csl2002-Niw,
  author =              {Niwi{\'n}ski, Damian},
  title =               {{\(\mu\)}-calculus via Games},
  booktitle =           {{P}roceedings of the 16th {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'02)},
  acronym =             {{CSL}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2471},
  pages =               {27-43},
  year =                {2002},
  month =               sep,
}

@patent{EP3907615B1,
  author =              {Noguchi, Reiya and J{\'e}ron, Thierry and Markey,
                         Nicolas and Sankur, Ocan},
  title =               {Method and system for testing the operation of a
                         target computer system by using timed requirements},
  number =              {EP 3 907 615 B1},
  year =                {2022},
  month =               nov,
}

@patent{EP4064057B1,
  author =              {Noguchi, Reiya and J{\'e}ron, Thierry and Markey,
                         Nicolas and Sankur, Ocan},
  title =               {Method and system for correcting the operation of a
                         target computer system by using timed requirements},
  number =              {EP 4 064 057 B1},
  year =                {2023},
  month =               jul,
}

@article{IEICEtransinfE93D(5)-NOK,
  author =              {Nagaoka, Takeshi and Okano, Kozo and Kusumoto,
                         Shinji},
  title =               {An abstraction refinement technique for timed
                         automata based on counterexample-guided abstraction
                         refinement loop},
  publisher =           {Institute of Electronics, Information and
                         Communication Engineers},
  journal =             {IEICE Transactions on Information and Systems},
  volume =              {5},
  number =              {5},
  pages =               {994-1005},
  year =                {2010},
  month =               may,
  doi =                 {10.1587/transinf.E93.D.994},
}

@inproceedings{hscc1992-NOSY,
  author =              {Nicollin, Xavier and Olivero, Alfredo and Sifakis,
                         Joseph and Yovine, Sergio},
  title =               {An Approach to the Description and Analysis of
                         Hybrid Systems},
  editor =              {Grossman, Robert L. and Nerode, Anil and Ravn,
                         Anders P. and Rischel, Hans},
  booktitle =           {{H}ybrid {S}ystems ({HSCC}'92)},
  acronym =             {{HSCC}'92},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {736},
  pages =               {149-178},
  year =                {1993},
}

@book{agt2007-NRTV,
  title =               {Algorithmic Game Theory},
  editor =              {Nisan, Noam and Roughgarden, Tim and Tardos, {\'E}va
                         and Vazirani, Vijay V.},
  booktitle =           {Algorithmic Game Theory},
  publisher =           {Cambridge University Press},
  year =                {2007},
}

@article{sttt5(1)-NS,
  author =              {Nielsen, Brian and Skou, Arne},
  title =               {Automated test generation from timed automata},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {5},
  number =              {1},
  pages =               {59-77},
  year =                {2003},
  month =               nov,
  doi =                 {10.1007/s10009-002-0094-1},
}

Résumé

We consider the problem of repairing inconsistent real-time requirements with respect to two consistency notions: non-vacuity, which means that each requirement can be realized without violating other ones, and rt-consistency, which means that inevitable violations are detected immediately. We provide an iterative algorithm, based on solving SMT queries, to replace designated parameters of real-time requirements with new Boolean expressions and time constraints, so that the resulting set of requirements becomes consistent.

@inproceedings{atva2022-NSJMM,
  author =              {Noguchi, Reiya and Sankur, Ocan and J{\'e}ron,
                         Thierry and Markey, Nicolas and Mentr{\'e}, David},
  title =               {Repairing Real-Time Requirements},
  editor =              {Bouajjani, Ahmed and Hol{\'\i}k, Luk{\'a}{\v s} and
                         Wu, Zhilin},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {S}ymposium on {A}utomated {T}echnology for
                         {V}erification and {A}nalysis ({ATVA}'22)},
  acronym =             {{ATVA}'22},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {13505},
  pages =               {371-387},
  year =                {2022},
  month =               oct,
  doi =                 {10.1007/978-3-031-19992-9_24},
  abstract =            {We~consider the problem of repairing inconsistent
                         real-time requirements with respect to two
                         consistency notions: non-vacuity, which means that
                         each requirement can be realized without violating
                         other ones, and rt-consistency, which means that
                         inevitable violations are detected immediately.
                         We~provide an iterative algorithm, based on solving
                         SMT queries, to replace designated parameters of
                         real-time requirements with new Boolean expressions
                         and time constraints, so that the resulting set of
                         requirements becomes consistent.},
}

@inproceedings{fm2012-NSLDL,
  author =              {Nguyen, Truong Khanh and Sun, Jun and Liu, Yang and
                         Dong, Jin Song and Liu, Yan},
  title =               {Improved {BDD}-Based Discrete Analysis of Timed
                         Systems},
  editor =              {Giannakopoulou, Dimitra and M{\'e}ry, Dominique},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {S}ymposium on {F}ormal {M}ethods ({FM}'12)},
  acronym =             {{FM}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7436},
  pages =               {326-340},
  year =                {2012},
  month =               aug,
  doi =                 {10.1007/978-3-642-32759-9_28},
}

@inproceedings{stoc1995-NT,
  author =              {Nisan, Noam and Ta-Shma, Amnon},
  title =               {Symmetric {LOGSPACE} is Closed Under Complement},
  booktitle =           {{P}roceedings of the 27th {A}nnual {ACM} {S}ymposium
                         on the {T}heory of {C}omputing ({STOC}'95)},
  acronym =             {{STOC}'95},
  publisher =           {ACM Press},
  pages =               {140-146},
  year =                {1995},
  month =               may,
}

@article{ja42(1)-NU,
  author =              {Nyk{\"a}nen, Matti and Ukkonen, Esko},
  title =               {The Exact Path Length Problem},
  publisher =           {Elsevier},
  journal =             {Journal of Algorithms},
  volume =              {42},
  number =              {1},
  pages =               {41-53},
  year =                {2002},
  month =               jan,
  doi =                 {10.1006/jagm.2001.1201},
}

@inproceedings{litp1990-DV,
  author =              {de Nicola, Rocco and Vaandrager, Frits},
  title =               {Action versus state based logics for transition
                         systems},
  editor =              {Guessarian, Ir{\`e}ne},
  booktitle =           {Semantics of Systems of Concurrent Processes},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {469},
  pages =               {407-419},
  year =                {1990},
  month =               apr,
  doi =                 {10.1007/3-540-53479-2_17},
}

@inproceedings{lcs1989-NYY,
  author =              {Nerode, Anil and Yakhnis, Alexander and Yakhnis,
                         Vladimir},
  title =               {Concurrent programs as strategies in games},
  editor =              {Moschovakis, Yiannis N.},
  booktitle =           {{L}ogic from {C}omputer {S}cience},
  publisher =           {Springer-Verlag},
  series =              {Mathematical Sciences Research Institute
                         Publications},
  volume =              {21},
  pages =               {405-479},
  year =                {1992},
  confyear =            {1989},
  confmonth =           {11},
}