M
[Mad80] Roger Maddux. The equational theory of CA3 is undecidable. Journal of Symbolic Logic 45(2):311-316. Association for Symbolic Logic, juin 1980.
@article{jsl45(2)-Mad,
  author =              {Maddux, Roger},
  title =               {The equational theory of \(CA_{3}\) is undecidable},
  publisher =           {Association for Symbolic Logic},
  journal =             {Journal of Symbolic Logic},
  volume =              {45},
  number =              {2},
  pages =               {311-316},
  year =                {1980},
  month =               jun,
  doi =                 {10.2307/2273191},
}
[Mad11] Parthasarathy Madhusudan. Synthesizing Reactive Programs. In CSL'11, Leibniz International Proceedings in Informatics 12, pages 428-442. Leibniz-Zentrum für Informatik, septembre 2011.
@inproceedings{csl2011-Mad,
  author =              {Madhusudan, Parthasarathy},
  title =               {Synthesizing Reactive Programs},
  editor =              {Bezem, Marc},
  booktitle =           {{P}roceedings of the 25th {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'11)},
  acronym =             {{CSL}'11},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {12},
  pages =               {428-442},
  year =                {2011},
  month =               sep,
}
[Mai78] David Maier. The Complexity of Some Problems on Subsequences and Supersequences. Journal of the ACM 25(2):322-336. ACM Press, avril 1978.
@article{jacm25(2)-Mai,
  author =              {Maier, David},
  title =               {The Complexity of Some Problems on Subsequences and
                         Supersequences},
  publisher =           {ACM Press},
  journal =             {Journal of the ACM},
  volume =              {25},
  number =              {2},
  pages =               {322-336},
  year =                {1978},
  month =               apr,
}
[Mai00] Monika Maidl. The Common Fragment of CTL and LTL. In FOCS'00, pages 643-652. IEEE Comp. Soc. Press, novembre 2000.
@inproceedings{focs2000-Mai,
  author =              {Maidl, Monika},
  title =               {The Common Fragment of {CTL} and~{LTL}},
  booktitle =           {{P}roceedings of the 41st {A}nnual {S}ymposium on
                         {F}oundations of {C}omputer {S}cience ({FOCS}'00)},
  acronym =             {{FOCS}'00},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {643-652},
  year =                {2000},
  month =               nov,
}
[Mal00] Oded Maler. Systèmes discrets, temporisés et hybrides. Mémoire d'habilitation, Université Joseph Fourier, Grenoble, France, Mai 2000.
@phdthesis{hab-maler,
  author =              {Maler, Oded},
  title =               {Syst{\`e}mes discrets, temporis{\'e}s et hybrides},
  year =                {2000},
  month =               may,
  institution =         {Universit{\'e} Joseph Fourier, Grenoble, France},
  school =              {Universit{\'e} Joseph Fourier, Grenoble, France},
  type =                {M\'emoire d'habilitation},
}
[Mal02] Oded Maler. Control from Computer Science. Annual Reviews in Control 26(2):175-187. Elsevier, 2002.
@article{aric26(2)-Mal,
  author =              {Maler, Oded},
  title =               {Control from Computer Science},
  publisher =           {Elsevier},
  journal =             {Annual Reviews in Control},
  volume =              {26},
  number =              {2},
  pages =               {175-187},
  year =                {2002},
}
[Man00] Panagiotis Manolios. Mu-Calculus Model-Checking. In Matt Kaufmann, Panagiotis Manolios et J. Strother Moore (eds.), Computer Aided Reasoning: ACL2 Case Studies. Kluwer Academic, juin 2000.
@incollection{CAR-ACL2CS-Man,
  author =              {Manolios, Panagiotis},
  title =               {Mu-Calculus Model-Checking},
  editor =              {Kaufmann, Matt and Manolios, Panagiotis and Moore,
                         J. Strother},
  booktitle =           {Computer Aided Reasoning: {ACL2} Case Studies},
  publisher =           {Kluwer Academic},
  pages =               {93-111},
  year =                {2000},
  month =               jun,
}
[Mar75] Donald A. Martin. Borel Determinacy. Annals of Mathematics 102(2):363-371. Princeton University, septembre 1975.
@article{am102(2)-Mar,
  author =              {Martin, Donald A.},
  title =               {{B}orel Determinacy},
  publisher =           {Princeton University},
  journal =             {Annals of Mathematics},
  volume =              {102},
  number =              {2},
  pages =               {363-371},
  year =                {1975},
  month =               sep,
}
[Mar00] Nicolas Markey. Complexité de la logique temporelle avec passé. Rapport de DEA, Lab. Spécification & Vérification, ENS Cachan, France, Juin 2000.
@mastersthesis{dea2000-Mar,
  author =              {Markey, Nicolas},
  title =               {Complexit{\'e} de la logique temporelle avec
                         pass{\'e}},
  year =                {2000},
  month =               jun,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {Rapport de~{DEA}},
}
[Mar02] Nicolas Markey. Past is for Free: On the Complexity of Verifying Linear Temporal Properties with Past. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 89-106. Elsevier, août 2002.
Résumé

We study the complexity of satisfiability and model-checking of the linear-time temporal logic with past (PLTL). More precisely, we consider several fragments of PLTL, depending on the allowed set of temporal modalities, the use of negations or the nesting of future formulae into past formulae. Our results show that "past is for free", that is it does not bring additional theoretical complexity, even for small fragments, and even when nesting future formulae into past formulae. We also remark that existential and universal model-checking can have different complexity for certain fragments.

@inproceedings{express2002-Mar,
  author =              {Markey, Nicolas},
  title =               {Past is for Free: On the Complexity of Verifying
                         Linear Temporal Properties with Past},
  editor =              {Nestmann, Uwe and Panangaden, Prakash},
  booktitle =           {{P}roceedings of the 9th {I}nternational {W}orkshop
                         on {E}xpressiveness in {C}oncurrency ({EXPRESS}'02)},
  acronym =             {{EXPRESS}'02},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {68},
  number =              {2},
  pages =               {89-106},
  year =                {2002},
  month =               aug,
  doi =                 {10.1016/S1571-0661(05)80366-4},
  abstract =            {We study the complexity of satisfiability and
                         model-checking of the linear-time temporal logic
                         with past~(PLTL). More precisely, we consider
                         several fragments of PLTL, depending on the allowed
                         set of temporal modalities, the use of negations or
                         the nesting of future formulae into past formulae.
                         Our~results show that {"}past is for free{"}, that
                         is it does not bring additional theoretical
                         complexity, even for small fragments, and even when
                         nesting future formulae into past formulae. We~also
                         remark that existential and universal model-checking
                         can have different complexity for certain
                         fragments.},
}
[Mar03] Nicolas Markey. Temporal Logic with Past is Exponentially More Succinct. EATCS Bulletin 79:122-128. EATCS, février 2003.
Résumé

We positively answer the old question whether temporal logic with past is more succinct than pure-future temporal logic. Surprisingly, the proof is quite simple and elementary, although the question has been open for twenty years.

@article{eatcs-bull79()-Mar,
  author =              {Markey, Nicolas},
  title =               {Temporal Logic with Past is Exponentially More
                         Succinct},
  publisher =           {EATCS},
  journal =             {EATCS Bulletin},
  volume =              {79},
  pages =               {122-128},
  year =                {2003},
  month =               feb,
  abstract =            {We positively answer the old question whether
                         temporal logic with past is more succinct than
                         pure-future temporal logic. Surprisingly, the proof
                         is quite simple and elementary, although the
                         question has been open for twenty years.},
}
[Mar03] Nicolas Markey. Logiques temporelles pour la vérification : expressivité, complexité, algorithmes. Thèse de doctorat, Lab. Informatique Fondamentale d'Orléans, France, Avril 2003.
@phdthesis{phd2003-Mar,
  author =              {Markey, Nicolas},
  title =               {Logiques temporelles pour la v{\'e}rification~:
                         expressivit{\'e}, complexit{\'e}, algorithmes},
  year =                {2003},
  month =               apr,
  school =              {Lab.~Informatique Fondamentale d'Orl{\'e}ans,
                         France},
  type =                {Th\`ese de doctorat},
}
[Mar04] Nicolas Markey. TSMV : model-checking symbolique de systémes simplement temporisés. In AFADL'04. Juin 2004.
@inproceedings{afadl2004-Mar,
  author =              {Markey, Nicolas},
  title =               {{TSMV}~: model-checking symbolique de syst{\'e}mes
                         simplement temporis{\'e}s},
  editor =              {Julliand, Jacques},
  booktitle =           {Actes de la 6\`eme Conf\'erence {A}pproches
                         {F}ormelles dans l'{A}ssistance au
                         {D}{\'e}veloppement de {L}ogiciels ({AFADL}'04)},
  acronym =             {{AFADL}'04},
  year =                {2004},
  month =               jun,
}
[Mar04] Nicolas Markey. Past is for Free: On the Complexity of Verifying Linear Temporal Properties with Past. Acta Informatica 40(6-7):431-458. Springer-Verlag, mai 2004.
Résumé

We study the complexity of satisfiability and model checking problems for fragments of linear-time temporal logic with past (PLTL). We consider many fragments of PLTL, obtained by restricting the set of allowed temporal modalities, the use of negations or the nesting of future formulas into past formulas. Our results strengthen the widely accepted fact that "past is for free", in the sense that allowing symmetric past-time modalities does not bring additional theoretical complexity. This result holds even for small fragments and even when nesting future formulas into past formulas.

@article{acta40(6-7)-Mar,
  author =              {Markey, Nicolas},
  title =               {Past is for Free: On the Complexity of Verifying
                         Linear Temporal Properties with Past},
  publisher =           {Springer-Verlag},
  journal =             {Acta Informatica},
  volume =              {40},
  number =              {6-7},
  pages =               {431-458},
  year =                {2004},
  month =               may,
  doi =                 {10.1007/s00236-003-0136-5},
  abstract =            {We study the complexity of satisfiability and model
                         checking problems for fragments of linear-time
                         temporal logic with past (PLTL). We consider many
                         fragments of PLTL, obtained by restricting the set
                         of allowed temporal modalities, the use of negations
                         or the nesting of future formulas into past
                         formulas. Our results strengthen the widely accepted
                         fact that {"}past is for free{"}, in the sense that
                         allowing symmetric past-time modalities does not
                         bring additional theoretical complexity. This result
                         holds even for small fragments and even when nesting
                         future formulas into past formulas.},
}
[Mar05] Wilfredo R. Marrero. Using BDDs to Decide CTL. In TACAS'05, Lecture Notes in Computer Science 3440, pages 222-236. Springer-Verlag, avril 2005.
@inproceedings{tacas2005-Mar,
  author =              {Marrero, Wilfredo R.},
  title =               {Using {BDD}s to Decide~{CTL}},
  editor =              {Halbwachs, Nicolas and Zuck, Lenore D.},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'05)},
  acronym =             {{TACAS}'05},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3440},
  pages =               {222-236},
  year =                {2005},
  month =               apr,
}
[Mar10] Manuel Biscaia Martins. Supervisory Control of Petri Nets using Linear Temporal Logic. Thèse de doctorat, Instituto Superior Técnico, Universidade Técnica de Lisboa, Portugal, Janvier 2010.
@phdthesis{phd-mbmartins,
  author =              {Martins, Manuel Biscaia},
  title =               {Supervisory Control of {P}etri Nets using Linear
                         Temporal Logic},
  year =                {2010},
  month =               jan,
  school =              {Instituto Superior T\'ecnico, Universidade T\'ecnica
                         de Lisboa, Portugal},
  type =                {Th\`ese de doctorat},
}
[Mar11] Nicolas Markey. Robustness in Real-time Systems. In SIES'11, pages 28-34. IEEE Comp. Soc. Press, juin 2011.
Résumé

We review several aspects of robustness of real-time systems, and present recent results on the robust verification of timed automata.

@inproceedings{sies2011-Mar,
  author =              {Markey, Nicolas},
  title =               {Robustness in Real-time Systems},
  booktitle =           {{P}roceedings of the 6th {IEEE} {I}nternational
                         {S}ymposium on {I}ndustrial {E}mbedded {S}ystems
                         ({SIES}'11)},
  acronym =             {{SIES}'11},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {28-34},
  year =                {2011},
  month =               jun,
  doi =                 {10.1109/SIES.2011.5953652},
  abstract =            {We~review several aspects of robustness of real-time
                         systems, and present recent results on the robust
                         verification of timed automata.},
}
[Mar11] Nicolas Markey. Verification of Embedded Systems – Algorithms and Complexity. Mémoire d'habilitation, École Normale Supérieure de Cachan, France, Avril 2011.
@phdthesis{hdr2011-Mar,
  author =              {Markey, Nicolas},
  title =               {Verification of Embedded Systems -- Algorithms and
                         Complexity},
  year =                {2011},
  month =               apr,
  school =              {{\'E}cole Normale Sup{\'e}rieure de Cachan, France},
  type =                {M\'emoire d'habilitation},
}
[Mar14] Nicolas Markey. Cassting: Synthesizing Complex Systems Using Non-Zero-Sum Games. ERCIM News 97:25-26. European Research Consortium for Informatics and Mathematics, avril 2014.
@article{ercimnews97-Mar,
  author =              {Markey, Nicolas},
  title =               {Cassting: Synthesizing Complex Systems Using
                         Non-Zero-Sum Games},
  publisher =           {European Research Consortium for Informatics and
                         Mathematics},
  journal =             {ERCIM News},
  volume =              {97},
  pages =               {25-26},
  year =                {2014},
  month =               apr,
  url =                 {http://ercim-news.ercim.eu/en97/special/
  cassting-synthesizing-complex-systems-using-non-zero-sum-games},
}
[Mar17] Nicolas Markey. Temporal logics for multi-agent systems (invited talk). In MFCS'17, Leibniz International Proceedings in Informatics 84, pages 84:1-84:3. Leibniz-Zentrum für Informatik, août 2017.
@inproceedings{mfcs2017-Mar,
  author =              {Markey, Nicolas},
  title =               {Temporal logics for multi-agent systems
                         (invited~talk)},
  editor =              {Larsen, Kim Guldstrand and Bodlaender, Hans L. and
                         Raskin, Jean-Fran{\c c}ois},
  booktitle =           {{P}roceedings of the 42th {I}nternational
                         {S}ymposium on {M}athematical {F}oundations of
                         {C}omputer {S}cience ({MFCS}'17)},
  acronym =             {{MFCS}'17},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {84},
  pages =               {84:1-84:3},
  year =                {2017},
  month =               aug,
  doi =                 {10.4230/LIPIcs.MFCS.2017.84},
}
[Mat02] Radu Mateescu. Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems. Research Report 4430, INRIA Rhône-Alpes, Montbonnot, France, Avril 2002.
@techreport{inria-4430,
  author =              {Mateescu, Radu},
  title =               {Local Model-Checking of Modal Mu-Calculus on Acyclic
                         Labeled Transition Systems},
  number =              {4430},
  year =                {2002},
  month =               apr,
  institution =         {INRIA Rh\^one-Alpes, Montbonnot, France},
  type =                {Research Report},
}
[Maz02] René Mazala. Infinite Games. In Erich Grädel, Wolfgang Thomas et Thomas Wilke (eds.), Automata, Logics, and Infinite Games, Lecture Notes in Computer Science 2500, pages 23-42. Springer-Verlag, 2002.
@incollection{lncs2500-mazala,
  author =              {Mazala, Ren{\'e}},
  title =               {Infinite Games},
  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 =               {23-42},
  year =                {2002},
}
[MB08] Oded Maler et Grégory Batt. Approximating continuous systems by timed automata. In FMSB'08, Lecture Notes in Bioinformatics 5054, pages 77-89. Springer-Verlag, juin 2008.
@inproceedings{fmsb2008-MB,
  author =              {Maler, Oded and Batt, Gr{\'e}gory},
  title =               {Approximating continuous systems by timed automata},
  editor =              {Fisher, Jasmin},
  booktitle =           {{P}roceedings of the 1st {I}nternational {W}okshop
                         on {F}ormal {M}ethods in {S}ystems {B}iology
                         ({FMSB}'08)},
  acronym =             {{FMSB}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Bioinformatics},
  volume =              {5054},
  pages =               {77-89},
  year =                {2008},
  month =               jun,
  doi =                 {10.1007/978-3-540-68413-8_6},
}
[MBK03] Malik Magdon-Ismail, Costas Busch et Mukkai S. Krishnamoorthy. Cake-Cutting is not a Piece of Cake. In STACS'03, Lecture Notes in Computer Science 2607, pages 596-607. Springer-Verlag, février 2003.
@inproceedings{stacs2003-MBK,
  author =              {Magdon{-}Ismail, Malik and Busch, Costas and
                         Krishnamoorthy, Mukkai S.},
  title =               {Cake-Cutting is not a Piece of Cake},
  editor =              {Alt, Helmut and Habib, Michel},
  booktitle =           {{P}roceedings of the 20th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'03)},
  acronym =             {{STACS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2607},
  pages =               {596-607},
  year =                {2003},
  month =               feb,
}
[MBL+98] Hervé Marchand, Patricia Bournai, Michel Le Borgne et Paul Le Guernic. A Design Environment for Discrete-Event Controllers based on the SIGNAL Language. In SMC'98, pages 770-775. IEEE Comp. Soc. Press, octobre 1998.
@inproceedings{ieeesmc1998-MBLL,
  author =              {Marchand, Herv{\'e} and Bournai, Patricia and
                         Le{~}Borgne, Michel and Le{~}Guernic, Paul},
  title =               {A Design Environment for Discrete-Event Controllers
                         based on the {SIGNAL} Language},
  booktitle =           {{P}roceedings of the 1998 {IEEE} {I}nternational
                         {C}onference on {S}ystems, {M}an, {A}nd
                         {C}ybernetics ({SMC}'98)},
  acronym =             {{SMC}'98},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {770-775},
  year =                {1998},
  month =               oct,
}
[McM93] Kenneth L. McMillan. Symbolic Model Checking –-mdash; An Approach to the State Explosion Problem. PhD thesis, Carnegie Mellon University, 1993.
@phdthesis{phd-mcmillan,
  author =              {McMillan, Kenneth L.},
  title =               {Symbolic Model Checking~--- An Approach to the State
                         Explosion Problem},
  year =                {1993},
  school =              {Carnegie Mellon University},
}
[McM93] Kenneth L. McMillan. Symbolic Model Checking. Kluwer Academic, 1993.
@book{McM93-book,
  author =              {McMillan, Kenneth L.},
  title =               {Symbolic Model Checking},
  publisher =           {Kluwer Academic},
  year =                {1993},
}
[McM99] Kenneth L. McMillan. Verification of infinite state systems by compositional model checking. In CHARME'99, Lecture Notes in Computer Science 1703, pages 219-237. Springer-Verlag, septembre 1999.
@inproceedings{charme1999-McM,
  author =              {McMillan, Kenneth L.},
  title =               {Verification of infinite state systems by
                         compositional model checking},
  editor =              {Pierre, Laurence and Kropf, {\relax Th}omas},
  booktitle =           {{P}roceedings of the 10th {C}orrect {H}ardware
                         {D}esign and {V}erification {M}ethods ({CHARME}'99)},
  acronym =             {{CHARME}'99},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1703},
  pages =               {219-237},
  year =                {1999},
  month =               sep,
  doi =                 {10.1007/3-540-48153-2_17},
}
[McM02] Kenneth L. McMillan. Applying SAT Methods in Unbounded Symbolic Model Checking. In CAV'02, Lecture Notes in Computer Science 2404, pages 250-264. Springer-Verlag, juillet 2002.
@inproceedings{cav2002-McM,
  author =              {McMillan, Kenneth L.},
  title =               {Applying {SAT} Methods in Unbounded Symbolic Model
                         Checking},
  editor =              {Brinksma, Ed and Larsen, Kim Guldstrand},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'02)},
  acronym =             {{CAV}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2404},
  pages =               {250-264},
  year =                {2002},
  month =               jul,
}
[McM06] Kenneth L. McMillan. Lazy Abstraction with Interpolants. In CAV'06, Lecture Notes in Computer Science 4144, pages 123-136. Springer-Verlag, juillet 2006.
@inproceedings{cav2006-McM,
  author =              {McMillan, Kenneth L.},
  title =               {Lazy Abstraction with Interpolants},
  editor =              {Ball, Thomas and Jones, Robert},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'06)},
  acronym =             {{CAV}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4144},
  pages =               {123-136},
  year =                {2006},
  month =               jul,
  doi =                 {10.1007/11817963_14},
}
[McN66] Robert McNaughton. Testing and Generating Infinite Sequences by a Finite Automaton. Information and Control 9(6):521-530. Academic Press, décembre 1966.
@article{icont9(6)-Mcn,
  author =              {McNaughton, Robert},
  title =               {Testing and Generating Infinite Sequences by a
                         Finite Automaton},
  publisher =           {Academic Press},
  journal =             {Information and Control},
  volume =              {9},
  number =              {6},
  pages =               {521-530},
  year =                {1966},
  month =               dec,
}
[McN93] Robert McNaughton. Infinite Games Played on Finite Graphs. Annals of Pure and Applied Logic 65(2):149-184. Elsevier, décembre 1993.
@article{apal65(2)-Mcn,
  author =              {McNaughton, Robert},
  title =               {Infinite Games Played on Finite Graphs},
  publisher =           {Elsevier},
  journal =             {Annals of Pure and Applied Logic},
  volume =              {65},
  number =              {2},
  pages =               {149-184},
  year =                {1993},
  month =               dec,
}
[MH84] Satoru Miyano et Takeshi Hayashi. Alternating Finite Automata on ω-words. Theoretical Computer Science 32:321-330. Elsevier, 1984.
@article{tcs32()-MH,
  author =              {Miyano, Satoru and Hayashi, Takeshi},
  title =               {Alternating Finite Automata on {\(\omega\)}-words},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {32},
  pages =               {321-330},
  year =                {1984},
}
[Mil80] Robin Milner. A Calculus of Communicating Systems. Lecture Notes in Computer Science 92. Springer-Verlag, 1980.
@book{Milner-lncs92,
  author =              {Milner, Robin},
  title =               {A Calculus of Communicating Systems},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {92},
  year =                {1980},
}
[Mil89] Robin Milner. Communication and concurrency. Prentice Hall International Series in Computer Science. Prentice Hall Int., décembre 1989.
@book{Milner-CC1989,
  author =              {Milner, Robin},
  title =               {Communication and concurrency},
  publisher =           {Prentice Hall Int.},
  series =              {Prentice Hall International Series in Computer
                         Science},
  year =                {1989},
  month =               dec,
}
[Mil00] Joseph S. Miller. Decidability and Complexity Results for Timed Automata and Semi-linear Hybrid Automata. In HSCC'00, Lecture Notes in Computer Science 1790, pages 296-310. Springer-Verlag, mars 2000.
@inproceedings{hscc2000-Mil,
  author =              {Miller, Joseph S.},
  title =               {Decidability and Complexity Results for Timed
                         Automata and Semi-linear Hybrid Automata},
  editor =              {Lynch, Nancy and Krogh, Bruce H.},
  booktitle =           {{P}roceedings of the 3rd {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'00)},
  acronym =             {{HSCC}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1790},
  pages =               {296-310},
  year =                {2000},
  month =               mar,
}
[Min61] Marvin L. Minsky. Recursive Unsolvability of Post's Problem of "Tag" and other Topics in Theory of Turing Machines. Annals of Mathematics 74(3):437-455. Princeton University, novembre 1961.
@article{am74(3)-Min,
  author =              {Minsky, Marvin L.},
  title =               {Recursive Unsolvability of {P}ost's Problem of
                         {"}Tag{"} and other Topics in Theory of {T}uring
                         Machines},
  publisher =           {Princeton University},
  journal =             {Annals of Mathematics},
  volume =              {74},
  number =              {3},
  pages =               {437-455},
  year =                {1961},
  month =               nov,
}
[Min67] Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice Hall, Inc., 1967.
@book{cfim1967-Min,
  author =              {Minsky, Marvin L.},
  title =               {Computation: Finite and Infinite Machines},
  booktitle =           {Computation: Finite and Infinite Machines},
  publisher =           {Prentice Hall, Inc.},
  year =                {1967},
}
[Min99] Marius Minea. Partial Order Reduction for Model Checking of Timed Automata. In CONCUR'99, Lecture Notes in Computer Science 1664, pages 431-446. Springer-Verlag, août 1999.
@inproceedings{concur1999-Min,
  author =              {Minea, Marius},
  title =               {Partial Order Reduction for Model Checking of Timed
                         Automata},
  editor =              {Baeten, Jos C. M. and Mauw, Sjouke},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'99)},
  acronym =             {{CONCUR}'99},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1664},
  pages =               {431-446},
  year =                {1999},
  month =               aug,
}
[Mit05] David G. Mitchell. A SAT Solver Primer. EATCS Bulletin 85:112-132. EATCS, février 2005.
@article{eatcs-bull85()-Mit,
  author =              {Mitchell, David G.},
  title =               {A {SAT} Solver Primer},
  publisher =           {EATCS},
  journal =             {EATCS Bulletin},
  volume =              {85},
  pages =               {112-132},
  year =                {2005},
  month =               feb,
}
[Miy91] Satoru Miyano. Δ2P-complete lexicographically first maximal subgraph problems. Theoretical Computer Science 88(1):33-57. Elsevier, 1991.
@article{tcs88(1)-Miy,
  author =              {Miyano, Satoru},
  title =               {{\(\Delta_2^P\)}-complete lexicographically first
                         maximal subgraph problems},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {88},
  number =              {1},
  pages =               {33-57},
  year =                {1991},
}
[MLA+99] Jesper B. Møller, Jakob Lichtenberg, Henrik Reif Andersen et Henrik Hulgaard. Difference Decision Diagrams. In CSL'99, Lecture Notes in Computer Science 1862, pages 111-125. Springer-Verlag, septembre 1999.
@inproceedings{csl1999-MLAH,
  author =              {M{\o}ller, Jesper B. and Lichtenberg, Jakob and
                         Andersen, Henrik Reif and Hulgaard, Henrik},
  title =               {Difference Decision Diagrams},
  editor =              {Flum, J{\"o}rg and Rodr{\'\i}guez{-}Artalejo, Mario},
  booktitle =           {{P}roceedings of the 13th {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'99)},
  acronym =             {{CSL}'99},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1862},
  pages =               {111-125},
  year =                {1999},
  month =               sep,
}
[MM02] Annabelle K. McIver et Carroll C. Morgan. Games, Probability and the Quantitative μ-calculus. In LPAR'02, Lecture Notes in Computer Science 2514, pages 292-310. Springer-Verlag, octobre 2002.
@inproceedings{lpar2002-MM,
  author =              {McIver, Annabelle K. and Morgan, Carroll C.},
  title =               {Games, Probability and the Quantitative
                         {\(\mu\)}-calculus},
  editor =              {Baaz, Matthias and Voronkov, Andrei},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference {L}ogic {P}rogramming and {A}utomated
                         {R}easoning ({LPAR}'02)},
  acronym =             {{LPAR}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2514},
  pages =               {292-310},
  year =                {2002},
  month =               oct,
}
[MMK+94] Louise E. Moser, P. Michael Melliar-Smith, George Kutty et Y. Srinivas Ramakrishna. Completeness and Soundness of Axiomatizations for Temporal Logics without Next. Fundamenta Informaticae 21(4):257-305. IOS Press, octobre 1994.
@article{fundi21(4)-MMKR,
  author =              {Moser, Louise E. and Melliar{-}Smith, P. Michael and
                         Kutty, George and Ramakrishna, Y. Srinivas},
  title =               {Completeness and Soundness of Axiomatizations for
                         Temporal Logics without Next},
  publisher =           {IOS Press},
  journal =             {Fundamenta Informaticae},
  volume =              {21},
  number =              {4},
  pages =               {257-305},
  year =                {1994},
  month =               oct,
}
[MMP+12] Fabio Mogavero, Aniello Murano, Giuseppe Perelli et Moshe Y. Vardi. What Makes ATL* Decidable? A Decidable Fragment of Strategy Logic. In CONCUR'12, Lecture Notes in Computer Science 7454, pages 193-208. Springer-Verlag, septembre 2012.
@inproceedings{concur2012-MMPV,
  author =              {Mogavero, Fabio and Murano, Aniello and Perelli,
                         Giuseppe and Vardi, Moshe Y.},
  title =               {What Makes {ATL\(^{*}\)} Decidable? {A}~Decidable
                         Fragment of Strategy Logic},
  editor =              {Koutny, Maciej and Ulidowski, Irek},
  booktitle =           {{P}roceedings of the 23rd {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'12)},
  acronym =             {{CONCUR}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7454},
  pages =               {193-208},
  year =                {2012},
  month =               sep,
}
[MMP+12] Fabio Mogavero, Aniello Murano, Giuseppe Perelli et Moshe Y. Vardi. Reasoning About Strategies: On the Model-Checking Problem. Research Report cs.LO/1112.6275, arXiv, Décembre 2012.
@techreport{arxiv-cd.LO-1112.6275,
  author =              {Mogavero, Fabio and Murano, Aniello and Perelli,
                         Giuseppe and Vardi, Moshe Y.},
  title =               {Reasoning About Strategies: On the Model-Checking
                         Problem},
  number =              {cs.LO/1112.6275},
  year =                {2012},
  month =               dec,
  institution =         {arXiv},
  type =                {Research Report},
}
[MMP+14] Fabio Mogavero, Aniello Murano, Giuseppe Perelli et Moshe Y. Vardi. Reasoning About Strategies: On the Model-Checking Problem. ACM Transactions on Computational Logic 15(4):34:1-34:47. ACM Press, août 2014.
@article{tocl15(4)-MMPV,
  author =              {Mogavero, Fabio and Murano, Aniello and Perelli,
                         Giuseppe and Vardi, Moshe Y.},
  title =               {Reasoning About Strategies: On the Model-Checking
                         Problem},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {15},
  number =              {4},
  pages =               {34:1-34:47},
  year =                {2014},
  month =               aug,
  doi =                 {10.1145/2631917},
}
[MMP+17] Fabio Mogavero, Aniello Murano, Giuseppe Perelli et Moshe Y. Vardi. Reasoning About Strategies: On the Satisfiability Problem. Logical Methods in Computer Science 13(1). Mars 2017.
@article{lmcs13(1)-MMPV,
  author =              {Mogavero, Fabio and Murano, Aniello and Perelli,
                         Giuseppe and Vardi, Moshe Y.},
  title =               {Reasoning About Strategies: On~the~Satisfiability
                         Problem},
  journal =             {Logical Methods in Computer Science},
  volume =              {13},
  number =              {1},
  year =                {2017},
  month =               mar,
  doi =                 {10.23638/LMCS-13(1:9)2017},
}
[MMS13] Fabio Mogavero, Aniello Murano et Luigi Sauro. On the Boundary of Behavioral Strategies. In LICS'13, pages 263-272. IEEE Comp. Soc. Press, juin 2013.
@inproceedings{lics2013-MMS,
  author =              {Mogavero, Fabio and Murano, Aniello and Sauro,
                         Luigi},
  title =               {On the Boundary of Behavioral Strategies},
  booktitle =           {{P}roceedings of the 28th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'13)},
  acronym =             {{LICS}'13},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {263-272},
  year =                {2013},
  month =               jun,
}
[MMS14] Fabio Mogavero, Aniello Murano et Luigi Sauro. A Behavioral Hierarchy of Strategy Logic. In CLIMA'14, Lecture Notes in Artificial Intelligence 8624, pages 148-165. Springer-Verlag, août 2014.
@inproceedings{clima2014-MMS,
  author =              {Mogavero, Fabio and Murano, Aniello and Sauro,
                         Luigi},
  title =               {A Behavioral Hierarchy of Strategy Logic},
  editor =              {Bulling, Nils and van der Torre, Leendert W. N. and
                         Villata, Serena and Jamroga, Wojciech and
                         Vasconcelos, Wamberto Weber},
  booktitle =           {{P}roceedings of the 15th {I}nternational {W}orkshop
                         on {C}omputational {L}ogic in {M}ulti-{A}gent
                         {S}ystems ({CLIMA}'14)},
  acronym =             {{CLIMA}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Artificial Intelligence},
  volume =              {8624},
  pages =               {148-165},
  year =                {2014},
  month =               aug,
  doi =                 {10.1007/978-3-319-09764-0_10},
}
[MMT+08] Arne Meier, Martin Mundhenk, Michael Thomas et Heribert Vollmer. The Complexity of Satisfiability for Fragmentf of CTL and CTL*. In RP'08, pages 201-213. Septembre 2008.
@inproceedings{mmtv-rp08,
  author =              {Meier, Arne and Mundhenk, Martin and Thomas, Michael
                         and Vollmer, Heribert},
  title =               {The Complexity of Satisfiability for Fragmentf of
                         {CTL} and {CTL}\(^{*}\)},
  editor =              {Halava, Vesa and Potapov, Igor},
  booktitle =           {{P}roceedings of the 2nd {W}orkshop on
                         {R}eachability {P}roblems in {C}omputational
                         {M}odels ({RP}'08)},
  acronym =             {{RP}'08},
  pages =               {201-213},
  year =                {2008},
  month =               sep,
}
[MMV10] Fabio Mogavero, Aniello Murano et Moshe Y. Vardi. Reasoning about strategies. In FSTTCS'10, Leibniz International Proceedings in Informatics 8, pages 133-144. Leibniz-Zentrum für Informatik, décembre 2010.
@inproceedings{fsttcs2010-MMV,
  author =              {Mogavero, Fabio and Murano, Aniello and Vardi, Moshe
                         Y.},
  title =               {Reasoning about strategies},
  editor =              {Lodaya, Kamal and Mahajan, Meena},
  booktitle =           {{P}roceedings of the 30th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'10)},
  acronym =             {{FSTTCS}'10},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {8},
  pages =               {133-144},
  year =                {2010},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2010.133},
}
[MMV10] Fabio Mogavero, Aniello Murano et Moshe Y. Vardi. Relentful Strategic Reasoning in Alternating-Time Temporal Logic. In LPAR'10, Lecture Notes in Artificial Intelligence 6355, pages 371-386. Springer-Verlag, avril 2010.
@inproceedings{lpar2010(dakar)-MMV,
  author =              {Mogavero, Fabio and Murano, Aniello and Vardi, Moshe
                         Y.},
  title =               {Relentful Strategic Reasoning in Alternating-Time
                         Temporal Logic},
  editor =              {Clarke, Edmund M. and Voronkov, Andrei},
  booktitle =           {{P}roceedings of the 16th {I}nternational
                         {C}onference {L}ogic {P}rogramming and {A}utomated
                         {R}easoning ({LPAR}'10)},
  acronym =             {{LPAR}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Artificial Intelligence},
  volume =              {6355},
  pages =               {371-386},
  year =                {2010},
  month =               apr,
}
[MvN47] Oskar Morgenstern et John von Neumann. The Theory of Games and Economic Behavior. Princeton University, 1947.
@book{MvN-game1947,
  author =              {Morgenstern, Oskar and von~Neumann, John},
  title =               {The Theory of Games and Economic Behavior},
  publisher =           {Princeton University},
  year =                {1947},
}
[MN04] Oded Maler et Dejan Nickovic. Monitoring Temporal Properties of Continuous Signals. In FORMATS-FTRTFT'04, Lecture Notes in Computer Science 3253, pages 152-166. Springer-Verlag, septembre 2004.
@inproceedings{formats2004-MN,
  author =              {Maler, Oded and Nickovic, Dejan},
  title =               {Monitoring Temporal Properties of Continuous
                         Signals},
  editor =              {Lakhnech, Yassine and Yovine, Sergio},
  booktitle =           {{P}roceedings of the {J}oint {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'04) and {F}ormal
                         {T}echniques in {R}eal-Time and {F}ault-Tolerant
                         {S}ystems ({FTRTFT}'04)},
  acronym =             {{FORMATS-FTRTFT}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3253},
  pages =               {152-166},
  year =                {2004},
  month =               sep,
}
[MN10] Janusz Malinowski et Peter Niebert. SAT Based Bounded Model Checking with Partial Order Semantics for Timed Automata. In TACAS'10, Lecture Notes in Computer Science 6015, pages 405-419. Springer-Verlag, mars 2010.
@inproceedings{tacas2010-MN,
  author =              {Malinowski, Janusz and Niebert, Peter},
  title =               {{SAT} Based Bounded Model Checking with Partial
                         Order Semantics for Timed Automata},
  editor =              {Esparza, Javier and Majumdar, Rupak},
  booktitle =           {{P}roceedings of the 16th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'10)},
  acronym =             {{TACAS}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6015},
  pages =               {405-419},
  year =                {2010},
  month =               mar,
}
[MNP06] Oded Maler, Dejan Nickovic et Amir Pnueli. From MITL to Timed Automata. In FORMATS'06, Lecture Notes in Computer Science 4202, pages 274-289. Springer-Verlag, septembre 2006.
@inproceedings{formats2006-MNP,
  author =              {Maler, Oded and Nickovic, Dejan and Pnueli, Amir},
  title =               {From {MITL} to Timed Automata},
  editor =              {Asarin, Eugene and Bouyer, Patricia},
  booktitle =           {{P}roceedings of the 4th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'06)},
  acronym =             {{FORMATS}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4202},
  pages =               {274-289},
  year =                {2006},
  month =               sep,
}
[MO97] Dieter van Melkebeek et Mitsunori Ogihara. Sparse Hard Sets for P. In Ding-zhu Du et Ker-I Ko (eds.), Advances in Algorithms, Languages and Complexity. Kluwer Academic, 1997.
@incollection{AALC1997-MO,
  author =              {Melkebeek, Dieter van and Ogihara, Mitsunori},
  title =               {Sparse Hard Sets for~{P}},
  editor =              {Du, Ding-zhu and Ko, Ker-I},
  booktitle =           {Advances in Algorithms, Languages and Complexity},
  publisher =           {Kluwer Academic},
  pages =               {191-208},
  year =                {1997},
}
[MO07] Maura Mazzarello et Ennio Ottaviani. A traffic management system for real-time traffic optimisation in railways. Transportation Research Part B: Methodological 41(2):246-274. Elsevier, février 2007.
@article{transpB41(2)-MO,
  author =              {Mazzarello, Maura and Ottaviani, Ennio},
  title =               {A~traffic management system for real-time traffic
                         optimisation in railways},
  publisher =           {Elsevier},
  journal =             {Transportation Research Part B: Methodological},
  volume =              {41},
  number =              {2},
  pages =               {246-274},
  year =                {2007},
  month =               feb,
  doi =                 {10.1016/j.trb.2006.02.005},
}
[Mon08] David Monniaux. A Quantifier Elimination Algorithm for Linear Real Arithmetic. In LPAR'08, Lecture Notes in Computer Science 5330, pages 243-257. Springer-Verlag, novembre 2008.
@inproceedings{lpar2008-Mon,
  author =              {Monniaux, David},
  title =               {A~Quantifier Elimination Algorithm for Linear Real
                         Arithmetic},
  editor =              {Cervesato, Iliano and Veith, Helmutand Voronkov,
                         Andrei},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference {L}ogic {P}rogramming and {A}utomated
                         {R}easoning ({LPAR}'08)},
  acronym =             {{LPAR}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5330},
  pages =               {243-257},
  year =                {2008},
  month =               nov,
  doi =                 {10.1007/978-3-540-89439-1_18},
}
[Moo96] Cristopher Moore. Recursion Theory on the Reals and Continuous-Time Computation. Theoretical Computer Science 162(1):23-44. Elsevier, août 1996.
@article{tcs162(1)-Moo,
  author =              {Moore, Cristopher},
  title =               {Recursion Theory on the Reals and Continuous-Time
                         Computation},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {162},
  number =              {1},
  pages =               {23-44},
  year =                {1996},
  month =               aug,
}
[Mos91] Andrzej Mostowski. Games with forbidden positions. Research Report 78, University of Danzig, 1991.
@techreport{TR78-Mos91,
  author =              {Mostowski, Andrzej},
  title =               {Games with forbidden positions},
  number =              {78},
  year =                {1991},
  institution =         {University of Danzig},
  type =                {Research Report},
}
[MP88] Zohar Manna et Amir Pnueli. The Anchored Version of the Temporal Framework. In REX'88, Lecture Notes in Computer Science 354, pages 201-284. Springer-Verlag, mai 1988.
@inproceedings{rex1988-MP,
  author =              {Manna, Zohar and Pnueli, Amir},
  title =               {The Anchored Version of the Temporal Framework},
  editor =              {de Bakker, Jaco W. and de Roever, Willem-Paul and
                         Rozenberg, Grzegorz},
  booktitle =           {{L}inear {T}ime, {B}ranching {T}ime and {P}artial
                         {O}rder in {L}ogics and {M}odels for
                         {C}oncurrency~--- {P}roceedings of {REX}
                         {S}chool{\slash}{W}orkshop~1988 ({REX}'88)},
  acronym =             {{REX}'88},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {354},
  pages =               {201-284},
  year =                {1988},
  month =               may,
}
[MP90] Oded Maler et Amir Pnueli. Tight Bounds on the Complexity of Cascaded Decomposition of Automata. In FOCS'90, pages 672-682. IEEE Comp. Soc. Press, octobre 1990.
@inproceedings{focs1990-MP,
  author =              {Maler, Oded and Pnueli, Amir},
  title =               {Tight Bounds on the Complexity of Cascaded
                         Decomposition of Automata},
  booktitle =           {{P}roceedings of the 31st {A}nnual {S}ymposium on
                         {F}oundations of {C}omputer {S}cience ({FOCS}'90)},
  acronym =             {{FOCS}'90},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {672-682},
  year =                {1990},
  month =               oct,
}
[MP90] Zohar Manna et Amir Pnueli. A Hierarchy of Temporal Properties. In PODC'90, pages 377-410. ACM Press, août 1990.
@inproceedings{podc1990-MP,
  author =              {Manna, Zohar and Pnueli, Amir},
  title =               {A Hierarchy of Temporal Properties},
  booktitle =           {{P}roceedings of the 9th {ACM} {S}ymposium on
                         {P}rinciples of {D}istributed {C}omputing
                         ({PODC}'90)},
  acronym =             {{PODC}'90},
  publisher =           {ACM Press},
  pages =               {377-410},
  year =                {1990},
  month =               aug,
}
[MP91] Zohar Manna et Amir Pnueli. Completing the Temporal Picture. Theoretical Computer Science 83(1):91-130. Elsevier, 1991.
@article{tcs83(1)-MP,
  author =              {Manna, Zohar and Pnueli, Amir},
  title =               {Completing the Temporal Picture},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {83},
  number =              {1},
  pages =               {91-130},
  year =                {1991},
}
[MP93] Zohar Manna et Amir Pnueli. Verifying Hybrid Systems. In HSCC'92, Lecture Notes in Computer Science 736, pages 4-35. Springer-Verlag, 1993.
@inproceedings{hscc1992-MP,
  author =              {Manna, Zohar and Pnueli, Amir},
  title =               {Verifying 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 =               {4-35},
  year =                {1993},
}
[MP05] Filippo Mera et Giovanni Pighizzini. Complementing Unary Nondeterministic Automata. Theoretical Computer Science 330(2):349-360. Elsevier, février 2005.
@article{tcs330(2)-MP,
  author =              {Mera, Filippo and Pighizzini, Giovanni},
  title =               {Complementing Unary Nondeterministic Automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {330},
  number =              {2},
  pages =               {349-360},
  year =                {2005},
  month =               feb,
}
[MPS95] Oded Maler, Amir Pnueli et Joseph Sifakis. On the Synthesis of Discrete Controllers for Timed Systems (An Extended Abstract). In STACS'95, Lecture Notes in Computer Science 900, pages 229-242. Springer-Verlag, mars 1995.
@inproceedings{stacs1995-MPS,
  author =              {Maler, Oded and Pnueli, Amir and Sifakis, Joseph},
  title =               {On the Synthesis of Discrete Controllers for Timed
                         Systems (An~Extended Abstract)},
  editor =              {Mayr, Ernst W. and Puech, Claude},
  booktitle =           {{P}roceedings of the 12th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'95)},
  acronym =             {{STACS}'95},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {900},
  pages =               {229-242},
  year =                {1995},
  month =               mar,
}
[MR99] Faron Moller et Alexander Rabinovich. On the expressive power of CTL*. In LICS'99, pages 360-368. IEEE Comp. Soc. Press, juillet 1999.
@inproceedings{lics1999-MR,
  author =              {Moller, Faron and Rabinovich, Alexander},
  title =               {On the expressive power of
                         {CTL}{\textsuperscript{*}}},
  booktitle =           {{P}roceedings of the 14th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'99)},
  acronym =             {{LICS}'99},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {360-368},
  year =                {1999},
  month =               jul,
  doi =                 {10.1109/LICS.1999.782631},
}
[MR03] Faron Moller et Alexander Rabinovich. Counting on CTL*: on the expressive power of monadic path logic. Information and Computation 184(1):147-159. Academic Press, juillet 2003.
@article{icomp184(1)-MR,
  author =              {Moller, Faron and Rabinovich, Alexander},
  title =               {Counting on {CTL}{\textsuperscript{*}}: on~the
                         expressive power of monadic path logic},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {184},
  number =              {1},
  pages =               {147-159},
  year =                {2003},
  month =               jul,
}
[MR04] Nicolas Markey et Jean-François Raskin. Model Checking Restricted Sets of Timed Paths. In CONCUR'04, Lecture Notes in Computer Science 3170, pages 432-447. Springer-Verlag, août 2004.
Résumé

In this paper, we study the complexity of model-checking formulas of three important real-time logics (MTL, MITL, and TCTL) over restricted sets of timed paths. The classes of restricted sets of timed paths that we consider are (i) a single finite (or ultimately periodic) timed path, (ii) a infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a region graph, (iii) a infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a zone graph.

@inproceedings{concur2004-MR,
  author =              {Markey, Nicolas and Raskin, Jean-Fran{\c c}ois},
  title =               {Model Checking Restricted Sets of Timed Paths},
  editor =              {Gardner, {\relax Ph}ilippa and Yoshida, Nobuko},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'04)},
  acronym =             {{CONCUR}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3170},
  pages =               {432-447},
  year =                {2004},
  month =               aug,
  doi =                 {10.1007/978-3-540-28644-8_28},
  abstract =            {In this paper, we study the complexity of
                         model-checking formulas of three important real-time
                         logics (MTL, MITL, and TCTL) over restricted sets of
                         timed paths. The classes of restricted sets of timed
                         paths that we consider are \textit{(i)} a single
                         finite (or ultimately periodic) timed path,
                         \textit{(ii)} a infinite set of finite (or infinite)
                         timed paths defined by a finite (or ultimately
                         periodic) path in a region graph, \textit{(iii)} a
                         infinite set of finite (or infinite) timed paths
                         defined by a finite (or ultimately periodic) path in
                         a zone graph.},
}
[MR06] Nicolas Markey et Jean-François Raskin. Model Checking Restricted Sets of Timed Paths. Theoretical Computer Science 358(2-3):273-292. Elsevier, août 2006.
Résumé

In this paper, we study the complexity of model-checking formulas of four important real-time logics (TPTL, MTL, MITL, and TCTL) over restricted sets of timed paths. The classes of restricted sets of timed paths that we consider are (i) a single finite (or ultimately periodic) timed path, (ii) an infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a region graph, (iii) an infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a zone graph.

Several results are quite negative: TPTL and MTL remain undecidable along region- and zone-paths. On the other hand, we obtained PTIME algorithms for model checking TCTL along a region path, and for MTL along a single timed path.

@article{tcs358(2-3)-MR,
  author =              {Markey, Nicolas and Raskin, Jean-Fran{\c c}ois},
  title =               {Model Checking Restricted Sets of Timed Paths},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {358},
  number =              {2-3},
  pages =               {273-292},
  year =                {2006},
  month =               aug,
  doi =                 {10.1016/j.tcs.2006.01.019},
  abstract =            {In this paper, we study the complexity of
                         model-checking formulas of four important real-time
                         logics (TPTL, MTL, MITL, and TCTL) over restricted
                         sets of timed paths. The classes of restricted sets
                         of timed paths that we consider are
                         \textit{(i)}~a~single finite (or ultimately
                         periodic) timed path, \textit{(ii)}~an~infinite set
                         of finite (or infinite) timed paths defined by a
                         finite (or ultimately periodic) path in a region
                         graph, \textit{(iii)}~an~infinite set of finite (or
                         infinite) timed paths defined by a finite (or
                         ultimately periodic) path in a zone graph. \par
                         Several results are quite negative: TPTL and MTL
                         remain undecidable along region- and zone-paths. On
                         the other hand, we obtained PTIME algorithms for
                         model checking TCTL along a region path, and for MTL
                         along a single timed path.},
}
[MRK88] Gary L. Miller, Vijaya Ramachandran et Erich Kaltofen. Efficient Parallel Evaluation of Straight-line Code and Arithmetic Circuits. SIAM Journal on Computing 17(4):687-695. Society for Industrial and Applied Math., août 1988.
@article{siamcomp17(4)-MRK,
  author =              {Miller, Gary L. and Ramachandran, Vijaya and
                         Kaltofen, Erich},
  title =               {Efficient Parallel Evaluation of Straight-line Code
                         and Arithmetic Circuits},
  publisher =           {Society for Industrial and Applied Math.},
  journal =             {SIAM Journal on Computing},
  volume =              {17},
  number =              {4},
  pages =               {687-695},
  year =                {1988},
  month =               aug,
}
[MRV99] Pierre McKenzie, Klaus Reinhardt et V. Vinay. Circuits and Context-free Languages. In COCOON'99, Lecture Notes in Computer Science 1627, pages 194-203. Springer-Verlag, juillet 1999.
@inproceedings{cocoon1999-MRV,
  author =              {McKenzie, Pierre and Reinhardt, Klaus and Vinay, V.},
  title =               {Circuits and Context-free Languages},
  editor =              {Asano, Takao and Imai, Hiroshi and Lee, D. T. and
                         Nakano, Shin-Ichi and Tokuyama, Takeshi},
  booktitle =           {{P}roceedings of the 5th {C}omputing and
                         {C}ombinatorics ({COCOON}'99)},
  acronym =             {{COCOON}'99},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1627},
  pages =               {194-203},
  year =                {1999},
  month =               jul,
}
[MRW05] Peter Bro Miltersen, Jaikumar Radhakrishnan et Ingo Wegener. On Converting CNF to DNF. Theoretical Computer Science 347(1-2):325-335. Elsevier, novembre 2005.
@article{tcs347(1-2)-MRW,
  author =              {Miltersen, Peter Bro and Radhakrishnan, Jaikumar and
                         Wegener, Ingo},
  title =               {On Converting {CNF} to {DNF}},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {347},
  number =              {1-2},
  pages =               {325-335},
  year =                {2005},
  month =               nov,
}
[MS72] Albert R. Meyer et Larry J. Stockmeyer. The Equivalence Problem for Regular Expressions with Squaring Requires Exponential Space. In FOCS'72, pages 125-129. IEEE Comp. Soc. Press, octobre 1972.
@inproceedings{focs1972-MS,
  author =              {Meyer, Albert R. and Stockmeyer, Larry J.},
  title =               {The Equivalence Problem for Regular Expressions with
                         Squaring Requires Exponential Space},
  booktitle =           {{P}roceedings of the 13th {A}nnual {S}ymposium on
                         {F}oundations of {C}omputer {S}cience ({FOCS}'72)},
  acronym =             {{FOCS}'72},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {125-129},
  year =                {1972},
  month =               oct,
}
[MS85] David E. Muller et Paul E. Schupp. Alternating automata on infinite objects, determinacy and Rabin's theorem. In EPIT'84, Lecture Notes in Computer Science 192, pages 99-107. Springer-Verlag, 1985.
@inproceedings{epit1984-MS,
  author =              {Muller, David E. and Schupp, Paul E.},
  title =               {Alternating automata on infinite objects,
                         determinacy and {R}abin's theorem},
  editor =              {Nivat, Maurice and Perrin, Dominique},
  booktitle =           {{A}utomata on {I}nfinite {W}ords~-- {{\'E}}cole de
                         {P}rintemps d'{I}nformatique {T}h{\'e}orique
                         ({EPIT}'84)},
  acronym =             {{EPIT}'84},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {192},
  pages =               {99-107},
  year =                {1985},
  confyear =            {1984},
  confmonth =           {5},
  doi =                 {10.1007/3-540-15641-0_27},
}
[MS87] David E. Muller et Paul E. Schupp. Alternating Automata on Infinite Trees. Theoretical Computer Science 54(2-3):267-276. Elsevier, octobre 1987.
@article{tcs54(2-3)-MS,
  author =              {Muller, David E. and Schupp, Paul E.},
  title =               {Alternating Automata on Infinite Trees},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {54},
  number =              {2-3},
  pages =               {267-276},
  year =                {1987},
  month =               oct,
}
[MS95] David E. Muller et Paul E. Schupp. Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra. Theoretical Computer Science 141(1-2):69-107. Elsevier, avril 1995.
@article{tcs141(1-2)-MS,
  author =              {Muller, David E. and Schupp, Paul E.},
  title =               {Simulating alternating tree automata by
                         nondeterministic automata: New results and new
                         proofs of the theorems of {R}abin, {M}c{N}aughton
                         and {S}afra},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {141},
  number =              {1-2},
  pages =               {69-107},
  year =                {1995},
  month =               apr,
}
[MS97] Oded Maler et Ludwig Staiger. On Syntactic Congruences fpr ω-languages. Theoretical Computer Science 183(1):93-112. Elsevier, août 1997.
@article{tcs183(1)-MS,
  author =              {Maler, Oded and Staiger, Ludwig},
  title =               {On Syntactic Congruences fpr {\(\omega\)}-languages},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {183},
  number =              {1},
  pages =               {93-112},
  year =                {1997},
  month =               aug,
}
[MS00] Zohar Manna et Henny Sipma. Alternating the Temporal Picture for Safety. In ICALP'00, Lecture Notes in Computer Science 1853, pages 429-450. Springer-Verlag, juillet 2000.
@inproceedings{icalp2000-MS,
  author =              {Manna, Zohar and Sipma, Henny},
  title =               {Alternating the Temporal Picture for Safety},
  editor =              {Montanari, Ugo and Rolim, Jos\'e D. P. and Welzl,
                         Emo},
  booktitle =           {{P}roceedings of the 27th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'00)},
  acronym =             {{ICALP}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1853},
  pages =               {429-450},
  year =                {2000},
  month =               jul,
}
[MS02] Paolo Maggi et Riccardo Sisto. Using SPIN to verify security properties of cryptographic protocols. In SPIN'02, Lecture Notes in Computer Science 2318, pages 187-204. Springer-Verlag, avril 2002.
@inproceedings{spin2002-MS,
  author =              {Maggi, Paolo and Sisto, Riccardo},
  title =               {Using SPIN to verify security properties of
                         cryptographic protocols},
  editor =              {Bosnacki, Dragan and Leue, Stefan},
  booktitle =           {{P}roceedings of the 9th {I}nternational {SPIN}
                         {W}orkshop ({SPIN}'02)},
  acronym =             {{SPIN}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2318},
  pages =               {187-204},
  year =                {2002},
  month =               apr,
}
[MS03] Nicolas Markey et Philippe Schnoebelen. Model Checking a Path (Preliminary Report). In CONCUR'03, Lecture Notes in Computer Science 2761, pages 251-265. Springer-Verlag, août 2003.
Résumé

We consider the problem of checking whether a finite (or ultimately periodic) run satisfies a temporal logic formula. This problem is at the heart of "runtime verification" but it also appears in many other situations. By considering several extended temporal logics, we show that the problem of model checking a path can usually be solved efficiently, and profit from specialized algorithms. We further show it is possible to efficiently check paths given in compressed form.

@inproceedings{concur2003-MS,
  author =              {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
  title =               {Model Checking a Path (Preliminary Report)},
  editor =              {Amadio, Roberto and Lugiez, Denis},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'03)},
  acronym =             {{CONCUR}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2761},
  pages =               {251-265},
  year =                {2003},
  month =               aug,
  doi =                 {10.1007/978-3-540-45187-7_17},
  abstract =            {We consider the problem of checking whether a finite
                         (or ultimately periodic) run satisfies a temporal
                         logic formula. This problem is at the heart of
                         {"}runtime verification{"} but it also appears in
                         many other situations. By considering several
                         extended temporal logics, we show that the problem
                         of model checking a path can usually be solved
                         efficiently, and profit from specialized algorithms.
                         We further show it is possible to efficiently check
                         paths given in compressed form.},
}
[MS04] Nicolas Markey et Philippe Schnoebelen. Symbolic Model Checking for Simply Timed Systems. In FORMATS-FTRTFT'04, Lecture Notes in Computer Science 3253, pages 102-117. Springer-Verlag, septembre 2004.
Résumé

We describe OBDD-based symbolic model checking algorithms for simply-timed systems, i.e. finite state graphs where transitions carry a duration. These durations can be arbitrary natural numbers. A simple and natural semantics for these systems opens the way for improved efficiency. Our algorithms have been implemented in NuSMV and perform well in practice (on standard case studies).

@inproceedings{formats2004-MS,
  author =              {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
  title =               {Symbolic Model Checking for Simply Timed Systems},
  editor =              {Lakhnech, Yassine and Yovine, Sergio},
  booktitle =           {{P}roceedings of the {J}oint {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'04) and {F}ormal
                         {T}echniques in {R}eal-Time and {F}ault-Tolerant
                         {S}ystems ({FTRTFT}'04)},
  acronym =             {{FORMATS-FTRTFT}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3253},
  pages =               {102-117},
  year =                {2004},
  month =               sep,
  doi =                 {10.1007/978-3-540-30206-3_9},
  abstract =            {We describe OBDD-based symbolic model checking
                         algorithms for simply-timed systems, i.e. finite
                         state graphs where transitions carry a duration.
                         These durations can be arbitrary natural numbers.
                         A~simple and natural semantics for these systems
                         opens the way for improved efficiency. Our
                         algorithms have been implemented in NuSMV and
                         perform well in practice (on standard case
                         studies).},
}
[MS04] Nicolas Markey et Philippe Schnoebelen. TSMV: Symbolic Model Checking for Simply Timed Systems. In QEST'04, pages 330-331. IEEE Comp. Soc. Press, septembre 2004.
Résumé

TSMV is an extension of NuSMV, the open-source symbolic model checker, aimed at dealing with timed versions of (models of) circuits, PLC controllers, protocols, etc. The underlying model is an extension of Kripke structures, where every transition carries an integer duration (possibly zero). This simple model supports efficient symbolic algorithms for RTCTL formulae.

@inproceedings{qest2004-MS,
  author =              {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
  title =               {{TSMV}: Symbolic Model Checking for Simply Timed
                         Systems},
  booktitle =           {{P}roceedings of the 1st {I}nternational
                         {C}onference on {Q}uantitative {E}valuation of
                         {S}ystems ({QEST}'04)},
  acronym =             {{QEST}'04},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {330-331},
  year =                {2004},
  month =               sep,
  doi =                 {10.1109/QEST.2004.1348052},
  abstract =            {TSMV is an extension of NuSMV, the open-source
                         symbolic model checker, aimed at dealing with timed
                         versions of (models of) circuits, PLC controllers,
                         protocols, etc. The underlying model is an extension
                         of Kripke structures, where every transition carries
                         an integer duration (possibly zero). This simple
                         model supports efficient symbolic algorithms for
                         RTCTL formulae.},
}
[MS04] Nicolas Markey et Philippe Schnoebelen. A PTIME-Complete Matching Problem for SLP-Compressed Words. Information Processing Letters 90(1):3-6. Elsevier, avril 2004.
Résumé

SLP-compressed words are words given by simple deterministic grammars called "straight-line programs". We prove that the problem of deciding whether an SLP-compressed word is recognized by a FSA is complete for polynomial-time.

@article{ipl90(1)-MS,
  author =              {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
  title =               {A {PTIME}-Complete Matching Problem for
                         {SLP}-Compressed Words},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {90},
  number =              {1},
  pages =               {3-6},
  year =                {2004},
  month =               apr,
  doi =                 {10.1016/j.ipl.2004.01.002},
  abstract =            {SLP-compressed words are words given by simple
                         deterministic grammars called {"}straight-line
                         programs{"}. We prove that the problem of deciding
                         whether an SLP-compressed word is recognized by a
                         FSA is complete for polynomial-time.},
}
[MS06] Nicolas Markey et Philippe Schnoebelen. Mu-calculus path checking. Information Processing Letters 97(6):225-230. Elsevier, mars 2006.
Résumé

We investigate the path model checking problem for the μ-calculus. Surprisingly, restricting to deterministic structures does not allow for more efficient model checking algorithm, as we prove that it can encode any instance of the standard model checking problem for the μ-calculus.

@article{ipl97(6)-MS,
  author =              {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
  title =               {Mu-calculus path checking},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {97},
  number =              {6},
  pages =               {225-230},
  year =                {2006},
  month =               mar,
  doi =                 {10.1016/j.ipl.2005.11.010},
  abstract =            {We investigate the path model checking problem for
                         the \(\mu\)-calculus. Surprisingly, restricting to
                         deterministic structures does not allow for more
                         efficient model checking algorithm, as we prove that
                         it can encode any instance of the standard model
                         checking problem for the \(\mu\)-calculus.},
}
[MSS86] David E. Muller, Ahmed Saoudi et Paul E. Schupp. Alternating Automata, the Weak Monadic Theory of the Tree, and its Complexity. In ICALP'86, Lecture Notes in Computer Science 226, pages 275-283. Springer-Verlag, juillet 1986.
@inproceedings{icalp1986-MSS,
  author =              {Muller, David E. and Saoudi, Ahmed and Schupp, Paul
                         E.},
  title =               {Alternating Automata, the Weak Monadic Theory of the
                         Tree, and its Complexity},
  editor =              {Kott, Laurent},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'86)},
  acronym =             {{ICALP}'86},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {226},
  pages =               {275-283},
  year =                {1986},
  month =               jul,
}
[MSS88] David E. Muller, Ahmed Saoudi et Paul E. Schupp. Weak Alternating Automata Give a Simple Explanation of Why Most Temporal Logics are Decidable in Exponential Time. In LICS'88, pages 422-427. IEEE Comp. Soc. Press, juillet 1988.
@inproceedings{lics1988-MSS,
  author =              {Muller, David E. and Saoudi, Ahmed and Schupp, Paul
                         E.},
  title =               {Weak Alternating Automata Give a Simple Explanation
                         of Why Most Temporal Logics are Decidable in
                         Exponential Time},
  booktitle =           {{P}roceedings of the 3rd {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'88)},
  acronym =             {{LICS}'88},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {422-427},
  year =                {1988},
  month =               jul,
}
[MST97] Masamichi Miyazaki, Ayumi Shinohara et Masayuki Takeda. An Improved Pattern-Matching Algorithm for Strings in Terms of Straight-Line Programs. In CPM'97, Lecture Notes in Computer Science 1264, pages 1-11. Springer-Verlag, juin 1997.
@inproceedings{cpm1997-MST,
  author =              {Miyazaki, Masamichi and Shinohara, Ayumi and Takeda,
                         Masayuki},
  title =               {An Improved Pattern-Matching Algorithm for Strings
                         in Terms of Straight-Line Programs},
  booktitle =           {{P}roceedings of the 8th {A}nnual {S}ymposium on
                         {C}ombinatorial {P}attern {M}atching ({CPM}'97)},
  acronym =             {{CPM}'97},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1264},
  pages =               {1-11},
  year =                {1997},
  month =               jun,
}
[MT99] Alexis Maciel et Denis Thérien. Efficient Threshold Circuits for Power Series. Information and Computation 152(1):62-73. Academic Press, juin 1999.
@article{icomp152(1)-MT,
  author =              {Maciel, Alexis and Th{\'e}rien, Denis},
  title =               {Efficient Threshold Circuits for Power Series},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {152},
  number =              {1},
  pages =               {62-73},
  year =                {1999},
  month =               jun,
}
[Mul99] Markus Müller-Olm. A Modal Fixpoint Logic with Chop. In STACS'99, Lecture Notes in Computer Science 1563, pages 510-520. Springer-Verlag, mars 1999.
@inproceedings{stacs1999-Mul,
  author =              {M{\"u}ller{-}Olm, Markus},
  title =               {A Modal Fixpoint Logic with Chop},
  editor =              {Meinel, {\relax Ch}ristoph and Tison, Sophie},
  booktitle =           {{P}roceedings of the 16th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'99)},
  acronym =             {{STACS}'99},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1563},
  pages =               {510-520},
  year =                {1999},
  month =               mar,
}
[Mun71] J. Ian Munro. Efficient Determination of the Transitive Closure of a Directed Graph. Information Processing Letters 1(2):56-58. Elsevier, juin 1971.
@article{ipl1(2)-Mun,
  author =              {Munro, J. Ian},
  title =               {Efficient Determination of the Transitive Closure of
                         a Directed Graph},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {1},
  number =              {2},
  pages =               {56-58},
  year =                {1971},
  month =               jun,
}
[MV14] Nicolas Markey et Steen Vester. Symmetry Reduction in Infinite Games with Finite Branching. In ATVA'14, Lecture Notes in Computer Science 8837, pages 281-296. Springer-Verlag, novembre 2014.
Résumé

Symmetry reductions have been applied extensively for the verification of finite-state concurrent systems and hardware designs using model-checking of temporal logics such as LTL, CTL and CTL*, as well as real-time and probabilistic-system model-checking. In this paper we extend the technique to handle infinite-state games on graphs with finite branching where the objectives of the players can be very general. As particular applications, it is shown that the technique can be applied to reduce the state space in parity games as well as when doing model-checking of the temporal logic ATL*.

@inproceedings{atva2014-MV,
  author =              {Markey, Nicolas and Vester, Steen},
  title =               {Symmetry Reduction in Infinite Games with Finite
                         Branching},
  editor =              {Cassez, Franck and Raskin, Jean-Fran{\c c}ois},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {S}ymposium on {A}utomated {T}echnology for
                         {V}erification and {A}nalysis ({ATVA}'14)},
  acronym =             {{ATVA}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8837},
  pages =               {281-296},
  year =                {2014},
  month =               nov,
  doi =                 {10.1007/978-3-319-11936-6_21},
  abstract =            {Symmetry reductions have been applied extensively
                         for the verification of finite-state concurrent
                         systems and hardware designs using model-checking of
                         temporal logics such as LTL, CTL and
                         CTL\textsuperscript{*}, as well as real-time and
                         probabilistic-system model-checking. In this paper
                         we extend the technique to handle infinite-state
                         games on graphs with finite branching where the
                         objectives of the players can be very general. As
                         particular applications, it is shown that the
                         technique can be applied to reduce the state space
                         in parity games as well as when doing model-checking
                         of the temporal logic ATL\textsuperscript{*}.},
}
[MVZ15] Pablo Muñoz, Nils Vortmeier et Thomas Zeume. Dynamic Graph Queries. Research Report 1512.05511, arXiv, Décembre 2015.
@techreport{arxiv-1512.05511,
  author =              {Mu{\~n}oz, Pablo and Vortmeier, Nils and Zeume,
                         Thomas},
  title =               {Dynamic Graph Queries},
  number =              {1512.05511},
  year =                {2015},
  month =               dec,
  institution =         {arXiv},
  type =                {Research Report},
}
[MW98] Helmut Melcher et Klaus Winkelmann. Controller synthesis for the `production cell' case study. In FMSP'98, pages 24-33. ACM Press, mars 1998.
@inproceedings{fmsp1998-MW,
  author =              {Melcher, Helmut and Winkelmann, Klaus},
  title =               {Controller synthesis for the `production cell' case
                         study},
  editor =              {Ardis, Mark},
  booktitle =           {{P}roceedings of the 2nd {W}orkshop on {F}ormal
                         {M}ethods in {S}oftware {P}ractice ({FMSP}'98)},
  acronym =             {{FMSP}'98},
  publisher =           {ACM Press},
  pages =               {24-33},
  year =                {1998},
  month =               mar,
}
[MW99] Angelika Mader et Hanno Wupper. Timed automaton models for simple programmable logic controllers. In ECRTS'99, pages 106-113. IEEE Comp. Soc. Press, juin 1999.
@inproceedings{ecrta1999-MW,
  author =              {Mader, Angelika and Wupper, Hanno},
  title =               {Timed automaton models for simple programmable logic
                         controllers},
  booktitle =           {{P}roceedings of the 11th {E}uromicro {C}onference
                         on {R}eal-{T}ime {S}ystems ({ECRTS}'99)},
  acronym =             {{ECRTS}'99},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {106-113},
  year =                {1999},
  month =               jun,
}
[MW03] Pierre McKenzie et Klaus W. Wagner. The Complexity of Membership Problems for Circuits over Sets of Natural Numbers. In STACS'03, Lecture Notes in Computer Science 2607, pages 571-582. Springer-Verlag, février 2003.
@inproceedings{stacs2003-MW,
  author =              {McKenzie, Pierre and Wagner, Klaus W.},
  title =               {The Complexity of Membership Problems for Circuits
                         over Sets of Natural Numbers},
  editor =              {Alt, Helmut and Habib, Michel},
  booktitle =           {{P}roceedings of the 20th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'03)},
  acronym =             {{STACS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2607},
  pages =               {571-582},
  year =                {2003},
  month =               feb,
}
[MW05] Anca Muscholl et Igor Walukiewicz. An NP-complete Fragment of LTL. International Journal of Foundations of Computer Science 16(4):743-753. Août 2005.
@article{ijfcs16(4)-MW,
  author =              {Muscholl, Anca and Walukiewicz, Igor},
  title =               {An {NP}-complete Fragment of~{LTL}},
  journal =             {International Journal of Foundations of Computer
                         Science},
  volume =              {16},
  number =              {4},
  pages =               {743-753},
  year =                {2005},
  month =               aug,
}
[MW10] Nicolas Markey et Jef Wijsen (eds.) Proceedings of the 17th International Symposium on Temporal Representation and Reasoning (TIME'10). IEEE Comp. Soc. Press, septembre 2010.
@proceedings{time2010-MW,
  title =               {{P}roceedings of the 17th {I}nternational
                         {S}ymposium on {T}emporal {R}epresentation and
                         {R}easoning ({TIME}'10)},
  editor =              {Markey, Nicolas and Wijsen, Jef},
  booktitle =           {{P}roceedings of the 17th {I}nternational
                         {S}ymposium on {T}emporal {R}epresentation and
                         {R}easoning ({TIME}'10)},
  acronym =             {{TIME}'10},
  publisher =           {IEEE Comp. Soc. Press},
  year =                {2010},
  month =               sep,
  doi =                 {10.1109/TIME.2010.4},
  url =                 {http://ieeexplore.ieee.org/xpl/ tocresult.jsp?
                         reload=true&isnumber=5601852},
}