Nicolas Markey

@phdthesis{phd-latorre,
  author =              {La{~}Torre, Salvatore},
  title =               {Verification of Reactive Systems and Decision
                         Problems in Temporal Logics},
  year =                {2001},
  school =              {University of Pennsylvania},
}

@inproceedings{popl1980-Lam,
  author =              {Lamport, Leslie},
  title =               {``{S}ometimes'' is sometimes ``{N}ot {N}ever''},
  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 =               {174-185},
  year =                {1980},
  month =               jan,
}

@inproceedings{ifipwcc1983-Lam,
  author =              {Lamport, Leslie},
  title =               {What good is Temporal Logic?},
  editor =              {Mason, R. E. A.},
  booktitle =           {{I}nformation {P}rocessing~83~-- {P}roceedings of
                         the 9th {IFIP} {W}orld {C}omputer {C}ongress
                         ({WCC}'83)},
  acronym =             {{WCC}'83},
  publisher =           {North-Holland/IFIP},
  pages =               {657-668},
  year =                {1983},
  month =               sep,
}

@article{tocs5(1)-Lam,
  author =              {Lamport, Leslie},
  title =               {A~Fast Mutual Exclusion Algorithm},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computer Systems},
  volume =              {5},
  number =              {1},
  pages =               {1-11},
  year =                {1987},
  month =               feb,
}

@inproceedings{concur2002-Lan,
  author =              {Lange, Martin},
  title =               {Local Model Checking Games for Fixed Point Logic
                         with Chop},
  editor =              {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v
                         r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era,
                         Anton{\'\i}n},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'02)},
  acronym =             {{CONCUR}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2421},
  pages =               {240-254},
  year =                {2002},
  month =               aug,
}

@inproceedings{express2002-Lan,
  author =              {Lange, Martin},
  title =               {Alternating Context-Free Languages and Linear Time
                         {\(\mu\)}-calculus with Sequential Composition},
  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 =               {71-87},
  year =                {2002},
  month =               aug,
}

@inproceedings{vmcai2005-Lan,
  author =              {Lange, Martin},
  title =               {Weak Automata for the Linear Time
                         {\(\mu\)}-Calculus},
  editor =              {Cousot, Radhia},
  booktitle =           {{P}roceedings of the 6th {I}nternational {W}orkshop
                         on {V}erification, {M}odel {C}hecking, and
                         {A}bstract {I}nterpretation ({VMCAI}'05)},
  acronym =             {{VMCAI}'05},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3385},
  pages =               {267-281},
  year =                {2005},
  month =               jan,
}

@inproceedings{concur2007-Lan,
  author =              {Lange, Martin},
  title =               {Linear-Time Logics Around~{PSL}: Complexity,
                         Expressiveness, and a Little Bit of Succinctness},
  editor =              {Caires, Lu{\'\i}s and Vasconcelos, Vasco T.},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'07)},
  acronym =             {{CONCUR}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4703},
  pages =               {90-104},
  year =                {2007},
  month =               sep,
}

@article{ipl108(5)-Lan,
  author =              {Lange, Martin},
  title =               {A purely model-theoretic proof of the exponential
                         succinctness gap between {CTL\(^{+}\)} and {CTL}},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {108},
  number =              {5},
  pages =               {308-312},
  year =                {2008},
  month =               nov,
}

@phdthesis{phd-larsen,
  author =              {Larsen, Kim Guldstrand},
  title =               {Context-dependent bisimulation between processes},
  year =                {1986},
  school =              {School of Informatics, University of Edinburgh, UK},
}

@inproceedings{avmfss1989-Lar,
  author =              {Larsen, Kim Guldstrand},
  title =               {Modal Specifications},
  editor =              {Sifakis, Joseph},
  booktitle =           {{P}roceedings of the {I}nternational {W}orkshop on
                         {A}utomatic {V}erification {M}ethods for {F}inite
                         {S}tate {S}ystems ({AVMFSS}'89)},
  acronym =             {{AVMFSS}'89},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {407},
  pages =               {232-246},
  year =                {1990},
  confyear =            {1989},
  confmonth =           {6},
}

@techreport{daimi-PB426,
  author =              {Larsen, Kim Skak},
  title =               {Length of Maximal Common Subsequences},
  number =              {PB-426},
  year =                {1992},
  month =               oct,
  institution =         {DAIMI, Faculty of Science, University of Aarhus,
                         Denmark},
  type =                {Technical Report},
}

@phdthesis{phd-laroussinie,
  author =              {Laroussinie, Fran{\c c}ois},
  title =               {Logiques temporelles avec pass{\'e} pour la
                         sp{\'e}cification et la v{\'e}rification des
                         syst{\`e}mes r{\'e}actifs},
  year =                {1994},
  school =              {INPG},
  type =                {Th\`ese de doctorat},
}

@article{ipl54(6)-Lar,
  author =              {Laroussinie, Fran{\c c}ois},
  title =               {About the Expressive Power of {CTL} Combinators},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {54},
  number =              {6},
  pages =               {343-345},
  year =                {1995},
  month =               jun,
}

@inproceedings{concur2002-Las,
  author =              {Lasota, S{\l}awomir},
  title =               {Decidability of Strong Bisimilarity for Timed {BPP}},
  editor =              {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v
                         r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era,
                         Anton{\'\i}n},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'02)},
  acronym =             {{CONCUR}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2421},
  pages =               {562-579},
  year =                {2002},
  month =               aug,
}

@inproceedings{cav2001-LBBFHPR,
  author =              {Larsen, Kim Guldstrand and Behrmann, Gerd and
                         Brinksma, Ed and Fehnker, Ansgar and Hune, Thomas
                         and Pettersson, Paul and Romijn, Judi},
  title =               {As~Cheap as Possible: Efficient Cost-Optimal
                         Reachability for Priced Timed Automata},
  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 =               {493-505},
  year =                {2001},
  month =               jul,
  doi =                 {10.1007/3-540-44585-4_47},
}

@inproceedings{ccs2003-LD,
  author =              {Linn, Cullen and Debray, Saumya},
  title =               {Obfuscation of Executable Code to Improve Resistance
                         to Static Disassembly},
  editor =              {Jajodia, Sushil and Atluri, Vijayalakshmi and
                         Jaeger, Trent},
  booktitle =           {{P}roceedings of the 10th {C}onference on {C}omputer
                         and {C}ommunications {S}ecurity ({CCS}'03)},
  acronym =             {{CCS}'03},
  publisher =           {ACM Press},
  pages =               {290-299},
  year =                {2003},
  month =               oct,
}

@inproceedings{re2019-LDWHP,
  author =              {Langenfeld, Vincent and Dietsch, Daniel and
                         Westphal, Bernd and Hoenicke, Jochen and Post,
                         Amalinda},
  title =               {Scalable Analysis of Real-Time Requirements},
  editor =              {Damian, Daniela E. and Perini, Anna and Lee,
                         Seok-Won},
  booktitle =           {{P}roceedings of the 27th {I}nternaitonal
                         {R}equirements Engineering {C}onference ({RE}'19)},
  acronym =             {{RE}'19},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {234-244},
  year =                {2019},
  month =               sep,
  doi =                 {10.1109/RE.2019.00033},
}

@article{tcs13(3)-Lei,
  author =              {Leiss, Ernst},
  title =               {Succinct representation of regular languages by
                         boolean automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {13},
  number =              {3},
  pages =               {323-330},
  year =                {1981},
}

@phdthesis{phd-leroux,
  author =              {Leroux, J{\'e}r{\^o}me},
  title =               {Algorithmique de la v{\'e}rification des
                         syst{\`e}mes {\`a} compteurs. Approximation et
                         acc{\'e}l{\'e}ration. Impl{\'e}mentation de l'outil
                         {FAST}},
  year =                {2003},
  month =               dec,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {Th\`ese de doctorat},
}

Résumé

We present a correct-by-design method of state-dependent control synthesis for linear discrete-time switching systems. Given an objective region R of the state space, the method builds a capture set S and a control which steers any element of S into R. The method works by iterated backward reachability from R. More precisely, S is given as a parametric extension of R, and the maximum value of the parameter is solved by linear programming. The method can also be used to synthesize a stability control which maintains indefinitely within R all the states starting at R. We explain how the synthesis method can be performed in a distributed manner. The method has been implemented and successfully applied to the synthesis of a distributed control of a concrete floor heating system with 11 rooms and 211 = 2048 switching modes.

@inproceedings{rp2016-LFMDC,
  author =              {Le{~}Co{\"e}nt, Adrien and Fribourg, Laurent and
                         Markey, Nicolas and De{~}Vuyst, Florian and Chamoin,
                         Ludovic},
  title =               {Distributed Synthesis of State-Dependent Switching
                         Control},
  editor =              {Larsen, Kim Guldstrand and Srba, Ji{\v r}{\'\i}},
  booktitle =           {{P}roceedings of the 10th {W}orkshop on
                         {R}eachability {P}roblems in {C}omputational
                         {M}odels ({RP}'16)},
  acronym =             {{RP}'16},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9899},
  pages =               {119-133},
  year =                {2016},
  month =               sep,
  doi =                 {10.1007/978-3-319-45994-3_9},
  abstract =            {We present a correct-by-design method of
                         state-dependent control synthesis for linear
                         discrete-time switching systems. Given an objective
                         region~\(R\) of the state space, the method builds a
                         capture set~\(S\) and a control which steers any
                         element of~\(S\) into~\(R\). The method works by
                         iterated backward reachability from~\(R\). More
                         precisely, \(S\)~is given as a parametric extension
                         of~\(R\), and the maximum value of the parameter is
                         solved by linear programming. The method can also be
                         used to synthesize a stability control which
                         maintains indefinitely within~\(R\) all the states
                         starting at~\(R\). We~explain how the synthesis
                         method can be performed in a distributed manner. The
                         method has been implemented and successfully applied
                         to the synthesis of a distributed control of a
                         concrete floor heating system with 11 rooms and
                         \(2^{11} = 2048\) switching modes.},
}

Résumé

We present a correct-by-design method of state-dependent control synthesis for sampled switching systems. Given a target region R of the state space, our method builds a capture set S and a control that steers any element of S into R. The method works by iterated backward reachability from R. It is also used to synthesize a recurrence control that makes any state of R return to R infinitely often. We explain how the synthesis method can be performed in a compositional manner, and apply it to the synthesis of a compositional control for a concrete floor-heating system with 11 rooms and up to 211=2048 switching modes.

@article{tcs750()-LFMDC,
  author =              {Le{~}Co{\"e}nt, Adrien and Fribourg, Laurent and
                         Markey, Nicolas and De{~}Vuyst, Florian and Chamoin,
                         Ludovic},
  title =               {Distributed Synthesis of State-Dependent Switching
                         Control},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {750},
  pages =               {53-68},
  year =                {2018},
  month =               nov,
  doi =                 {10.1016/j.tcs.2018.01.021},
  abstract =            {We present a correct-by-design method of
                         state-dependent control synthesis for sampled
                         switching systems. Given a target region~\(R\) of
                         the state space, our~method builds a capture
                         set~\(S\) and a~control that steers any element
                         of~\(S\) into~\(R\). The~method works by iterated
                         backward reachability from~\(R\). It~is also used to
                         synthesize a recurrence control that makes any state
                         of~\(R\) return to~\(R\) infinitely often.
                         We~explain how the synthesis method can be performed
                         in a compositional manner, and apply it to the
                         synthesis of a compositional control for a concrete
                         floor-heating system with 11~rooms and up to
                         \(2^{11}=2048\) switching modes.},
}

@mastersthesis{master05-limaye,
  author =              {Limaye, Nutan},
  title =               {Parallel Complexity Classes Centered around
                         {LOGCFL}},
  year =                {2005},
  month =               apr,
  school =              {Anna University, Chennai, India},
}

@inproceedings{forte1998-LL,
  author =              {Laroussinie, Fran{\c c}ois and Larsen, Kim
                         Guldstrand},
  title =               {{CMC}: A~Tool for Compositional Model-Checking of
                         Real-Time Systems},
  editor =              {Budkowski, Stanislaw and Cavalli, Anna R. and Najm,
                         Elie},
  booktitle =           {{P}roceedings of the {IFIP} {TC6} {WG}6.1 {J}oint
                         {I}nternational {C}onference on {F}ormal
                         {D}escription {T}echniques for {D}istributed
                         {S}ystems and {C}ommunication {P}rotocols
                         ({FORTE}'98) and {P}rotocol {S}pecification,
                         {T}esting and {V}erification ({PSTV}'98)},
  acronym =             {{FORTE/PSTV}'98},
  publisher =           {Kluwer Academic},
  series =              {IFIP Conference Proceedings},
  volume =              {135},
  pages =               {439-456},
  year =                {1998},
  month =               oct,
}

@article{aric45()-LLH,
  author =              {Lafortune, St{\'e}phane and Lin, Feng and
                         Hadjicostis, Christoforos N.},
  title =               {On~the history of diagnosability and opacity in
                         discrete event systems},
  publisher =           {Elsevier},
  journal =             {Annual Reviews in Control},
  volume =              {45},
  pages =               {257-266},
  year =                {2018},
  doi =                 {10.1016/j.arcontrol.2018.04.002},
}

@inproceedings{rtss1997-LLPY,
  author =              {Larsen, Kim Guldstrand and Larsson, Fredrik and
                         Pettersson, Paul and Yi, Wang},
  title =               {Efficient verification of real-time systems: compact
                         data structure and state-space reduction},
  booktitle =           {{P}roceedings of the 18th {S}ymposium on {R}eal-Time
                         {S}ystems ({RTSS}'97)},
  acronym =             {{RTSS}'97},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {14-24},
  year =                {1997},
  month =               dec,
}

@article{tcs515-LLTW,
  author =              {Larsen, Kim Guldstrand and Legay, Axel and
                         Traonouez, Louis-Marie and W{\k a}sowski, Andrzej},
  title =               {Robust synthesis for real-time systems},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {515},
  pages =               {96-122},
  year =                {2014},
  month =               jan,
}

@inproceedings{mfcs1995-LLW,
  author =              {Laroussinie, Fran{\c c}ois and Larsen, Kim
                         Guldstrand and Weise, Carsten},
  title =               {From Timed Automata to Logic~-- and Back},
  editor =              {Wiedermann, Jir{\'\i} and H{\'a}jek, Petr},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {S}ymposium on {M}athematical {F}oundations of
                         {C}omputer {S}cience ({MFCS}'95)},
  acronym =             {{MFCS}'95},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {969},
  pages =               {529-539},
  year =                {1995},
  month =               aug,
  doi =                 {10.1007/3-540-60246-1_158},
}

@techreport{arxiv-1510.05774,
  author =              {Larsen, Kim Guldstrand and Laursen, Simon and
                         Zimmermann, Martin},
  title =               {Limit Your Consumption! Finding Bounds in
                         Average-energy Games},
  number =              {1510.05774},
  year =                {2015},
  month =               oct,
  institution =         {arXiv},
  type =                {Research Report},
}

@inproceedings{lics2002-LM,
  author =              {Lynch, Christopher and Morawska, Barbara},
  title =               {Automatic Decidability},
  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 =               {9-16},
  year =                {2002},
  month =               jul,
}

Résumé

Various extensions of the temporal logic ATL have recently been introduced to express rich properties of multi-agent systems. Among these, ATLsc extends ATL with strategy contexts, while Strategy Logic has first-order quantification over strategies. There is a price to pay for the rich expressiveness of these logics: model-checking is non-elementary, and satisfiability is undecidable.

We prove in this paper that satisfiability is decidable in several special cases. The most important one is when restricting to turn-based games. We prove that decidability also holds for concurrent games if the number of moves available to the agents is bounded. Finally, we prove that restricting strategy quantification to memoryless strategies brings back undecidability.

@inproceedings{gandalf2013-LM,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas},
  title =               {Satisfiability of {ATL} with strategy contexts},
  editor =              {Puppis, Gabriele and Villa, Tiziano},
  booktitle =           {{P}roceedings of the 4th {I}nternational {S}ymposium
                         on {G}ames, {A}utomata, {L}ogics and {F}ormal
                         {V}erification ({GandALF}'13)},
  acronym =             {{GandALF}'13},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {119},
  pages =               {208-223},
  year =                {2013},
  month =               aug,
  doi =                 {10.4204/EPTCS.119.18},
  abstract =            {Various extensions of the temporal logic ATL have
                         recently been introduced to express rich properties
                         of multi-agent systems. Among these, ATLsc extends
                         ATL with \emph{strategy contexts}, while Strategy
                         Logic has \emph{first-order quantification} over
                         strategies. There is a price to pay for the rich
                         expressiveness of these logics: model-checking is
                         non-elementary, and satisfiability is
                         undecidable.\par We prove in this paper that
                         satisfiability is decidable in several special
                         cases. The most important one is when restricting to
                         \emph{turn-based} games. We~prove that decidability
                         also holds for concurrent games if the number of
                         moves available to the agents is bounded. Finally,
                         we~prove that restricting strategy quantification to
                         memoryless strategies brings back undecidability.},
}

Résumé

While it was defined long ago, the extension of CTL with quantification over atomic propositions has never been studied extensively. Considering two different semantics (depending whether propositional quantification refers to the Kripke structure or to its unwinding tree), we study its expressiveness (showing in particular that QCTL coincides with Monadic Second-Order Logic for both semantics) and characterise the complexity of its model-checking and satisfiability problems, depending on the number of nested propositional quantifiers (showing that the structure semantics populates the polynomial hierarchy while the tree semantics populates the exponential hierarchy).

@article{lmcs10(4)-LM,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas},
  title =               {Quantified~{CTL}: expressiveness and complexity},
  journal =             {Logical Methods in Computer Science},
  volume =              {10},
  number =              {4},
  year =                {2014},
  month =               dec,
  doi =                 {10.2168/LMCS-10(4:17)2014},
  abstract =            {While it was defined long ago, the extension of CTL
                         with quantification over atomic propositions has
                         never been studied extensively. Considering two
                         different semantics (depending whether propositional
                         quantification refers to the Kripke structure or to
                         its unwinding tree), we~study its expressiveness
                         (showing in particular that QCTL coincides with
                         Monadic Second-Order Logic for both semantics) and
                         characterise the complexity of its model-checking
                         and satisfiability problems, depending on the number
                         of nested propositional quantifiers (showing that
                         the structure semantics populates the polynomial
                         hierarchy while the tree semantics populates the
                         exponential hierarchy).},
}

Résumé

We study the extension of the alternating-time temporal logic (ATL) with strategy contexts: contrary to the original semantics, in this semantics the strategy quantifiers do not reset the previously selected strategies.

We show that our extension ATLsc is very expressive, but that its decision problems are quite hard: model checking is k-EXPTIME-complete when the formula has k nested strategy quantifiers; satisfiability is undecidable, but we prove that it is decidable when restricting to turn-based games. Our algorithms are obtained through a very convenient translation to QCTL (the computation-tree logic CTL extended with atomic quantification), which we show also applies to Strategy Logic, as well as when strategy quantification ranges over memoryless strategies.

@article{icomp245()-LM,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas},
  title =               {Augmenting {ATL} with strategy contexts},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {245},
  pages =               {98-123},
  year =                {2015},
  month =               dec,
  doi =                 {10.1016/j.ic.2014.12.020},
  abstract =            {We study the extension of the alternating-time
                         temporal logic (ATL) with strategy contexts:
                         contrary to the original semantics, in this
                         semantics the strategy quantifiers do not reset the
                         previously selected strategies.\par We show that our
                         extension ATLsc is very expressive, but that its
                         decision problems are quite hard: model checking is
                         \(k\)-EXPTIME-complete when the formula has \(k\)
                         nested strategy quantifiers; satisfiability is
                         undecidable, but we prove that it is decidable when
                         restricting to turn-based games. Our algorithms are
                         obtained through a very convenient translation to
                         QCTL (the~computation-tree logic CTL extended with
                         atomic quantification), which we show also applies
                         to Strategy Logic, as well as when strategy
                         quantification ranges over memoryless strategies.},
}

Résumé

We introduce a new class of automata (which we coin EU-automata) running on infininte trees of arbitrary (finite) arity. We develop and study several algorithms to perform classical operations (union, intersection, complement, projection, alternation removal) for those automata, and precisely characterise their complexities. We also develop algorithms for solving membership and emptiness for the languages of trees accepted by EU-automata.

We then use EU-automata to obtain several algorithmic and expressiveness results for the temporal logic QCTL (which extends CTL with quantification over atomic propositions) and for MSO. On the one hand, we obtain decision procedures with optimal complexity for QCTL satisfiability and model checking; on the other hand, we obtain an algorithm for translating any QCTL formula with k quantifier alternations to formulas with at most one quantifier alternation, at the expense of a (k+1)-exponential blow-up in the size of the formulas. Using the same techniques, we prove that any MSO formula can be translated into a formula with at most four quantifier alternations (and only two second-order-quantifier alternations), again with a (k+1)-exponential blow-up in the size of the formula.

@techreport{arxiv2410.18799-LM,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas},
  title =               {Arbitrary-arity Tree Automata and QCTL},
  number =              {2410.18799},
  year =                {2024},
  month =               oct,
  doi =                 {10.48550/arXiv.2410.18799},
  institution =         {arXiv},
  abstract =            {We~introduce a new class of automata (which we coin
                         \emph{EU-automata}) running on infininte trees of
                         arbitrary (finite) arity. We~develop and study
                         several algorithms to perform classical operations
                         (union, intersection, complement, projection,
                         alternation removal) for those automata, and
                         precisely characterise their complexities. We~also
                         develop algorithms for solving membership and
                         emptiness for the languages of trees accepted by
                         EU-automata. \par We~then use EU-automata to obtain
                         several algorithmic and expressiveness results for
                         the temporal logic \textsf{QCTL} (which extends
                         \textsf{CTL} with quantification over atomic
                         propositions) and for \textsf{MSO}. On the one hand,
                         we obtain decision procedures with optimal
                         complexity for \textsf{QCTL} satisfiability and
                         model checking; on the other hand, we obtain an
                         algorithm for translating any \textsf{QCTL} formula
                         with \(k\) quantifier alternations to formulas with
                         at most one quantifier alternation, at~the~expense
                         of a \((k+1)\)-exponential blow-up in the size of
                         the formulas. Using the same techniques, we~prove
                         that any \textsf{MSO} formula can be translated into
                         a formula with at most four quantifier alternations
                         (and only two second-order-quantifier alternations),
                         again with a \((k+1)\)-exponential blow-up in the
                         size of the formula.},
}

@inproceedings{hsnmc2004-LMG,
  author =              {L{\'e}vy, {\relax Th}omas and Marc{\'e}, Olivier and
                         Galand, Damien},
  title =               {Embedded {BGP} Routing Monitoring},
  editor =              {Mammeri, Zoubir and Lorenz, Pascal},
  booktitle =           {{P}roceedings of the 7th {IEEE} {I}nternational
                         {C}onference on {H}igh {S}peed {N}etworks and
                         {M}ultimedia {C}ommunications ({HSNMC}'04)},
  acronym =             {{HSNMC}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3079},
  pages =               {348-359},
  year =                {2004},
  month =               jun,
}

@inproceedings{LMN-fates2004,
  author =              {Larsen, Kim Guldstrand and Miku{\v{c}}ionis, Marius
                         and Nielsen, Brian},
  title =               {Online Testing of Real-time Systems Using {U}ppaal},
  editor =              {Grabowski, Jens and Nielsen, Brian},
  booktitle =           {{P}roceedings of the 4th {I}nternational {W}orkshop
                         on {F}ormal {A}pproaches to {S}oftware {T}esting
                         ({FATES}'04)},
  acronym =             {{FATES}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3395},
  pages =               {79-94},
  year =                {2004},
  month =               sep,
  doi =                 {10.1007/978-3-540-31848-4_6},
}

Résumé

We extend the framework of ATL model-checking to "simply timed" concurrent game structures, i.e., multi-agent structures where each transition carry an integral duration (or interval thereof). While the case of single durations is easily handled from the semantics point of view, intervals of durations raise several interesting questions. Moreover subtle algorithmic problems have to be handled when dealing with model checking. We propose a semantics for which we develop efficient (PTIME) algorithms for timed ATL without equality constraints, while the general case is shown to be EXPTIME-complete.

@inproceedings{formats2006-LMO,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Oreiby, Ghassan},
  title =               {Model-Checking Timed~{ATL} for Durational Concurrent
                         Game Structures},
  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 =               {245-259},
  year =                {2006},
  month =               sep,
  doi =                 {10.1007/11867340_18},
  abstract =            {We extend the framework of ATL model-checking to
                         {"}simply timed{"} concurrent game structures, i.e.,
                         multi-agent structures where each transition carry
                         an integral duration (or interval thereof). While
                         the case of single durations is easily handled from
                         the semantics point of view, intervals of durations
                         raise several interesting questions. Moreover subtle
                         algorithmic problems have to be handled when dealing
                         with model checking. We propose a semantics for
                         which we develop efficient (PTIME) algorithms for
                         timed ATL without equality constraints, while the
                         general case is shown to be EXPTIME-complete.},
}

Résumé

ATL is a temporal logic geared towards the specification and verification of properties in multi-agents systems. It allows to reason on the existence of strategies for coalitions of agents in order to enforce a given property. We prove that the standard definition of ATL (built on modalities "Next", "Always" and "Until") has to be completed in order to express the duals of its modalities: it is necessary to add the modality "Release". We then precisely characterize the complexity of ATL model-checking when the number of agents is not fixed. We prove that it is Δ2P and Δ3P-complete, depending on the underlying multi-agent model (ATS and CGS, resp.). We also prove that ATL+ model-checking is Δ3P-complete over both models, even with a fixed number of agents.

@inproceedings{fossacs2007-LMO,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Oreiby, Ghassan},
  title =               {On the Expressiveness and Complexity of~{ATL}},
  editor =              {Seidl, Helmut},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'07)},
  acronym =             {{FoSSaCS}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4423},
  pages =               {243-257},
  year =                {2007},
  month =               mar,
  doi =                 {10.1007/978-3-540-71389-0_18},
  abstract =            {ATL is a temporal logic geared towards the
                         specification and verification of properties in
                         multi-agents systems. It allows to reason on the
                         existence of strategies for coalitions of agents in
                         order to enforce a given property. We prove that the
                         standard definition of~ATL (built on modalities
                         {"}Next{"}, {"}Always{"} and~{"}Until{"}) has to be
                         completed in order to express the duals of its
                         modalities: it~is necessary to add the modality
                         {"}Release{"}. We~then precisely characterize the
                         complexity of ATL model-checking when the number of
                         agents is not fixed. We prove that it is
                         \(\Delta_{2}^{P}\) and \(\Delta_{3}^{P}\)-complete,
                         depending on the underlying multi-agent model (ATS
                         and CGS,~resp.). We also prove that~ATL\({}^{+}\)
                         model-checking is \(\Delta_{3}^{P}\)-complete over
                         both models, even with a fixed number of agents.},
}

Résumé

ATL is a temporal logic geared towards the specification and verification of properties in multi-agents systems. It allows to reason on the existence of strategies for coalitions of agents in order to enforce a given property. We prove that the standard definition of ATL (built on modalities "Next", "Always" and "Until") has to be completed in order to express the duals of its modalities: it is necessary to add the modality "Release". We then precisely characterize the complexity of ATL model-checking when the number of agents is not fixed. We prove that it is Δ2P and Δ3P-complete, depending on the underlying multi-agent model (ATS and CGS, resp.). We also prove that ATL+ model-checking is Δ3P-complete over both models, even with a fixed number of agents.

@article{lmcs4(2)-LMO,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Oreiby, Ghassan},
  title =               {On the Expressiveness and Complexity of~{ATL}},
  journal =             {Logical Methods in Computer Science},
  volume =              {4},
  number =              {2},
  year =                {2008},
  month =               may,
  doi =                 {10.2168/LMCS-4(2:7)2008},
  abstract =            {ATL is a temporal logic geared towards the
                         specification and verification of properties in
                         multi-agents systems. It allows to reason on the
                         existence of strategies for coalitions of agents in
                         order to enforce a given property. We prove that the
                         standard definition of~ATL (built on modalities
                         {"}Next{"}, {"}Always{"} and~{"}Until{"}) has to be
                         completed in order to express the duals of its
                         modalities: it~is necessary to add the modality
                         {"}Release{"}. We~then precisely characterize the
                         complexity of ATL model-checking when the number of
                         agents is not fixed. We prove that it is
                         \(\Delta_{2}^{P}\) and \(\Delta_{3}^{P}\)-complete,
                         depending on the underlying multi-agent model (ATS
                         and CGS,~resp.). We also prove that~ATL\({}^{+}\)
                         model-checking is \(\Delta_{3}^{P}\)-complete over
                         both models, even with a fixed number of agents.},
}

Résumé

Among the branching-time temporal logics used for the specification and verification of systems, CTL+, FCTL and ECTL+ are the most notable logics for which the precise computational complexity of model checking is not known. We answer this longstanding open problem and show that model checking these (and some related) logics is Δ2p-complete.

@inproceedings{fossacs2001-LMS,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Schnoebelen, {\relax Ph}ilippe},
  title =               {Model Checking {CTL}{\(^+\)} and {FCTL} is hard},
  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 =               {318-331},
  year =                {2001},
  month =               apr,
  doi =                 {10.1007/3-540-45315-6_21},
  abstract =            {Among the branching-time temporal logics used for
                         the specification and verification of systems,
                         CTL\(^+\), FCTL and ECTL\(^+\) are the most notable
                         logics for which the precise computational
                         complexity of model checking is not known. We answer
                         this longstanding open problem and show that model
                         checking these (and some related) logics is
                         \(\Delta_2^p\)-complete.},
}

Résumé

We consider quantitative model checking in durational Kripke structures (Kripke structures where transitions have integer durations) with timed temporal logics where subscripts put quantitative constraints on the time it takes before a property is satisfied. We investigate the conditions that allow polynomial-time model checking algorithms for timed versions of CTL and exhibit an important gap between logics where subscripts of the form "= c" (exact duration) are allowed, and simpler logics that only allow subscripts of the form "≤ c" or "≥ c" (bounded duration).

A surprising outcome of this study is that it provides the second example of a Δ2P-complete model checking problem.

@inproceedings{fossacs2002-LMS,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Schnoebelen, {\relax Ph}ilippe},
  title =               {On Model Checking Durational {K}ripke Structures
                         (Extended Abstract)},
  editor =              {Nielsen, Mogens and Engberg, Uffe},
  booktitle =           {{P}roceedings of the 5th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'02)},
  acronym =             {{FoSSaCS}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2303},
  pages =               {264-279},
  year =                {2002},
  month =               apr,
  doi =                 {10.1007/3-540-45931-6_19},
  abstract =            {We consider quantitative model checking in
                         \emph{durational Kripke structures} (Kripke
                         structures where transitions have integer durations)
                         with timed temporal logics where subscripts put
                         quantitative constraints on the time it takes before
                         a property is satisfied. We investigate the
                         conditions that allow polynomial-time model checking
                         algorithms for timed versions of CTL and exhibit an
                         important gap between logics where subscripts of the
                         form {"}\(= c\){"} (exact duration) are allowed, and
                         simpler logics that only allow subscripts of the
                         form {"}\(\leq c\){"} or {"}\(\geq c\){"} (bounded
                         duration).\par A surprising outcome of this study is
                         that it provides the second example of a
                         \(\Delta_2^P\)-complete model checking problem.},
}

Résumé

We investigate NLTL, a linear-time temporal logic with forgettable past. NLTL can be exponentially more succinct than LTL + Past (which in turn can be more succinct than LTL). We study satisfiability and model checking for NLTL and provide optimal automata-theoretic algorithms for these EXPSPACE-complete problems.

@inproceedings{lics2002-LMS,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Schnoebelen, {\relax Ph}ilippe},
  title =               {Temporal Logic with Forgettable Past},
  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 =               {383-392},
  year =                {2002},
  month =               jul,
  doi =                 {10.1109/LICS.2002.1029846},
  abstract =            {We investigate NLTL, a linear-time temporal logic
                         with forgettable past. NLTL can be exponentially
                         more succinct than LTL + Past (which in turn can be
                         more succinct than LTL). We study satisfiability and
                         model checking for NLTL and provide optimal
                         automata-theoretic algorithms for these
                         EXPSPACE-complete problems.},
}

Résumé

In this paper, we study model checking of timed automata (TAs), and more precisely we aim at finding efficient model checking for subclasses of TAs. For this, we consider model checking TCTL and TCTL, over TAs with one clock or two clocks.

First we show that the reachability problem is NLOGSPACE-complete for one clock TAs (i.e. as complex as reachability in classical graphs) and we give a polynomial time algorithm for model checking TCTL, over this class of TAs. Secondly we show that model checking becomes PSPACE-complete for full TCTL over one clock TAs. We also show that model checking CTL (without any timing constraint) over two clock TAs is PSPACE-complete and that reachability is NP-hard.

@inproceedings{concur2004-LMS,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Schnoebelen, {\relax Ph}ilippe},
  title =               {Model Checking Timed Automata with One or Two
                         Clocks},
  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 =               {387-401},
  year =                {2004},
  month =               aug,
  doi =                 {10.1007/978-3-540-28644-8_25},
  abstract =            {In this paper, we study model checking of timed
                         automata (TAs), and more precisely we aim at finding
                         efficient model checking for subclasses of TAs. For
                         this, we consider model checking TCTL and TCTL, over
                         TAs with one clock or two clocks.\par First we show
                         that the reachability problem is NLOGSPACE-complete
                         for one clock TAs (i.e. as complex as reachability
                         in classical graphs) and we give a polynomial time
                         algorithm for model checking TCTL, over this class
                         of TAs. Secondly we show that model checking becomes
                         PSPACE-complete for full TCTL over one clock TAs. We
                         also show that model checking CTL (without any
                         timing constraint) over two clock TAs is
                         PSPACE-complete and that reachability is NP-hard.},
}

Résumé

We consider model checking of timed temporal formulae in durational transition graphs (DTGs), i.e., Kripke structures where transitions have integer durations. Two semantics for DTGs are presented and motivated. We consider timed versions of CTL where subscripts put quantitative constraints on the time it takes before a property is satisfied.

We exhibit an important gap between logics where subscripts of the form "= c" (exact duration) are allowed, and simpler logics that only allow subscripts of the form "≤ c" or "≥ c" (bounded duration).

Without exact durations, model checking can be done in polynomial time, but with exact durations, it becomes Δ2P-complete or PSPACE-complete depending on the considered semantics.

@article{tcs353(1-3)-LMS,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Schnoebelen, {\relax Ph}ilippe},
  title =               {Efficient timed model checking for discrete-time
                         systems},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {353},
  number =              {1-3},
  pages =               {249-271},
  year =                {2006},
  month =               mar,
  doi =                 {10.1016/j.tcs.2005.11.020},
  abstract =            {We consider model checking of timed temporal
                         formulae in \emph{durational transition graphs}
                         (DTGs), \emph{i.e.}, Kripke structures where
                         transitions have integer durations. Two semantics
                         for DTGs are presented and motivated. We consider
                         timed versions of CTL where subscripts put
                         quantitative constraints on the time it takes before
                         a property is satisfied. \par We exhibit an
                         important gap between logics where subscripts of the
                         form {"}\(= c\){"} (exact duration) are allowed, and
                         simpler logics that only allow subscripts of the
                         form {"}\(\leq c\){"} or {"}\(\geq c\){"} (bounded
                         duration).\par Without exact durations, model
                         checking can be done in polynomial time, but with
                         exact durations, it becomes
                         \(\Delta_{2}^{P}\)-complete or PSPACE-complete
                         depending on the considered semantics.},
}

Résumé

Alternating-time temporal logic with strategy contexts (ATLsc) is a powerful formalism for expressing properties of multi-agent systems: it extends CTL with strategy quantifiers, offering a convenient way of expressing both collaboration and antagonism between several agents. Incomplete observation of the state space is a desirable feature in such a framework, but it quickly leads to undecidable verification problems. In this paper, we prove that uniform incomplete observation (where all players have the same observation) preserves decidability of the model checking problem, even for very expressive logics such as ATLsc.

@inproceedings{gandalf2015-LMS,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Sangnier, Arnaud},
  title =               {{{\(\textsf{ATL}_{\textsf{sc}}\)}} with partial
                         observation},
  editor =              {Esparza, Javier and Tronci, Enrico},
  booktitle =           {{P}roceedings of the 6th {I}nternational {S}ymposium
                         on {G}ames, {A}utomata, {L}ogics and {F}ormal
                         {V}erification ({GandALF}'15)},
  acronym =             {{GandALF}'15},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {193},
  pages =               {43-57},
  year =                {2015},
  month =               sep,
  doi =                 {10.4204/EPTCS.193.4},
  abstract =            {Alternating-time temporal logic with strategy
                         contexts ({{\(\textsf{ATL}_{\textsf{sc}}\)}}) is a
                         powerful formalism for expressing properties of
                         multi-agent systems: it~extends \textsf{CTL} with
                         \emph{strategy quantifiers}, offering a convenient
                         way of expressing both collaboration and antagonism
                         between several agents. Incomplete observation of
                         the state space is a desirable feature in such a
                         framework, but it quickly leads to undecidable
                         verification problems. In this paper, we prove that
                         \emph{uniform} incomplete observation (where all
                         players have the same observation) preserves
                         decidability of the model checking problem, even for
                         very expressive logics such as
                         {{\(\textsf{ATL}_{\textsf{sc}}\)}}.},
}

@inproceedings{stacs1999-LMSV,
  author =              {Lautermann, Clemens and McKenzie, Pierre and
                         Schwentick, Thomas and Vollmer, Heribert},
  title =               {The Descriptive Complexity Approach to {LOGCFL}},
  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 =               {444-454},
  year =                {1999},
  month =               mar,
}

@inproceedings{fsttcs2000-LN,
  author =              {La{~}Torre, Salvatore and Napoli, Margherita},
  title =               {A Decidable Dense Branching-time Temporal Logic},
  editor =              {Kapoor, Sanjiv and Prasad, Sanjiva},
  booktitle =           {{P}roceedings of the 20th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'00)},
  acronym =             {{FSTTCS}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1974},
  pages =               {139-150},
  year =                {2000},
  month =               dec,
}

@article{acta38(2)-LN,
  author =              {La{~}Torre, Salvatore and Napoli, Margherita},
  title =               {Timed tree automata with an application to temporal
                         logic},
  publisher =           {Springer-Verlag},
  journal =             {Acta Informatica},
  volume =              {38},
  number =              {2},
  pages =               {89-116},
  year =                {2001},
}

@inproceedings{tacas2004-LNZ,
  author =              {Lugiez, Denis and Niebert, Peter and Zennou, Sarah},
  title =               {A~partial order semantics approach to the clock
                         explosion problem of timed automata},
  editor =              {Jensen, Kurt and Podelski, Andreas},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'04)},
  acronym =             {{TACAS}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2988},
  pages =               {296-311},
  year =                {2004},
  month =               mar,
}

@article{tcs345(1)-LNZ,
  author =              {Lugiez, Denis and Niebert, Peter and Zennou, Sarah},
  title =               {A~partial order semantics approach to the clock
                         explosion problem of timed automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {345},
  number =              {1},
  pages =               {27-59},
  year =                {2005},
  month =               nov,
}

@article{ipl79(3)-Lod,
  author =              {L{\"o}ding, Christof},
  title =               {Efficient minimization of deterministic weak
                         {\(\omega\)}-automata},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {79},
  number =              {3},
  pages =               {105-109},
  year =                {2001},
  month =               jul,
}

@incollection{hat-ch8,
  author =              {L{\"o}ding, Christof},
  title =               {Automata on infinite trees},
  editor =              {Pin, Jean-{\'E}ric},
  booktitle =           {Handbook of automata theory},
  publisher =           {EMS~Press},
  volume =              {1},
  pages =               {265-302},
  chapter =             {8},
  year =                {2021},
  doi =                 {10.4171/AUTOMATA-1/8},
}

@inproceedings{lics2005-Loh,
  author =              {Lohrey, Markus},
  title =               {Model Checking Hierarchical Structures},
  booktitle =           {{P}roceedings of the 20th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'05)},
  acronym =             {{LICS}'05},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {168- 177},
  year =                {2005},
  month =               jul,
}

@inproceedings{popl1985-LP,
  author =              {Lichtenstein, Orna and Pnueli, Amir},
  title =               {Checking that Finite State Concurrent Programs
                         Satisfy their Linear Specifiction},
  booktitle =           {Conference Record of the 12th {ACM} {S}ymposium on
                         {P}rinciples of {P}rogramming {L}anguages
                         ({POPL}'85)},
  acronym =             {{POPL}'85},
  publisher =           {ACM Press},
  pages =               {97-107},
  year =                {1985},
  month =               jan,
}

@inproceedings{formats2006-LP,
  author =              {Lodaya, Kamal and Pandya, Paritosh K.},
  title =               {A Dose of Timed Logic, in Guarded Measure},
  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 =               {260-273},
  year =                {2006},
  month =               sep,
}

@article{jms145(3)-LP,
  author =              {Lifshits, Yuri M. and Pavlov, Dmitri S.},
  title =               {Potential Theory for Mean Payoff Games},
  publisher =           {Springer-Verlag},
  journal =             {Journal of Mathematical Science},
  volume =              {145},
  number =              {3},
  pages =               {4967-4974},
  year =                {2007},
  month =               sep,
}

@inproceedings{icra2014-LP,
  author =              {Liu, Jun and Prabhakar, Pavithra},
  title =               {Switching control of dynamical systems from metric
                         temporal logic specifications},
  booktitle =           {{P}roceedings of the 2014 {IEEE} {I}nternational
                         {C}onference on {R}obotics and {A}utomation
                         ({ICRA}'14)},
  acronym =             {{ICRA}'01},
  publisher =           {IEEE Robotics~\& Automation Soc.},
  pages =               {5333-5338},
  year =                {2014},
  month =               may,
  doi =                 {10.1109/ICRA.2014.6907643},
}

@inproceedings{eurocrypt2004-LPS,
  author =              {Lynn, Banjamin and Prabhakaran, Manoj and Sahai,
                         Amit},
  title =               {Positive Results and Techniques for Obfuscation},
  editor =              {Cachin, Christian and Camenisch, Jan},
  booktitle =           {{P}roceedings of the 23rd {I}nternational
                         {C}onference on the {T}heory and {A}pplications of
                         {C}ryptographic {T}echniques ({EUROCRYPT}'04)},
  acronym =             {{EUROCRYPT}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3027},
  pages =               {20-39},
  year =                {2004},
  month =               aug,
}

@inproceedings{emsoft2009-LPT,
  author =              {Lampka, Kai and Perathoner, Simon and Thiele,
                         Lothar},
  title =               {Analytic Real-time Analysis and Timed Automata:
                         A~Hybrid Method for Analyzing Embedded Real-time
                         Systems},
  editor =              {Chakraborty, Samarjit and Halbwachs, Nicolas},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {E}mbedded {S}oftware ({EMSOFT}'09)},
  acronym =             {{EMSOFT}'09},
  publisher =           {ACM Press},
  pages =               {107-116},
  year =                {2009},
  month =               oct,
  doi =                 {10.1145/1629335.1629351},
}

@article{njc6(3)-LPWY,
  author =              {Larsen, Kim Guldstrand and Pearson, Justin and
                         Weise, Carsten and Yi, Wang},
  title =               {Clock Difference Diagrams},
  publisher =           {Publishing Association Nordic Journal of Computing},
  journal =             {Nordic Journal of Computing},
  volume =              {6},
  number =              {3},
  pages =               {271-298},
  year =                {1999},
}

@article{sttt1(1-2)-LPY,
  author =              {Larsen, Kim Guldstrand and Pettersson, Paul and Yi,
                         Wang},
  title =               {{\textsc{Uppaal}} in a nutshell},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {1},
  number =              {1-2},
  pages =               {134-152},
  year =                {1997},
  month =               oct,
}

@inproceedings{clp1985-LPZ,
  author =              {Lichtenstein, Orna and Pnueli, Amir and Zuck, Lenore
                         D.},
  title =               {The Glory of the Past},
  editor =              {Parikh, Rohit},
  booktitle =           {Proceedings of the Conference on Logics of Programs
                         ({CLP}'85)},
  acronym =             {{CLP}'85},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {193},
  pages =               {413-424},
  year =                {1985},
  month =               jun,
}

@inproceedings{mfcs2003-LR,
  author =              {L{\"o}ding, Christof and Rohde, Philipp},
  title =               {Solving the Sabotage Game is {PSPACE}-hard},
  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 =               {531-540},
  year =                {2003},
  month =               aug,
}

@inproceedings{fossacs2005-LR,
  author =              {Larsen, Kim Guldstrand and Rasmussen, Jacob Illum},
  title =               {Optimal Conditional reachability for Multi-Priced
                         Timed Automata},
  editor =              {Sassone, Vladimiro},
  booktitle =           {{P}roceedings of the 8th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'05)},
  acronym =             {{FoSSaCS}'05},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3441},
  pages =               {234-249},
  year =                {2005},
  month =               apr,
}

@article{tcs390(2-3)-LR,
  author =              {Larsen, Kim Guldstrand and Rasmussen, Jacob Illum},
  title =               {Optimal Conditional reachability for Multi-Priced
                         Timed Automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {390},
  number =              {2-3},
  pages =               {197-213},
  year =                {2008},
  month =               jan,
}

@inproceedings{cav2016-LR,
  author =              {Lin, Anthony W. and R{\"u}mmer, Philipp},
  title =               {Liveness of Randomised Parameterised Systems under
                         Arbitrary Schedulers},
  editor =              {Chaudhuri, Swarat and Farzan, Azadeh},
  booktitle =           {{P}roceedings of the 28th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'16)},
  acronym =             {{CAV}'16},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9779},
  pages =               {112-133},
  year =                {2016},
  month =               jul,
  doi =                 {10.1007/978-3-319-41540-6_7},
}

@inproceedings{ifipprocomet1998-LRL,
  author =              {Liu, Zhiming and Ravn, Anders P. and Li, Xiaochan},
  title =               {Verifying Duration Properties of Timed Transition
                         Systems},
  editor =              {Gries, David and de Roever, Willem-Paul},
  booktitle =           {{P}roceedings of the 2nd {IFIP} {I}nternational
                         {C}onference on {P}rogramming {C}oncepts and
                         {M}ethods ({PROCOMET}'98)},
  acronym =             {{PROCOMET}'98},
  publisher =           {Chapman \& Hall},
  series =              {IFIP Conference Proceedings},
  volume =              {125},
  pages =               {327-345},
  year =                {1998},
  month =               jun,
}

@inproceedings{rts1992-LS,
  author =              {Lynch, Nancy and Shavit, Nir},
  title =               {Timing-Based Mutual Exclusion},
  booktitle =           {{P}roceedings of the 13th {S}ymposium on {R}eal-Time
                         {S}ystems ({RTSS}'92)},
  acronym =             {{RTSS}'92},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {2-11},
  year =                {1992},
  month =               dec,
}

@inproceedings{stacs1994-LS,
  author =              {Laroussinie, Fran{\c c}ois and Schnoebelen, {\relax
                         Ph}ilippe},
  title =               {A Hierarchy of Temporal Logics with Past},
  editor =              {Enjalbert, Patrice and Mayr, Ernst W. and Wagner,
                         Klaus W.},
  booktitle =           {{P}roceedings of the 11th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'94)},
  acronym =             {{STACS}'94},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {775},
  pages =               {47-58},
  year =                {1994},
  month =               feb,
}

@article{tcs148(2)-LS,
  author =              {Laroussinie, Fran{\c c}ois and Schnoebelen, {\relax
                         Ph}ilippe},
  title =               {A Hierarchy of Temporal Logics with Past},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {148},
  number =              {2},
  pages =               {303-324},
  year =                {1995},
  month =               sep,
}

@inproceedings{icalp1998-LS,
  author =              {Liu, Xinxin and Smolka, Scott A.},
  title =               {Simple Linear-Time Algorithms for Minimal Fixed
                         Points},
  editor =              {Larsen, Kim Guldstrand and Skyum, Sven and Winskel,
                         Glynn},
  booktitle =           {{P}roceedings of the 25th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'98)},
  acronym =             {{ICALP}'98},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1443},
  pages =               {53-66},
  year =                {1998},
  month =               jul,
}

@article{icomp156(1-2)-LS,
  author =              {Laroussinie, Fran{\c c}ois and Schnoebelen, {\relax
                         Ph}ilippe},
  title =               {Specification in {CTL}+{P}ast for Verification in
                         {CTL}},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {156},
  number =              {1-2},
  pages =               {236-263},
  year =                {2000},
  month =               jan,
}

@inproceedings{fossacs2000-LS,
  author =              {Laroussinie, Fran{\c c}ois and Schnoebelen, {\relax
                         Ph}ilippe},
  title =               {The State-Explosion Problem from Trace to
                         Bisimulation Equivalence},
  editor =              {Tiuryn, Jerzy},
  booktitle =           {{P}roceedings of the 3rd {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'00)},
  acronym =             {{FoSSaCS}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1784},
  pages =               {192-207},
  year =                {2000},
  month =               mar,
  doi =                 {10.1007/3-540-46432-8_13},
}

@article{deds11(4)-LS,
  author =              {Lunze, Jan and Schr{\"o}der, Jochen},
  title =               {State observation and diagnosis of discrete-event
                         systems described by stochastic automata},
  publisher =           {Kluwer Academic},
  journal =             {Discrete Event Dynamic Systems},
  volume =              {11},
  number =              {4},
  pages =               {319-369},
  year =                {2001},
  month =               oct,
  doi =                 {10.1023/A:1011273108731},
}

@inproceedings{fossacs2002-LS,
  author =              {Lange, Martin and Stirling, Colin},
  title =               {Model Checking Fixed Point Logic with Chop},
  editor =              {Nielsen, Mogens and Engberg, Uffe},
  booktitle =           {{P}roceedings of the 5th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'02)},
  acronym =             {{FoSSaCS}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2303},
  pages =               {250-263},
  year =                {2002},
  month =               apr,
}

@article{jlap78(5)-LS,
  author =              {Leucker, Martin and Schallart, Christian},
  title =               {A brief account of runtime verification},
  publisher =           {Elsevier},
  journal =             {Journal of Logic and Algebraic Programming},
  volume =              {78},
  number =              {5},
  pages =               {293-303},
  year =                {2009},
  month =               may,
  doi =                 {10.1016/j.jlap.2008.08.004},
}

@inproceedings{latin2000-LST,
  author =              {Laroussinie, Fran{\c c}ois and Schnoebelen, {\relax
                         Ph}ilippe and Turuani, Mathieu},
  title =               {On the Expressive and Complexity of Quantitative
                         Branching-Time Temporal Logics},
  editor =              {Gonnet, Gastn H. and Panario, Daniel and Viola,
                         Alfredo},
  booktitle =           {{P}roceedings of the 4th {L}atin {A}merican
                         {S}ymposium on {T}heoretical {IN}formatics
                         ({LATIN}'00)},
  acronym =             {{LATIN}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1776},
  pages =               {437-446},
  year =                {2000},
  month =               apr,
}

@article{tcs297(1-3)-LST,
  author =              {Laroussinie, Fran{\c c}ois and Schnoebelen, {\relax
                         Ph}ilippe and Turuani, Mathieu},
  title =               {On the expressivity and complexity of quantitative
                         branching-time temporal logics},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {297},
  number =              {1-3},
  pages =               {297-315},
  year =                {2003},
  month =               mar,
}

@inproceedings{csl2001-LSW,
  author =              {Lutz, Carsten and Sattler, Ulrike and Wolter, Frank},
  title =               {Modal Logic and the Two-Variable Fragment},
  editor =              {Fribourg, Laurent},
  booktitle =           {{P}roceedings of the 15th {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'01)},
  acronym =             {{CSL}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2142},
  pages =               {247-261},
  year =                {2001},
  month =               sep,
}

@inproceedings{ifiptcs2000-LT,
  author =              {L{\"o}ding, Christof and Thomas, Wolfgang},
  title =               {Alternating Automata and Logics over Infinite Words},
  editor =              {van Leeuwen, Jan and Watanabe, Osamu and Hagiya,
                         Masami and Mosses, Peter D. and Ito, Takayasu},
  booktitle =           {{E}xploring {N}ew {F}rontiers of {T}heoretical
                         {I}nformatics~--- {P}roceedings of the 1st {IFIP}
                         {I}nternational {C}onference on {T}heoretical
                         {C}omputer {S}cience ({IFIPTCS}'00)},
  acronym =             {{IFIPTCS}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1872},
  pages =               {521-535},
  year =                {2000},
  month =               aug,
}

@inproceedings{fossacs2003-Lug,
  author =              {Lugiez, Denis},
  title =               {Counting and Equality Constraints for Multitree
                         Automata},
  editor =              {Gordon, Andrew D.},
  booktitle =           {{P}roceedings of the 6th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'03)},
  acronym =             {{FoSSaCS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2620},
  pages =               {328-342},
  year =                {2003},
  month =               apr,
}

@techreport{arxiv-cs.GT/0806.2923,
  author =              {Luttenberger, Michael},
  title =               {Strategy Iteration using Non-Deterministic
                         Strategies for Solving Parity Games},
  number =              {cs.GT/0806.2923},
  year =                {2008},
  month =               jun,
  institution =         {arXiv},
  type =                {Research Report},
}

@inproceedings{focs1999-LV,
  author =              {Lipton, Richard J. and Viglas, Anastasios},
  title =               {On the Complexity of {SAT}},
  booktitle =           {{P}roceedings of the 40th {A}nnual {S}ymposium on
                         {F}oundations of {C}omputer {S}cience ({FOCS}'99)},
  acronym =             {{FOCS}'99},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {459-464},
  year =                {1999},
  month =               nov,
}

@inproceedings{fossacs2005-LW,
  author =              {Lasota, S{\l}awomir and Walukiewicz, Igor},
  title =               {Alternating Timed Automata},
  editor =              {Sassone, Vladimiro},
  booktitle =           {{P}roceedings of the 8th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'05)},
  acronym =             {{FoSSaCS}'05},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3441},
  pages =               {250-265},
  year =                {2005},
  month =               apr,
}

@article{tocl9(2)-LW,
  author =              {Lasota, S{\l}awomir and Walukiewicz, Igor},
  title =               {Alternating Timed Automata},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {9},
  number =              {2},
  year =                {2008},
  month =               mar,
}

@article{lww-icomp2007,
  author =              {Lutz, Carsten and Walther, Dirk and Wolter, Frank},
  title =               {Quantitative temporal logics over the reals:
                         {PSPACE} and below},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {205},
  number =              {1},
  pages =               {99-123},
  year =                {2007},
  month =               jan,
  doi =                 {10.1016/j.ic.2006.08.006},
}

@inproceedings{mfps1993-LY,
  author =              {Larsen, Kim Guldstrand and Yi, Wang},
  title =               {Time Abstracted Bisimiulation: Implicit
                         Specifications and Decidability},
  editor =              {Brookes, Setphen D. and Main, Michael G. and Melton,
                         Austin and Mislove, Michael W. and Schmidt, David
                         A.},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {M}athematical {F}oundations of
                         {P}rogramming {S}emantics ({MFPS}'93)},
  acronym =             {{MFPS}'93},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {802},
  pages =               {160-176},
  year =                {1994},
  confyear =            {1993},
  confmonth =           {4},
}

@inproceedings{lics2020-LZ,
  author =              {Lehtinen, Karoliina and Zimmermann, Martin},
  title =               {Good-for-games {\(\omega\)}-pushdown automata},
  editor =              {Hermanns, Holger and Zhang, Lijun and Kobayashi,
                         Naoki and Miller, Dale},
  booktitle =           {{P}roceedings of the 35th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'20)},
  acronym =             {{LICS}'20},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {689-702},
  year =                {2020},
  month =               jul,
  doi =                 {10.1145/3373718.3394737},
}