Nicolas Markey

@inproceedings{concur1990-vGl,
  author =              {van Glabbeek, Rob},
  title =               {The linear-time--branching-time spectrum},
  editor =              {Baeten, Jos C. M. and Klop, Jan Willem},
  booktitle =           {{P}roceedings of the 1st {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'90)},
  acronym =             {{CONCUR}'90},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {458},
  pages =               {278-297},
  year =                {1990},
  month =               aug,
}

@inproceedings{apl1977-Gab,
  author =              {Gabbay, Dov M.},
  title =               {Expressive Functional Completeness in Tense Logic},
  editor =              {M{\"o}nnich, Uwe},
  booktitle =           {Aspects of Philosophical Logic},
  publisher =           {Springer-Verlag},
  series =              {Synthese Library},
  volume =              {147},
  pages =               {91-117},
  year =                {1981},
  month =               dec,
  confyear =            {1977},
}

@inproceedings{tls1987-Gab,
  author =              {Gabbay, Dov M.},
  title =               {The Declarative Past and Imperative Future:
                         Executable Temporal Logic for Interactive Systems},
  editor =              {Banieqbal, Behnam and Barringer, Howard and Pnueli,
                         Amir},
  booktitle =           {{P}roceedings of the 1st {C}onference on {T}emporal
                         {L}ogic in {S}pecification ({TLS}'87)},
  acronym =             {{TLS}'87},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {398},
  pages =               {409-448},
  year =                {1989},
  confyear =            {1987},
  confmonth =           {4},
}

@article{acta6()-Gal,
  author =              {Galil, Zvi},
  title =               {Hierarchies of Complete Problems},
  publisher =           {Springer-Verlag},
  journal =             {Acta Informatica},
  volume =              {6},
  pages =               {77-88},
  year =                {1976},
}

@inproceedings{fossacs2015-Gan,
  author =              {Ganardi, Moses},
  title =               {Parity Games of Bounded Tree- and Clique-Width},
  editor =              {Pitts, Andrew},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'15)},
  acronym =             {{FoSSaCS}'15},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9034},
  pages =               {390-404},
  year =                {2015},
  month =               apr,
  doi =                 {10.1007/978-3-662-46678-0_25},
}

@phdthesis{phd-ganguly,
  author =              {Ganguly, Ritam},
  title =               {Runtime verification of distributed systems},
  year =                {2023},
  school =              {Michigan State University, USA},
  type =                {{PhD} thesis},
}

@phdthesis{phd-gardy,
  author =              {Gardy, Patrick},
  title =               {Semantics of Strategy Logic},
  year =                {2017},
  month =               jun,
  school =              {Lab.~Sp\'ecification \& V\'erification, Univ.
                         Paris-Saclay, France},
  type =                {{PhD} thesis},
}

Résumé

Energy consumption problems (e.g., electric vehicles charging) are very related to communication problems. The "water-filling" algorithm can be used, but it is not robust w.r.t. the noise of the "non-flexible", i.e. not-controllable, energy consumption forecasting. We propose a robust algorithm using the probabilistic model-checker PRISM, to exploit the idea of discretizing the consumption action (as for a modulation to small constellation) and the dynamic structure of the problem in a Markov-decision-process model.

@inproceedings{gretsi2017-GBBLM,
  author =              {Gonz{\'a}lez, Mauricio and Beaude, Olivier and
                         Bouyer, Patricia and Lasaulce, Samson and Markey,
                         Nicolas},
  title =               {Strat{\'e}gies d'ordonnancement de consommation
                         d'{\'e}nergie en pr{\'e}sence d'information
                         imparfaite de pr{\'e}vision},
  booktitle =           {{A}ctes du 26{\`e}me {C}olloque du {G}roupe
                         d'{\'E}tudes du {T}raitement du {S}ignal et des
                         {I}mages ({GRETSI}'17)},
  acronym =             {{GRETSI}'17},
  year =                {2017},
  month =               sep,
  abstract =            {Energy consumption problems (e.g., electric vehicles
                         charging) are very related to communication
                         problems. The "water-filling" algorithm can be used,
                         but it is not robust w.r.t. the noise of the
                         "non-flexible", i.e. not-controllable, energy
                         consumption forecasting. We~propose a robust
                         algorithm using the probabilistic model-checker
                         PRISM, to exploit the idea of discretizing the
                         consumption action (as~for a modulation to small
                         constellation) and the dynamic structure of the
                         problem in a Markov-decision-process model.},
}

@inproceedings{fmcad2002-GBD,
  author =              {Ganesh, Vijay and Berezin, Sergey and Dill, David
                         L.},
  title =               {Deciding {P}resburger Arithmetic by Model Checking
                         and Comparisons with Other Methods},
  editor =              {Aagaard, Mark D. and O'Leary, John W.},
  booktitle =           {{P}roceedings of the 4th {I}nternational
                         {C}onference on {F}ormal {M}ethods in
                         {C}omputer-{A}ided {D}esign ({FMCAD}'02)},
  acronym =             {{FMCAD}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2517},
  pages =               {171-398},
  year =                {2002},
  month =               nov,
}

Résumé

This article focuses on the existence and synthesis of strategies in double-weighted Markov decision processes, which satisfy both a probability constraint over a weighted reachability condition, and a quantitative constraint on the expected value of a random variable defined using another reachability condition. This work generalizes a scheduling problem for energy consumption (typically the problem of charging electric vehicles). We study the set of values of a parameter (a threshold) for which the problem has a solution, and show how a partial characterization of this set can be obtained via two sequences of optimization problems. We also discuss the completeness and feasibility of the resulting approach.

@inproceedings{gretsi2019-GBLM,
  author =              {Gonz{\'a}lez, Mauricio and Bouyer, Patricia and
                         Lasaulce, Samson and Markey, Nicolas},
  title =               {Optimisation en pr\'esence de contraintes en
                         probabilit\'es et processus markoviens
                         contr\^ol\'es},
  booktitle =           {{A}ctes du 27{\`e}me {C}olloque du {G}roupe
                         d'{\'E}tudes du {T}raitement du {S}ignal et des
                         {I}mages ({GRETSI}'19)},
  acronym =             {{GRETSI}'19},
  year =                {2019},
  month =               aug,
  abstract =            {This article focuses on the existence and synthesis
                         of strategies in double-weighted Markov decision
                         processes, which satisfy both a probability
                         constraint over a weighted reachability condition,
                         and a quantitative constraint on the expected value
                         of a random variable defined using another
                         reachability condition. This work generalizes a
                         scheduling problem for energy consumption (typically
                         the problem of charging electric vehicles). We~study
                         the set of values of a parameter (a~threshold) for
                         which the problem has a solution, and show how a
                         partial characterization of this set can be obtained
                         via two sequences of optimization problems. We~also
                         discuss the completeness and feasibility of the
                         resulting approach.},
}

Résumé

Strategy Logic (SL) is a very expressive temporal logic for specifying and verifying properties of multi-agent systems: in SL, one can quantify over strategies, assign them to agents, and express LTL properties of the resulting plays. Such a powerful framework has two drawbacks: first, model checking SL has non-elementary complexity; second, the exact semantics of SL is rather intricate, and may not correspond to what is expected. In this paper, we focus on strategy dependences in SL, by tracking how existentially-quantified strategies in a formula may (or may not) depend on other strategies selected in the formula, revisiting the approach of [Mogavero et al., Reasoning about strategies: On the model-checking problem, 2014]. We explain why elementary dependences, as defined by Mogavero et al., do not exactly capture the intended concept of behavioral strategies. We address this discrepancy by introducing timeline dependences, and exhibit a large fragment of SL for which model checking can be performed in 2EXPTIME under this new semantics.

@inproceedings{stacs2018-GBM,
  author =              {Gardy, Patrick and Bouyer, Patricia and Markey,
                         Nicolas},
  title =               {Dependences in Strategy Logic},
  editor =              {Niedermeier, Rolf and Vall{\'e}e, Brigitte},
  booktitle =           {{P}roceedings of the 35th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'18)},
  acronym =             {{STACS}'18},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {96},
  pages =               {34:1-34:14},
  year =                {2018},
  month =               feb,
  doi =                 {10.4230/LIPIcs.STACS.2018.34},
  abstract =            {Strategy Logic~(\textsf{SL}) is a very expressive
                         temporal logic for specifying and verifying
                         properties of multi-agent systems: in~\textsf{SL},
                         one can quantify over strategies, assign them to
                         agents, and express \textsf{LTL} properties of the
                         resulting plays. Such a powerful framework has two
                         drawbacks: first, model checking \textsf{SL} has
                         non-elementary complexity; second, the exact
                         semantics of \textsf{SL} is rather intricate, and
                         may not correspond to what is expected. In~this
                         paper, we~focus on \emph{strategy dependences}
                         in~\textsf{SL}, by tracking how
                         existentially-quantified strategies in a formula may
                         (or~may~not) depend on other strategies selected in
                         the formula, revisiting the approach of~[Mogavero
                         \emph{et~al.}, Reasoning about strategies: On~the
                         model-checking problem,~2014]. We~explain why
                         \emph{elementary} dependences, as defined by
                         Mogavero~\emph{et~al.}, do not exactly capture the
                         intended concept of behavioral strategies.
                         We~address this discrepancy by introducing
                         \emph{timeline} dependences, and exhibit a large
                         fragment of \textsf{SL} for which model checking can
                         be performed in \textsf{2EXPTIME} under this new
                         semantics.},
}

Résumé

Strategy Logic (SL) is a very expressive temporal logic for specifying and verifying properties of multi-agent systems: in SL, one can quantify over strategies, assign them to agents, and express LTL properties of the resulting plays. Such a powerful framework has two drawbacks: first, model checking SL has non-elementary complexity; second, the exact semantics of SL is rather intricate, and may not correspond to what is expected. In this paper, we focus on strategy dependences in SL, by tracking how existentially-quantified strategies in a formula may (or may not) depend on other strategies selected in the formula, revisiting the approach of [Mogavero et al., Reasoning about strategies: On the model-checking problem, 2014]. We explain why elementary dependences, as defined by Mogavero et al., do not exactly capture the intended concept of behavioral strategies. We address this discrepancy by introducing timeline dependences, and exhibit a large fragment of SL for which model checking can be performed in 2EXPTIME under this new semantics.

@article{tocsys64(3)-GBM,
  author =              {Gardy, Patrick and Bouyer, Patricia and Markey,
                         Nicolas},
  title =               {Dependences in Strategy Logic},
  publisher =           {Springer-Verlag},
  journal =             {Theory of Computing Systems},
  volume =              {64},
  number =              {3},
  pages =               {467-507},
  year =                {2020},
  month =               apr,
  doi =                 {10.1007/s00224-019-09926-y},
  abstract =            {Strategy Logic~(\textsf{SL}) is a very expressive
                         temporal logic for specifying and verifying
                         properties of multi-agent systems: in~\textsf{SL},
                         one can quantify over strategies, assign them to
                         agents, and express \textsf{LTL} properties of the
                         resulting plays. Such a powerful framework has two
                         drawbacks: first, model checking \textsf{SL} has
                         non-elementary complexity; second, the exact
                         semantics of \textsf{SL} is rather intricate, and
                         may not correspond to what is expected. In~this
                         paper, we~focus on \emph{strategy dependences}
                         in~\textsf{SL}, by tracking how
                         existentially-quantified strategies in a formula may
                         (or~may~not) depend on other strategies selected in
                         the formula, revisiting the approach of~[Mogavero
                         \emph{et~al.}, Reasoning about strategies: On~the
                         model-checking problem,~2014]. We~explain why
                         \emph{elementary} dependences, as defined by
                         Mogavero~\emph{et~al.}, do not exactly capture the
                         intended concept of behavioral strategies.
                         We~address this discrepancy by introducing
                         \emph{timeline} dependences, and exhibit a large
                         fragment of \textsf{SL} for which model checking can
                         be performed in \textsf{2EXPTIME} under this new
                         semantics.},
}

@inproceedings{fmcad2004-GC,
  author =              {Gurfinkel, Arie and Chechik, Marsha},
  title =               {Extending extended vacuity},
  editor =              {Hu, Alan J. and Martin, Andrew K.},
  booktitle =           {{P}roceedings of the 5th {I}nternational
                         {C}onference on {F}ormal {M}ethods in
                         {C}omputer-{A}ided {D}esign ({FMCAD}'04)},
  acronym =             {{FMCAD}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3312},
  pages =               {306-321},
  year =                {2004},
  month =               nov,
  doi =                 {10.1007/978-3-540-30494-4_22},
}

@inproceedings{charme2005-GC,
  author =              {Gurfinkel, Arie and Chechik, Marsha},
  title =               {How Thorough Is Thorough Enough?},
  editor =              {Borrine, Dominique and Paul, Wolfgang J.},
  booktitle =           {{P}roceedings of the 13th {C}orrect {H}ardware
                         {D}esign and {V}erification {M}ethods ({CHARME}'05)},
  acronym =             {{CHARME}'05},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3725},
  pages =               {65-80},
  year =                {2005},
  month =               oct,
}

@techreport{arxiv-cs.LO/1002.4616,
  author =              {Gurfinkel, Arie and Chechik, Marsha},
  title =               {Robust Vacuity for Branching Temporal Logic},
  number =              {cs.LO/1002.4616},
  year =                {2010},
  month =               feb,
  institution =         {arXiv},
  type =                {Research Report},
}

@article{tocl13(1)-GC,
  author =              {Gurfinkel, Arie and Chechik, Marsha},
  title =               {Robust Vacuity for Branching Temporal Logic},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {13},
  number =              {1},
  year =                {2012},
  month =               jan,
  doi =                 {10.1145/2071368.2071369},
}

@inproceedings{cats2001-GC,
  author =              {Gerdsmeier, Thorsten and Cardell-Oliver, Rachel},
  title =               {Analysis of Scheduling Behaviour using Generic Timed
                         Automata},
  editor =              {Fidge, Colin},
  booktitle =           {Computing: The Australasian Theory Symposium
                         ({CATS}'01)},
  acronym =             {{CATS}'01},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {42},
  year =                {2001},
  month =               jan,
}

@article{tcs353(1-3)-GvD,
  author =              {Goranko, Valentin and van Drimmelen, Govert},
  title =               {Complete Axiomatization and decidability of
                         Alternating-time Temporal Logic},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {353},
  number =              {1-3},
  pages =               {93-117},
  year =                {2006},
  month =               mar,
}

@inproceedings{clima2012-GD,
  author =              {Guelev, Dimitar P. and Dima, C{\u a}t{\u a}lin},
  title =               {Epistemic {ATL} with Perfect Recall, Past and
                         Strategy Contexts},
  editor =              {Fisher, Michael and van der Torre, Leendert W. N.
                         and Dastani, Mehdi and Governatori, Guido},
  booktitle =           {{P}roceedings of the 13th {I}nternational {W}orkshop
                         on {C}omputational {L}ogic in {M}ulti-{A}gent
                         {S}ystems ({CLIMA}'12)},
  acronym =             {{CLIMA}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Artificial Intelligence},
  volume =              {7486},
  pages =               {77-93},
  year =                {2012},
  month =               aug,
  doi =                 {10.1007/978-3-642-32897-8_7},
}

@inproceedings{rv2001-Gei,
  author =              {Geilen, Marc C.W.},
  title =               {On the Construction of Monitors for Temporal Logic
                         Properties},
  editor =              {Havelund, Klaus and Ro{\c{s}}u, Grigore},
  booktitle =           {{P}roceedings of the 1st {I}nternational {W}orkshop
                         on {R}untime {V}erification ({RV}'01)},
  acronym =             {{RV}'01},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {55},
  number =              {2},
  year =                {2001},
  month =               jul,
}

@inproceedings{icalp2013-Gel,
  author =              {Gelderie, Marcus},
  title =               {Strategy Composition in Compositional Games},
  editor =              {Fomin, Fedor V. and Freivalds, Rusins and
                         Kwiatkowska, Marta and Peleg, David},
  booktitle =           {{P}roceedings of the 40th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'13)~-- Part~{II}},
  acronym =             {{ICALP}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7966},
  pages =               {263-274},
  year =                {2013},
  month =               jul,
  doi =                 {10.1007/978-3-642-39212-2_25},
}

@phdthesis{phd-gelderie,
  author =              {Gelderie, Marcus},
  title =               {Strategy Machines~-- Representation and Complexity
                         of Strategies in Infinite Games},
  year =                {2014},
  month =               feb,
  school =              {RWTH Aachen, Germany},
  type =                {{PhD} thesis},
}

@inproceedings{mfcs1999-GGR,
  author =              {G{\k a}sieniec, Leszek and Gibbons, Alan and Rytter,
                         Wojciech},
  title =               {Efficiency of Fast Parallel Pattern-Searching in
                         Highly Compressed Texts},
  editor =              {Kutylowski, Miroslaw and Pacholski, Leszek and
                         Wierzbicki, Tomasz},
  booktitle =           {{P}roceedings of the 24th {I}nternational
                         {S}ymposium on {M}athematical {F}oundations of
                         {C}omputer {S}cience ({MFCS}'99)},
  acronym =             {{MFCS}'99},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1672},
  pages =               {48-58},
  year =                {1999},
  month =               sep,
}

@inproceedings{tark2003-GGS,
  author =              {Gottlob, Georg and Greco, Gianluigi and Scarcello,
                         Francesco},
  title =               {Pure {N}ash Equilibria: Hard and Easy Games},
  editor =              {Halpern, Joseph Y. and Tennenholtz, Moshe},
  booktitle =           {{P}roceedings of the 9th {C}onference on
                         {T}heoretical {A}spects of {R}ationality and
                         {K}nowledge ({TARK}'03)},
  acronym =             {{TARK}'03},
  publisher =           {ACM Press},
  pages =               {215-230},
  year =                {2003},
  month =               jun,
}

@inproceedings{stoc1982-GH,
  author =              {Gurevich, Yuri and Harrington, Leo},
  title =               {Trees, automata and games},
  booktitle =           {{P}roceedings of the 14th {A}nnual {ACM} {S}ymposium
                         on the {T}heory of {C}omputing ({STOC}'82)},
  acronym =             {{STOC}'82},
  publisher =           {ACM Press},
  pages =               {60-65},
  year =                {1982},
  month =               may,
}

@incollection{HATC1998-GH,
  author =              {Greenlaw, Raymond and Hoover, H. James},
  title =               {Parallel Computation: Models and Complexity Issues},
  editor =              {Atallah, Mikhail J.},
  booktitle =           {Handbook of Algorithms and Theory of Computation},
  publisher =           {CRC Press},
  chapter =             {48},
  year =                {1998},
  month =               nov,
}

@inproceedings{soda2010-GH,
  author =              {Gimbert, Hugo and Horn, Florian},
  title =               {Solving simple stochastic tail games},
  booktitle =           {{P}roceedings of the 21st {A}nnual {ACM}-{SIAM}
                         {S}ymposium on {D}iscrete {A}lgorithms ({SODA}'10)},
  acronym =             {{SODA}'10},
  publisher =           {Society for Industrial and Applied Math.},
  pages =               {847-862},
  year =                {2010},
  month =               jan,
  doi =                 {10.1137/1.9781611973075.69},
}

@inproceedings{hart1997-GHJ,
  author =              {Gupta, Vineet and Henzinger, Thomas A. and
                         Jagadeesan, Radha},
  title =               {Robust Timed Automata},
  editor =              {Maler, Oded},
  booktitle =           {{P}roceedings of the 1997 {I}nternational {W}orkshop
                         on {H}ybrid and {R}eal-Time {S}ystems ({HART}'97)},
  acronym =             {{HART}'97},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1201},
  pages =               {331-345},
  year =                {1997},
  month =               mar,
}

@inproceedings{wine2008-GHKSW,
  author =              {Gassner, Elisabeth and Hatzl, Johannes and Krumke,
                         Sven O. and Sperber, Heike and Woeginger, Gerhard
                         J.},
  title =               {How hard is it to find extreme {N}ash equilibria in
                         network congestion games?},
  editor =              {Papadimitriou, {\relax Ch}ristos H. and Zhang,
                         Shuzhong},
  booktitle =           {{P}roceedings of the 4th {I}nternational {W}orkshop
                         on {I}nternet and {N}etwork {E}conomics ({WINE}'08)},
  acronym =             {{WINE}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5385},
  pages =               {82-93},
  year =                {2008},
  month =               dec,
  doi =                 {10.1007/978-3-540-92185-1_17},
}

@inproceedings{icalp2010-GHOW,
  author =              {G{\"o}ller, Stefan and Haase, Christoph and
                         Ouaknine, Jo{\"e}l and Worrell, James},
  title =               {Model Checking Succinct and Parametric One-Counter
                         Automata},
  editor =              {Abramsky, Samson and Gavoille, Cyril and Kirchner,
                         Claude and Meyer auf der Heide, Friedhelm and
                         Spirakis, Paul G.},
  booktitle =           {{P}roceedings of the 37th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'10)~-- Part~{II}},
  acronym =             {{ICALP}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6199},
  pages =               {575-586},
  year =                {2010},
  month =               jul,
  doi =                 {10.1007/978-3-642-14162-1_48},
}

@inproceedings{concur2017-GHPW,
  author =              {Gutierrez, Julian and Harrenstein, Paul and Perelli,
                         Giuseppe and Wooldridge, Michael},
  title =               {{N}ash Equilibrium and Bisimulation Invariance},
  editor =              {Meyer, Roland and Nestmann, Uwe},
  booktitle =           {{P}roceedings of the 28th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'17)},
  acronym =             {{CONCUR}'17},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {85},
  pages =               {17:1-17:16},
  year =                {2017},
  month =               sep,
  doi =                 {10.4230/LIPIcs.CONCUR.2017.17},
}

@book{GHR95,
  author =              {Greenlaw, Raymond and Hoover, H. James and Ruzzo,
                         Walter L.},
  title =               {Limits to Parallel Computation: {P}-Completeness
                         Theory},
  publisher =           {Oxford University Press},
  year =                {1995},
}

@phdthesis{phd-gimbert,
  author =              {Gimbert, Hugo},
  title =               {Jeux positionnels},
  year =                {2006},
  month =               dec,
  school =              {Lab.~Informatique Algorithmique: Fondements et
                         Applications, Universit{\'e} Paris~7, France},
  type =                {Th\`ese de doctorat},
}

@article{jacm5(3)-Gin,
  author =              {Ginsburg, Seymour},
  title =               {On~the Length of the Smallest Uniform Experiment
                         which Distinguishes the Terminal States of a
                         Machine},
  publisher =           {ACM Press},
  journal =             {Journal of the~ACM},
  volume =              {5},
  number =              {3},
  pages =               {266-280},
  year =                {1958},
  month =               jul,
  doi =                 {10.1145/320932.320938},
}

@inproceedings{adhs2012-Gir,
  author =              {Girard, Antoine},
  title =               {Low-complexity switching controllers for safety
                         using symbolic models},
  editor =              {Giua, Alessandro and Silva, Manuel and Heemels,
                         Maurice and De{~}Schutter, Bart},
  booktitle =           {Proceedings of the 4th {IFAC} conference on
                         {A}nalysis and {D}esign of {H}ybrid {S}ystems
                         ({ADHS}'12)},
  acronym =             {{ADHS}'12},
  publisher =           {International Federation of Automatic Control},
  year =                {2012},
  month =               jun,
}

@book{GJ79,
  author =              {Garey, Michael R. and Johnson, David S.},
  title =               {Computers and Intractability: A Guide to the Theory
                         of {NP}-Completeness},
  publisher =           {W.~H. Freeman~\&~Co.},
  year =                {1979},
}

@article{synthese139(2)-GJ,
  author =              {Goranko, Valentin and Jamroga, Wojciech},
  title =               {Comparing Semantics of Logics for Multi-agent
                         Systems},
  publisher =           {Springer-Verlag},
  journal =             {Synthese},
  volume =              {139},
  number =              {2},
  pages =               {241-280},
  year =                {2004},
  month =               mar,
}

@article{smj13(2)-GK,
  author =              {Gurevich, Yuri and Koryakov, Igor O.},
  title =               {Remarks on {B}erger's paper on the domino problem},
  publisher =           {Springer-Verlag},
  journal =             {Siberian Mathematical Journal},
  volume =              {13},
  number =              {2},
  pages =               {459-463},
  year =                {1972},
  month =               mar,
}

@inproceedings{lics2002-GK,
  author =              {Gottlob, Georg and Koch, Christoph},
  title =               {Monadic Queries over Tree-Structured Data},
  booktitle =           {{P}roceedings of the 17th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'02)},
  acronym =             {{LICS}'02},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {189-202},
  year =                {2002},
  month =               jul,
}

@inproceedings{swat1996-GKPR,
  author =              {G{\k a}sieniec, Leszek and Karpinski, Marek and
                         Plandowski, Wojciech and Rytter, Wojciech},
  title =               {Efficient Algorithms for {L}empel-{Z}iv Encoding
                         (Extended Abstract)},
  editor =              {Karlsson, Rolf G. and Lingas, Andrzej},
  booktitle =           {{P}roceedings of the 5th {S}candinavian {W}orkshop
                         on {A}lgorithm {T}heory ({SWAT}'96)},
  acronym =             {{SWAT}'96},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1097},
  pages =               {392-403},
  year =                {1996},
  month =               jul,
}

@inproceedings{charme2003-GKSV,
  author =              {Gurumurthy, Sankar and Kupferman, Orna and Somenzi,
                         Fabio and Vardi, Moshe Y.},
  title =               {On Complementing Nondeterministic B{\"u}chi
                         Automata},
  editor =              {Geist, Daniel and Tronci, Enrico},
  booktitle =           {{P}roceedings of the 12th {C}orrect {H}ardware
                         {D}esign and {V}erification {M}ethods ({CHARME}'03)},
  acronym =             {{CHARME}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2860},
  year =                {2003},
  month =               oct,
}

@inproceedings{forte2002-GL,
  author =              {Giannakopoulou, Dimitra and Lerda, Flavio},
  title =               {From States to Transitions: Improving Translation of
                         {LTL} Formulae to {B}{\"u}chi Automata},
  editor =              {Peled, Doron A. and Vardi, Moshe Y.},
  booktitle =           {{P}roceedings of the 22th {IFIP} {WG}6.1
                         {I}nternational {C}onference on {F}ormal
                         {T}echniques for {N}etworked and {D}istributed
                         {S}ystems ({FORTE}'02)},
  acronym =             {{FORTE}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2529},
  pages =               {308-326},
  year =                {2002},
  month =               nov,
}

@article{Automatica45(2)-GL,
  author =              {Genc, Sahika and Lafortune, St{\'e}phane},
  title =               {Predictability of event occurrences in
                         partially-observed discrete-event systems},
  publisher =           {Elsevier},
  journal =             {Automatica},
  volume =              {45},
  number =              {2},
  pages =               {301-311},
  year =                {2009},
  month =               feb,
  doi =                 {10.1016/j.automatica.2008.06.022},
}

@inproceedings{stacs2010-GL,
  author =              {G{\"o}ller, Stefan and Lohrey, Markus},
  title =               {Branching-time model checking of one-counter
                         processes},
  editor =              {Marion, Jean-Yves and Schwentick, Thomas},
  booktitle =           {{P}roceedings of the 27th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'10)},
  acronym =             {{STACS}'10},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {20},
  pages =               {405-416},
  year =                {2010},
  month =               feb,
}

@article{siamcomp42(3)-GL,
  author =              {G{\"o}ller, Stefan and Lohrey, Markus},
  title =               {Branching-time model checking of one-counter
                         processes and timed automata},
  publisher =           {Society for Industrial and Applied Math.},
  journal =             {SIAM Journal on Computing},
  volume =              {42},
  number =              {3},
  pages =               {884-923},
  year =                {2013},
  doi =                 {10.1137/120876435},
}

@inproceedings{cav2005-GLMR,
  author =              {Gardey, Guillaume and Lime, Didier and Magnin,
                         Morgan and Roux, Olivier H.},
  title =               {Romeo: A~Tool for Analyzing Time {P}etri Nets},
  editor =              {Etessami, Kousha and Rajamani, Sriram},
  booktitle =           {{P}roceedings of the 17th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'05)},
  acronym =             {{CAV}'05},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3576},
  pages =               {418-423},
  year =                {2005},
  month =               jul,
  doi =                 {10.1007/11513988_41},
}

@inproceedings{PSTV1994-GLS94,
  author =              {Godskesen, Jens Christian and Larsen, Kim Guldstrand
                         and Skou, Arne},
  title =               {Automatic verification of real-tim systems using
                         epsilon},
  editor =              {Vuong, Son T. and Chanson, Samuel T.},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {S}ymposium on {P}rotocol {S}pecification, {T}esting
                         and {V}erification ({PSTV}'94)},
  acronym =             {{PSTV}'94},
  publisher =           {Chapman \& Hall},
  series =              {IFIP Conference Proceedings},
  volume =              {1},
  pages =               {323-330},
  year =                {1995},
  confyear =            {1994},
}

Résumé

A chronicle is a temporal model introduced by Dousson et al. for situation recognition. In short, a chronicle consists of a set of events and a set of real-valued temporal constraints on the delays between pairs of events. This work investigates the relationship between chronicles and classical temporal model formalisms, namely TPTL and MTL. More specifically, we answer the following question: is it possible to find an equivalent formula in such formalisms for any chronicle? This question arises from the observation that a single chronicle captures complex temporal behaviours that do not order the events in time.

In this article, we introduce the subclass of linear chronicles, which defines a temporal order of occurrence of the event to be recognized in a temporal sequence. Our first result is that any chronicle can be expressed as a disjunction of linear chronicles. Our second result is that any linear chronicle has an equivalent TPTL formula. Using existing expressiveness results between TPTL and MTL, we show that some chronicles have no equivalent in MTL. This confirms that the model of chronicle has interesting properties for situation recognition.

@inproceedings{time2022-GM,
  author =              {Guyet, {\relax Th}omas and Markey, Nicolas},
  title =               {Logical forms of chronicles},
  editor =              {Artikis, Alexander and Posenato, Roberto and
                         Tonetta, Stefano},
  booktitle =           {{P}roceedings of the 29th {I}nternational
                         {S}ymposium on {T}emporal {R}epresentation and
                         {R}easoning ({TIME}'22)},
  acronym =             {{TIME}'22},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  pages =               {7:1-7:15},
  year =                {2022},
  month =               nov,
  doi =                 {10.4230/LIPIcs.TIME.2022.7},
  abstract =            {A~chronicle is a temporal model introduced by
                         Dousson~\textit{et~al.} for situation recognition.
                         In~short, a chronicle consists of a set of events
                         and a set of real-valued temporal constraints on the
                         delays between pairs of events. This~work
                         investigates the relationship between chronicles and
                         classical temporal model formalisms, namely
                         \textsf{TPTL} and~\textsf{MTL}. More~specifically,
                         we~answer the following question: is~it possible to
                         find an equivalent formula in such formalisms for
                         any chronicle? This~question arises from the
                         observation that a single chronicle captures complex
                         temporal behaviours that do not order the events in
                         time.\par In~this article, we~introduce the subclass
                         of linear chronicles, which defines a temporal order
                         of occurrence of the event to be recognized in a
                         temporal sequence. Our~first result is that any
                         chronicle can be expressed as a disjunction of
                         linear chronicles. Our~second result is that any
                         linear chronicle has an equivalent \textsf{TPTL}
                         formula. Using existing expressiveness results
                         between \textsf{TPTL} and~\textsf{MTL}, we~show that
                         some chronicles have no equivalent in~\textsf{MTL}.
                         This confirms that the model of chronicle has
                         interesting properties for situation recognition.},
}

@article{tcs295(1-3)-GMP,
  author =              {Geffert, Villiam and Mereghetti, Carlo and
                         Pighizzini, Giovanni},
  title =               {Converting Two-way Nondeterministic Unary Automata
                         into Simpler Automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {295},
  number =              {1-3},
  pages =               {189-203},
  year =                {2003},
  month =               feb,
}

@article{icomp205(8)-GMP,
  author =              {Geffert, Villiam and Mereghetti, Carlo and
                         Pighizzini, Giovanni},
  title =               {Complementing Two-way Finite Automata},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {205},
  number =              {8},
  pages =               {1173-1187},
  year =                {2007},
  month =               aug,
}

Résumé

Network congestion games are a convenient model for reasoning about routing problems in a network: agents have to move from a source to a target vertex while avoiding congestion, measured as a cost depending on the number of players using the same link. Network congestion games have been extensively studied over the last 40 years, while their extension with timing constraints were considered more recently.

Most of the results on network congestion games consider blind strategies: they are static, and do not adapt to the strategies selected by the other players. We extend the recent results of [Bertrand et al., Dynamic network congestion games. FSTTCS'20] to timed network congestion games, in which the availability of the edges depend on (discrete) time. We prove that computing Nash equilibria satisfying some constraint on the total cost (and in particular, computing the best and worst Nash equilibria), and computing the social optimum, can be achieved in exponential space. The social optimum can be computed in polynomial space if all players have the same source and target.

@inproceedings{formats2022-GMS,
  author =              {Goeminne, Aline and Markey, Nicolas and Sankur,
                         Ocan},
  title =               {Non-Blind Strategies in Timed Network Congestion
                         Games},
  editor =              {Bogomolov, Sergiy and Parker, David},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'22)},
  acronym =             {{FORMATS}'22},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {13465},
  pages =               {183-199},
  year =                {2022},
  month =               sep,
  doi =                 {10.1007/978-3-031-15839-1_11},
  abstract =            {Network congestion games are a convenient model for
                         reasoning about routing problems in a network:
                         agents have to move from a source to a target vertex
                         while avoiding congestion, measured as a cost
                         depending on the number of players using the same
                         link. Network congestion games have been extensively
                         studied over the last 40 years, while their
                         extension with timing constraints were considered
                         more recently. \par Most of the results on network
                         congestion games consider blind strategies: they are
                         static, and do not adapt to the strategies selected
                         by the other players. We extend the recent results
                         of [Bertrand~\textit{et~al.}, Dynamic network
                         congestion games. FSTTCS'20] to timed network
                         congestion games, in which the availability of the
                         edges depend on (discrete) time. We prove that
                         computing Nash equilibria satisfying some constraint
                         on the total cost (and in particular, computing the
                         best and worst Nash equilibria), and computing the
                         social optimum, can be achieved in exponential
                         space. The social optimum can be computed in
                         polynomial space if all players have the same source
                         and target.},
}

@inproceedings{cav2001-GO,
  author =              {Gastin, Paul and Oddoux, Denis},
  title =               {Fast {LTL} to {B}{\"u}chi Automata Translation},
  editor =              {Berry, G{\'e}rard and Comon, Hubert and Finkel,
                         Alain},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'01)},
  acronym =             {{CAV}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2102},
  pages =               {53-65},
  year =                {2001},
  month =               jul,
}

@inproceedings{mfcs2003-GO,
  author =              {Gastin, Paul and Oddoux, Denis},
  title =               {{LTL} with Past and Two-way Very-weak Alternating
                         Automata},
  editor =              {Rovan, Branislav and Vojt{\'a}s, Peter},
  booktitle =           {{P}roceedings of the 28th {I}nternational
                         {S}ymposium on {M}athematical {F}oundations of
                         {C}omputer {S}cience ({MFCS}'03)},
  acronym =             {{MFCS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2747},
  pages =               {439-448},
  year =                {2003},
  month =               aug,
}

@article{ipl10(1)-Gol,
  author =              {Goldschlager, Leslie M.},
  title =               {A Space Efficient Algorithm for the Monotone Planar
                         Circuit Value Problem},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {10},
  number =              {1},
  pages =               {25-27},
  year =                {1980},
  month =               feb,
}

@techreport{eccc2005-Gol,
  author =              {Goldreich, Oded},
  title =               {On promise problems},
  number =              {05-014},
  year =                {2005},
  month =               aug,
  institution =         {Electronic Colloquium on Computational Complexity},
  type =                {Research Report},
}

@article{jolli5(1)-Gor,
  author =              {Goranko, Valentin},
  title =               {Hierarchies of Modal and Temporal Logics with
                         Reference Pointers},
  publisher =           {Kluwer Academic},
  journal =             {Journal of Logic, Language and Information},
  volume =              {5},
  number =              {1},
  pages =               {1-24},
  year =                {1996},
  month =               apr,
}

@inproceedings{esslli2000-Gor,
  author =              {Goranko, Valentin},
  title =               {Temporal Logics of Computations},
  booktitle =           {{P}roceedings of the 12th {E}uropean {S}ummer
                         {S}chool in {L}ogic, {L}anguage and {I}nformation
                         ({ESSLLI}'00)},
  acronym =             {{ESSLLI}'00},
  year =                {2000},
  month =               aug,
}

@inproceedings{tark2001-Gor,
  author =              {Goranko, Valentin},
  title =               {Coalition Games and Alternating Temporal Logics},
  editor =              {van Benthem, Johan},
  booktitle =           {{P}roceedings of the 8th {C}onference on
                         {T}heoretical {A}spects of {R}ationality and
                         {K}nowledge ({TARK}'01)},
  acronym =             {{TARK}'01},
  publisher =           {Morgan Kaufmann Publishers},
  pages =               {259-272},
  year =                {2001},
  month =               jul,
}

@article{jacm42(2)-Got,
  author =              {Gottlob, Georg},
  title =               {{NP} Trees and {C}arnap's Modal Logic},
  publisher =           {ACM Press},
  journal =             {Journal of the~ACM},
  volume =              {42},
  number =              {2},
  pages =               {421-457},
  year =                {1995},
  month =               mar,
}

@inproceedings{fct2001-GP,
  author =              {G{\k a}sieniec, Leszek and Potapov, Igor},
  title =               {Time{\slash}Space Efficient Compressed Pattern
                         Matching},
  editor =              {Freivalds, Rusins},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {S}ymposium on {F}undamentals of {C}omputation
                         {T}heory ({FCT}'01)},
  acronym =             {{FCT}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2138},
  pages =               {138-149},
  year =                {2001},
  month =               aug,
}

@inproceedings{rv2002-GP,
  author =              {Gunter, Elsa and Peled, Doron A.},
  title =               {Tracing the Executions of Concurrent Programs},
  editor =              {Havelund, Klaus and Ro{\c{s}}u, Grigore},
  booktitle =           {{P}roceedings of the 2nd {I}nternational {W}orkshop
                         on {R}untime {V}erification ({RV}'02)},
  acronym =             {{RV}'02},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {70},
  number =              {4},
  year =                {2002},
  month =               jul,
}

@techreport{NASACR10-216724-GP,
  author =              {Goodloe, Alwyn and Pike, Lee},
  title =               {Monitoring distributed real-time systems: a~survey
                         and future directions},
  number =              {NASA/CR-2010-216724},
  year =                {2010},
  month =               jul,
  institution =         {NASA},
  type =                {Technical Report},
}

@inproceedings{popl1980-GPSS,
  author =              {Gabbay, Dov M. and Pnueli, Amir and Shelah, Saharon
                         and Stavi, Jonathan},
  title =               {On the Temporal Analysis of Fairness},
  booktitle =           {Conference Record of the 7th {ACM} {S}ymposium on
                         {P}rinciples of {P}rogramming {L}anguages
                         ({POPL}'80)},
  acronym =             {{POPL}'80},
  publisher =           {ACM Press},
  pages =               {163-173},
  year =                {1980},
  month =               jan,
}

@inproceedings{pstv1995-GPVW,
  author =              {Gerth, Rob and Peled, Doron A. and Vardi, Moshe Y.
                         and Wolper, Pierre},
  title =               {Simple On-the-fly Automatic Verification of Linear
                         Temporal Logic},
  editor =              {Dembinski, Piotr and Sredniawa, Marek},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {S}ymposium on {P}rotocol {S}pecification, {T}esting
                         and {V}erification ({PSTV}'95)},
  acronym =             {{PSTV}'95},
  publisher =           {Chapman \& Hall},
  series =              {IFIP Conference Proceedings},
  volume =              {38},
  pages =               {3-18},
  year =                {1996},
  confyear =            {1995},
  confmonth =           {6},
}

@incollection{HFL1997(3)-GR,
  author =              {Giammarresi, Dora and Restivo, Antonio},
  title =               {Two-dimensional Languages},
  editor =              {Rozenberg, Grzegorz and Salomaa, Arto},
  booktitle =           {Handbook of Formal Languages},
  publisher =           {Springer-Verlag},
  volume =              {3},
  pages =               {215-267},
  year =                {1997},
}

@inproceedings{dcc1999-GR,
  author =              {G{\k a}sieniec, Leszek and Rytter, Wojciech},
  title =               {Almost Optimal Fully {LZW}-Compressed Pattern
                         Matching},
  booktitle =           {{P}roceedings of the 9th {D}ata {C}ompression
                         {C}onference ({DCC}'99)},
  acronym =             {{DCC}'99},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {316-325},
  year =                {1999},
  month =               mar,
}

@techreport{imag348-Gra,
  author =              {Graf, Susanne},
  title =               {On {L}amport's Comparison between Linear and
                         Branching Time Logic},
  number =              {348},
  year =                {1983},
  month =               jan,
  institution =         {Lab.~Informatique et Math{\'e}matiques Apppliqu\'ees
                         de Grenoble, France},
  type =                {Research Report},
}

@article{rairo-ita18(4)-Gra,
  author =              {Graf, Susanne},
  title =               {On {L}amport's Comparison between Linear and
                         Branching Time Logic},
  publisher =           {EDP Sciences},
  journal =             {RAIRO~-- Informatique Th{\'e}orique et Applications},
  volume =              {18},
  number =              {4},
  pages =               {345-353},
  year =                {1984},
}

@phdthesis{phd-grinchtein,
  author =              {Grinchtein, Olga},
  title =               {Learning of Timed Systems},
  year =                {2008},
  school =              {Deparment of Information Technology, Uppsala
                         University, Sweden},
}

@techreport{lifo-2000-16-GRS,
  author =              {Gouranton, Val{\'e}rie and R{\'e}ty, Pierre and
                         Seidl, Helmut},
  title =               {Synchronized Tree Languages Revisited and New
                         Applications},
  number =              {2000-16},
  year =                {2000},
  institution =         {Lab.~Informatique Fondamentale d'Orl{\'e}ans,
                         France},
  type =                {Research Report},
}

@inproceedings{fossacs2001-GRS,
  author =              {Gouranton, Val{\'e}rie and R{\'e}ty, Pierre and
                         Seidl, Helmut},
  title =               {Synchronized Tree Languages Revisited and New
                         Applications},
  editor =              {Honsell, Furio and Miculan, Marino},
  booktitle =           {{P}roceedings of the 4th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'01)},
  acronym =             {{FoSSaCS}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2030},
  pages =               {214-229},
  year =                {2001},
  month =               apr,
}

@inproceedings{formats2011-GRS,
  author =              {Geeraerts, Gilles and Raskin, Jean-Fran{\c c}ois and
                         Sznajder, Tali},
  title =               {Event-clock automata: form theory to practice},
  editor =              {Fahrenberg, Uli and Tripakis, Stavros},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'11)},
  acronym =             {{FORMATS}'11},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6919},
  pages =               {209-224},
  year =                {2011},
  month =               sep,
  doi =                 {10.1007/978-3-642-24310-3_15},
}

@article{icomp125(1)-GRST,
  author =              {Giammarresi, Dora and Restivo, Antonio and Seibert,
                         Sebastian and Thomas, Wolfgang},
  title =               {Monadic Second-Order Logic over Rectangular Pictures
                         and Recognizability by Tiling Systems},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {125},
  number =              {1},
  pages =               {32-45},
  year =                {1996},
  month =               feb,
  doi =                 {10.1006/inco.1996.0018},
}

@inproceedings{ifiptcs2010-GRT,
  author =              {Gross, James and Radmacher, Frank G. and Thomas,
                         Wolfgang},
  title =               {A~Game-Theoretic Approach to Routing under
                         Adversarial Conditions},
  editor =              {Calude, Cristian S. and Sassone, Vladimiro},
  booktitle =           {{P}roceedings of the 6th {IFIP} {I}nternational
                         {C}onference on {T}heoretical {C}omputer {S}cience
                         ({IFIPTCS}'10)},
  acronym =             {{IFIPTCS}'10},
  publisher =           {Springer-Verlag},
  series =              {IFIP Conference Proceedings},
  volume =              {323},
  pages =               {355-370},
  year =                {2010},
  month =               sep,
}

@inproceedings{gandalf2011-GRT,
  author =              {Gr{\"u}ner, Sten and Radmacher, Frank G. and Thomas,
                         Wolfgang},
  title =               {Connectivity Games over Dynamic Networks},
  editor =              {D{'}Agostino, Giovanna and La{~}Torre, Salvatore},
  booktitle =           {{P}roceedings of the 2nd {I}nternational {S}ymposium
                         on {G}ames, {A}utomata, {L}ogics and {F}ormal
                         {V}erification ({GandALF}'11)},
  acronym =             {{GandALF}'11},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {54},
  pages =               {131-145},
  year =                {2011},
  month =               jun,
}

@inproceedings{cav2005-GRV,
  author =              {Geeraerts, Gilles and Raskin, Jean-Fran{\c c}ois and
                         Van{~}Begin, Laurent},
  title =               {Expand, Enlarge and Check... Made Efficient},
  editor =              {Etessami, Kousha and Rajamani, Sriram},
  booktitle =           {{P}roceedings of the 17th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'05)},
  acronym =             {{CAV}'05},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3576},
  pages =               {394-407},
  year =                {2005},
  month =               jul,
}

@article{jcss72(1)-GRV,
  author =              {Geeraerts, Gilles and Raskin, Jean-Fran{\c c}ois and
                         Van{~}Begin, Laurent},
  title =               {Expand, Enlarge and Check: New algorithms for the
                         coverability problem of~{WSTS}},
  publisher =           {Elsevier},
  journal =             {Journal of Computer and System Sciences},
  volume =              {72},
  number =              {1},
  pages =               {180-203},
  year =                {2006},
  month =               feb,
}

@article{ijfcs21(2)-GRV,
  author =              {Geeraerts, Gilles and Raskin, Jean-Fran{\c c}ois and
                         Van{~}Begin, Laurent},
  title =               {On the Efficient Computation of the Minimal
                         Coverability Set of {P}etri Nets},
  journal =             {International Journal of Foundations of Computer
                         Science},
  volume =              {21},
  number =              {2},
  pages =               {135-165},
  year =                {2010},
  month =               apr,
}

@article{pjm16(2)-GS,
  author =              {Ginsburg, Seymour and Spanier, Edwin},
  title =               {Semigroups, {P}resburger formulas, and languages},
  journal =             {Pacific Journal of Mathematics},
  volume =              {16},
  number =              {2},
  pages =               {285-296},
  year =                {1966},
  month =               dec,
}

@article{jacm39(3)-GS,
  author =              {German, Steven M. and Sistla, A. Prasad},
  title =               {Reasoning about Systems with Many Processes},
  publisher =           {ACM Press},
  journal =             {Journal of the~ACM},
  volume =              {39},
  number =              {3},
  pages =               {675-735},
  year =                {1992},
  month =               jul,
  doi =                 {10.1145/146637.146681},
}

@inproceedings{cav1994-GS,
  author =              {Gorrieri, Roberto and Siliprandi, Glauco},
  title =               {Real-time System Verification using {P/T} Nets},
  editor =              {Dill, David L.},
  booktitle =           {{P}roceedings of the 6th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'94)},
  acronym =             {{CAV}'94},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {818},
  pages =               {14-26},
  year =                {1994},
  month =               jun,
}

@article{lmcs1(1)-GS,
  author =              {Grohe, Martin and Schweikardt, Nicole},
  title =               {The Succinctness of First-Order Logic on Linear
                         Orders},
  journal =             {Logical Methods in Computer Science},
  volume =              {1},
  number =              {1},
  pages =               {1-25},
  year =                {2006},
  month =               jun,
}

@inproceedings{cav2009-GS,
  author =              {Gawlitza, Thomas and Seidl, Helmut},
  title =               {Games through Nested Fixpoints},
  editor =              {Bouajjani, Ahmed and Maler, Oded},
  booktitle =           {{P}roceedings of the 21st {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'09)},
  acronym =             {{CAV}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5643},
  pages =               {291-305},
  year =                {2009},
  month =               jun,
  doi =                 {10.1007/978-3-642-02658-4_24},
}

@article{fmsd34(3)-GSZ,
  author =              {Gastin, Paul and Sznajder, Tali and Zeitoun, Marc},
  title =               {Distributed synthesis for well-connected
                         architectures},
  publisher =           {Springer-Verlag},
  journal =             {Formal Methods in System Design},
  volume =              {34},
  number =              {3},
  pages =               {215-237},
  year =                {2009},
  month =               jun,
}

@inproceedings{focs2005-GT,
  author =              {Goldwasser, Shafi and Tauman Kalai, Yael},
  title =               {On the Impossibility of Obfuscation with Auxiliary
                         Input},
  booktitle =           {{P}roceedings of the 46th {A}nnual {S}ymposium on
                         {F}oundations of {C}omputer {S}cience ({FOCS}'05)},
  acronym =             {{FOCS}'05},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {553-562},
  year =                {2005},
  month =               oct,
}

@book{GTW-lncs2500,
  title =               {Automata Logics, and Infinite Games~-- A~Guide to
                         Current Research},
  editor =              {Gr{\"a}del, Erich and Thomas, Wolfgang and Wilke,
                         Thomas},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2500},
  year =                {2002},
  doi =                 {10.1007/3-540-36387-4},
}

@article{tcs345(1)-GV,
  author =              {Geldenhuys, Jaco and Valmari, Antti},
  title =               {More Efficient On-the-fly {LTL} Verification with
                         {T}arjan's Algorithm},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {345},
  number =              {1},
  pages =               {60-82},
  year =                {2005},
  month =               nov,
}

@inproceedings{mfcs2004-GZ,
  author =              {Gimbert, Hugo and Zielonka, Wies{\l}aw},
  title =               {When Can You Play Positionnaly?},
  editor =              {Fiala, Ji{\v r}{\'\i} and Koubek, V{\'a}clav and
                         Kratoch{\'\i}l, Jan},
  booktitle =           {{P}roceedings of the 29th {I}nternational
                         {S}ymposium on {M}athematical {F}oundations of
                         {C}omputer {S}cience ({MFCS}'04)},
  acronym =             {{MFCS}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3153},
  pages =               {686-697},
  year =                {2004},
  month =               aug,
}

@inproceedings{concur2005-GZ,
  author =              {Gimbert, Hugo and Zielonka, Wies{\l}aw},
  title =               {Games Where You Can Play Optimally Without Any
                         Memory},
  editor =              {Abadi, Mart{\'\i}n and de Alfaro, Luca},
  booktitle =           {{P}roceedings of the 16th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'05)},
  acronym =             {{CONCUR}'05},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3653},
  pages =               {428-442},
  year =                {2005},
  month =               aug,
  doi =                 {10.1007/11539452_33},
}