@inproceedings{Demri94,
  address = {Sofia, Bulgaria},
  month = sep,
  year = 1994,
  publisher = {World Scientific},
  editor = {Jorrand, {\relax Ph}ilippe and Sgurev, Vasil},
  booktitle = {{P}roceedings of the 6th {I}nternational
               {C}onference on {A}rtificial {I}ntelligence:
               {M}ethodology, {S}ystems, {A}pplications},
  author = {Demri, St{\'e}phane},
  title = {Resolution for Weak Modal Logics},
  pages = {131-140},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/demri-aimsa94.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/demri-aimsa94.ps}
}
@inproceedings{BoydelaTour::Demri95,
  address = {Montr{\'e}al, Qu{\'e}bec, Canada},
  month = aug,
  year = 1995,
  publisher = {Morgan Kaufmann},
  editor = {Wermter, Stefan and Riloff, Ellen and Scheler, Gabriele},
  acronym = {{IJCAI}'85},
  booktitle = {{P}roceedings of the 14th {I}nternational {J}oint 
               {C}onference on {A}rtificial {I}ntelligence
               ({IJCAI}'85)},
  author = {Boy de la Tour, {\relax Th}ierry and 
                 Demri, St{\'e}phane},
  title = {On the Complexity of Extending Ground Resolution 
                 with Symmetry Rules},
  pages = {289-295},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BoyDem-ijcai95.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BoyDem-ijcai95.ps}
}
@article{Demri95a,
  publisher = {Taylor \& Francis},
  journal = {Journal of Applied Non-Classical Logics},
  author = {Demri, St{\'e}phane},
  title = {Uniform and Non Uniform Strategies for Tableaux
                 Calculi for Modal Logics},
  volume = {5},
  number = {1},
  pages = {77-96},
  year = {1995}
}
@article{Demri95b,
  publisher = {Elsevier Science Publishers},
  journal = {Information Processing Letters},
  author = {Demri, St{\'e}phane},
  title = {{SAT} = 3-{SAT} for a Class of Normal Modal 
                 Logics},
  volume = {54},
  number = {5},
  pages = {281-287},
  year = {1995},
  month = jun
}
@inproceedings{Demri95d,
  address = {Paris, France},
  month = jul,
  year = 1995,
  optaddress = {Paris, France},
  publisher = {Angkor},
  editor = {De Glas, Michel and Pawlak, Zdzislaw},
  acronym = {{WOCFAI}'95},
  booktitle = {{P}roceedings of the 2nd {W}orld {C}onference
               on the {F}oundamentals of {A}rtificial 
               {I}ntelligence
               ({WOCFAI}'95)},
  author = {Demri, St{\'e}phane},
  title = {A Hierarchy of Backward Translations: 
                 {A}pplications to Modal Logics},
  pages = {121-132}
}
@inproceedings{Demri96c,
  address = {Cracow, Poland},
  month = sep,
  year = 1996,
  volume = 1113,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Penczek, Wojciech and Szalas, Andrzej},
  acronym = {{MFCS}'96},
  booktitle = {{P}roceedings of the 21st
               {I}nternational {S}ymposium on
               {M}athematical {F}oundations of 
               {C}omputer {S}cience
               ({MFCS}'96)},
  author = {Demri, St{\'e}phane},
  title = {A Class of Information Logics with a Decidable
                 Validity Problem},
  pages = {291-302}
}
@inproceedings{Demri96d,
  address = {Terrasini, Palermo, Italy},
  month = may,
  year = 1996,
  volume = 1071,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Miglioli, Pierangelo and Moscato, Ugo and
            Mundici, Daniele and Ornaghi, Mario},
  acronym = {{TABLEAUX}'96},
  booktitle = {{P}roceedings of the 5th {I}nternational
               {W}orkshop on {T}heorem {P}roving with 
               {A}nalytic {T}ableaux and {R}elated {M}ethods
               ({TABLEAUX}'96)},
  author = {Demri, St{\'e}phane},
  title = {A Simple Tableau System for the Logic of Elsewhere},
  pages = {177-192},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri96d.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri96d.pdf}
}
@article{Demri::Orlowska96e,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Demri, St{\'e}phane and Or{\l}owska, Ewa},
  title = {Logical Analysis of Demonic Nondeterministic
                 Programs},
  volume = {166},
  number = {1-2},
  pages = {173-202},
  year = {1996},
  month = oct,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DemOrl96e.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DemOrl96e.pdf}
}
@inproceedings{Balbiani::Demri97,
  address = {Nagoya, Japan},
  month = aug,
  year = 1997,
  publisher = {Morgan Kaufmann},
  editor = {Ralescu, Anca L. and Shanahan, James G.},
  acronym = {{IJCAI}'97},
  booktitle = {{P}roceedings of the 15th {I}nternational {J}oint 
               {C}onference on {A}rtificial {I}ntelligence
               ({IJCAI}'97)},
  author = {Balbiani, {\relax Ph}ilippe and Demri, St{\'e}phane},
  title = {Prefixed Tableaux Systems for Modal Logics with
                 Enriched Languages},
  pages = {190-195},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/balbiani-demri-ijcai97.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/
  		  balbiani-demri-ijcai97.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/balbiani-demri-ijcai97.pdf}
}
@article{Demri97a,
  publisher = {Kluwer Academic Publishers},
  journal = {Studia Logica},
  author = {Demri, St{\'e}phane},
  title = {A Completeness Proof for a Logic with an Alternative
                 Necessity Operator},
  volume = {58},
  number = {1},
  pages = {99-112},
  year = {1997},
  month = jan
}
@article{Demri98a,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Demri, St{\'e}phane},
  title = {A Class of Decidable Information Logics},
  volume = {195},
  number = {1},
  pages = {33-60},
  year = {1998},
  month = mar,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri98a.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri98a.pdf}
}
@inproceedings{Demri::Konikowska98,
  address = {Dagstuhl, Germany},
  month = oct,
  year = 1998,
  volume = 1489,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Dix, J{\"u}rgen and Fari{\~n}as, Luis and
            Furbach, Ulrich},
  acronym = {{JELIA}'98},
  booktitle = {{P}roceedings of the {E}uropean {W}orkshop
               on {L}ogics in {A}rtificial {I}ntelligence
               ({JELIA}'98)},
  author = {Demri, St{\'e}phane and Konikowska, Beata},
  title = {Relative Similarity Logics are Decidable: 
                 {R}eduction to
                 {FO\(^2\)} with Equality},
  pages = {279-293},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DemKon-jelia98.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DemKon-jelia98.ps}
}
@incollection{Demri::Orlowska98a,
  author = {Demri, St{\'e}phane and Or{\l}owska, Ewa},
  title = {Complementarity Relations: {R}eduction of 
                 Decision Rules
                 and Informational Representability},
  editor = {Polkowski, Lech and Skowron, Andrzej},
  booktitle = {Rough Sets in Knowledge Discovery~--- 
                  1.~Methodology and Applications},
  series = {Studies in Fuzziness and Soft Computing},
  volume = 18,
  chapter = {5},
  type = {chapter},
  pages = {99-106},
  year = {1998},
  month = oct,
  publisher = {Physica Verlag}
}
@incollection{Demri::Orlowska98c,
  author = {Demri, St{\'e}phane and Or{\l}owska, Ewa},
  title = {Informational representability of models for
                 information logics},
  editor = {Rasiowa, Helena and Or{\l}owska, Ewa},
  booktitle = {Logic at Work. Essays Dedicated to the Memory of
                 Helena Rasiowa},
  chapter = {22},
  type = {chapter},
  pages = {383-409},
  series = {Studies in Fuzziness and Soft Computing},
  volume = 24,
  year = {1999},
  month = may,
  publisher = {Physica Verlag}
}
@incollection{Demri::Orlowska98d,
  author = {Demri, St{\'e}phane and Or{\l}owska, Ewa},
  title = {Logical analysis of indiscernibility},
  editor = {Or{\l}owska, Ewa},
  booktitle = {Incomplete Information: Rough Set Analysis},
  chapter = {11},
  type = {chapter},
  pages = {347-380},
  series = {Studies in Fuzziness and Soft Computing},
  volume = 13,
  year = {1998},
  month = jan,
  publisher = {Physica Verlag}
}
@inproceedings{demri98,
  address = {Paris, France},
  month = feb,
  year = 1998,
  volume = 1373,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Morvan, Michel and Meinel, {\relax Ch}ristoph and
            Krob, Daniel},
  acronym = {{STACS}'98},
  booktitle = {{P}roceedings of the 15th {A}nnual
               {S}ymposium on {T}heoretical {A}spects of
               {C}omputer {S}cience
               ({STACS}'98)},
  author = {Demri, St{\'e}phane and Schnoebelen, {\relax Ph}ilippe},
  title = {The Complexity of Propositional Linear Temporal Logics
                 in Simple Cases (Extended Abstract)},
  pages = {61-72},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DemSch-stacs98.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DemSch-stacs98.ps},
  doi = {10.1007/BFb0028549}
}
@article{Demri99a,
  publisher = {Kluwer Academic Publishers},
  journal = {Journal of Logic, Language and Information},
  author = {Demri, St{\'e}phane},
  title = {A~Logic with Relative Knowledge Operators},
  volume = {8},
  number = {2},
  pages = {167-185},
  year = {1999},
  month = jan,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Dem-JOLLI99.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Dem-JOLLI99.ps}
}
@inproceedings{Demri99c,
  address = {Saratoga Springs, New York, USA},
  month = jun,
  year = 1999,
  volume = 1617,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Murray, Neil V.},
  acronym = {{TABLEAUX}'99},
  booktitle = {{P}roceedings of the 8th {I}nternational
               {W}orkshop on {T}heorem {P}roving with 
               {A}nalytic {T}ableaux and {R}elated {M}ethods
               ({TABLEAUX}'99)},
  author = {Demri, St{\'e}phane},
  title = {Sequent Calculi for Nominal Tense Logics: {A}~Step
                 towards Mechanization?},
  pages = {140-154},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri99c.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri99c.pdf}
}
@inproceedings{Demri::Gore99a,
  address = {Saratoga Springs, New York, USA},
  month = jun,
  year = 1999,
  volume = 1617,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Murray, Neil V.},
  acronym = {{TABLEAUX}'99},
  booktitle = {{P}roceedings of the 8th {I}nternational
               {W}orkshop on {T}heorem {P}roving with 
               {A}nalytic {T}ableaux and {R}elated {M}ethods
               ({TABLEAUX}'99)},
  author = {Demri, St{\'e}phane and Gor{\'e}, Rajeev P.},
  title = {Cut-Free Display Calculi for Nominal Tense Logics},
  pages = {155-170}
}
@inproceedings{Demri::Gore99c,
  address = {Trento, Italy},
  month = jul,
  year = 1999,
  volume = 1632,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Ganzinger, Harald},
  acronym = {{CADE}'99},
  booktitle = {{P}roceedings of the 16th {I}nternational 
               {C}onference on {A}utomated {D}eduction
               ({CADE}'99)},
  author = {Demri, St{\'e}phane and Gor{\'e}, Rajeev P.},
  title = {Tractable Transformations from Modal Provability
                 Logics into First-Order Logic},
  pages = {16-30},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DG-cade99.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DG-cade99.ps}
}
@article{Demri::Orlowska99a,
  publisher = {Kluwer Academic Publishers},
  journal = {Studia Logica},
  author = {Demri, St{\'e}phane and Or{\l}owska, Ewa},
  title = {Every Finitely Reducible Logic has the Finite Model
                 Property with Respect to the Class of 
                 {{\(\diamond\)}}-Formulae},
  volume = {62},
  number = {2},
  pages = {177-200},
  year = {1999},
  month = mar,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DO-STUDLOG99.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DO-STUDLOG99.ps}
}
@inproceedings{Demri::Orlowska99b,
  author = {Demri, St{\'e}phane and Or{\l}owska, Ewa},
  title = {Informational Representability: {A}bstract Models 
                 versus Concrete Models},
  editor = {Dubois, Didier and Prade, Henri and Klement, Erich Peter},
  booktitle = {Fuzzy sets, Logics and Reasoning about Knowledge},
  pages = {301-314},
  year = {1999},
  publisher = {Kluwer Academic Publishers}
}
@inproceedings{Demri::Orlowska::Vakarelov99,
  month = jun,
  year = 1999,
  editor = {Gerbrandy, Jelle and Marx, Maarten and 
                   de Rijke, Maarten and Venema, Venema Yde},
  booktitle = {{JFAK}: {E}ssays {D}edicated to {J}ohan van
               {B}enthem on the {O}ccasion of his
               50th {B}irthday},
  author = {Demri, St{\'e}phane and Or{\l}owska, Ewa and 
                 Vakarelov, Dimiter},
  title = {Indiscernibility and Complementarity Relations in
                 {P}awlak's Information Systems},
  nopages = {},
  url-invalid = {http://www.illc.uva.nl/~j50/},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DOV99.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DOV99.pdf}
}
@inproceedings{Demri00a,
  address = {St Andrews, Scotland, UK},
  month = jul,
  year = 2000,
  volume = 1847,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Dyckhoff, Roy},
  acronym = {{TABLEAUX} 2000},
  booktitle = {{P}roceedings of the 9th {I}nternational
               {W}orkshop on {T}heorem {P}roving with 
               {A}nalytic {T}ableaux and {R}elated {M}ethods
               ({TABLEAUX} 2000)},
  author = {Demri, St{\'e}phane},
  title = {Complexity of Simple Dependent Bimodal Logics},
  pages = {190-204},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Dem-tableaux2000.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Dem-tableaux2000.ps}
}
@article{Demri00b,
  publisher = {{IOS} Press},
  journal = {Fundamenta Informaticae},
  author = {Demri, St{\'e}phane},
  title = {The Nondeterministic Information Logic {NIL} is
                 {PSPACE}-complete},
  volume = {42},
  number = {3-4},
  pages = {211-234},
  year = {2000},
  month = apr # {-} # may,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Dem-FUNDI2000.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Dem-FUNDI2000.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Dem-FUNDI2000.pdf}
}
@article{Demri00d,
  journal = {Multiple-Valued Logic},
  author = {Demri, St{\'e}phane},
  title = {A Simple Modal Encoding of Propositional Finite
                 Many-Valued Logics},
  volume = {6},
  pages = {443-461},
  year = {2000},
  missingmonth = {},
  missingnmonth = {},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/sd-ijmvl00.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/sd-ijmvl00.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/sd-ijmvl00.pdf}
}
@article{Demri::Gabbay00a,
  publisher = {Kluwer Academic Publishers},
  journal = {Studia Logica},
  author = {Demri, St{\'e}phane and Gabbay, Dov M.},
  title = {On Modal Logics Characterized by Models with  
                 Relative
                 Accessibility Relations: {P}art {I}},
  volume = {65},
  number = {3},
  pages = {323-353},
  year = {2000},
  month = aug,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/demri-gabbay-sl00-1.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/demri-gabbay-sl00-1.ps}
}
@article{Demri::Gabbay00b,
  publisher = {Kluwer Academic Publishers},
  journal = {Studia Logica},
  author = {Demri, St{\'e}phane and Gabbay, Dov M.},
  title = {On Modal Logics Characterized by Models with 
                 Relative
                 Accessibility Relations: {P}art {II}},
  volume = {66},
  number = {3},
  pages = {349-384},
  year = {2000},
  month = dec,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/demri-gabbay-sl00-2.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/demri-gabbay-sl00-2.ps}
}
@article{Demri::Gore00a,
  publisher = {Kluwer Academic Publishers},
  journal = {Journal of Logic, Language and Information},
  author = {Demri, St{\'e}phane and Gor{\'e}, Rajeev P.},
  title = {Display Calculi for Logics with Relative Accessibility
                 Relations},
  volume = {9},
  number = {2},
  pages = {213-236},
  year = {2000},
  month = apr,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri-Gore00a.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri-Gore00a.pdf}
}
@inproceedings{Demri::Gore00b,
  address = {Schloss Wilhelminenberg, Vienna, Austria},
  year = 2000,
  volume = 1761,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Caferra, Ricardo and Salzer, Gernot},
  acronym = {{FTP}'98},
  booktitle = {{S}elected {P}apers in {A}utomated
               {D}eduction in {C}lassical and {N}on-{C}lassical
               {L}ogics
               ({FTP}'98)},
  author = {Demri, St{\'e}phane and Gor{\'e}, Rajeev P.},
  title = {An {{\(O((n\cdot\log \ n)^3)\)}}-Time 
                 Transformation from
                 {Grz} into Decidable Fragments of Classical 
                 First-Order
                 Logic},
  pages = {153-167},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri-Gore00b.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri-Gore00b.pdf}
}
@article{Demri::Stepaniuk00,
  publisher = {{IOS} Press},
  journal = {Fundamenta Informaticae},
  author = {Demri, St{\'e}phane and Stepaniuk, Jaroslaw},
  title = {Computational Complexity of Multimodal Logics 
                 Based on Rough Sets},
  volume = {44},
  number = {4},
  pages = {373-396},
  year = {2000},
  month = nov # {-} # dec,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DemStep-FUNDI2000.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DemStep-FUNDI2000.ps}
}
@inproceedings{Alechina::Demri::deRijke01,
  address = {Rome, Italy},
  month = sep,
  year = 2001,
  volume = 45,
  series = {CEUR Workshop Proceedings},
  publisher = {RWTH Aachen, Germany},
  editor = {Lenzerini, Maurizio and Nardi, Daniele and Nutt, Werner
            and Suciu, Dan},
  acronym = {{KRDB}'01},
  booktitle = {{P}roceedings of the 8th {I}nternational 
               {W}orkshop on {K}nowledge {R}epresentation meets
               {D}atabases
               ({KRDB}'01)},
  author = {Alechina, Natasha and Demri, St{\'e}phane and 
                  de Rijke, Maarten},
  title = {Path Constraints from a Modal Logic Point of View
                 (Extended Abstract)},
  missingpages = {},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ADdR-krdb01.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ADdR-krdb01.ps}
}
@inproceedings{Demri01a,
  address = {Warsaw, Poland},
  year = 2001,
  volume = 65,
  series = {Studies in Fuzziness and Soft Computing},
  publisher = {Springer},
  editor = {Or{\l}pwska, Ewa and Szalas, Andrzej},
  acronym = {{RelMiCS}'98},
  booktitle = {{R}elational {M}ethods for {C}omputer 
           {S}cience {A}pplications.
           {S}elected {P}apers from 4th {I}nternational
           {S}eminar  on {R}elational {M}ethods in {L}ogic,
           {A}lgebra and {C}omputer {S}cience
           ({RelMiCS}'98)},
  author = {Demri, St{\'e}phane},
  title = {Coping with Semilattices of Relations in Logics with
                 Relative Accessibility Relations},
  pages = {163-181},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri01a.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri01a.pdf}
}
@article{demri-jlc2001,
  publisher = {Oxford University Press},
  journal = {Journal of Logic and Computation},
  author = {Demri, St{\'e}phane},
  title = {The Complexity of Regularity in Grammar Logics and
                 Related Modal Logics},
  volume = {11},
  number = {6},
  pages = {933-960},
  year = {2001},
  missingmonth = {},
  missingnmonth = {},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-jlc2001.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/demri-jlc2001.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-jlc2001.pdf}
}
@inproceedings{DD-fsttcs2002,
  address = {Kanpur, India},
  month = dec,
  year = 2002,
  volume = 2556,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Agrawal, Manindra and Seth, Anil},
  acronym = {{FSTTCS}'02},
  booktitle = {{P}roceedings of the 22nd {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'02)},
  author = {Demri, St{\'e}phane and D'Souza, Deepak},
  title = {An Automata-Theoretic Approach to Constraint {LTL}},
  pages = {121-132},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DemDsou-fsttcs02.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DemDsou-fsttcs02.ps}
}
@inproceedings{DLS-stacs2002,
  address = {Antibes Juan-les-Pins, France},
  month = mar,
  year = 2002,
  volume = 2285,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Alt, Helmut and Ferreira, Afonso},
  acronym = {{STACS}'02},
  booktitle = {{P}roceedings of the 19th {A}nnual
               {S}ymposium on {T}heoretical {A}spects of
               {C}omputer {S}cience
               ({STACS}'02)},
  author = {Demri, St{\'e}phane and Laroussinie, Fran{\c{c}}ois and
                 Schnoebelen, {\relax Ph}ilippe},
  title = {A Parametric Analysis of the State Explosion Problem
                 in Model Checking (Extended Abstract)},
  pages = {620-631},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLS-stacs2002.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DLS-stacs2002.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLS-stacs2002.pdf},
  abstract = {In model checking, the state explosion problem occurs when 
one checks a
\emph{non-flat system}, \emph{i.e.}~a system implicitly described as a
synchronized product of elementary subsystems. In this paper, we
investigate the complexity of a wide variety of model checking problems for
non-flat systems under the light of \emph{parameterized complexity}, taking
the number of synchronized components as a parameter. We provide precise
complexity measures (in the parameterized sense) for most of the problems
we investigate, and evidence that the results are robust.}
}
@article{DS-ICOMP2001,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Demri, St{\'e}phane and Schnoebelen, {\relax Ph}ilippe},
  title = {The Complexity of Propositional Linear Temporal Logics
                 in Simple Cases},
  volume = {174},
  number = {1},
  pages = {84-103},
  year = {2002},
  month = apr,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DS-ICOMP2001.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DS-ICOMP2001.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DS-ICOMP2001.pdf},
  doi = {10.1006/inco.2001.3094},
  abstract = {It is well-known that model 
	checking and satisfiability for PLTL are 
	PSPACE-complete. By contrast, very little is 
	known about whether there exist some 
	interesting fragments of PLTL with a lower 
	worst-case complexity. Such results would help 
	understand why PLTL model checkers are 
	successfully used in practice.\par
	In this paper we investigate this issue and 
	consider model checking and satisfiability for 
	all fragments of PLTL obtainable by 
	restricting (1) the temporal connectives 
	allowed, (2) the number of atomic 
	propositions, and (3) the temporal height.}
}
@inproceedings{Demri01b,
  address = {Leipzig, Germany},
  year = 2002,
  publisher = {World Scientific},
  editor = {de Rijke, Maarten and Wansing, Heinrich and
            Wolter, Frank and Zakharyaschev, Michael},
  acronym = {{AiML} 2000},
  booktitle = {{S}elected {P}apers from the 3rd
               {W}orkshop on {A}dvances in {M}odal {L}ogics
               ({AiML} 2000)},
  author = {Demri, St{\'e}phane},
  title = {Modal Logics with Weak Forms of Recursion: {PSPACE}
                 Specimens},
  pages = {113-138},
  note = {Invited paper},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/sd-aiml00.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/sd-aiml00.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/sd-aiml00.pdf}
}
@article{Demri::Gore01a,
  publisher = {Oxford University Press},
  journal = {Journal of Logic and Computation},
  author = {Demri, St{\'e}phane and Gor{\'e}, Rajeev P.},
  title = {Display Calculi for Nominal Tense Logics},
  volume = {12},
  number = {6},
  pages = {993-1016},
  year = {2002},
  month = dec,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DemGor-jlc02-1.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DemGor-jlc02-1.ps}
}
@article{Demri::Gore01b,
  publisher = {Oxford University Press},
  journal = {Journal of Logic and Computation},
  author = {Demri, St{\'e}phane and Gor{\'e}, Rajeev P.},
  title = {Theoremhood Preserving Maps Characterising Cut
                 Elimination for Modal Provability Logics},
  volume = {12},
  number = {5},
  pages = {861-884},
  year = {2002},
  month = oct,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DemGor-jlc02-2.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DemGor-jlc02-2.ps}
}
@book{Demri::Orlowska02,
  author = {Demri, St{\'e}phane and Or{\l}owska, Ewa},
  title = {Incomplete Information: Structure, Inference,
                 Complexity},
  series = {EATCS Monographs},
  year = {2002},
  missingnumber = {},
  missingmonth = {},
  missingnmonth = {},
  publisher = {Springer},
  isbn = {3-540-41904-7},
  url = {http://www.springer.com/978-3-540-41904-7},
  olderurl = {http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-41904-7}
}
@article{Demri::Sattler02,
  publisher = {{IOS} Press},
  journal = {Fundamenta Informaticae},
  author = {Demri, St{\'e}phane and Sattler, Ulrike},
  title = {Automata-Theoretic Decision Procedures for Information
                 Logics},
  volume = {53},
  number = {1},
  pages = {1-22},
  year = {2002},
  missingmonth = {},
  missingnmonth = {},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ds-fund-02.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ds-fund-02.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ds-fund-02.pdf}
}
@techreport{JGL:dico:3.1,
  author = {Goubault{-}Larrecq, Jean and 
                 Pouzol, Jean-{\relax Ph}ilippe and Demri, St{\'e}phane
                 and M{\'e}, Ludovic and Carle, P.},
  missingauthor = {},
  title = {Langages de d{\'e}tection d'attaques par signatures},
  year = {2002},
  month = jun,
  type = {Contract Report},
  number = {(Sous-projet~3, livrable~1)},
  institution = {Projet RNTL DICO},
  oldhowpublished = {Sous-projet 3, livrable 1 du projet RNTL DICO. Version
                 1},
  note = {30 pages}
}
@article{Alechina::Demri::DeRijke02,
  publisher = {Oxford University Press},
  journal = {Journal of Logic and Computation},
  author = {Alechina, Natasha and Demri, St{\'e}phane and 
                  de Rijke, Maarten},
  title = {A Modal Perspective on Path Constraints},
  volume = {13},
  number = {6},
  pages = {939-956},
  year = {2003},
  missingmonth = {},
  missingnmonth = {},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/final-jlc-adr.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/final-jlc-adr.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/final-jlc-adr.pdf}
}
@article{Demri02,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Demri, St{\'e}phane},
  title = {A Polynomial-Space Construction of Tree-Like Models
                 for Logics with Local Chains of Modal Connectives},
  volume = {300},
  number = {1-3},
  pages = {235-258},
  year = {2003},
  month = may,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-tcs02.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/demri-tcs02.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-tcs02.pdf},
  doi = {10.1016/S0304-3975(02)00082-8}
}
@misc{Demri03,
  author = {Demri, St{\'e}phane},
  title = {({M}odal) Logics for Semistructured Data (Bis)},
  year = 2003,
  month = sep,
  howpublished = {Invited talk, 3rd
           {W}orkshop on {M}ethods for {M}odalities
           ({M4M}'03), Nancy, France}
}
@inproceedings{Demri::DeNivelle03b,
  address = {Nancy, France},
  month = sep,
  year = 2003,
  acronym = {{M4M-3}},
  booktitle = {{P}roceedings of the 3rd
               {W}orkshop on {M}ethods for {M}odalities
               ({M4M-3})},
  author = {Demri, St{\'e}phane and de Nivelle, Hans},
  title = {Relational Translations into {GF2}},
  pages = {93-108}
}
@techreport{JGL:dico:3.3,
  author = {Demri, St{\'e}phane and Ducass{\'e}, Mireille and 
                 Goubault{-}Larrecq, Jean
                 and M{\'e}, Ludovic and Olivain, Julien and 
                 Picaronny, Claudine and 
                 Pouzol, Jean-{\relax Ph}ilippe and 
                 Totel, {\'E}ric and Vivinis, Bernard},
  title = {Algorithmes de d{\'e}tection et langages de
                 signatures},
  year = {2003},
  month = oct,
  type = {Contract Report},
  number = {(Sous-projet~3, livrable~3)},
  institution = {projet RNTL DICO},
  oldhowpublished = {Sous-projet 3, livrable 3 du projet RNTL DICO. 
                 Version~1},
  note = {72~pages}
}
@inproceedings{Dem-fossacs2004,
  address = {Barcelona, Spain},
  month = mar,
  year = 2004,
  volume = 2987,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Walukiewicz, Igor},
  acronym = {{FoSSaCS}'04},
  booktitle = {{P}roceedings of the 7th {I}nternational 
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'04)},
  author = {Demri, St{\'e}phane},
  title = {{LTL} over Integer Periodicity Constraints},
  pages = {121-135},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri-fossacs04.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Demri-fossacs04.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri-fossacs04.pdf}
}
@misc{demri-RSFDGrC05,
  author = {Demri, St{\'e}phane},
  title = {On the complexity of information logics},
  year = 2005,
  month = aug,
  howpublished = {Invited talk, Workshop on Logical and Algebraic 
		Foundations of Rough Sets, Regina, Canada}
}
@article{demri-JLC05,
  publisher = {Oxford University Press},
  journal = {Journal of Logic and Computation},
  author = {Demri, St{\'e}phane},
  title = {A reduction from {DLP} to~{PDL}},
  year = 2005,
  month = oct,
  volume = 15,
  number = 5,
  pages = {767-785},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-jlc05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-jlc05.pdf},
  doi = {10.1093/logcom/exi043},
  abstract = {We present a reduction from a new logic extending van der Meyden's
dynamic logic of permission~(DLP) into propositional dynamic logic (PDL),
providing a 2EXPTIME decision procedure and showing that all the machinery 
for~PDL can be reused for reasoning about dynamic policies. As a 
side-effect, we establish that DLP is EXPTIME-complete. The logic we introduce
extends the logic~DLP so that the policy set can be updated depending on its
current value and such an update corresponds to add\slash delete transitions 
in the model, showing similarities with van Benthem's sabotage modal logic.}
}
@article{ddn-jlli05,
  publisher = {Kluwer Academic Publishers},
  journal = {Journal of Logic, Language and Information},
  author = {Demri, St{\'e}phane and de Nivelle, Hans},
  title = {Deciding Regular Grammar Logics with Converse through 
		  First-Order Logic},
  volume = 14,
  number = 3,
  pages = {289-319},
  year = {2005},
  month = jun,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ddn-gf-issue.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ddn-gf-issue.pdf},
  oldnote = {special issue dedicated to guarded logics.},
  doi = {10.1007/s10849-005-5788-9},
  abstract = {We provide a simple translation of the satisfiability problem for regular
grammar logics with converse into GF2 , which is the intersection of the guarded
fragment and the 2-variable fragment of first-order logic. The translation is theoretically 
interesting because it translates modal logics with certain frame conditions into
first-order logic, without explicitly expressing the frame conditions. It is practically
relevant because it makes it possible to use a decision procedure for the guarded
fragment in order to decide regular grammar logics with converse. The class of
regular grammar logics includes numerous logics from various application domains.\par
A consequence of the translation is that the general satisfiability problem for
every regular grammar logics with converse is in~EXPTIME. This extends a previous
result of the first author for grammar logics without converse. Other logics that
can be translated into GF2 include nominal tense logics and intuitionistic logic.
In our view, the results in this paper show that the natural first-order fragment
corresponding to regular grammar logics is simply GF2 without extra machinery
such as fixed point-operators.}
}
@inproceedings{DG-concur2005,
  address = {San Francisco, California, USA},
  month = aug,
  year = 2005,
  volume = 3653,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Abadi, Mart{\'\i}n and de Alfaro, Luca},
  acronym = {{CONCUR}'05},
  booktitle = {{P}roceedings of the 16th 
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'05)},
  author = {Demri, St{\'e}phane and Gascon, R{\'e}gis},
  title = {Verification of Qualitative 
		 {\(\mathbb{\MakeUppercase{Z}}\)}-Constraints},
  pages = {518-532},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-Concur05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-Concur05.pdf},
  doi = {10.1007/11539452_39},
  abstract = {We introduce an LTL-like logic with atomic formulae built
over a constraint language interpreting variables in~\(\mathbb{Z}\). The constraint
language includes periodicity constraints, comparison constraints of the
form \(x = y\) and \(x < y\), it is closed under Boolean operations and it
admits a restricted form of existential quantification. This is the largest
set of qualitative constraints over~\(\mathbb{Z}\) known so far, shown to admit a
decidable LTL extension. Such constraints are those used for instance
in calendar formalisms or in abstractions of counter automata by using
congruences modulo some power of two. Indeed, various programming
languages perform arithmetic operators modulo some integer. We show
that the satisfiability and model-checking problems (with respect to an
appropriate class of constraint automata) for this logic are decidable in
polynomial space improving significantly known results about its strict
fragments. As a by-product, LTL model-checking over integral relational
automata is proved complete for polynomial space which contrasts with
the known undecidability of its CTL counterpart.}
}
@inproceedings{DLN-time05,
  address = {Burlington, Vermont, USA},
  month = jun,
  year = 2005,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{TIME}'05},
  booktitle = {{P}roceedings of the 12th {I}nternational {S}ymposium on 
	       {T}emporal {R}epresentation and {R}easoning
	       ({TIME}'05)},
  author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko and  
		 Nowak, David},
  title = {On the Freeze Quantifier in Constraint {LTL}: 
		Decidability and Complexity},
  pages = {113-121},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-03.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
		  rr-lsv-2005-03.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-03.pdf},
  doi = {10.1109/TIME.2005.28},
  abstract = {Constraint LTL, a generalization of LTL over Presburger
constraints, is often used as a formal language to specify the
behavior of operational models with constraints. The freeze
quantifier can be part of the language, as in some real-time
logics, but this variable-binding mechanism is quite general
and ubiquitous in many logical languages (first-order temporal 
logics, hybrid logics, logics for sequence diagrams,
navigation logics, etc.). We show that Constraint LTL over
the simple domain \(\langle \mathbb{N}, = \rangle\) augmented 
with the freeze operator is undecidable which is a 
surprising result regarding the
poor language for constraints (only equality tests). Many
versions of freeze-free Constraint LTL are decidable over
domains with qualitative predicates and our undecidability
result actually establishes \(\Sigma_{1}^{1}\)-completeness. 
On the positive side, we provide complexity results when the domain is
finite (EXPSPACE-completeness) or when the formulae are
flat in a sense introduced in the paper. Our undecidability
results are quite sharp (\emph{i.e.}~with restrictions on the 
number of variables) and all our complexity characterizations
insure completeness with respect to some complexity class
(mainly PSPACE and~EXPSPACE).}
}
@inproceedings{DN-atva05,
  address = {Taipei, Taiwan},
  month = oct,
  year = {2005},
  volume = 3707,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Peled, Doron A. and Tsay, Yih-Kuen},
  acronym = {{ATVA}'05},
  booktitle = {{P}roceedings of the 3rd {I}nternational
               {S}ymposium on {A}utomated {T}echnology
               for {V}erification and {A}nalysis
               ({ATVA}'05)},
  author = {Demri, St{\'e}phane and Nowak, David},
  title = {Reasoning about transfinite sequences (extended abstract)},
  pages = {248-262},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DN-atva2005.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DN-atva2005.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DN-atva2005.ps},
  doi = {10.1007/11562948_20},
  abstract = {We introduce a family of temporal logics to specify the 
behavior of systems with Zeno behaviors. We extend linear-time temporal
logic LTL to authorize models admitting Zeno sequences of actions and
quantitative temporal operators indexed by ordinals replace the standard 
next-time and until future-time operators. Our aim is to control
such systems by designing controllers that safely work on \(\omega\)-sequences
but interact synchronously with the system in order to restrict their behaviors. 
We show that the satisfiability problem for the logics working
on \(\omega^{k}\)-sequences is EXPSPACE-complete when the integers are represented
in binary, and PSPACE-complete with a unary representation. To do so,
we substantially extend standard results about LTL by introducing a
new class of succinct ordinal automata that can encode the interaction
between the different quantitative temporal operators.}
}
@inproceedings{DDFG-atva06,
  address = {Beijing, China},
  month = oct,
  year = {2006},
  volume = 4218,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Graf, Susanne and Zhang, Wenhui},
  acronym = {{ATVA}'06},
  booktitle = {{P}roceedings of the 4th {I}nternational
               {S}ymposium on {A}utomated {T}echnology
               for {V}erification and {A}nalysis
               ({ATVA}'06)},
  author = {Demri, St{\'e}phane and Finkel, Alain
		and Goranko, Valentin and van Drimmelen, Govert},
  title = {Towards a model-checker for counter systems},
  pages = {493-507},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDFG-atva06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDFG-atva06.pdf},
  doi = {10.1007/11901914_36},
  abstract = {This paper deals with model-checking of fragments and extensions
of~\(\mathrm{CTL}^{*}\) on infinite-state Presburger counter systems, where
the states are vectors of integers and the transitions are determined by means
of relations definable within Presburger arithmetic. We have identified a
natural class of admissible counter systems~(ACS) for which we show that the
quantification over paths in~\(\mathrm{CTL}^{*}\) can be simulated by
quantification over tuples of natural numbers, eventually allowing translation
of the whole Presburger-\(\mathrm{CTL}^{*}\) into Presburger arithmetic,
thereby enabling effective model checking. We have provided evidence that our
results are close to optimal with respect to the class of counter systems
described above. Finally, we design a complete semi-algorithm to verify
first-order~\(\mathrm{LTL}\) properties over trace-flattable counter systems,
extending the previous underlying FAST semi-algorithm to verify reachability
questions over flattable counter systems. }
}
@inproceedings{DL-lics2006,
  address = {Seattle, Washington, USA},
  month = aug,
  year = 2006,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{LICS}'06},
  booktitle = {{P}roceedings of the 21st
               {A}nnual {IEEE} {S}ymposium on
               {L}ogic in {C}omputer {S}cience
               ({LICS}'06)},
  author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko},
  title = {{LTL} with the freeze quantifier and register automata},
  pages = {17-26},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DL-lics2006.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DL-lics2006.pdf},
  doi = {10.1109/LICS.2006.31},
  abstract = {Temporal logics, first-order logics, and automata over data
words have recently attracted considerable attention. A~data word is a word
over a finite alphabet, together with a datum (an element of an infinite
domain) at each position. Examples include timed words and XML documents. To
refer to the data, temporal logics are extended with the freeze quantifier,
first-order logics with predicates over the data domain, and automata with
registers or pebbles.\par
    We investigate relative expressiveness and complexity of standard decision
problems for~\(\mathrm{LTL}\) with the freeze
quantifier~(\(\mathrm{LTL}^{\downarrow}\)), 2-variable first-order logic
(\(\mathrm{FO}^{2}\)) over data words, and register automata. The only
predicate available on data is equality. Previously undiscovered connections
among those formalisms, and to counter automata with in- crementing errors,
enable us to answer several questions left open in recent literature.\par
    We show that the future-time fragment of~\(\mathrm{LTL}^{\downarrow}\)
which corresponds to \(\mathrm{FO}^{2}\) over finite data words can be
extended considerably while preserving decidability, but at the expense of
non-primitive recursive complexity, and that most of further extensions are
undecidable. We also prove that surprisingly, over infinite data words,
\(\mathrm{LTL}^{\downarrow}\) without the `until' operator, as well as
nonemptiness of one-way universal register automata, are undecidable even when
there is only one register.}
}
@inproceedings{DL-ijcar06,
  address = {Seattle, Washington, USA},
  month = aug,
  year = 2006,
  volume = 4130,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer-Verlag},
  editor = {Furbach, Ulrich and Shankar, Natarajan},
  acronym = {{IJCAR}'06},
  booktitle = {{P}roceedings of the 3rd {I}nternational {J}oint
           {C}onference on {A}utomated {R}easoning
           ({IJCAR}'06)},
  author = {Demri, St{\'e}phane and Lugiez, Denis},
  title = {{P}resburger Modal Logic is Only {PSPACE}-complete},
  pages = {541-556},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-25.pdf},
  doi = {10.1007/11814771_44},
  abstract = {We introduce a Presburger modal logic PML with regularity
constraints and full Presburger constraints on the number of children that
generalize graded modalities, also known as number restrictions in description
logics. We~show that PML satisfiability is only PSPACE-complete by designing a
Ladner-like algorithm that can be turned into an analytic proof system 
algorithm. This extends a well-known and non-trivial PSPACE upper bound for
graded modal logic. Furthermore, we provide a detailed comparison with logics
that contain Presburger constraints and that are dedicated to query XML
documents. As~an application, we show that satisfiability for Sheaves Logic SL
is PSPACE-complete, improving significantly its best known upper bound.}
}
@article{Demri06,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Demri, St{\'e}phane},
  title = {{LTL} over integer periodicity constraints},
  year = {2006},
  volume = 360,
  number = {1-3},
  pages = {96-123},
  month = aug,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-tcs06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-tcs06.pdf},
  doi = {10.1016/j.tcs.2006.02.019},
  abstract = {Periodicity constraints are used 
	in many logical formalisms, in fragments of Presburger~LTL, 
	in calendar logics, and in  logics for access 
	control, to quote a few examples. In the paper, we 
	introduce the logic PLTL\(^{\mathrm{mod}}\), an 
	extension of Linear-Time Temporal Logic LTL with 
	past-time operators whose atomic formulae are defined 
	from a first-order constraint language dealing with 
	periodicity. Although the underlying constraint language 
	is a fragment of Presburger arithmetic shown to admit a 
	{\scshape pspace}-complete satisfiability problem, we establish 
	that PLTL\(^{\mathrm{mod}}\) model-checking and 
	satisfiability problems remain in {\scshape pspace} as plain~LTL 
	(full Presburger LTL is known to be highly undecidable). 
	This is particularly interesting for dealing with 
	periodicity constraints since the language of 
	PLTL\(^{\mathrm{mod}}\) has a language more concise than 
	existing languages and the temporalization of our 
	first-order language of periodicity constraints has the 
	same worst case complexity as the underlying constraint 
	language. Finally, we show examples of introduction the 
	quantification in the logical language that provide to 
	PLTL\(^{\mathrm{mod}}\), {\scshape expspace}-complete 
	problems. As another application, we establish that the 
	equivalence problem for extended single-string automata, 
	known to express the equality of time granularities, is 
	{\scshape pspace}-complete by designing a reduction from~QBF and by 
	using our results for PLTL\(^{\mathrm{mod}}\). }
}
@article{DLS-jcss-param,
  publisher = {Elsevier Science Publishers},
  journal = {Journal of Computer and System Sciences},
  author = {Demri, St{\'e}phane and Laroussinie, Fran{\c{c}}ois
        and Schnoebelen, {\relax Ph}ilippe},
  title = {A Parametric Analysis of the State Explosion Problem in
		Model Checking},
  year = 2006,
  month = jun,
  volume = 72,
  number = 4,
  pages = {547-575},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLS-jcss-param.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLS-jcss-param.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DLS-jcss-param.ps},
  doi = {10.1016/j.jcss.2005.11.003},
  abstract = {In model checking, the 
	state-explosion problem occurs when one checks a 
	non-flat system, \emph{i.e.}, a system implicitly 
	described as a synchronized product of elementary 
	subsystems. In this paper, we investigate the 
	complexity of a wide variety of model checking 
	problems for non-flat systems under the light of 
	parameterized complexity, taking the number of 
	synchronized components as a parameter.  We provide 
	precise complexity measures (in the parameterized 
	sense) for most of the problems we investigate, and 
	evidence that the results are robust.}
}
@inproceedings{DLS-fossacs08,
  address = {Budapest, Hungary},
  month = mar # {-} # apr,
  year = 2008,
  volume = 4962,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Amadio, Roberto},
  acronym = {{FoSSaCS}'08},
  booktitle = {{P}roceedings of the 11th {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'08)},
  author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko and Sangnier, Arnaud},
  title = {Model checking  freeze {LTL} over one-counter automata},
  pages = {490-504},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLS-fossacs08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLS-fossacs08.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DLS-fossacs08.ps},
  doi = {10.1007/978-3-540-78499-9_34},
  abstract = {We study complexity issues related to the model-checking
    problem for LTL with registers (a.k.a. freeze LTL) over
    one-counter automata. We~consider several classes of one-counter
    automata (mainly deterministic vs.~nondeterministic) and several
    syntactic fragments (restriction on the number of registers and on
    the use of propositional variables for control
    locations). The~logic has the ability to store a counter value and
    to test it later against the current counter value. By~introducing
    a non-trivial abstraction on counter values, we~show that model
    checking LTL with registers over deterministic one-counter
    automata is PSPACE-complete with infinite accepting
    runs. By~constrast, we prove that model checking LTL with
    registers over nondeterministic one-counter automata is
    \(\Sigma_{1}^{1}\)-complete [resp. \(\Sigma_{1}^{0}\)-complete] in
    the infinitary [resp. finitary] case even if only one register is
    used and with no propositional variable. This makes a difference
    with the facts that several verification problems for one-counter
    automata are known to be decidable with relatively low complexity,
    and that finitary satisfiability for LTL with a unique register is
    decidable. Our~results pave the way for model-checking LTL with
    registers over other classes of operational models, such as
    reversal-bounded counter machines and deterministic pushdown
    systems.}
}
@inproceedings{DR-lpar07,
  address = {Yerevan, Armenia},
  month = oct,
  year = 2007,
  volume = 4790,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Dershowitz, Nachum and Voronkov, Andrei},
  acronym = {{LPAR}'07},
  booktitle = {{P}roceedings of the 14th {I}nternational
               {C}onference on {L}ogic for {P}rogramming,
               {A}rtificial {I}ntelligence, and {R}easoning
               ({LPAR}'07)},
  author = {Demri, St{\'e}phane and Rabinovich, Alexander},
  title = {The complexity of temporal logic with until and since over ordinals},
  pages = {531-545},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DR-lpar07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DR-lpar07.pdf},
  doi = {10.1007/978-3-540-75560-9_38},
  abstract = {We consider the temporal logic with since and until 
    modalities. This temporal logic is expressively equivalent over the 
    class of ordinals to first-order logic thanks to Kamp's theorem. 
    We~show that it has a PSPACE-complete satisfiability problem over the 
    class of ordinals. Among the consequences of our proof, we show that 
    given the code of some countable ordinal~\(\alpha\) and a formula, we 
    can decide in PSPACE whether the formula has a model over~\(\alpha\). 
    In~order to show these results, we~introduce a class of simple ordinal 
    automata, as expressive as B{\"u}chi ordinal automata. The PSPACE 
    upper bound for the satisfiability problem of the temporal logic is 
    obtained through a reduction to the nonemptiness problem for the 
    simple ordinal automata.}
}
@phdthesis{demri-hab2007,
  author = {Demri, St{\'e}phane},
  title = {Logiques pour la sp{\'e}cification et v{\'e}rification},
  year = 2007,
  month = jun,
  type = {M{\'e}moire d'habilitation},
  school = {Universit{\'e} Paris~7, Paris, France},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SD-habil07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SD-habil07.pdf},
  futureslides = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/
                SD-habil-slides.ps.gz}
}
@inproceedings{DG-time07,
  address = {Alicante, Spain},
  month = jun,
  year = 2007,
  publisher = {{IEEE} Computer Society Press},
  editor = {Goranko, Valentin and Wang, X. Sean},
  acronym = {{TIME}'07},
  booktitle = {{P}roceedings of the 14th {I}nternational {S}ymposium on 
	       {T}emporal {R}epresentation and {R}easoning
	       ({TIME}'07)},
  author = {Demri, St{\'e}phane and Gascon, R{\'e}gis},
  title = {The Effects of Bounding Syntactic Resources on {P}resburger
		  {LTL} (Extended Abstract)},
  pages = {94-104},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-time07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-time07.pdf},
  doi = {10.1109/TIME.2007.63},
  abstract = {We study decidability and complexity issues for fragments of LTL
    with Presburger constraints by restricting the syntactic resources of the
    formulae (the~class of constraints, the number of variables and the
    distance between two states for which counters can be compared) while
    preserving the strength of the logical operators. We provide a complete
    picture refining known results from the literature, in some cases pushing
    forward the known decidability limits. By~way of example, we show that
    model-checking formulae from LTL with quantifier-free Presburger
    arithmetic over one-counter automata is only PSPACE-complete. In~order to
    establish the PSPACE upper bound, we show that the nonemptiness problem
    for Buchi one-counter automata taking values in~\(\mathbb{Z}\) and
    allowing zero tests and sign tests, is only NLOGSPACE-complete.}
}
@inproceedings{BDL-hav07,
  address = {Braga, Portugal},
  month = mar,
  year = 2007,
  editor = {Berdine, Josh and Sagiv, Mooly},
  acronym = {{HAV}'07},
  booktitle = {{P}roceedings of the 1st {W}orkshop on {H}eap {A}nalysis and 
		{V}erification ({HAV}'07)},
  author = {Brochenin, R{\'e}mi and Demri, St{\'e}phane and Lozes, {\'E}tienne},
  title = {Reasoning about Sequences of Memory States},
  preliminary-version-of = {BDL-lfcs2007},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-hav07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-hav07.pdf},
  abstract = {In order to verify programs with pointer variables, 
    we introduce a temporal logic LTL\textsuperscript{mem} whose 
    underlying 
    assertion language is the 
    quantifier-free fragment of separation logic and the temporal logic on 
    the 
    top of it is  the standard linear-time temporal logic~LTL. We~state 
    the 
    complexity of various model-checking and satisfiability problems for 
    LTL\textsuperscript{mem} , considering various  
    fragments of separation logic (including pointer arithmetic), various 
    classes of models (with or without constant heap), and the influence  
    of fixing the initial memory state.
    Our main decidability result is PSPACE-completeness of the 
    satisfiability problems on the record fragment and on a classical 
    fragment allowing pointer arithmetic. 
    \(\Sigma^{0}_{1}\)-completeness or \(\Sigma^{1}_{1}\)-completeness 
    results 
    are established for various problems, and underline the tightness of 
    our decidability results.}
}
@inproceedings{BDL-lfcs2007,
  address = {New~York, New~York, USA},
  month = jun,
  year = 2007,
  volume = 4514,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Artemov, Sergei N. and Nerode, Anil},
  acronym = {{LFCS}'07},
  booktitle = {{P}roceedings of the {S}ymposium on {L}ogical {F}oundations of
	{C}omputer {S}cience ({LFCS}'07)},
  author = {Brochenin, R{\'e}mi and Demri, St{\'e}phane and Lozes, {\'E}tienne},
  title = {Reasoning about sequences of memory states},
  pages = {100-114},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-lfcs07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-lfcs07.pdf},
  doi = {	10.1007/978-3-540-72734-7_8},
  abstract = {Motivated by the verification of programs with pointer
    variables, we introduce a temporal logic LTL\textsuperscript{mem} whose
    underlying assertion language is the quantifier-free fragment of
    separation logic and the temporal logic on the top of it is the standard
    linear-time temporal logic~LTL. We analyze the complexity of various
    model-checking and satisfiability problems for LTL\textsuperscript{mem},
    considering various fragments of separation logic (including pointer
    arithmetic), various classes of models (with or without constant heap),
    and the influence of fixing the initial memory state. We~provide a
    complete picture based on these criteria. Our main decidability result is
    PSPACE-completeness of the satisfiability problems on the record fragment
    and on a classical fragment allowing pointer arithmetic. 
    \(\Sigma^{0}_{1}\)-completeness or \(\Sigma^{1}_{1}\)-completeness
    results are established for various problems by reducing standard problems
    for Minsky machines, and underline the tightness of our decidability
    results.}
}
@article{DO-fi2007,
  publisher = {{IOS} Press},
  journal = {Fundamenta Informaticae},
  author = {Demri, St{\'e}phane and Or{\l}owska, Ewa},
  title = {Relative Nondeterministic Information Logic is 
		  {EXPTIME}-complete},
  year = {2007},
  volume = {75},
  number = {1-4},
  pages = {163-178},
  nmnote = {Special issue in memory of Z.~Paw{\l}ak},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DO-fi07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DO-fi07.pdf},
  abstract = {We define a relative version of the logic NIL introduced by
                  Or{\l}owska, Paw{\l}ak and Vakarelov and we show that its
                  satisfiability is not only decidable but also
                  EXPTIME-complete. Such a logic combines two ingredients that
                  are seldom present simultaneously in information logics:
                  frame conditions involving more than one information
                  relation and relative frames. The~EXPTIME upper bound is
                  obtained by designing a well-suited decision procedure based
                  on the nonemptiness problem of B{\"u}chi automata on
                  infinite trees. The paper provides evidence that B{\"u}chi
                  automata on infinite trees are crucial language acceptors
                  even for relative information logics with multiple types of
                  relations.}
}
@inproceedings{DDG-lfcs2007,
  address = {New~York, New~York, USA},
  month = jun,
  year = 2007,
  volume = 4514,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Artemov, Sergei N. and Nerode, Anil},
  acronym = {{LFCS}'07},
  booktitle = {{P}roceedings of the {S}ymposium on {L}ogical {F}oundations of
	{C}omputer {S}cience ({LFCS}'07)},
  author = {Demri, St{\'e}phane and D'Souza, Deepak and Gascon, R{\'e}gis},
  title = {Decidable Temporal Logic with Repeating Values},
  pages = {180-194},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDG-lfcs07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDG-lfcs07.pdf},
  doi = {10.1007/978-3-540-72734-7_13},
  abstract = {Various logical formalisms with the freeze quantifier have been
    recently considered to model computer systems even though this is a
    powerful mechanism that often leads to undecidability. In~this paper, we
    study a linear-time temporal logic with past-time operators such that the
    freeze operator is only used to express that some value from an infinite
    set is repeated in the future or in the past. Such a restriction has been
    inspired by a recent work on spatio-temporal logics. We~show decidability
    of finitary and infinitary satisfiability by reduction into the
    verification of temporal properties in Petri nets. This is a surprising
    result since the logic is closed under negation, contains future-time and
    past-time temporal operators and can express the nonce property and its
    negation. These ingredients are known to lead to undecidability with a
    more liberal use of the freeze quantifier. The~paper contains also
    insights about the relationships between temporal logics with the freeze
    operator and counter automata.}
}
@article{DLN-icomp2006,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko and Nowak, David},
  title = {On the freeze quantifier in constraint~{LTL}: Decidability
		   and complexity},
  pages = {2-24},
  year = {2007},
  month = jan,
  volume = 205,
  number = 1,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLN-icomp06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLN-icomp06.pdf},
  doi = {10.1016/j.ic.2006.08.003},
  abstract = {Constraint LTL, a generalisation of LTL over Presburger
constraints, is often used as a formal language to specify the behavior of
operational models with constraints. The freeze quantifier can be part of the
language, as in some real-time logics, but this variable-binding mechanism is
quite general and ubiquitous in many logical languages (first-order temporal
logics, hybrid logics, logics for sequence diagrams, navigation logics, logics
with \(\lambda\)-abstraction,~etc.). We show that Constraint~LTL over the
simple domain~\(\langle\mathbb{N}, =\rangle\) augmented with the freeze
quantifier is undecidable which is a surprising result in view of the poor
language for constraints (only equality tests). Many versions of freeze-free
Constraint LTL are decidable over domains with qualitative predicates and our
undecidability result actually establishes \(\Sigma_{1}^{1}\)-completeness. On
the positive side, we provide complexity results when the domain is finite
({\scshape ExpSpace}-completeness) or when the formulae are flat in a sense
introduced in the paper. Our undecidability results are sharp
(\emph{i.e.}~with restrictions on the number of variables) and all our
complexity characterisations ensure completeness with respect to some
complexity class (mainly {\scshape PSpace} and {\scshape ExpSpace}).}
}
@article{DN-ijfcs07,
  publisher = {World Scientific},
  journal = {International Journal of Foundations of Computer Science},
  author = {Demri, St{\'e}phane and Nowak, David},
  title = {Reasoning about transfinite sequences},
  year = 2007,
  volume = {18},
  number = {1},
  pages = {87-112},
  month = feb,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DN-ijfcs07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DN-ijfcs07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DN-ijfcs07.ps},
  doi = {10.1142/S0129054107004589},
  abstract = {We introduce a family of temporal logics to specify the behavior
of systems with Zeno behaviors. We~extend linear-time temporal logic LTL to
authorize models admitting Zeno sequences of actions and quantitative temporal
operators indexed by ordinals replace the standard next-time and until
future-time operators. Our aim is to control such systems by designing
controllers that safely work on \(\omega\)-sequences but interact
synchronously with the system in order to restrict their behaviors. We show
that the satisfiability and model-checking for the logics working on
\(\omega^{k}\)-sequences is \textsc{expspace}-complete when the integers are
represented in binary, and pspace-complete with a unary representation. To do
so, we substantially extend standard results about LTL by introducing a new
class of succinct ordinal automata that can encode the interaction between the
different quantitative temporal operators. }
}
@article{DD-icomp06,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Demri, St{\'e}phane and D'Souza, Deepak},
  title = {An automata-theoretic approach to constraint~{LTL}},
  year = 2007,
  pages = {380-415},
  volume = 205,
  number = 3,
  month = mar,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DD-icomp06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DD-icomp06.pdf},
  doi = {10.1016/j.ic.2006.09.006},
  abstract = {We consider an extension of linear-time temporal logic~(LTL)
with constraints interpreted over a concrete domain. We~use a new
automata-theoretic technique to show pspace decidability of the logic for the
constraint systems \((\mathbb{Z}, <, =)\) and \((\mathbb{N}, <, =)\). Along
the way, we give an automata-theoretic proof of a result of [Ph.~Balbiani,
J.~Condotta, \textit{Computational complexity of propositional linear temporal logics
based on qualitative spatial or temporal reasoning}, 2002] when the constraint system
satisfies the completion property. Our decision procedures extend easily to
handle extensions of the logic with past-time operators and constants, as well
as an extension of the temporal language itself to monadic second order logic.
Finally we show that the logic becomes undecidable when one considers
constraint systems that allow a counting mechanism.}
}
@article{Demri-jancl06,
  publisher = {Taylor \& Francis},
  journal = {Journal of Applied Non-Classical Logics},
  author = {Demri, St{\'e}phane},
  title = {Linear-Time Temporal Logics with {P}resburger Constraints: An~Overview},
  year = 2006,
  volume = 16,
  number = {3-4},
  pages = {311-347},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-jancl06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-jancl06.pdf},
  abstract = {We present an overview of linear-time temporal logics with
Presburger constraints whose models are sequences of tuples of integers. Such
formal specification languages are well-designed to specify and verify systems
that can be modelled with counter systems. The paper recalls the general
framework of LTL over concrete domains and presents the main decidability and
complexity results related to fragments of Presburger~LTL. Related formalisms
are also briefly presented.}
}
@article{DG-tcs08,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Demri, St{\'e}phane and Gascon, R{\'e}gis},
  title = {Verification of Qualitative {\(\mathbb{\MakeUppercase{Z}}\)}~constraints},
  volume = 409,
  number = 1,
  month = dec,
  year = 2008,
  pages = {24-40},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-tcs08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-tcs08.pdf},
  doi = {10.1016/j.tcs.2008.07.023},
  abstract = {We introduce an LTL-like logic with atomic formulae built over a
    constraint language interpreting variables in~\(\mathbb{Z}\).
    The~constraint language includes periodicity constraints, comparison
    constraints of the form \({x = y}\) and \({x < y}\), is~closed under Boolean
    operations and admits a restricted form of existential quantification.
    Such constraints are used for instance in calendar formalisms or
    abstractions of counter automata by using congruences modulo some power of
    two. Indeed, various programming languages perform arithmetic operators
    modulo some integer. We~show that the satisfiability and model-checking
    problems (with respect to an appropriate class of constraint automata) for
    this logic are decidable in polynomial space improving significantly known
    results about its strict fragments. This is the largest set of qualitative
    constraints over~\(\mathbb{Z}\) known so~far, shown to admit a decidable
    LTL extension.}
}
@article{DL-tocl08,
  publisher = {ACM Press},
  journal = {ACM Transactions on Computational Logic},
  author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko},
  title = {{LTL} with the freeze quantifier and register automata},
  volume = 10,
  number = 3,
  nopages = {},
  month = apr,
  year = 2009,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DL-tocl08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DL-tocl08.pdf},
  doi = {10.1145/1507244.1507246},
  abstract = {A data word is a sequence of pairs of a letter from a finite
    alphabet and an element from an infinite set, where the latter can only be
    compared for equality. To reason about data words, linear temporal logic
    is extended by the freeze quantifier, which stores the element at the
    current word position into a register, for equality comparisons deeper in
    the formula. By translations from the logic to alternating automata with
    registers and then to faulty counter automata whose counters may
    erroneously increase at any time, and from faulty and error-free counter
    automata to the logic, we obtain a complete complexity table for logical
    fragments defined by varying the set of temporal operators and the number
    of registers. In~particular, the~logic with future-time operators and
    \(1\)~register is decidable but not primitive recursive over finite data
    words. Adding past-time operators or \(1\)~more register, or switching to
    infinite data words, cause undecidability.}
}
@inproceedings{BDL-csl08,
  address = {Bertinoro, Italy},
  month = sep,
  year = 2008,
  volume = 5213,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Kaminski, Michael and Martini, Simone},
  acronym = {{CSL}'08},
  booktitle = {{P}roceedings of the 17th {A}nnual {EACSL} {C}onference on
                  {C}omputer {S}cience {L}ogic ({CSL}'08)},
  author = {Brochenin, R{\'e}mi and Demri, St{\'e}phane and
		 Lozes, {\'E}tienne},
  title = {On~the Almighty Wand},
  pages = {323-338},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-csl08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-csl08.pdf},
  doi = {10.1007/978-3-540-87531-4_24},
  abstract = {We investigate decidability, complexity and expressive power
    issues for (first-order) separation logic with one record field (herein
    called~SL) and its fragments. SL~can specify properties about the memory
    heap of programs with singly-linked lists. Separation logic with two
    record fields is known to be undecidable by reduction of finite
    satisfiability for classical predicate logic with one binary relation.
    Surprisingly, we~show that second-order logic is as expressive as SL and
    as a by-product we get undecidability of~SL. This is refined by showing
    that SL without the separating conjunction is as expressive as~SL, whence
    undecidable too. As~a consequence of this deep result, in~SL the magic
    wand can simulate the separating conjunction. By~contrast, we~establish
    that SL without the magic wand is decidable with non-elementary complexity
    by reduction from satisfiability for the first-order theory over finite
    words. Equivalence between second-order logic and separation logic extends
    to the case with more than one selector.}
}
@misc{Demri0506,
  author = {Demri, St{\'e}phane},
  title = {Temporal logics},
  year = {2005},
  note = {Course notes, {M}aster {P}arisien de {R}echerche en 
	{I}nformatique, Paris, France},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri-2.8-TL.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri-2.8-TL.pdf}
}
@misc{Demri0304,
  author = {Demri, St{\'e}phane},
  title = {Complexit{\'e} algorithmique de variantes de {LTL} pour la v{\'e}rification},
  year = {2004},
  note = {Course notes, {DEA} Algorithmique, Paris, France},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri-coursLTL.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri-coursLTL.pdf}
}
@inproceedings{DS-fossacs10,
  address = {Paphos, Cyprus},
  month = mar,
  year = 2010,
  volume = {6014},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Ong, C.-H. Luke},
  acronym = {{FoSSaCS}'10},
  booktitle = {{P}roceedings of the 13th {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'10)},
  author = {Demri, St{\'e}phane and Sangnier, Arnaud},
  title = {When Model-Checking
                  Freeze {LTL} over Counter Machines Becomes Decidable},
  pages = {176-190},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DS-fossacs10.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DS-fossacs10.pdf},
  doi = {10.1007/978-3-642-12032-9_13},
  abstract = {We study the decidability status of model-checking freeze LTL
    over various subclasses of counter machines for which the reachability
    problem is known to be decidable (reversal-bounded counter machines,
    vector additions systems with states, flat counter machines, one-counter
    machines). In freeze LTL, a register can store a counter value and at some
    future position an equality test can be done between a register and a
    counter value. Herein, we complete an earlier work started on one-counter
    machines by considering other subclasses of counter machines, and
    especially the class of reversal-bounded counter machines. This gives us
    the opportuniy to provide a systematic classification that distinguishes
    determinism vs. nondeterminism and we consider subclasses of formulae by
    restricting the set of atomic formulae or\slash and the polarity of the
    occurrences of the freeze operators, leading to the flat fragment.}
}
@inproceedings{DJLL-fsttcs09,
  address = {Kanpur, India},
  month = dec,
  year = 2009,
  volume = 4,
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Kannan, Ravi and Narayan Kumar, K.},
  acronym = {{FSTTCS}'09},
  booktitle = {{P}roceedings of the 29th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'09)},
  author = {Demri, St{\'e}phane and Jurdzi{\'n}ski, Marcin and Lachish,
                  Oded and Lazi{\'c}, Ranko},
  title = {The covering and boundedness problems for branching vector addition systems},
  pages = {181-192},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/djll-fsttcs09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/djll-fsttcs09.pdf},
  doi = {10.4230/LIPIcs.FSTTCS.2009.2317},
  abstract = {The covering and boundedness problems for branching vector
    addition systems are shown complete for doubly-exponential time.}
}
@article{BDL-apal09,
  publisher = {Elsevier Science Publishers},
  journal = {Annals of Pure and Applied Logics},
  author = {Brochenin, R{\'e}mi and Demri, St{\'e}phane and Lozes,
                  {\'E}tienne},
  title = {Reasoning about sequences of memory states},
  volume = {161},
  number = {3},
  pages = {305-323},
  year = 2009,
  month = dec,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-apal09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-apal09.pdf},
  doi = {10.1016/j.apal.2009.07.004},
  abstract = {Motivated by the verification of programs with pointer
    variables, we introduce a temporal logic LTL\textsuperscript{mem} whose
    underlying assertion language is the quantifier-free fragment of
    separation logic and the temporal logic on the top of it is the standard
    linear-time temporal logic LTL. We analyze the complexity of various
    model-checking and satisfiability problems for LTL\textsuperscript{mem},
    considering various fragments of separation logic (including pointer
    arithmetic), various classes of models (with or without constant heap),
    and the influence of fixing the initial memory state. We provide a
    complete picture based on these criteria. Our main decidability result is
    pspace-completeness of the satisfiability problems on the record fragment
    and on a classical fragment allowing pointer arithmetic.
    \(\Sigma_1^0\)-completeness or \(\Sigma_1^1\)-completeness results are
    established for various problems by reducing standard problems for Minsky
    machines, and underline the tightness of our decidability results.}
}
@article{DG-jlc09,
  publisher = {Oxford University Press},
  journal = {Journal of Logic and Computation},
  author = {Demri, St{\'e}phane and Gascon, R{\'e}gis},
  title = {The Effects of Bounding Syntactic Resources on {P}resburger
                  {LTL}},
  pages = {1541-1575},
  volume = {19},
  number = {6},
  month = dec,
  year = 2009,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DG-jlc09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DG-jlc09.pdf},
  doi = {10.1093/logcom/exp037},
  abstract = {LTL over Presburger constraints is the extension of LTL where
    the atomic formulae are quantifier-free Presburger formulae having as free
    variables the counters at different states of the model. This logic is
    known to admit undecidable satisfiability and model-checking problems.
    We~study decidability and complexity issues for fragments of LTL with
    Presburger constraints obtained by restricting the syntactic resources of
    the formulae (the number of variables, the maximal distance between two
    states for which counters can be compared and, to a smaller extent, the
    set of Presburger constraints) while preserving the strength of the
    logical operators. We~provide a complete picture refining known results
    from the literature. We~show that model-checking and satisfiability
    problems for the fragments of LTL with difference constraints restricted
    to two variables and distance one and to one variable and distance two are
    highly undecidable, enlarging significantly the class of known undecidable
    fragments. On the positive side, we prove that the fragment restricted to
    one variable and to distance one augmented with propositional variables is
    \textsc{pspace}-complete. Since the atomic formulae can state quantitative
    properties on the counters, this extends some results about model-checking
    pushdown systems and one-counter automata. In~order to establish the
    pspace upper bound, we show that the nonemptiness problem for B{\"u}chi
    one-counter automata taking values in~\(\mathbb{Z}\) and allowing zero
    tests and sign tests, is~only \textsc{nlogspace}-complete. Finally,
    we~establish that model-checking one-counter automata with complete
    quantifier-free Presburger LTL restricted to one variable is also
    \textsc{pspace}-complete whereas the satisfiability problem is
    undecidable.}
}
@article{DR-lmcs10,
  journal = {Logical Methods in Computer Science},
  author = {Demri, St{\'e}phane and Rabinovich, Alexander},
  title = {The Complexity of Linear-time Temporal Logic over the Class
                  of Ordinals},
  volume = 6,
  number = 4,
  nopages = {},
  month = dec,
  year = 2010,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DR-lmcs10.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DR-lmcs10.pdf},
  doi = {10.2168/LMCS-6(4:9)2010},
  abstract = {We consider the temporal logic with since and until modalities.
    This temporal logic is expressively equivalent over the class of ordinals
    to first-order logic by Kamp's theorem. We show that it has a
    PSPACE-complete satisfiability problem over the class of ordinals. Among
    the consequences of our proof, we show that given the code of some
    countable ordinal~\(\alpha\) and a formula, we can decide in PSPACE
    whether the formula has a model over~\(\alpha\). In order to show these
    results, we introduce a class of simple ordinal automata, as expressive as
    B{\"u}chi ordinal automata. The PSPACE upper bound for the satisfiability
    problem of the temporal logic is obtained through a reduction to the
    nonemptiness problem for the simple ordinal automata.}
}
@inproceedings{SD-jelia10,
  address = {Helsinki, Finland},
  month = sep,
  year = 2010,
  volume = 6431,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Niemel{\"a}, Ilkka and Janhunen, Tomi},
  acronym = {{JELIA}'10},
  booktitle = {{P}roceedings of the 12th {E}uropean {C}onference on {L}ogics in
                  {A}rtificial {I}ntelligence ({JELIA}'10)},
  author = {Demri, St{\'e}phane},
  title = {Counter Systems for Data Logics},
  pages = {10},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/SD-jelia10.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SD-jelia10.pdf},
  doi = {10.1007/978-3-642-15675-5_3},
  abstract = {Data logics are logical formalisms that are used to specify
    properties on structures equipped with data (data words, data trees, runs
    from counter systems, timed words, etc.). In this survey talk, we shall
    see how satisfiability problems for such data logics are related to
    reachability problems for counter systems (including counter automata with
    errors, vector addition systems with states, etc.). This is the
    opportunity to provide an overview about the relationships between data
    logics and verification problems for counter systems.}
}
@inproceedings{demri-infinity2010,
  address = {Singapore},
  month = sep,
  year = 2010,
  volume = 39,
  series = {Electronic Proceedings in Theoretical Computer Science},
  editor = {Chen, Yu-Fang and Rezine, Ahmed},
  acronym = {{INFINITY}'10},
  booktitle = {{P}roceedings of the 12th {I}nternational 
           {W}orkshops on {V}erification of {I}nfinite
           {S}tate {S}ystems
           ({INFINITY}'10)},
  author = {Demri, St{\'e}phane},
  title = {On Selective Unboundedness of~{VASS}},
  pages = {1-15},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/demri-infinity10.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/demri-infinity10.pdf},
  doi = {10.4204/EPTCS.39.1},
  abstract = {Numerous properties of vector addition systems with states
    amount to checking the (un)boundedness of some selective feature
    (\textit{e.g.}, number of reversals, run length). Some of these features
    can be checked in exponential space by using Rackoff's proof or its
    variants, combined with Savitch's theorem. However, the question is still
    open for many others, e.g., reversal-boundedness. In the paper, we
    introduce the class of generalized unboundedness properties that can be
    verified in exponential space by extending Rackoff's technique, sometimes
    in an unorthodox way. We obtain new optimal upper bounds, for example for
    place-boundedness problem, reversal-boundedness detection (several
    variants exist), strong promptness detection problem and regularity
    detection. Our analysis is sufficiently refined so as we also obtain a
    polynomial-space bound when the dimension is fixed.}
}
@article{DL-jal10,
  publisher = {Elsevier Science Publishers},
  journal = {Journal of Applied Logic},
  author = {Demri, St{\'e}phane and Lugiez, Denis},
  title = {Complexity of Modal Logics with {P}resburger Constraints},
  year = {2010},
  volume = {8},
  number = {3},
  pages = {233-252},
  month = sep,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DL-jal10.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DL-jal10.pdf},
  doi = {10.1016/j.jal.2010.03.001},
  abstract = {We introduce the extended modal logic EML with regularity
    constraints and full Presburger constraints on the number of children that
    generalize graded modalities, also known as number restrictions in
    description logics. We show that EML satisfiability is only
    \textsc{pspace}-complete by designing a Ladner-like algorithm. This
    extends a well-known and non-trivial \textsc{pspace} upper bound for
    graded modal logic. Furthermore, we provide a detailed comparison with
    logics that contain Presburger constraints and that are dedicated to query
    XML documents. As an application, we provide a logarithmic space reduction
    from a variant of Sheaves logic SL into EML that allows us to establish
    that its satisfiability problem is also \textsc{pspace}-complete,
    significantly improving the best known upper bound.}
}
@article{DLS-tcs10,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko and 
		Sangnier, Arnaud},
  title = {Model checking  memoryful linear-time logics over
		 one-counter automata},
  year = {2010},
  volume = {411},
  number = {22-24},
  pages = {2298-2316},
  month = may,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DLS-tcs10.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DLS-tcs10.pdf},
  doi = {10.1016/j.tcs.2010.02.021},
  abstract = {We study complexity of the model-checking problems for LTL with
                  registers (also known as freeze LTL and written
                  LTL\(^{\downarrow}\)) and for first-order logic with data
                  equality tests (written \(\textrm{FO}(\sim, <, +1)\)) over
                  one-counter automata. We consider several classes of
                  one-counter automata (mainly deterministic vs.
                  nondeterministic) and several logical fragments (restriction
                  on the number of registers or variables and on the use of
                  propositional variables for control states). The logics have
                  the ability to store a counter value and to test it later
                  against the current counter value. We show that model
                  checking LTL\(^{\downarrow}\) and \(\textrm{FO}(\sim , <,
                  +1)\) over deterministic one-counter automata is
                  PSpace-complete with infinite and finite accepting runs. By
                  constrast, we prove that model checking LTL\(^{\downarrow}\)
                  in which the until operator~\(\mathbf{U}\) is restricted to
                  the eventually~\(\mathbf{F}\) over nondeterministic
                  one-counter automata is \(\Sigma_1^1\)-complete [resp.
                  \(\Sigma_1^0\)-complete] in the infinitary [resp. finitary]
                  case even if only one register is used and with no
                  propositional variable. As a corollary of our proof, this
                  also holds for \(\textrm{FO}(\sim, <, +1)\) restricted to
                  two variables (written \(\textrm{FO}_2 (\sim, <, +1)\)).
                  This makes a difference with the facts that several
                  verification problems for one-counter automata are known to
                  be decidable with relatively low complexity, and that
                  finitary satisfiability for LTL\(^{\downarrow}\) and
                  \(\textrm{FO}_2 (\sim, <, +1)\) are decidable. Our results
                  pave the way for model-checking memoryful (linear-time)
                  logics over other classes of operational models, such as
                  reversal-bounded counter machines.}
}
@inproceedings{CD-lopstr11,
  address = {Odense, Denmark},
  year = 2012,
  volume = {7225},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Vidal, Germ{\'a}n},
  acronym = {{LOPSTR}'11},
  booktitle = {{P}roceedings of the 21st {I}nternational 
               {W}orkshop on {L}ogic {P}rogram {S}ynthesis
               and {T}ransformation
               ({LOPSTR}'11)},
  author = {Cabalar, Pedro and Demri, St{\'e}phane},
  title = {Automata-Based Computation of Temporal Equilibrium Models},
  pages = {57-72},
  doi = {10.1007/978-3-642-32211-2_5},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-lopstr11.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-lopstr11.pdf},
  abstract = {Temporal Equilibrium Logic~(TEL) is a formalism for temporal
    logic programming that generalizes the paradigm of Answer Set
    Programming~(ASP) introducing modal temporal operators from standard
    Linear-time Temporal Logic~(LTL). In this paper we solve some problems
    that remained open for TEL like decidability, bounds for computational
    complexity as well as computation of temporal equilibrium models for
    arbitrary theories. We propose a method for the latter that consists in
    building a B{\"u}chi automaton that accepts exactly the temporal
    equilibrium models of a given theory, providing an automata-based decision
    procedure and illustrating the \(\omega\)-regularity of such sets. We show
    that TEL satisfiability can be solved in exponential space and it is hard
    for polynomial space. Finally, given two theories, we provide a decision
    procedure to check if they have the same temporal equilibrium models.}
}
@inproceedings{BD-frocos11,
  address = {Saarbr{\"u}cken, Germany},
  month = oct,
  year = 2011,
  volume = 6989,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Tinelli, Cesare and Sofronie-Stokkermans, Viorica},
  acronym = {{FroCoS}'11},
  booktitle = {{P}roceedings of the 8th {I}nternational {S}ymposium on {F}rontiers of
                  {C}ombining {S}ystems ({FroCoS}'11)},
  author = {Bersani, Marcello and  Demri, St{\'e}phane},
  title = {The complexity of reversal-bounded model-checking},
  pages = {71-86},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BD-frocos11.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BD-frocos11.pdf},
  doi = {10.1007/978-3-642-24364-6_6},
  abstract = {We study model-checking problems on counter systems when guards
                  are quantifier-free Presburger formulae, the specification
                  languages are LTL-like dialects with arithmetical
                  constraints and the runs are restricted to reversal-bounded
                  ones. We introduce a generalization of reversal-boundedness
                  and we show the NExpTime-completeness of the
                  reversal-bounded model-checking problem as well as for
                  related reversalbounded reachability problems. As a
                  by-product, we show the effective Presburger definability
                  for sets of configurations for which there is a
                  reversal-bounded run verifying a given temporal formula. Our
                  results generalize existing results about reversal-bounded
                  counter automata and provides a uniform and more general
                  framework.}
}
@inproceedings{DDMM-fsttcs11,
  address = {Mumbai, India},
  month = dec,
  year = 2011,
  volume = 13,
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Chakraborty, Supratik and Kumar, Amit},
  acronym = {{FSTTCS}'11},
  booktitle = {{P}roceedings of the 31st {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'11)},
  author = {Darondeau, {\relax Ph}ilippe and Demri, St{\'e}phane and
                  Meyer, Roland and Morvan, {\relax Ch}ristophe},
  title = {{P}etri Net Reachability Graphs: Decidability Status of {FO}
                  Properties},
  pages = {140-151},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDMM-fsttcs11.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDMM-fsttcs11.pdf},
  doi = {10.4230/LIPIcs.FSTTCS.2011.140},
  abstract = {We investigate the decidability and complexity status of
    model-checking problems on unlabelled reachability graphs of Petri nets by
    considering first-order, modal and pattern-based languages without labels
    on transitions or atomic propositions on markings. We consider several
    parameters to separate decidable problems from undecidable ones. Not only
    are we able to provide precise borders and a systematic analysis, but we
    also demonstrate the robustness of our proof techniques.}
}
@incollection{DP-DS11b,
  author = {Demri, St{\'e}phane and Poitrenaud, Denis},
  title = {Verification of Infinite-State Systems},
  booktitle = {Models and Analysis in Distributed Systems},
  editor = {Haddad, Serge and Kordon, Fabrice and Pautet, Laurent and
                  Petrucci, Laure},
  publisher = {John Wiley \& Sons, Ltd.},
  chapter = 8,
  pages = {221-269},
  year = 2011,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DP-DS11b.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DP-DS11b.pdf}
}
@article{DDG-jlc11,
  publisher = {Oxford University Press},
  journal = {Journal of Logic and Computation},
  author = {Demri, St{\'e}phane  and D'Souza, Deepak and Gascon, R{\'e}gis},
  title = {Temporal Logics of Repeating Values},
  year = {2012},
  month = oct,
  volume = 22,
  number = 5,
  pages = {1059-1096},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDG-jlc11.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDG-jlc11.pdf},
  doi = {10.1093/logcom/exr013},
  abstract = {Various logical formalisms with the freeze quantifier have been
    recently considered to model computer systems even though this is a
    powerful mechanism that often leads to undecidability. In this paper, we
    study a linear-time temporal logic with past-time operators such that the
    freeze operator is only used to express that some value from an infinite
    set is repeated in the future or in the past. Such a restriction has been
    inspired by a recent work on spatio-temporal logics that suggests such a
    restricted use of the freeze operator. We show decidability of finitary
    and infinitary satisfiability by reduction into the verification of
    temporal properties in Petri nets by proposing a symbolic representation
    of models. This is a quite surprising result in view of the expressive
    power of the logic since the logic is closed under negation, contains
    future-time and past-time temporal operators and can express the nonce
    property and its negation. These ingredients are known to lead to
    undecidability with a more liberal use of the freeze quantifier. The paper
    also contains developments about the relationships between temporal logics
    with the freeze operator and counter automata as well as reductions into
    first-order logics over data words.}
}
@article{DFGD-jancl10,
  publisher = {Taylor \& Francis},
  journal = {Journal of Applied Non-Classical Logics},
  author = {Demri, St{\'e}phane and Finkel, Alain and Goranko, Valentin
                  and van Drimmelen, Govert},
  title = {Model-checking \(\textsf{CTL}^{*}\) over Flat {P}resburger Counter
      		 	Systems},
  year = {2010},
  volume = {20},
  number = {4},
  pages = {313-344},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DFGD-jancl10.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DFGD-jancl10.pdf},
  doi = {10.3166/jancl.20.313-344},
  abstract = {This paper studies model-checking of fragments and extensions of
    \(\textsf{CTL}^{*}\) on infinite-state counter systems, where the states
    are vectors of integers and the transitions are determined by means of
    relations definable within Presburger arithmetic. In general, reachability
    properties of counter systems are undecidable, but we have identified a
    natural class of admissible counter systems (ACS) for which we show that
    the quantification over paths in \(\textsf{CTL}^{*}\) can be simulated by
    quantification over tuples of natural numbers, eventually allowing
    translation of the whole Presburger-\(\textsf{CTL}^{*}\) into Presburger
    arithmetic, thereby enabling effective model checking. We provide evidence
    that our results are close to optimal with respect to the class of counter
    systems described above.}
}
@incollection{DG-iis09,
  author = {Demri, St{\'e}phane and Gastin, Paul},
  title = {Specification and Verification using Temporal Logics},
  booktitle = {Modern applications of automata theory},
  editor = {D'Souza, Deepak and Shankar, Priti},
  series = {IISc Research Monographs},
  volume = 2,
  publisher = {World Scientific},
  chapter = 15,
  pages = {457-494},
  year = 2012,
  month = jul,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DG-iis09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DG-iis09.pdf},
  abstract = {This chapter illustrates two aspects of automata theory related
    to linear-time temporal logic LTL used for the verification of computer
    systems. First, we present a translation from LTL formulae to B{\"u}chi
    automata. The aim is to design an elementary translation which is
    reasonably efficient and produces small automata so that it can be easily
    taught and used by hand on real examples. Our translation is in the spirit
    of the classical tableau constructions but is optimized in several ways.
    Secondly, we recall how temporal operators can be defined from regular
    languages and we explain why adding even a single operator definable by a
    context-free language can lead to undecidability.}
}
@article{DDMM-lmcs12,
  journal = {Logical Methods in Computer Science},
  author = {Darondeau, {\relax Ph}ilippe and Demri, St{\'e}phane and
                  Meyer, Roland and Morvan, {\relax Ch}ristophe},
  title = {{P}etri Net Reachability Graphs: Decidability Status of {FO}
                  Properties},
  volume = 8,
  number = {4:9},
  nopages = {},
  month = oct,
  year = 2012,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDMM-lmcs12.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDMM-lmcs12.pdf},
  doi = {10.2168/LMCS-8(4:9)2012},
  abstract = {We investigate the decidability and complexity status of
    model-checking problems on unlabelled reachability graphs of Petri nets by
    considering first-order and modal languages without labels on transitions
    or atomic propositions on markings. We consider several parameters to
    separate decidable problems from undecidable ones. Not only are we able to
    provide precise borders and a systematic analysis, but we also demonstrate
    the robustness of our proof techniques.}
}
@inproceedings{CD-aiml12,
  address = {Copenhagen, Denmark},
  month = aug,
  year = 2012,
  publisher = {College Publications},
  editor = {Bolander, Thomas and Bra{\"u}ner, Torben and Ghilardi, Silvio and Moss, Lawrence},
  acronym = {{AiML}'12},
  booktitle = {{S}elected {P}apers from the 9th
           {W}orkshop on {A}dvances in {M}odal {L}ogics
           ({AiML}'12)},
  author = {Carreiro, Facundo and Demri, St{\'e}phane},
  title = {Beyond Regularity for {P}resburger Modal Logics},
  pages = {161-182},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-aiml12.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-aiml12.pdf},
  abstract = {Satisfiability problem for modal logic~K with quantifier-free
    Presburger and regularity constraints~(EML) is known to be
    pspace-complete. In this paper, we consider its extension with nonregular
    constraints, and more specifically those expressed by visibly pushdown
    languages~(VPL). This class of languages behaves nicely, in particular
    when combined with Propositional Dynamic Logic~(PDL). By extending EML, we
    show that decidability is preserved if we allow at most one positive
    VPL-constraint at each modal depth. However, the presence of two
    VPL-contraints or the presence of a negative occurrence of a single
    VPL-constraint leads to undecidability. These results contrast with the
    decidability of PDL augmented with VPL-constraints.}
}
@inproceedings{DDS-ijcar12,
  address = {Manchester, UK},
  month = jun,
  year = 2012,
  volume = {7364},
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer-Verlag},
  editor = {Gramlich, Bernhard and Miller, Dale and Sattler, Uli},
  acronym = {{IJCAR}'12},
  booktitle = {{P}roceedings of the 6th {I}nternational {J}oint
           {C}onference on {A}utomated {R}easoning
           ({IJCAR}'12)},
  author = {Demri, St{\'e}phane and Dhar, Amit Kumar and Sangnier, Arnaud},
  title = {Taming Past {LTL} and Flat Counter Systems},
  pages = {179-193},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-ijcar12.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-ijcar12.pdf},
  doi = {10.1007/978-3-642-31365-3_16},
  abstract = {Reachability and LTL model-checking problems for flat counter
   systems are known to be decidable but whereas the reachability problem can
   be shown in NP, the best known complexity upper bound for the latter
   problem is made of a tower of several exponentials. Herein, we show that
   the problem is only NP-complete even if LTL admits past-time operators and
   arithmetical constraints on counters. Actually, the NP upper bound is shown
   by adequately combining a new stuttering theorem for Past LTL and the
   property of small integer solutions for quantifier-free Presburger
   formulae. Other complexity results are proved, for instance for restricted
   classes of flat counter systems.}
}
@article{jcss12-DJLL,
  publisher = {Elsevier Science Publishers},
  journal = {Journal of Computer and System Sciences},
  author = {Demri, St{\'e}phane and Jurdzi{\'n}ski, Marcin and Lachish, Oded and
  	 	 Lazi{\'c}, Ranko},
  title = {The covering and boundedness problems for branching
  		   vector addition systems},
  year = {2012},
  volume = 79,
  number = 1,
  pages = {23-38},
  month = feb,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/djll-jcss12.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/djll-jcss12.pdf},
  doi = {10.1016/j.jcss.2012.04.002},
  abstract = {The covering and boundedness problems for branching vector
    addition systems are shown complete for doubly-exponential time.}
}
@article{BDL-icomp12,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Brochenin, R{\'e}mi and Demri, St{\'e}phane and Lozes, {\'E}tienne},
  title = {On the Almighty Wand},
  year = {2012},
  volume = 211,
  pages = {106-137},
  month = feb,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDL-icomp12.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDL-icomp12.pdf},
  doi = {10.1016/j.ic.2011.12.003},
  abstract = {We investigate decidability, complexity and expressive power
    issues for (first-order) separation logic with one record field (herein
    called~\texttt{SL}) and its fragments. \texttt{SL}~can specify properties
    about the memory heap of programs with singly-linked lists. Separation
    logic with two record fields is known to be undecidable by reduction of
    finite satisfiability for classical predicate logic with one binary
    relation. Surprisingly, we show that second-order logic is as expressive
    as \texttt{SL} and as a by-product we get undecidability of~\texttt{SL}.
    This is refined by showing that \texttt{SL} without the separating
    conjunction is as expressive as~\texttt{SL}, whence undecidable too. As a
    consequence, in \texttt{SL} the separating implication (also known as the
    magic wand) can simulate the separating conjunction. By~contrast, we
    establish that \texttt{SL} without the magic wand is decidable, and
    we~prove a non-elementary complexity by reduction from satisfiability for
    the first-order theory over finite words. This result is extended with a
    bounded use of the magic wand that appears in Hoare-style rules. As a
    generalisation, it~is shown that~\(k\texttt{SL}\), the separation logic
    over heaps with \(k\geq 1\) record fields, is equivalent
    to~\(k\texttt{SO}\), the second-order logic over heaps with \(k\) record
    fields.}
}
@inproceedings{BD-csr13,
  address = {Ekaterinburg, Russia},
  month = jun,
  year = 2013,
  volume = {7913},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Bulatov, Andrei A. and Shur, Arseny M.},
  acronym = {{CSR}'13},
  booktitle = {{P}roceedings of the 8th {I}nternational {C}omputer {S}cience
                  {S}ymposium in {R}ussia ({CSR}'13)},
  author = {Bansal, Kshitij and Demri, St{\'e}phane},
  title = {Model-checking bounded multi-pushdown systems},
  pages = {405-417},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BD-csr13.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BD-csr13.pdf},
  doi = {10.1007/978-3-642-38536-0_35},
  abstract = {We provide complexity characterizations of model checking
    multi-pushdown systems. We consider three standard notions for
    boundedness: context boundedness, phase boundedness and stack ordering.
    The logical formalism is a linear-time temporal logic extending well-known
    logic \texttt{CaRet} but dedicated to multi-pushdown systems in which abstract
    operators are parameterized by stacks. We show that the problem is
    ExpTime-complete for context-bounded runs and unary encoding of the number
    of context switches; we also prove that the problem is 2ExpTime-complete
    for phase-bounded runs and unary encoding of the number of phase switches.
    In both cases, the value~\(k\) is given as an input, which makes a
    substantial difference in the complexity.}
}
@inproceedings{DDS-icalp13,
  address = {Riga, Latvia},
  month = jul,
  year = 2013,
  volume = {7966},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Fomin, Fedor V. and Freivalds, R{\=u}si{\c{n}}{\v{s}} 
  	 	and Kwiatkowska, Marta and Peleg, David},
  acronym = {{ICALP}'13},
  booktitle = {{P}roceedings of the 40th {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming ({ICALP}'13)~-- {P}art~{II}},
  author = {Demri, St{\'e}phane and Dhar, Amit Kumar and Sangnier, Arnaud},
  title = {On the Complexity of Verifying Regular Properties on Flat Counter Systems},
  pages = {162-173},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-icalp13.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-icalp13.pdf},
  doi = {10.1007/978-3-642-39212-2_17},
  abstract = {Among the approximation methods for the verification of counter
    systems, one of them consists in model-checking their flat unfoldings.
    Unfortunately, the complexity characterization of model-checking problems
    for such operational models is not always well studied except for
    reachability queries or for Past LTL. In this paper, we characterize the
    complexity of model-checking problems on flat counter systems for the
    specification languages including first-order logic, linear mu-calculus,
    infinite automata, and related formalisms. Our results span different
    complexity classes (mainly from PTime to PSpace) and they apply to
    languages in which arithmetical constraints on counter values are
    systematically allowed. As far as the proof techniques are concerned, we
    provide a uniform approach that focuses on the main issues.}
}
@inproceedings{DFP-lics13,
  address = {New-Orleans, Louisiana, USA},
  month = jun,
  year = 2013,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{LICS}'13},
  booktitle = {{P}roceedings of the 28th
               {A}nnual {IEEE} {S}ymposium on
               {L}ogic in {C}omputer {S}cience
               ({LICS}'13)},
  author = {Demri, St{\'e}phane and Figueira, Diego and Praveen, M.},
  title = {Reasoning about Data Repetitions with Counter Systems},
  pages = {33-42},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DFP-lics13.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DFP-lics13.pdf},
  doi = {10.1109/LICS.2013.8},
  abstract = {We study linear-time temporal logics interpreted over data words
    with multiple attributes. We restrict the atomic formulas to equalities of
    attribute values in successive positions and to repetitions of attribute
    values in the future or past. We demonstrate correspondences between
    satisfiability problems for logics and reachability-like decision problems
    for counter systems. We show that allowing/disallowing atomic formulas
    expressing repetitions of values in the past corresponds to the
    reachability\slash coverability problem in Petri nets. This gives us
    2EXPSPACE upper bounds for several satisfiability problems. We prove
    matching lower bounds by reduction from a reachability problem for a newly
    introduced class of counter systems. This new class is a succinct version
    of vector addition systems with states in which counters are accessed via
    pointers, a potentially useful feature in other contexts. We strengthen
    further the correspondences between data logics and counter systems by
    characterizing the complexity of fragments, extensions and variants of the
    logic. For instance, we precisely characterize the relationship between
    the number of attributes allowed in the logic and the number of counters
    needed in the counter system.}
}
@article{demri-jcss13,
  publisher = {Elsevier Science Publishers},
  journal = {Journal of Computer and System Sciences},
  author = {Demri, St{\'e}phane},
  title = {On selective unboundedness of~{VASS}},
  year = {2013},
  volume = {79},
  number = {5},
  pages = {689-713},
  month = aug,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/demri-jcss13.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/demri-jcss13.pdf},
  doi = {10.1016/j.jcss.2013.01.014},
  abstract = {Numerous properties of vector addition systems with states
    amount to checking the (un)boundedness of some selective feature (e.g.,
    number of reversals, counter values, run lengths). Some of these features
    can be checked in exponential space by using Rackoff's proof or its
    variants, combined with Savitch's Theorem. However, the question is still
    open for many others, e.g., regularity detection problem and
    reversal-boundedness detection problem. In the paper, we introduce the
    class of generalized unboundedness properties that can be verified in
    exponential space by extending Rackoff's technique, sometimes in an
    unorthodox way. We obtain new optimal upper bounds, for example for place
    boundedness problem, reversal-boundedness detection (several variants are
    present in the paper), strong promptness detection problem and regularity
    detection. Our analysis is sufficiently refined so as to obtain a
    polynomial-space bound when the dimension is fixed.}
}
@inproceedings{DDS-rp14,
  address = {Oxford, UK},
  month = sep,
  year = 2014,
  volume = {8762},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell, James},
  acronym = {{RP}'14},
  booktitle = {{P}roceedings of the 8th {W}orkshop
           on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'14)},
  author = {Demri, St{\'e}phane and Dhar, Amit Kumar and Sangnier, Arnaud},
  title = {Equivalence Between Model-Checking Flat Counter Systems and
  	          {P}resburger Arithmetic},
  pages = {85-97},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-rp14.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-rp14.pdf},
  doi = {10.1007/978-3-319-11439-2_7},
  abstract = {We show that model-checking flat counter systems over
    CTL\textsuperscript{*} (with arithmetical constraints on counter values)
    has the same complexity as the satisfiability problem for Presburger
    arithmetic. The lower bound already holds with the temporal operator EF
    only, no~arithmetical constraints in the logical language and with guards
    on transitions made of simple linear constraints. This complements our
    understanding of model-checking flat counter systems with linear-time
    temporal logics, such as LTL for which the problem is already known to be
    (only) NP-complete with guards restricted to the linear fragment.}
}
@inproceedings{DD-aiml14,
  address = {Groningen, The Netherlands},
  month = aug,
  year = 2014,
  publisher = {College Publications},
  editor = {Gor{\'e}, Rajeev and Kooi, Barteld P. and Kurucz, Agi},
  acronym = {{AiML}'14},
  booktitle = {{P}roceedings of the 10th
           {C}onference on {A}dvances in {M}odal {L}ogics
           ({AiML}'14)},
  author = {Demri, St{\'e}phane and Deters, Morgan},
  title = {The effects of modalities in separation logics (extended abstract)},
  pages = {134-138},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-aiml14.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-aiml14.pdf},
  abstract = {Like modal logic, temporal logic, or description logic,
    separation logic has become a popular class of logical formalisms in
    computer science, conceived as assertion languages for Hoare-style proof
    systems with the goal to perform automatic program analysis. We present
    similarities with modal and temporal logics, and we present landmark
    results about decidability, complexity and expressive power.}
}
@inproceedings{DD-csllics14,
  address = {Vienna, Austria},
  month = jul,
  year = 2014,
  publisher = {ACM Press},
  acronym = {{CSL\slash LICS}'14},
  booktitle = {{P}roceedings of the Joint Meeting of the 23rd {EACSL} {A}nnual {C}onference on
  	    {C}omputer {S}cience {L}ogic and the 29th {A}nnual {ACM\slash
            IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({CSL\slash LICS}'14)},
  author = {Demri, St{\'e}phane and Deters, Morgan},
  title = {Expressive Completeness of Separation Logic With Two
                  Variables and No Separating Conjunction},
  nopages = {},
  chapter = {37},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-csllics14.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-csllics14.pdf},
  doi = {10.1145/2603088.2603142},
  abstract = {We show that first-order separation logic with one record field
    restricted to two variables and the separating implication (no separating
    conjunction) is as expressive as weak second-order logic, substantially
    sharpening a previous result. Capturing weak second-order logic with such
    a restricted form of separation logic requires substantial updates to
    known proof techniques. We develop these, and as a by-product identify the
    smallest fragment of separation logic known to be undecidable: first-order
    separation logic with one record field, two variables, and no separating
    conjunction.}
}
@inproceedings{DGLM-csr14,
  address = {Moscow, Russia},
  month = jun,
  year = 2014,
  volume = {8476},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Pin, Jean-{\'E}ric},
  acronym = {{CSR}'14},
  booktitle = {{P}roceedings of the 9th {I}nternational {C}omputer {S}cience
                  {S}ymposium in {R}ussia ({CSR}'14)},
  author = {Demri, St{\'e}phane and Galmiche, Didier and
                  Larchey-Wendling, Dominique and M{\'e}ry, Daniel},
  title = {Separation Logic with One Quantified Variable},
  pages = {125-138},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DGLM-csr14.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DGLM-csr14.pdf},
  doi = {10.1007/978-3-319-06686-8_10},
  abstract = {We investigate first-order separation logic with one record
    field restricted to a unique quantified variable (1SL1). Undecidability is
    known when the number of quantified variables is unbounded and the
    satisfiability problem is PSPACE-complete for the propositional fragment.
    We show that the satisfiability problem for 1SL1 is PSPACE-complete and we
    characterize its expressive power by showing that every formula is
    equivalent to a Boolean combination of atomic properties. This contributes
    to our understanding of fragments of first-order separation logic that can
    specify properties about the memory heap of programs with singly-linked
    lists. When the number of program variables is fixed, the complexity drops
    to polynomial time. All the fragments we consider contain the magic wand
    operator and first-order quantification over a single variable.}
}
@inproceedings{BDD-frocos13,
  address = {Nancy, France},
  month = sep,
  year = 2013,
  volume = 8152,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Fontaine, Pascal and Ringeissen, Christophe and Schmidt, Renate A.},
  acronym = {{FroCoS}'13},
  booktitle = {{P}roceedings of the 9th {I}nternational {S}ymposium on {F}rontiers of
                  {C}ombining {S}ystems ({FroCoS}'13)},
  author = {Barrett, Clark and Demri, St{\'e}phane and Deters, Morgan},
  title = {Witness runs for counter machines},
  pages = {120-150},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDD-frocos13.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDD-frocos13.pdf},
  doi = {10.1007/978-3-642-40885-4_9},
  abstract = {In this paper, we present recent results about the verification
    of counter machines by using decision procedures for Presburger
    arithmetic. We recall several known classes of counter machines for which
    the reachability sets are Presburger-definable as well as temporal logics
    with arithmetical constraints. We discuss issues related to flat counter
    machines, path schema enumeration, and the use of SMT solvers.}
}
@unpublished{DD-esslli15,
  author = {Demri, St{\'e}phane and Deters, Morgan},
  title = {Logical Investigations on Separation Logics},
  month = aug,
  year = 2015,
  note = {Lecture Notes, European Summer School on Logic, Language and
                  Information ({ESSLLI}'15)},
  address = {Barcelona, Spain},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-esslli15.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-esslli15.pdf}
}
@article{DD-jlc15,
  publisher = {Oxford University Press},
  journal = {Journal of Logic and Computation},
  author = {Demri, St{\'e}phane and Deters, Morgan},
  title = {Temporal Logics on Strings with Prefix Relation},
  year = 2016,
  volume = {26},
  number = {3},
  pages = {989-1017},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-jlc15-v2.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-jlc15-v2.pdf},
  doi = {10.1093/logcom/exv028},
  abstract = {We show that linear-time temporal logic over concrete domains
    made of finite strings and the prefix relation admits a PSpace-complete
    satisfiability problem. Actually, we extend a known result with the
    concrete domain made of the set of natural numbers and the greater than
    relation (corresponding to the singleton alphabet case) and we solve an
    open problem mentioned in several publications. Since the prefix relation
    is not a total ordering, it~is not possible to take advantage of existing
    techniques dedicated to temporal logics with concrete domains that are
    essentially linearly ordered structures. Instead, we introduce an adequate
    encoding of string constraints into length constraints that allows us to
    reduce the problem on strings to the problem on natural numbers. To~do~so,
    we~also propose an extended version of the logic on strings that is able
    to compare lengths of longest common prefixes and for which the
    satisfiability problem is shown in PSpace. Finally, we show how to lift
    the result for the branching-time case in order to get decidability when
    the underlying temporal logic is~CTL\textsuperscript*.}
}
@article{DDS-ic15,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Demri, St{\'e}phane and Dhar, Amit Kumar and Sangnier, Arnaud},
  title = {Taming Past {LTL} and Flat Counter Systems},
  volume = {242},
  month = jun,
  year = 2015,
  pages = {306-339},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-ic15.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-ic15.pdf},
  doi = {10.1016/j.ic.2015.03.007},
  abstract = {Reachability and LTL model-checking problems for flat counter
    systems are known to be decidable but whereas the reachability problem can
    be shown in NP, the best known complexity upper bound for the latter
    problem is made of a tower of several exponentials. Herein, we show that
    this problem is only NP-complete even if LTL admits past-time operators
    and arithmetical constraints on counters. As far as past-time operators
    are concerned, their addition to LTL immediately leads to complications
    and hence an NP upper bound cannot be deduced by translating formulae into
    LTL and studying the problem only for this latter logic. Actually, the NP
    upper bound is shown by adequately combining a new stuttering theorem for
    Past LTL and the property of small integer solutions for quantifier-free
    Presburger formulae. This latter complexity bound extends known and recent
    results on model-checking weak Kripke structures with LTL formulae as
    well as reachability problems for flat counter systems. We also provide
    other complexity results obtained by restricting further the class of flat
    counter systems.}
}
@article{DD-jancl15,
  publisher = {Taylor \& Francis},
  journal = {Journal of Applied Non-Classical Logics},
  author = {Demri, St{\'e}phane and Deters, Morgan},
  title = {Separation Logics and Modalities: A~Survey},
  volume = 25,
  number = 1,
  pages = {50-99},
  year = 2015,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-jancl15.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-jancl15.pdf},
  doi = {10.1080/11663081.2015.1018801},
  abstract = {Like modal logic, temporal logic, or description logic,
    separation logic has become a popular class of logical formalisms in
    computer science, conceived as assertion languages for Hoare-style proof
    systems with the goal to perform automatic program analysis. In a broad
    sense, separation logic is often understood as a programming language, an
    assertion language and a family of rules involving Hoare triples. In this
    survey, we present similarities between separation logic as an assertion
    language and modal and temporal logics. Moreover, we propose a selection
    of landmark results about decidability, complexity and expressive power.}
}
@article{DD-tocl15,
  publisher = {ACM Press},
  journal = {ACM Transactions on Computational Logic},
  author = {Demri, St{\'e}phane and Deters, Morgan},
  title = {Two-variable separation logic and its inner circle},
  volume = 16,
  number = {2:15},
  nopages = {},
  month = mar,
  year = 2015,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-tocl15.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-tocl15.pdf},
  doi = {10.1145/2724711},
  abstract = {Separation logic is a well-known assertion language for
    Hoare-style proof systems. We show that first-order separation logic with
    a unique record field restricted to two quantified variables and no
    program variables is undecidable. This is among the smallest fragments of
    separation logic known to be undecidable, and this contrasts with
    decidability of two-variable first-order logic. We also investigate its
    restriction by dropping the magic wand connective, known to be decidable
    with non-elementary complexity, and we show that the satisfiability
    problem with only two quantified variables is not yet elementary
    recursive. Furthermore, we establish insightful and concrete relationships
    between two-variable separation logic and propositional in- terval
    temporal logic (PITL), data logics, and modal logics, providing an inner
    circle of closely-related logics.}
}
@book{DGL-cup2016,
  author = {Demri, St{\'e}phane and Goranko, Valentin and Lange, Martin},
  title = {{T}emporal {L}ogics in {C}omputer {S}cience},
  publisher = {Cambridge University Press},
  series = {Cambridge Tracts in Theoretical Computer Science},
  volume = {58},
  year = {2016},
  month = oct,
  url = {http://www.cambridge.org/9781107028364},
  isbn = {9781107028364}
}
@article{ADFLP-fi2016,
  publisher = {{IOS} Press},
  journal = {Fundamenta Informaticae},
  author = {Abdulla, Parosh Aziz and Demri, St{\'e}phane and Finkel, Alain and Leroux, J{\'e}r{\^o}me and Potapov, Igor},
  editor = {Abdulla, Parosh Aziz and Demri, St{\'e}phane and Finkel, Alain and Leroux, J{\'e}r{\^o}me and Potapov, Igor},
  number = {3--4},
  title = {Selected papers of Reachability Problems Workshop 2012 (Bordeaux) and 2013 (Uppsala)},
  url = {http://content.iospress.com/journals/fundamenta-informaticae/143/3-4},
  volume = {143},
  year = {2016}
}
@inproceedings{ABDL-rp16,
  address = {Aalborg, Denmark},
  month = sep,
  year = 2016,
  volume = {9899},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Larsen, Kim G. and Srba, Ji{\v{r}}{\'\i}},
  acronym = {{RP}'16},
  booktitle = {{P}roceedings of the 10th {W}orkshop
           on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'16)},
  author = {Alechina, Natasha and Bulling, Nils and Demri,
                  St{\'e}phane and Logan, Brian},
  title = {On the Complexity of Resource-Bounded Logics},
  pages = {36-50},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABDL-rp16.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABDL-rp16.pdf},
  doi = {10.1007/978-3-319-45994-3_3},
  abstract = {We revisit decidability results for resource-bounded
    logics and use decision problems on VASS to establish complexity
    characterisation of (decidable) model-checking problems. We show
    that the model-checking problem for the logic RB\(\pm\)ATL is
    2EXPTIME-complete by using recent results on alternating VASS.
    Moreover, we establish that the model-checking problem for RBTL is
    EXPSPACE-complete and that the problem is decidable and of the same
    complexity for RBTL\textsuperscript{*}, proving a new decidability
    result as a by-product of the approach. We establish that the
    model-checking problem for RB\(\pm\)ATL\textsuperscript{*}, the
    extension of RB\(\pm\)ATL with arbitrary path formulae is decidable
    by a reduction into parity games. We are also able to synthesise
    values for resource parameters. Hence, the paper establishes formal
    correspondences between model-checking problems and decision
    problems on alternating VASS, paving the way to more applications.}
}
@article{DFP-lmcs16,
  journal = {Logical Methods in Computer Science},
  author = {Demri, St{\'e}phane and Figueira, Diego and Praveen, M},
  title = {Reasoning about Data Repetitions with Counter Systems},
  year = 2016,
  volume = {12},
  number = {3},
  month = aug,
  pages = {1:1-1:55},
  url = {http://arxiv.org/abs/1604.02887},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DFP-lmcs16.pdf},
  doi = {10.2168/LMCS-12(3:1)2016},
  abstract = {We study linear-time temporal logics interpreted over data words
     with multiple attributes. We restrict the atomic formulas to equalities
     of attribute values in successive positions and to repetitions of
     attribute values in the future or past. We demonstrate correspondences
     between satisfiability problems for logics and reachability-like decision
     problems for counter systems. We show that allowing\slash disallowing
     atomic formulas expressing repetitions of values in the past corresponds
     to the reachability\slash coverability problem in Petri nets. This gives
     us 2EXPSPACE upper bounds for several satisfiability problems. We prove
     matching lower bounds by reduction from a reachability problem for a
     newly introduced class of counter systems. This new class is a succinct
     version of vector addition systems with states in which counters are
     accessed via pointers, apotentially useful feature in other contexts. We
     strengthen further the correspondences between data logics and counter
     systems by characterizing the complexity of fragments, extensions and
     variants of the logic. For instance, we precisely characterize the
     relationship between the number of attributes allowed in the logic and
     the number of counters needed in the counter system.}
}
@comment{{B-arxiv16,
  author =		Bollig, Benedikt, 
  affiliation = 	aff-LSVmexico,
  title =    		One-Counter Automata with Counter Visibility, 
  institution = 	Computing Research Repository, 
  number =    		1602.05940, 
  month = 		feb, 
  nmonth =     		2,
  year = 		2016, 
  type = 		RR, 
  axeLSV = 		mexico,
  NOcontrat = 		"",
  
  url =			http://arxiv.org/abs/1602.05940, 
  PDF =			"http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf",
  lsvdate-new =  	20160222,
  lsvdate-upd =  	20160222,
  lsvdate-pub =  	20160222,
  lsv-category = 	"rapl",
  wwwpublic =    	"public and ccsb",
  note = 		18~pages, 

  abstract = "In a one-counter automaton (OCA), one can read a letter
    from some finite alphabet, increment and decrement the counter by
    one, or test it for zero. It is well-known that universality and
    language inclusion for OCAs are undecidable. We consider here OCAs
    with counter visibility: Whenever the automaton produces a letter,
    it outputs the current counter value along with~it. Hence, its
    language is now a set of words over an infinite alphabet. We show
    that universality and inclusion for that model are in PSPACE, thus
    no harder than the corresponding problems for finite automata, which
    can actually be considered as a special case. In fact, we show that
    OCAs with counter visibility are effectively determinizable and
    closed under all boolean operations. As~a~strict generalization, we
    subsequently extend our model by registers. The general nonemptiness
    problem being undecidable, we impose a bound on the number of
    register comparisons and show that the corresponding nonemptiness
    problem is NP-complete.",
}}
@article{DGLM-tocs16,
  publisher = {Springer},
  journal = {Theory of Computing Systems},
  author = {Demri, St{\'e}phane and Galmiche, Didier and
                  Larchey-Wendling, Dominique and Mery, Daniel},
  title = {Separation Logic with One Quantified Variable},
  year = 2017,
  volume = {61},
  number = {2},
  pages = {371-461},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DGLM-tocs16.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DGLM-tocs16.pdf},
  doi = {10.1007/s00224-016-9713-1},
  abstract = {We investigate first-order separation logic with one record
    field restricted to a unique quantified variable (1SL1). Undecidability is
    known when the number of quantified variables is unbounded and the
    satisfiability problem is pspace-complete for the propositional fragment.
    We show that the satisfiability problem for 1SL1 is pspace-complete and we
    characterize its expressive power by showing that every formula is
    equivalent to a Boolean combination of atomic properties. This contributes
    to our understanding of fragments of first-order separation logic that can
    specify properties about the memory heap of programs with singly-linked
    lists. All the fragments we consider contain the magic wand operator and
    first-order quantification over a single variable.}
}
@article{DD-tocl15b,
  publisher = {ACM Press},
  journal = {ACM Transactions on Computational Logic},
  author = {Demri, St{\'e}phane and Deters, Morgan},
  title = {Expressive Completeness of Separation Logic With Two Variables and
                 No Separating Conjunction},
  volume = {17},
  number = {2},
  pages = {12:1-12:44},
  month = mar,
  year = 2016,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-tocl15b.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-tocl15b.pdf},
  doi = {10.1145/2835490},
  abstract = {Separation logic is used as an assertion language for
    Hoare-style proof systems about programs with pointers, and there is an
    ongoing quest for understanding its complexity and expressive power.
    Herein, we show that first-order separation logic with one record field
    restricted to two variables and the separating implication (no~separating
    conjunction) is as expressive as weak second-order logic, substantially
    sharpening a previous result. Capturing weak second-order logic with such
    a restricted form of separation logic requires substantial updates to
    known proof techniques. We develop these, and as a by-product identify the
    smallest fragment of separation logic known to be undecidable: first-order
    separation logic with one record field, two variables, and no separating
    conjunction. Because we forbid ourselves the use of many syntactic
    resources, this underscores even further the power of separating
    implication on concrete heaps.}
}
@article{DDS-tcs17,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Demri, St{\'e}phane and Dhar, Amit and Sangnier, Arnaud},
  title = {Equivalence Between Model-Checking Flat Counter Systems and Presburger Arithmetic},
  volume = {735},
  optnumber = {},
  year = {2017},
  pages = {2-23},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-tcs17.pdf}
}
@inproceedings{DLL-fsttcs17,
  address = {Kanpur, India},
  month = dec,
  year = 2017,
  volume = {93},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Satya Lokam and R. Ramanujam},
  acronym = {{FSTTCS}'17},
  booktitle = {{P}roceedings of the 37th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'17)},
  author = {St{\'e}phane Demri and {\'E}tienne Lozes and Denis Lugiez},
  title = {On Symbolic Heaps Modulo Permission Theories},
  pages = {25:1-25:14},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DLL-fsttcs17.pdf},
  url = {https://doi.org/10.4230/LIPIcs.FSTTCS.2017.25},
  doi = {10.4230/LIPIcs.FSTTCS.2017.25}
}
@article{DKP-jar2017,
  publisher = {Springer},
  journal = {Journal of Automated Reasoning},
  author = {Demri, St{\'e}phane and Kapur, Deepak and Weidenbach, Christoph},
  editor = {Demri, St{\'e}phane and Kapur, Deepak and Weidenbach, Christoph},
  title = {Special Issue of Selected Extended Papers of IJCAR 2014},
  url = {http://link.springer.com/journal/10817/58/1/page/1},
  volume = {58},
  number = {1},
  year = {2017}
}
@incollection{SD-EORM18,
  author = {Demri, St{\'e}phane},
  title = {Reasoning about reversal-bounded counter machines},
  editor = {Goli{\'n}ska-Pilarek, Joanna and Zawidzki, Micha\l},
  booktitle = {Ewa Orlowska on Relational Methods in Logic and Computer Science},
  publisher = {Springer},
  series = {Outstanding Contributions to Logic},
  volume = {17},
  year = {2018},
  pages = {441-479},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/SD-EORM.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SD-EORM.pdf}
}
@inproceedings{D-time18,
  address = {Warsaw, Poland},
  month = oct,
  year = 2018,
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Natasha Alechina and Kjetil Norvag and Wojciech Penczek},
  acronym = {{TIME}'18},
  booktitle = {{P}roceedings of the 25th {I}nternational {S}ymposium on 
	       {T}emporal {R}epresentation and {R}easoning
	       ({TIME}'18)},
  author = {Demri, St{\'e}phane},
  title = {On temporal and separation logics},
  pages = {1:1-1:4},
  url = {http://drops.dagstuhl.de/opus/volltexte/2018/9766/pdf/LIPIcs-TIME-2018-1.pdf}
}
@inproceedings{DF-aiml18,
  address = {Bern, Switzerland},
  month = aug,
  year = 2018,
  publisher = {College Publications},
  editor = {Guram Bezhanishvili and Giovanna D'Agostino and
                  George Metcalfe and Thomas Studer},
  acronym = {{AiML}'18},
  booktitle = {{P}roceedings of the 10th
           {C}onference on {A}dvances in {M}odal {L}ogics
           ({AiML}'18)},
  author = {Demri, St{\'e}phane and Fervari, Raul},
  title = {On the complexity of modal separation logics},
  pages = {179-198},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DF-aiml18.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DF-aiml18.pdf}
}
@article{ABDL-tcs18,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Alechina, Natasha and Bulling, Nils and Demri,
                  St{\'e}phane and Logan, Brian},
  title = {On the Complexity of Resource-Bounded Logics},
  volume = {750},
  year = {2018},
  pages = {69--100},
  doi = {10.1016/j.tcs.2018.01.019},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABDL-tcs18.pdf}
}
@inproceedings{DLM-fossacs18,
  address = {Thessaloniki, Greece},
  month = apr,
  year = 2018,
  volume = {10803},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Baier, Christel and {Dal Lago}, Ugo},
  acronym = {{FoSSaCS}'18},
  booktitle = {{P}roceedings of the 21st {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'18)},
  author = {St{\'e}phane Demri and {\'E}tienne Lozes and Alessio Mansutti},
  title = {The Effects of Adding Reachability Predicates in Propositional Separation Logic},
  pages = {476-493},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DLM-fossacs18.pdf}
}
@inproceedings{DLM-csl20,
  address = {Barcelona, Spain},
  month = jan,
  year = 2020,
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Fern{\'a}ndel, Maribel and Muscholl, Anca},
  acronym = {{CSL}'20},
  booktitle = {{P}roceedings of the 28th {A}nnual {EACSL} {C}onference on
                  {C}omputer {S}cience {L}ogic ({CSL}'20)},
  author = {St{\'e}phane Demri and {\'E}tienne Lozes and Alessio Mansutti},
  title = {Internal Calculi for Separation Logics},
  note = {To appear}
}
@article{DF-jlc19,
  publisher = {Oxford University Press},
  journal = {Journal of Logic and Computation},
  author = {Demri, St{\'e}phane and Fervari, Raul},
  title = {The power of modal separation logics},
  year = 2019,
  note = {To appear},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DF-jlc19.pdf}
}
@inproceedings{BD-aamas19,
  address = {Montreal, Canada},
  month = jun,
  publisher = {ACM Press},
  acronym = {{AAMAS}'19},
  booktitle = {{P}roceedings of the 18th {I}nternational {J}oint {C}onference on
                  {A}utonomous {A}gents and {M}ulti-{A}gent {S}ystems
		  ({AAMAS}'19)},
  author = {Belardinelli, Francesco and Demri, St{\'e}phane},
  title = {Resource-bounded ATL: the Quest for Tractable Fragments},
  pages = {206--214},
  year = 2019,
  pdf = {http://www.ifaamas.org/Proceedings/aamas2019/pdfs/p206.pdf},
  url = {http://www.ifaamas.org/Proceedings/aamas2019/forms/contents.htm#3F}
}
@inproceedings{DFM-jelia19,
  address = {Rende, Italy},
  month = jun,
  year = 2019,
  volume = 11468,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Calimeri, Francesco and Leone, Nicola and Manna, Marco},
  acronym = {{JELIA}'19},
  booktitle = {{P}roceedings of the 16th {E}uropean {C}onference on {L}ogics in
                  {A}rtificial {I}ntelligence ({JELIA}'19)},
  author = {Demri, St{\'e}phane and Fervari, Raul and Mansutti, Alessio},
  title = {Axiomatising logics with separating conjunctions and modalities},
  pages = {692-708},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFM-jelia19.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFM-jelia19.pdf},
  doi = {10.1007/978-3-030-19570-0_45}
}
@inproceedings{BD-lics19,
  address = {Vancouver, Canada},
  month = jun,
  publisher = {{IEEE} Press},
  editor = {Bouyer, Patricia},
  acronym = {{LICS}'19},
  booktitle = {{P}roceedings of the 34th {A}nnual {ACM\slash
            IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'19)},
  author = {Bednarczyk, Bartosz and Demri, St{\'e}phane},
  title = {Why propositional quantification makes modal logics on trees robustly hard ?},
  pages = {1-13},
  year = 2019,
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BD-lics2019.pdf},
  doi = {10.1109/LICS.2019.8785656}
}

This file was generated by bibtex2html 1.98.