@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},
url = {https://drops.dagstuhl.de/opus/volltexte/2020/11662/},
doi = {10.4230/LIPIcs.CSL.2020.19}
}
@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},
volume = {29},
number = {8},
pages = {1139--1184},
year = 2019,
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}
}
@article{DFM-jlc21,
publisher = {Oxford University Press},
journal = {Journal of Logic and Computation},
author = {Demri, St{\'e}phane and Fervari, Raul and Mansutti, Alessio},
title = {Internal proof calculi for modal logics with separating conjunction},
year = 2021,
note = {Accepted for publication to the Special issue of JLC on
External and Internal Calculi for Non Classical Logics.},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFM-jlc21.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFM-jlc21.pdf}
}
@article{DLM-jlc21,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Demri, St{\'e}phane and {\'E}tienne Lozes and Mansutti, Alessio},
title = {The Effects of Adding Reachability Predicates in Quantifier-Free Separation Logic},
year = 2021,
note = {To appear},
url = {http://arxiv.org/abs/1810.05410},
pdf = {http://arxiv.org/abs/1810.05410}
}
@techreport{DLM-arxiv20,
author = {St{\'e}phane Demri and {\'E}tienne Lozes and Alessio Mansutti},
institution = {Computing Research Repository},
month = feb,
note = {63~pages},
number = {2006.05156v2},
type = {Research Report},
title = {A {C}omplete {A}xiomatisation for {Q}uantifier-{F}ree {S}eparation {L}ogic},
year = {2021},
url = {https://arxiv.org/abs/2006.05156},
pdf = {https://arxiv.org/pdf/2006.05156v2.pdf}
}
@inproceedings{ADL-aaai20,
month = feb,
publisher = {AAAI Press},
editor = {Rossi, Francesca and Conitzer, Vincent and Sha, Fei},
acronym = {{AAAI}'20},
booktitle = {{P}roceedings of the 34th {AAAI} {C}onference on {A}rtificial
{I}ntelligence ({AAAI}'20)},
author = {Alechina, Natasha and Demri, St{\'e}phane and Logan, Brian},
title = {Parameterised Resource-Bounded ATL},
pages = {7040--7046},
year = {2020},
doi = {https://doi.org/10.1609/aaai.v34i05.6189},
url = {https://aaai.org/ojs/index.php/AAAI/article/view/6189}
}
@inproceedings{BDFM-lics20,
address = {Saarbrucken, Germany},
month = jul,
publisher = {{IEEE} Press},
editor = {Kobayashi, Naoki},
acronym = {{LICS}'19},
booktitle = {{P}roceedings of the 35th {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'20)},
author = {Bednarczyk, Bartosz and Demri, St{\'e}phane and Fervari, Ra{\'u}l and Mansutti, Alessio},
title = {Modal Logics with Composition on Finite Forests: Expressivity and Complexity},
pages = {167--180},
year = 2020,
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDFM-lics2020.pdf},
doi = {https://dl.acm.org/doi/10.1145/3373718.3394787}
}
@inproceedings{BDM-ijcai20,
month = jul,
publisher = {IJCAI organization},
editor = {Bessi{\`e}re, Christian},
acronym = {{IJCAI}'20},
booktitle = {{P}roceedings of the 29th {I}nternational {J}oint
{C}onference on {A}rtificial {I}ntelligence
({IJCAI}'20)},
author = {Bednarczyk, Bartosz and Demri, St{\'e}phane and Mansutti, Alessio},
title = {A Framework for Reasoning about Dynamic Axioms in Description Logics},
optpages = {},
year = 2020,
optpdf = {},
url = {https://www.ijcai.org/Proceedings/2020/233},
optdoi = {}
}
@inproceedings{BD-ecai20,
address = {Santiago de Compostela, Spain},
month = sep,
optvolume = {??},
optseries = {Frontiers in Artificial Intelligence and Applications},
publisher = {{IOS} Press},
editor = {Lang, J{\'e}r{\^o}me and De Giacomo, Giuseppe and Barro and Sen{\'e}n Barro and O'Sullivan, Barry},
acronym = {{ECAI}'20},
booktitle = {{P}roceedings of the 24th {E}uropean {C}onference on
{A}rtificial {I}ntelligence ({ECAI}'20)},
author = {Belardinelli, Francesco and Demri, St{\'e}phane},
title = {Reasoning with a Bounded Number of Resources in ATL+},
pages = {624-631},
year = 2020,
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BD-ecai2020.pdf},
url = {http://ebooks.iospress.nl/publication/54942},
doi = {10.3233/FAIA200147}
}
This file was generated by bibtex2html 1.98.