M
[Mad80] Roger Maddux. The equational theory of CA3 is undecidable. Journal of Symbolic Logic 45(2):311-316. Association for Symbolic Logic, June 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, September 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, April 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, November 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, May 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, and J. Strother Moore (eds.), Computer Aided Reasoning: ACL2 Case Studies. Kluwer Academic, June 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 Press, September 1975.
@article{am102(2)-Mar,
  author =              {Martin, Donald A.},
  title =               {{B}orel Determinacy},
  publisher =           {Princeton University Press},
  journal =             {Annals of Mathematics},
  volume =              {102},
  number =              {2},
  pages =               {363-371},
  year =                {1975},
  month =               sep,
  doi =                 {10.2307/1971035},
}
[Mar00] Nicolas Markey. Complexité de la logique temporelle avec passé. Rapport de DEA, Lab. Spécification & Vérification, ENS Cachan, France, June 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, August 2002.
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.

@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, February 2003.
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.

@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, April 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. June 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, May 2004.
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.

@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, April 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] Pavel V. Martyugin. Complexity of Problems Concerning Carefully Synchronizing Words for PFA and Directing Words for NFA. In CSR'10, Lecture Notes in Computer Science 6072, pages 288-302. Springer-Verlag, June 2010.
@inproceedings{csr2010-Mar,
  author =              {Martyugin, Pavel V.},
  title =               {Complexity of Problems Concerning Carefully
                         Synchronizing Words for~{PFA} and Directing Words
                         for~{NFA}},
  editor =              {Ablayev, Farid M. and Mayr, Ernst W.},
  booktitle =           {{P}roceedings of the 5th {I}nternational {C}omputer
                         {S}cience {S}ymposium in {R}usia ({CSR}'10)},
  acronym =             {{CSR}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6072},
  pages =               {288-302},
  year =                {2010},
  month =               jun,
  doi =                 {10.1007/978-3-642-13182-0_27},
}
[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, January 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, June 2011.
Abstract

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, April 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, April 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, August 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 42nd {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},
}
[Mar23] Nicolas Markey. Computing the price of anarchy in atomic network congestion games (invited talk). In FORMATS'23, Lecture Notes in Computer Science 14138, pages 3-12. Springer-Verlag, September 2023.
Abstract

Network congestion games are a simple model for reasoning about routing problems in a network. They are a very popular topic in algorithmic game theory, and a huge amount of results about existence and (in)efficiency of equilibrium strategy profiles in those games have been obtained over the last 20 years.

In particular, the price of anarchy has been defined as an important notion for measuring the inefficiency of Nash equilibria. Generic bounds have been obtained for the price of anarchy over various classes of networks, but little attention has been put on the effective computation of this value for a given network. This talk presents recent results on this problem in different settings.

@inproceedings{formats2023-Mar,
  author =              {Markey, Nicolas},
  title =               {Computing the price of anarchy in atomic network
                         congestion games (invited~talk)},
  editor =              {Petrucci, Laure and Sproston, Jeremy},
  booktitle =           {{P}roceedings of the 21st {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'23)},
  acronym =             {{FORMATS}'23},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {14138},
  pages =               {3-12},
  year =                {2023},
  month =               sep,
  doi =                 {10.1007/978-3-031-42626-1_1},
  abstract =            {Network congestion games are a simple model for
                         reasoning about routing problems in a network. They
                         are a very popular topic in algorithmic game theory,
                         and a huge amount of results about existence and
                         (in)efficiency of equilibrium strategy profiles in
                         those games have been obtained over the last
                         20~years. \par In~particular, the price of anarchy
                         has been defined as an important notion for
                         measuring the inefficiency of Nash equilibria.
                         Generic bounds have been obtained for the price of
                         anarchy over various classes of networks, but little
                         attention has been put on the effective computation
                         of this value for a given network. This talk
                         presents recent results on this problem in different
                         settings.},
}
[Mat02] Radu Mateescu. Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems. Research Report 4430, INRIA Rhône-Alpes, Montbonnot, France, April 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, and 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},
  chapter =             {2},
  year =                {2002},
}
[MB08] Oded Maler and Grégory Batt. Approximating continuous systems by timed automata. In FMSB'08, Lecture Notes in Bioinformatics 5054, pages 77-89. Springer-Verlag, June 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, and 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, February 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, and 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, October 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 – 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, September 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, July 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, July 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, December 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, December 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 and 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, December 1989.
@book{Milner-CC1989,
  author =              {Milner, Robin},
  title =               {Communication and concurrency},
  publisher =           {Prentice Hall},
  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, March 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 Press, November 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 Press},
  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, August 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,
}
[Min99] Marius Minea. Partial-order reduction for verification of timed systems. PhD thesis, Computer Science Deparment, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA, December 1999.
@phdthesis{phd-minea,
  author =              {Minea, Marius},
  title =               {Partial-order reduction for verification of timed
                         systems},
  year =                {1999},
  month =               dec,
  school =              {Computer Science Deparment, Carnegie Mellon
                         University, Pittsburgh, Pennsylvania, USA},
}
[Mit05] David G. Mitchell. A SAT Solver Primer. EATCS Bulletin 85:112-132. EATCS, February 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, and Henrik Hulgaard. Difference Decision Diagrams. In CSL'99, Lecture Notes in Computer Science 1862, pages 111-125. Springer-Verlag, September 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 and Carroll C. Morgan. Games, Probability and the Quantitative μ-calculus. In LPAR'02, Lecture Notes in Computer Science 2514, pages 292-310. Springer-Verlag, October 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, and Y. Srinivas Ramakrishna. Completeness and Soundness of Axiomatizations for Temporal Logics without Next. Fundamenta Informaticae 21(4):257-305. IOS Press, October 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+20] Bastien Maubert, Aniello Murano, Sophie Pinchinat, François Schwarzentruber, and Silvia Stranieri. Dynamic Epistemic Logic Games with Epistemic Temporal Goals. Technical Report 2001-07141, arXiv, January 2020.
@techreport{arxiv2001.07141-MMPSS,
  author =              {Maubert, Bastien and Murano, Aniello and Pinchinat,
                         Sophie and Schwarzentruber, Fran{\c c}ois and
                         Stranieri, Silvia},
  title =               {Dynamic Epistemic Logic Games with Epistemic
                         Temporal Goals},
  number =              {2001-07141},
  year =                {2020},
  month =               jan,
  institution =         {arXiv},
}
[MMP+12] Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and 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, September 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, and Moshe Y. Vardi. Reasoning About Strategies: On the Model-Checking Problem. Research Report cs.LO/1112.6275, arXiv, December 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, and Moshe Y. Vardi. Reasoning About Strategies: On the Model-Checking Problem. ACM Transactions on Computational Logic 15(4):34:1-34:47. ACM Press, August 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, and Moshe Y. Vardi. Reasoning About Strategies: On the Satisfiability Problem. Logical Methods in Computer Science 13(1). March 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, and Luigi Sauro. On the Boundary of Behavioral Strategies. In LICS'13, pages 263-272. IEEE Comp. Soc. Press, June 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, and Luigi Sauro. A Behavioral Hierarchy of Strategy Logic. In CLIMA'14, Lecture Notes in Artificial Intelligence 8624, pages 148-165. Springer-Verlag, August 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, and Heribert Vollmer. The Complexity of Satisfiability for Fragmentf of CTL and CTL*. In RP'08, pages 201-213. September 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, and Moshe Y. Vardi. Reasoning about strategies. In FSTTCS'10, Leibniz International Proceedings in Informatics 8, pages 133-144. Leibniz-Zentrum für Informatik, December 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, and 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, April 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 and John von Neumann. The Theory of Games and Economic Behavior. Princeton University Press, 1947.
@book{MvN-game1947,
  author =              {Morgenstern, Oskar and von~Neumann, John},
  title =               {The Theory of Games and Economic Behavior},
  publisher =           {Princeton University Press},
  year =                {1947},
}
[MN04] Oded Maler and Dejan Nickovic. Monitoring Temporal Properties of Continuous Signals. In FORMATS-FTRTFT'04, Lecture Notes in Computer Science 3253, pages 152-166. Springer-Verlag, September 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 and 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, March 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, and Amir Pnueli. From MITL to Timed Automata. In FORMATS'06, Lecture Notes in Computer Science 4202, pages 274-289. Springer-Verlag, September 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 and Mitsunori Ogihara. Sparse Hard Sets for P. In Ding-zhu Du and 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 and Ennio Ottaviani. A traffic management system for real-time traffic optimisation in railways. Transportation Research Part B: Methodological 41(2):246-274. Elsevier, February 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, November 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},
}
[Moo56] Edward F. Moore. Gedanken-Experiments on Sequential Machines. In Claude E. Shannon and John McCarthy (eds.), Automata Studies, Annals of Mathematics Studies 34, pages 129-153. Princeton University Press, 1956.
@incollection{am34-Moo,
  author =              {Moore, Edward F.},
  title =               {Gedanken-Experiments on Sequential Machines},
  editor =              {Shannon, Claude E. and McCarthy, John},
  booktitle =           {Automata Studies},
  publisher =           {Princeton University Press},
  series =              {Annals of Mathematics Studies},
  volume =              {34},
  pages =               {129-153},
  year =                {1956},
  doi =                 {10.1515/9781400882618-006},
}
[Moo96] Cristopher Moore. Recursion Theory on the Reals and Continuous-Time Computation. Theoretical Computer Science 162(1):23-44. Elsevier, August 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 and Amir Pnueli. The Anchored Version of the Temporal Framework. In REX'88, Lecture Notes in Computer Science 354, pages 201-284. Springer-Verlag, May 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 and Amir Pnueli. Tight Bounds on the Complexity of Cascaded Decomposition of Automata. In FOCS'90, pages 672-682. IEEE Comp. Soc. Press, October 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 and Amir Pnueli. A Hierarchy of Temporal Properties. In PODC'90, pages 377-410. ACM Press, August 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 and 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 and 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 and Giovanni Pighizzini. Complementing Unary Nondeterministic Automata. Theoretical Computer Science 330(2):349-360. Elsevier, February 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, and 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, March 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,
}
[MPS19] Bastien Maubert, Sophie Pinchinat, and François Schwarzentruber. Reachability Games in Dynamic Epistemic Logic. In IJCAI'19, pages 499-505. IJCAI organization, August 2019.
@inproceedings{ijcai2019-MPS,
  author =              {Maubert, Bastien and Pinchinat, Sophie and
                         Schwarzentruber, Fran{\c c}ois},
  title =               {Reachability Games in Dynamic Epistemic Logic},
  editor =              {Kraus, Sarit},
  booktitle =           {{P}roceedings of the 28th {I}nternational {J}oint
                         {C}onference on {A}rtificial {I}ntelligence
                         ({IJCAI}'19)},
  acronym =             {{IJCAI}'19},
  publisher =           {IJCAI organization},
  pages =               {499-505},
  year =                {2019},
  month =               aug,
  doi =                 {10.24963/ijcai.2019/71},
}
[MPS+21] Bastien Maubert, Sophie Pinchinat, François Schwarzentruber, and Silvia Stranieri. Concurrent Games in Dynamic Epistemic Logic. In IJCAI'20, pages 1877-1883. IJCAI organization, January 2021.
@inproceedings{ijcai2020-MPSS,
  author =              {Maubert, Bastien and Pinchinat, Sophie and
                         Schwarzentruber, Fran{\c c}ois and Stranieri,
                         Silvia},
  title =               {Concurrent Games in Dynamic Epistemic Logic},
  editor =              {Bessiere, Christian},
  booktitle =           {{P}roceedings of the 29th {I}nternational {J}oint
                         {C}onference on {A}rtificial {I}ntelligence
                         ({IJCAI}'20)},
  acronym =             {{IJCAI}'20},
  publisher =           {IJCAI organization},
  pages =               {1877-1883},
  year =                {2021},
  month =               jan,
  doi =                 {10.24963/ijcai.2020/260},
}
[MR95] Rajeev Motwani and Prabhakar Raghavan. Randomized algorithms. Cambridge University Press, 1995.
@book{MR95-RA,
  author =              {Motwani, Rajeev and Raghavan, Prabhakar},
  title =               {Randomized algorithms},
  publisher =           {Cambridge University Press},
  year =                {1995},
}
[MR99] Faron Moller and Alexander Rabinovich. On the expressive power of CTL*. In LICS'99, pages 360-368. IEEE Comp. Soc. Press, July 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 and Alexander Rabinovich. Counting on CTL*: on the expressive power of monadic path logic. Information and Computation 184(1):147-159. Academic Press, July 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 and 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, August 2004.
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 (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 and Jean-François Raskin. Model Checking Restricted Sets of Timed Paths. Theoretical Computer Science 358(2-3):273-292. Elsevier, August 2006.
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 (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, and 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., August 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, and V. Vinay. Circuits and Context-free Languages. In COCOON'99, Lecture Notes in Computer Science 1627, pages 194-203. Springer-Verlag, July 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, and Ingo Wegener. On Converting CNF to DNF. Theoretical Computer Science 347(1-2):325-335. Elsevier, November 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 and Larry J. Stockmeyer. The Equivalence Problem for Regular Expressions with Squaring Requires Exponential Space. In FOCS'72, pages 125-129. IEEE Comp. Soc. Press, October 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 and 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 and Paul E. Schupp. Alternating Automata on Infinite Trees. Theoretical Computer Science 54(2-3):267-276. Elsevier, October 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 and 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, April 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,
}
[MS96] Dov Monderer and Lloyd S. Shapley. Potential Games. Games and Economic Behavior 14(1):124-143. May 1996.
@article{geb14(1)-MS,
  author =              {Monderer, Dov and Shapley, Lloyd S.},
  title =               {Potential Games},
  journal =             {Games and Economic Behavior},
  volume =              {14},
  number =              {1},
  pages =               {124-143},
  year =                {1996},
  month =               may,
  doi =                 {10.1006/game.1996.0044},
}
[MS97] Oded Maler and Ludwig Staiger. On Syntactic Congruences fpr ω-languages. Theoretical Computer Science 183(1):93-112. Elsevier, August 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 and Henny Sipma. Alternating the Temporal Picture for Safety. In ICALP'00, Lecture Notes in Computer Science 1853, pages 429-450. Springer-Verlag, July 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 and 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, April 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 and Philippe Schnoebelen. Model Checking a Path (Preliminary Report). In CONCUR'03, Lecture Notes in Computer Science 2761, pages 251-265. Springer-Verlag, August 2003.
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.

@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 and Philippe Schnoebelen. Symbolic Model Checking for Simply Timed Systems. In FORMATS-FTRTFT'04, Lecture Notes in Computer Science 3253, pages 102-117. Springer-Verlag, September 2004.
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).

@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 and Philippe Schnoebelen. TSMV: Symbolic Model Checking for Simply Timed Systems. In QEST'04, pages 330-331. IEEE Comp. Soc. Press, September 2004.
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.

@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 and Philippe Schnoebelen. A PTIME-Complete Matching Problem for SLP-Compressed Words. Information Processing Letters 90(1):3-6. Elsevier, April 2004.
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.

@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 and Philippe Schnoebelen. Mu-calculus path checking. Information Processing Letters 97(6):225-230. Elsevier, March 2006.
Abstract

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.},
}
[MS07] Marios Mavronicolas and Paul G. Spirakis. The price of selfish routing. Algorithmica 48(1):91-126. Springer-Verlag, May 2007.
@article{alga48(1)-MS,
  author =              {Mavronicolas, Marios and Spirakis, Paul G.},
  title =               {The price of selfish routing},
  publisher =           {Springer-Verlag},
  journal =             {Algorithmica},
  volume =              {48},
  number =              {1},
  pages =               {91-126},
  year =                {2007},
  month =               may,
  doi =                 {10.1007/s00453-006-0056-1},
}
[MS12] Carol A. Meyers and Andreas S. Schulz. The complexity of welfare maximization in congestion games. Networks 59(2):252-260. John Wiley & Sons, March 2012.
@article{netw59(2)-MS,
  author =              {Meyers, Carol A. and Schulz, Andreas S.},
  title =               {The~complexity of welfare maximization in congestion
                         games},
  publisher =           {John Wiley \& Sons},
  journal =             {Networks},
  volume =              {59},
  number =              {2},
  pages =               {252-260},
  year =                {2012},
  month =               mar,
  doi =                 {10.1002/net.20439},
}
[MSS86] David E. Muller, Ahmed Saoudi, and 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, July 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, and 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, July 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, and 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, June 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 and Denis Thérien. Efficient Threshold Circuits for Power Series. Information and Computation 152(1):62-73. Academic Press, June 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, March 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, June 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 and Steen Vester. Symmetry Reduction in Infinite Games with Finite Branching. In ATVA'14, Lecture Notes in Computer Science 8837, pages 281-296. Springer-Verlag, November 2014.
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*, 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, and Thomas Zeume. Dynamic Graph Queries. Research Report 1512.05511, arXiv, December 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 and Klaus Winkelmann. Controller synthesis for the `production cell' case study. In FMSP'98, pages 24-33. ACM Press, March 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 and Hanno Wupper. Timed automaton models for simple programmable logic controllers. In ECRTS'99, pages 106-113. IEEE Comp. Soc. Press, June 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 and 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, February 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 and Igor Walukiewicz. An NP-complete Fragment of LTL. International Journal of Foundations of Computer Science 16(4):743-753. August 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 and Jef Wijsen (eds.) Proceedings of the 17th International Symposium on Temporal Representation and Reasoning (TIME'10). IEEE Comp. Soc. Press, September 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},
}
List of authors