@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.*