@techreport{jorrand85,
author = {Jorrand, {\relax Ph}ilippe and
Hufflen, Jean-Michel and Marty, Annick
and Marty, Jean-{\relax Ch}arles and
Schnoebelen, {\relax Ph}ilippe},
title = {{FP2}: {T}he Language and its Formal Definition},
type = {Research Report},
number = {537},
year = {1985},
month = may,
institution = {Laboratoire d'Informatique Fondamentale et
d'Intelligence Artificielle, Grenoble, France},
lsvhowpublished = {Esprit Project 415, Deliverable D1}
}
@techreport{schnoebelen85,
author = {Schnoebelen, {\relax Ph}ilippe},
title = {The Semantics of Concurrency in {FP2}},
type = {Research Report},
number = {558},
year = {1985},
month = oct,
institution = {Laboratoire d'Informatique Fondamentale et
d'Intelligence Artificielle, Grenoble, France}
}
@mastersthesis{schnoebelen85b,
author = {Schnoebelen, {\relax Ph}ilippe},
title = {S{\'e}mantique du parall{\'e}lisme en {FP2}},
year = {1985},
month = jun,
type = {Rapport de {DEA}},
school = {Universit{\'e} de Grenoble, France}
}
@techreport{microfp2,
author = {Schnoebelen, {\relax Ph}ilippe},
title = {{\(\mu\)-FP2}: {A} Prototype Interpreter for {FP2}},
type = {Research Report},
number = {573},
year = {1986},
month = jan,
institution = {Laboratoire d'Informatique Fondamentale et
d'Intelligence Artificielle, Grenoble, France}
}
@techreport{schnoebelen86,
author = {Schnoebelen, {\relax Ph}ilippe},
title = {About the Implementation of {FP2}},
type = {Research Report},
number = {574},
year = {1986},
month = jan,
institution = {Laboratoire d'Informatique Fondamentale et
d'Intelligence Artificielle, Grenoble, France}
}
@inproceedings{schaefer87,
address = {Eindhoven, The Netherlands},
month = jun,
year = 1987,
volume = 258,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {de Bakker, Jaco W. and Nijman, A. J. and
Treleaven, Philip C.},
acronym = {{PARLE}'87},
booktitle = {{P}roceedings of the 1st {I}nternational {C}onference
{P}arallel {A}rchitectures and {L}anguages {E}urope
({PARLE}'87),
{V}olume~{I}: {P}arallel {A}rchitectures},
author = {Sch{\"a}fer, Peter and
Schnoebelen, {\relax Ph}ilippe},
title = {Specification of a Pipelined Event-Driven Simulator
Using~{FP2}},
pages = {311-328},
doi = {10.1007/3-540-17943-7_136}
}
@inproceedings{schnoebelen87,
address = {Eindhoven, The Netherlands},
month = jun,
year = 1987,
volume = 259,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {de Bakker, Jaco W. and Nijman, A. J. and
Treleaven, Philip C.},
acronym = {{PARLE}'87},
booktitle = {{P}roceedings of the 1st {I}nternational {C}onference
{P}arallel {A}rchitectures and {L}anguages {E}urope
({PARLE}'87),
{V}olume~{II}: {P}arallel {L}anguages},
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Rewriting Techniques for the Temporal Analysis of
Communicating Processes},
pages = {402-419},
doi = {10.1007/3-540-17945-3_23}
}
@article{schnoebelen87b,
publisher = {Elsevier Science Publishers},
journal = {Science of Computer Programming},
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Refined Compilation of Pattern-Matching for Functional
Languages},
volume = {11},
number = {2},
pages = {133-159},
year = {1988},
month = dec,
doi = {10.1016/0167-6423(88)90002-0}
}
@inproceedings{schnoebelen88,
address = {Gaussig, German Democratic Republic},
month = nov,
year = 1988,
volume = 343,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Grabowski, Jan and Lescanne, Pierre and
Wechler, Wolfgang},
acronym = {{ALP}'88},
booktitle = {{P}roceedings of the 1st {I}nternational
{W}orkshop on {A}lgebraic and {L}ogic {P}rogramming
({ALP}'88)},
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Refined Compilation of Pattern-Matching for Functional
Languages},
pages = {233-243},
doi = {10.1007/3-540-50667-5_75}
}
@techreport{tica-report,
author = {Schnoebelen, {\relax Ph}ilippe and Lugiez, Denis
and Comon, Hubert},
title = {A Semantics for Polymorphic Subtypes in Computer
Algebra},
type = {Research Report},
number = {711},
year = {1988},
month = mar,
institution = {Laboratoire d'Informatique Fondamentale et
d'Intelligence Artificielle, Grenoble, France}
}
@misc{jorrand89,
author = {Jorrand, {\relax Ph}ilippe and
Hufflen, Jean-Michel and
Ib{\'a}{\~n}ez, Mar{\'\i}a Blanca and
Karasek, T. and Rog\'e, S. and
Schnoebelen, {\relax Ph}ilippe and V{\'e}ron, A.},
missingauthor = {},
title = {Parallel Specification of the Connection Method on an
{FP2} Machine},
year = {1989},
month = oct,
howpublished = {Esprit Project 415, Deliverable D17}
}
@incollection{schnoebelen89,
author = {Schnoebelen, {\relax Ph}ilippe and Jorrand, {\relax Ph}ilippe},
title = {Principles of {FP2}: {T}erm Algebras for Specification
of Parallel Machines},
editor = {de Bakker, Jaco W.},
booktitle = {Languages for Parallel Architectures: {D}esign,
Semantics, Implementation Models},
chapter = {5},
pages = {223-273},
year = {1989},
publisher = {John Wiley \& Sons, Ltd.},
month = dec
}
@techreport{belmesk90,
author = {Belmesk, Zoubir and Schnoebelen, {\relax Ph}ilippe},
title = {Une g{\'e}n{\'e}ralisation des pr{\'e}sentations {FP2}
bas{\'e}e sur la th{\'e}orie des r{\'e}seaux},
type = {Research Report},
number = {832-I},
year = {1990},
month = nov,
institution = {Laboratoire d'Informatique Fondamentale et
d'Intelligence Artificielle, Grenoble, France}
}
@inproceedings{belmesk90b,
address = {Paris, France},
month = jun,
year = 1990,
editor = {Finkel, Alain},
acronym = {{APN}'90},
booktitle = {{P}roceedings of the 11th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({APN}'90)},
author = {Autant, Cyril and Belmesk, Zoubir and
Schnoebelen, {\relax Ph}ilippe},
title = {A Net-Theoretic Approach to the Efficient
Implementation of the {FP2} Parallel Language},
pages = {451-470}
}
@inproceedings{schnoebelen89b,
address = {Copenhagen, Denmark},
month = may,
year = 1990,
volume = 432,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Jones, Neil D.},
acronym = {{ESOP}'90},
booktitle = {{P}roceedings of the 3rd
{E}uropean {S}ymposium on {P}rogramming
({ESOP}'90)},
author = {Schnoebelen, {\relax Ph}ilippe and Pinchinat, Sophie},
title = {On the Weak Adequacy of Branching-Time Temporal
Logic},
pages = {377-388},
doi = {10.1007/3-540-52592-0_75}
}
@techreport{schnoebelen89c,
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Congruence Properties of the Process Equivalence
Induced by Temporal Logic},
type = {Research Report},
number = {831-I},
year = {1990},
month = oct,
institution = {Laboratoire d'Informatique Fondamentale et
d'Intelligence Artificielle, Grenoble, France}
}
@phdthesis{schnoebelen90,
author = {Schnoebelen, {\relax Ph}ilippe},
title = {S{\'e}mantique du parall{\'e}lisme et logique
temporelle. {A}pplication au langage {FP2}},
year = {1990},
month = jun,
type = {Th{\`e}se de doctorat},
school = {Institut National Polytechnique de Grenoble, France}
}
@inproceedings{autant90b,
address = {Eindhoven, The Netherlands},
month = jun,
year = 1991,
volume = 506,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Aarts, Emile H. L. and van Leeuwen, Jan and
Rem, Martin},
acronym = {{PARLE}'91},
booktitle = {{P}roceedings of the 3rd {I}nternational {C}onference
{P}arallel {A}rchitectures and {L}anguages {E}urope
({PARLE}'91),
{V}olume~{II}: {P}arallel {L}anguages},
author = {Autant, Cyril and Belmesk, Zoubir and
Schnoebelen, {\relax Ph}ilippe},
title = {Strong Bisimilarity on Nets Revisited},
pages = {295-312},
doi = {10.1007/3-540-54152-7_71}
}
@article{cherief90,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Cherief, Ferroudja and
Schnoebelen, {\relax Ph}ilippe},
title = {{\(\tau\)}-Bisimulations and Full Abstraction for
Refinement of Actions},
volume = {40},
number = {4},
pages = {219-222},
year = {1991},
month = nov,
doi = {10.1016/0020-0190(91)90081-R}
}
@article{comon91,
publisher = {Elsevier Science Publishers},
journal = {Journal of Symbolic Computation},
author = {Comon, Hubert and Lugiez, Denis and
Schnoebelen, {\relax Ph}ilippe},
title = {A Rewrite-Based Type Discipline for a Subset of
Computer Algebra},
volume = {11},
number = {4},
pages = {349-368},
year = {1991},
month = apr
}
@inproceedings{schnoebelen91,
address = {Amsterdam, The Netherlands},
month = aug,
year = 1991,
volume = 527,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Baeten, Jos C. M. and Groote, Jan Friso},
acronym = {{CONCUR}'91},
booktitle = {{P}roceedings of the 2nd
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'91)},
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Experiments on Processes with Backtracking},
pages = {480-494},
doi = {10.1007/3-540-54430-5_108}
}
@inproceedings{autant92,
address = {Sheffield, UK},
month = jun,
year = 1992,
volume = 616,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Jensen, Kurt},
acronym = {{APN}'92},
booktitle = {{P}roceedings of the 13th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({APN}'92)},
author = {Autant, Cyril and Schnoebelen, {\relax Ph}ilippe},
title = {Place Bisimulations in {P}etri Nets},
pages = {45-61},
doi = {10.1007/3-540-55676-1_3}
}
@inproceedings{laroussinie93,
address = {Twente, The Netherlands},
year = 1994,
series = {Workshops in Computing},
publisher = {Springer-Verlag},
editor = {Nivat, Maurice and Rattray, Charles and Rus, Teodor
and Scollo, Giuseppe},
acronym = {{AMAST}'93},
booktitle = {{P}roceedings of the 3rd {I}nternational
{C}onference on {A}lgebraic {M}ethodology and
{S}oftware {T}echnology
({AMAST}'93)},
author = {Laroussinie, Fran{\c{c}}ois and Pinchinat, Sophie
and Schnoebelen, {\relax Ph}ilippe},
title = {Translation Results for Modal Logics of Reactive
Systems},
pages = {299-310}
}
@inproceedings{autant94,
address = {Peterborough, Ontario, Canada},
month = may,
year = 1994,
missinghowpublished = {},
lsv-info = {Published as JCI 1(1), 1995 --> journals ??},
acronym = {{ICCI}'94},
booktitle = {{P}roceedings of the 6th {I}nternational
{C}onference on {C}omputing and {I}nformation
({ICCI}'94)},
author = {Autant, Cyril and Pfister, Wilfried and
Schnoebelen, {\relax Ph}ilippe},
title = {Place Bisimulations for the Reduction of Labeled
{P}etri Nets with Silent Moves},
pages = {230-246},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/APS-icci94.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/APS-icci94.ps}
}
@inproceedings{laroussinie94,
address = {Caen, France},
month = feb,
year = 1994,
volume = 775,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Enjalbert, Patrice and Mayr, Ernst W. and
Wagner, Klaus W.},
acronym = {{STACS}'94},
booktitle = {{P}roceedings of the 11th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'94)},
author = {Laroussinie, Fran{\c{c}}ois and
Schnoebelen, {\relax Ph}ilippe},
title = {A Hierarchy of Temporal Logics with Past},
pages = {47-58},
doi = {10.1007/3-540-57785-8_130}
}
@techreport{pinchinat94,
author = {Pinchinat, Sophie and Laroussinie, Fran{\c{c}}ois
and Schnoebelen, {\relax Ph}ilippe},
title = {Logical Characterizations of Truly Concurrent
Bisimulation},
type = {Technical Report},
number = {114},
year = {1994},
month = mar,
institution = {Laboratoire d'Informatique Fondamentale et
d'Intelligence Artificielle, Grenoble, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/PLS-rrimag114.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/PLS-rrimag114.ps}
}
@article{laroussinie94b,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Laroussinie, Fran{\c{c}}ois and Pinchinat, Sophie
and Schnoebelen, {\relax Ph}ilippe},
title = {Translations between Modal Logics of Reactive
Systems},
volume = {140},
number = {1},
pages = {53-71},
year = {1995},
month = mar,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LPS-TCS95.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LPS-TCS95.ps},
doi = {10.1016/0304-3975(94)00204-V}
}
@article{laroussinie94c,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Laroussinie, Fran{\c{c}}ois and
Schnoebelen, {\relax Ph}ilippe},
title = {A Hierarchy of Temporal Logics with Past},
volume = {148},
number = {2},
pages = {303-324},
year = {1995},
month = sep,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LarSch-TCS95.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LarSch-TCS95.ps},
doi = {10.1016/0304-3975(95)00035-U}
}
@inproceedings{schnoebelen95,
address = {Yaroslavl, Russia},
month = nov,
year = 1995,
publisher = {Yaroslavl University Press},
booktitle = {{P}roceedings of the {C}onference
{P}robl{\`e}mes {A}ctuels des {S}ciences
{N}aturelles et {H}umaines},
author = {Schnoebelen, {\relax Ph}ilippe and
Laroussinie, Fran{\c{c}}ois},
title = {Temporal Logic with Past for the Specification and
Verification of Reactive Systems},
pages = {143-146},
note = {Invited talk}
}
@inproceedings{kouchnarenko96,
address = {Bordeaux, France},
month = may,
year = 1996,
acronym = {{RENPAR}'96},
booktitle = {{A}ctes des 8{\`e}mes {R}encontres
{F}rancophones du {P}arall{\'e}lisme
({RENPAR}'96)},
author = {Kouchnarenko, Olga and Schnoebelen, {\relax Ph}ilippe},
title = {Mod{\`e}les formels pour les programmes
r{\'e}cursifs-parall{\`e}les},
pages = {85-88},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/KouSch-renpar96.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/KouSch-renpar96.ps}
}
@inproceedings{laroussinie96fac,
address = {Toulouse, France},
month = feb,
year = 1996,
acronym = {{FAC}'96},
booktitle = {{A}ctes des 5{\`e}mes {J}ourn{\'e}es sur la
{F}ormalisation des {A}ctivit{\'e}s {C}oncurrentes
({FAC}'96)},
author = {Laroussinie, Fran{\c{c}}ois and Schnoebelen, {\relax Ph}ilippe},
title = {Translations for Model-Checking Temporal Logic with
Past},
pages = {17-19},
note = {Invited talk}
}
@inproceedings{kouchnarenko97,
address = {Yaroslavl, Russia},
month = sep,
year = 1997,
volume = 1277,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Malyshkin, Victor E.},
acronym = {{PaCT}'97},
booktitle = {{P}roceedings of the 4th {I}nternational
{C}onference on {P}arallel {C}omputing
{T}echnologies
({PaCT}'97)},
author = {Kouchnarenko, Olga and Schnoebelen, {\relax Ph}ilippe},
title = {A Formal Framework for the Analysis of
Recursive-Parallel Programs},
pages = {45-59},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KusSch-pact97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/KusSch-pact97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KusSch-pact97.pdf},
doi = {10.1007/3-540-63371-5_6}
}
@inproceedings{kouchnarenko97b,
address = {Pisa, Italy},
year = 1997,
volume = 5,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Steffen, B. and Caucal, Didier},
acronym = {{INFINITY}'96},
booktitle = {{P}roceedings of the 1st {I}nternational
{W}orkshop on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'96)},
author = {Kouchnarenko, Olga and Schnoebelen, {\relax Ph}ilippe},
title = {A Model for Recursive-Parallel Programs},
pages = {30},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KouSch-infin96.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/KouSch-infin96.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KouSch-infin96.pdf},
doi = {10.1016/S1571-0661(05)82512-5}
}
@inproceedings{laroussinie97,
address = {Santa Margherita Ligure, Italy},
month = sep,
year = 1997,
volume = 7,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Palamidessi, Catuscia and Parrow, Joachim},
acronym = {{EXPRESS}'97},
booktitle = {{P}roceedings of the 4th {I}nternational
{W}orkshop on {E}xpressiveness in
{C}oncurrency
({EXPRESS}'97)},
author = {Laroussinie, Fran{\c{c}}ois and
Schnoebelen, {\relax Ph}ilippe},
title = {Specification in {CTL}+{P}ast, Verification in {CTL}},
pages = {161-184},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LarSch-express97.pdf},
ps = {LarSch-express97.ps},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LarSch-express97.pdf},
doi = {10.1016/S1571-0661(05)80472-4}
}
@techreport{DD1-98,
author = {Laroussinie, Fran{\c{c}}ois and Petit, Antoine and
Schnoebelen, {\relax Ph}ilippe},
title = {Le model-checking, une technique de
v{\'e}rification en
plein essor. {I}~--- {P}rincipes et techniques},
year = {1998},
month = oct,
type = {Contract Report},
institution = {EDF/DER/MOS - LSV},
lsv-lang = {FR}
}
@techreport{DD2-98,
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Le model-checking, une technique de
v{\'e}rification en
plein essor. {III}~--- {S}p{\'e}cifier pour
v{\'e}rifier},
year = {1998},
month = oct,
type = {Contract Report},
institution = {EDF/DER/MOS - LSV},
lsv-lang = {FR}
}
@techreport{DD3-98,
author = {B{\'e}rard, B{\'e}atrice and
C{\'e}c{\'e}, G{\'e}rard and
Dufourd, Catherine and Finkel, Alain and
Laroussinie, Fran{\c{c}}ois and Petit, Antoine and
Schnoebelen, {\relax Ph}ilippe and
Sutre, Gr{\'e}goire},
title = {Le model-checking, une technique de
v{\'e}rification en
plein essor. {II}~--- {Q}uelques outils},
year = {1998},
month = oct,
type = {Contract Report},
institution = {EDF/DER/MOS - LSV},
lsv-lang = {FR}
}
@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}
}
@inproceedings{dufourd98,
address = {Aalborg, Denmark},
month = jul,
year = 1998,
volume = 1443,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Larsen, Kim G. and Skyum, Sven and Winskel, Glynn},
acronym = {{ICALP}'98},
booktitle = {{P}roceedings of the 25th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming
({ICALP}'98)},
author = {Dufourd, Catherine and Finkel, Alain and
Schnoebelen, {\relax Ph}ilippe},
title = {Reset Nets between Decidability and
Undecidability},
pages = {103-115},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DFS-icalp98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DFS-icalp98.ps},
doi = {10.1007/BFb0055044},
abstract = {We study Petri nets with Reset arcs (also Transfer and
Doubling arcs) in combination with other extensions of
the basic Petri net model. While Reachability is
undecidable in all these extensions (indeed they are
Turing-powerful), we exhibit unexpected frontiers for
the decidability of Termination, Coverability,
Boundedness and place-Boundedness. In particular, we
show counter-intuitive separations between seemingly
related problems. Our main theorem is the very
surprising fact that boundedness is undecidable for
Petri nets with Reset arcs.}
}
@inproceedings{finkel98,
address = {Campinas, Brasil},
month = apr,
year = 1998,
volume = 1380,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Lucchesi, Claudio L. and Moura, Arnaldo V.},
acronym = {{LATIN}'98},
booktitle = {{P}roceedings of the 3rd {L}atin {A}merican
{S}ymposium on {T}heoretical {I}nformatics
({LATIN}'98)},
author = {Finkel, Alain and Schnoebelen, {\relax Ph}ilippe},
title = {Fundamental Structures in Well-Structured Infinite
Transition Systems},
pages = {102-118},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FinSch-latin98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FinSch-latin98.ps},
doi = {10.1007/BFb0054314}
}
@inproceedings{lugiez98,
address = {Nice, France},
month = sep,
year = 1998,
volume = 1466,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Sangiorgi, Davide and de Simone, Robert},
acronym = {{CONCUR}'98},
booktitle = {{P}roceedings of the 9th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'98)},
author = {Lugiez, Denis and Schnoebelen, {\relax Ph}ilippe},
title = {The Regular Viewpoint on {PA}-Processes},
pages = {50-66},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LugSch-concur98.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LugSch-concur98.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LugSch-concur98.ps},
doi = {10.1007/BFb0055615}
}
@misc{phs-infinity98,
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Regular Tree Languages for Process Algebra},
year = 1998,
month = jul,
howpublished = {Invited lecture, 3rd {I}nternational
{W}orkshop on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'98), Aalborg, Denmark}
}
@book{docdor99,
author = {Schnoebelen, {\relax Ph}ilippe and
B{\'e}rard, B{\'e}atrice and Bidoit, Michel
and Laroussinie, Fran{\c{c}}ois and Petit, Antoine},
title = {V{\'e}rification de logiciels : techniques et
outils du model-checking},
year = {1999},
month = apr,
publisher = {Vuibert},
isbn = {2-7117-8646-3},
url = {http://www.vuibert.com/livre593.html},
lsv-lang = {FR}
}
@inproceedings{dufourd99,
address = {Prague, Czech Republic},
month = jul,
year = 1999,
volume = 1644,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Wiedermann, Jir{\'i} and van Emde Boas, Peter and
Nielsen, Mogens},
acronym = {{ICALP}'99},
booktitle = {{P}roceedings of the 26th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming
({ICALP}'99)},
author = {Dufourd, Catherine and Jan{\v c}ar, Petr and
Schnoebelen, {\relax Ph}ilippe},
title = {Boundedness of Reset {P/T} Nets},
pages = {301-310},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DJS-icalp99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DJS-icalp99.ps},
abstract = {P/T nets with reset and transfer arcs can be seen as
counter-machines with some restricted set of
operations. Surprisingly, several problems related to
boundedness are harder for Reset nets than for the more
expressive Transfer nets. Our main result is that
boundedness is undecidable for nets with three reset
arcs, while it is decidable for nets with two resetable
places.}
}
@article{schnoebelen99,
publisher = {European Association for
Theoretical Computer Science},
journal = {EATCS Bulletin},
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Decomposable Regular Languages and the Shuffle
Operator},
volume = {67},
pages = {283-289},
year = {1999},
month = feb,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Sch-BEATCS99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Sch-BEATCS99.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-BEATCS99.pdf}
}
@inproceedings{SchSid-atpn2000,
address = {\AA rhus, Denmark},
month = jun,
year = 2000,
volume = 1825,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Nielsen, Mogens and Simpson, Dan},
acronym = {{ICATPN} 2000},
booktitle = {{P}roceedings of the 21st
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({ICATPN} 2000)},
author = {Schnoebelen, {\relax Ph}ilippe and
Sidorova, Natalia},
title = {Bisimulation and the Reduction of {P}etri Nets},
pages = {409-423},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/SchSid-atpn2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/SchSid-atpn2000.ps}
}
@inproceedings{VULC-icp2000,
address = {Utrecht, The Netherlands},
month = oct,
year = {2000},
optaddress = {Zaltbommel, The Netherlands},
publisher = {PLCopen},
acronym = {{ICP} 2000},
booktitle = {{P}roceedings of the 4th {I}nternational
{PLC}open {C}onference on {I}ndustrial
{C}ontrol {P}rogramming
({ICP} 2000)},
author = {De{~}Smet, Olivier and Couffin, Sandrine and
Rossi, Olivier and
Canet, G{\'e}raud
and Lesage, Jean-Jacques and
Schnoebelen, {\relax Ph}ilippe and Papini, H{\'e}l{\`e}ne},
title = {Safe Programming of {PLC} Using Formal Verification
Methods},
pages = {73-78},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/VULC-icp2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/VULC-icp2000.ps}
}
@inproceedings{bls-fossacs2000,
address = {Berlin, Germany},
month = mar,
year = 2000,
volume = 1784,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Tiuryn, Jerzy},
acronym = {{FoSSaCS} 2000},
booktitle = {{P}roceedings of the 3rd {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS} 2000)},
author = {B{\'e}rard, B{\'e}atrice and Labroue, Anne and
Schnoebelen, {\relax Ph}ilippe},
title = {Verifying Performance Equivalence for {T}imed
{B}asic {P}arallel {P}rocesses},
pages = {35-47},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BLS-fossacs2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BLS-fossacs2000.ps}
}
@inproceedings{cclps-smc2000,
address = {Nashville, Tennessee, USA},
month = oct,
year = 2000,
publisher = {Argos Press},
acronym = {{SMC} 2000},
booktitle = {{P}roceedings of the {IEEE} {I}nternational
{C}onference on {S}ystems, {M}an and {C}ybernetics
({SMC} 2000)},
author = {Canet, G{\'e}raud and Couffin, Sandrine and
Lesage, Jean-Jacques and Petit, Antoine
and Schnoebelen, {\relax Ph}ilippe},
title = {Towards the Automatic Verification of {PLC}
Programs
Written in {I}nstruction {L}ist},
pages = {2449-2454},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CCLPS-smc2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CCLPS-smc2000.ps},
doi = {10.1109/ICSMC.2000.884359},
abstract = {We propose a framework for the automatic verification of PLC
(programmable logic controller) programs written in Instruction List, one of
the five languages defined in the IEC 61131-3 standard. We~propose a formal
semantics for a significant fragment of the IL language, and a direct coding
of this semantics into a model checking tool. We then automatically verify
rich behavioral properties written in linear temporal logic. Our~approach is
illustrated on the example of the tool-holder of a turning center}
}
@inproceedings{cdprs-cifa2000,
address = {Lille, France},
month = jul,
year = 2000,
optaddress = {Villeneuve d'Ascq, France},
publisher = {Union des Chercheurs Ing{\'e}nieurs et {S}cientifiques, Villeneuve d'Ascq, France},
editor = {Borne, Pierre and Richard, Jean-Pierre and
Vanheeghe, {\relax Ph}ilippe},
acronym = {{CIFA} 2000},
booktitle = {{A}ctes de la 1{\`e}re {C}onf{\'e}rence
{I}nternationale {F}rancophone
d'{A}utomatique
({CIFA} 2000)},
author = {Canet, G{\'e}raud and Denis, Bruno and
Petit, Antoine and Rossi, Olivier and
Schnoebelen, {\relax Ph}ilippe},
title = {Un cadre pour la v{\'e}rification automatique de
programmes~{IL}},
pages = {693-698},
noisbn = {2-9512309-1-5},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CDPRS-cifa2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CDPRS-cifa2000.ps},
lsv-lang = {FR}
}
@article{laroussinie98,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Laroussinie, Fran{\c{c}}ois and
Schnoebelen, {\relax Ph}ilippe},
title = {Specification in {CTL}+Past for verification in
{CTL}},
volume = {156},
number = {1-2},
pages = {236-263},
year = {2000},
month = jan,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LarSch-IC98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LarSch-IC98.ps},
doi = {10.1006/inco.1999.2817}
}
@inproceedings{larsch-fossacs2000,
address = {Berlin, Germany},
month = mar,
year = 2000,
volume = 1784,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Tiuryn, Jerzy},
acronym = {{FoSSaCS} 2000},
booktitle = {{P}roceedings of the 3rd {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS} 2000)},
author = {Laroussinie, Fran{\c{c}}ois and
Schnoebelen, {\relax Ph}ilippe},
title = {The State-Explosion Problem from Trace to
Bisimulation Equivalence},
pages = {192-207},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LarSch-fossacs2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LarSch-fossacs2000.ps}
}
@inproceedings{lomazova99,
address = {Novosibirsk, Russia},
year = 2000,
volume = 1755,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Bj{\o}rner, Dines and Broy, Manfred and
Zamulin, Alexandre V.},
acronym = {{PSI}'99},
booktitle = {{P}roceedings of the 3rd {I}nternational
{A}ndrei {E}rshov {M}emorial {C}onference
on {P}erspectives of {S}ystem {I}nformatics
({PSI}'99)},
author = {Lomazova, Irina A. and
Schnoebelen, {\relax Ph}ilippe},
title = {Some Decidability Results for Nested {P}etri Nets},
pages = {208-220},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LomSch-psi99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LomSch-psi99.ps}
}
@inproceedings{lst-quant,
address = {Punta del Este, Uruguay},
month = apr,
year = 2000,
volume = 1776,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gonnet, Gaston H. and Panario, Daniel and
Viola, Alfredo},
acronym = {{LATIN} 2000},
booktitle = {{P}roceedings of the 4th {L}atin {A}merican
{S}ymposium on {T}heoretical {I}nformatics
({LATIN} 2000)},
author = {Laroussinie, Fran{\c{c}}ois and
Schnoebelen, {\relax Ph}ilippe and
Turuani, Mathieu},
title = {On the Expressivity and Complexity of Quantitative
Branching-Time Temporal Logics},
pages = {437-446},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LST-latin2000.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LST-latin2000.ps},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LST-latin2000.pdf},
doi = {10.1007/10719839_43}
}
@inproceedings{lugsch-icalp2000,
address = {Geneva, Switzerland},
month = jul,
year = 2000,
volume = 1853,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Montanari, Ugo and Rolim, Jos{\'e} D. P. and
Welzl, Emo},
acronym = {{ICALP} 2000},
booktitle = {{P}roceedings of the 27th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming
({ICALP} 2000)},
author = {Lugiez, Denis and Schnoebelen, {\relax Ph}ilippe},
title = {Decidable First-Order Transition Logics for
{PA}-Processes},
pages = {342-353},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LugSch-icalp2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LugSch-icalp2000.ps}
}
@inproceedings{rossch-adpm2000,
address = {Dortmund, Germany},
month = sep,
year = 2000,
optaddress = {Aachen, Germany},
publisher = {Shaker Verlag},
editor = {Engell, Sebastian and Kowalewski, Stefan and
Zaytoon, Janan},
acronym = {{ADPM} 2000},
booktitle = {{P}roceedings of the 4th {I}nternational
{C}onference on {A}utomation of {M}ixed
{P}rocesses: {H}ybrid {D}ynamic {S}ystems
({ADPM} 2000)},
author = {Rossi, Olivier and Schnoebelen, {\relax Ph}ilippe},
title = {Formal modeling of timed function blocks for the
automatic verification of {L}adder {D}iagram
programs},
pages = {177-182},
noisbn = {3-8265-7836-8},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/RosSch-adpm2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/RosSch-adpm2000.ps}
}
@misc{phs-jm2000,
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Le probl{\`e}me de l'explosion du nombre
d'{\'e}tats},
year = {2000},
month = mar,
howpublished = {Invited talk, 8{\`e}me Journ\'ees Montoises
d'Informatique Th\'eorique (JM 2000),
Marne-la-Vall\'ee, France},
lsv-lang = {FR}
}
@inproceedings{Sch-tacs2001,
address = {Sendai, Japan},
month = oct,
year = 2001,
volume = 2215,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Kobayashi, Naoki and Pierce, Benjamin C.},
acronym = {{TACS}'01},
booktitle = {{P}roceedings of the 4th {I}nternational
{W}orkshop on {T}heoretical {A}spects of
{C}omputer {S}oftware
({TACS}'01)},
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Bisimulation and Other Undecidable Equivalences for
Lossy Channel Systems},
pages = {385-399},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-tacs2001.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-tacs2001.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Sch-tacs2001.ps},
abstract = {Lossy channel systems are systems of
finite state automata that communicate via unreliable
unbounded fifo channels. Today the main open question
in the theory of lossy channel systems is whether
bisimulation is decidable. \par
We show that bisimulation, simulation, and in fact
all relations between bisimulation and trace
inclusion are undecidable for lossy channel systems
(and for lossy vector addition systems).}
}
@article{finkel98b,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Finkel, Alain and Schnoebelen, {\relax Ph}ilippe},
title = {Well-Structured Transition Systems Everywhere!},
volume = {256},
number = {1-2},
pages = {63-92},
year = {2001},
month = apr,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FinSch-TCS99.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FinSch-TCS99.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FinSch-TCS99.ps},
doi = {10.1016/S0304-3975(00)00102-X},
abstract = {Well-structured transition systems
(WSTS's) are a general class of infinite state
systems for which decidability results rely on the
existence of a well-quasi-ordering between states
that is compatible with the transitions.\par
In this article, we provide an extensive treatment
of the WSTS idea and show several new results.
Our improved definitions allow many examples of
classical systems to be seen as instances of
WSTS's.}
}
@inproceedings{lms-fossacs2001,
address = {Genova, Italy},
month = apr,
year = 2001,
volume = 2030,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Honsell, Furio and Miculan, Marino},
acronym = {{FoSSaCS}'01},
booktitle = {{P}roceedings of the 4th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'01)},
author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and
Schnoebelen, {\relax Ph}ilippe},
title = {Model checking {CTL}{\(^+\)} and {FCTL} is~hard},
pages = {318-331},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMS-fossacs2001.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LMS-fossacs2001.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMS-fossacs2001.pdf},
abstract = {Among the branching-time temporal logics used for the
specification and verification of systems, CTL\(^+\), FCTL and ECTL\(^+\)
are the
most notable logics for which the precise computational complexity of
model checking is not known. We answer this longstanding open
problem and show that model checking these (and some related) logics is
\(\Delta_2^p\)-complete.}
}
@book{lsvmcbook01,
author = {B{\'e}rard, B{\'e}atrice and Bidoit, Michel and Finkel, Alain
and Laroussinie, Fran{\c{c}}ois and
Petit, Antoine and Petrucci, Laure and
Schnoebelen, {\relax Ph}ilippe},
title = {Systems and Software Verification. {M}odel-Checking
Techniques and Tools},
year = {2001},
missingmonth = {},
missingnmonth = {},
publisher = {Springer},
isbn = {3-540-41523-8},
url = {http://www.springer.com/978-3-540-41523-8},
olderurl = {http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-41523-8}
}
@phdthesis{phs-hab-01,
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Sp{\'e}cification et v{\'e}rification des syst{\`e}mes
concurrents},
year = {2001},
month = oct,
type = {M{\'e}moire d'habilitation},
school = {Universit{\'e} Paris~7, Paris, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/phs-habile.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/phs-habile.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{HS-amast2002,
address = {Saint Gilles les Bains, Reunion Island, France},
month = sep,
year = 2002,
volume = 2422,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Kirchner, H{\'e}l{\`e}ne and
Ringeissen, {\relax Ch}ristophe},
acronym = {{AMAST}'02},
booktitle = {{P}roceedings of the 9th {I}nternational
{C}onference on {A}lgebraic {M}ethodology and
{S}oftware {T}echnology
({AMAST}'02)},
author = {Hornus, Samuel and Schnoebelen, {\relax Ph}ilippe},
title = {On Solving Temporal Logic Queries},
pages = {163-177},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HS-amast2002.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HS-amast2002.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HS-amast2002.ps},
abstract = {Temporal query checking is an extension of temporal model
checking where one asks what propositional formulae can be inserted in a
temporal query (a temporal formula with a placeholder) so that the
resulting formula is satisfied in the model at hand.\par
We study the problem of computing all minimal solutions to a temporal
query without restricting to so-called {"}valid{"} queries (queries
guaranteed to have a unique minimal solution). While this problem is
intractable in general, we show that deciding uniqueness of the minimal
solution (and computing it) can be done in polynomial-time. }
}
@inproceedings{LMS-fossacs2002,
address = {Grenoble, France},
month = apr,
year = 2002,
volume = 2303,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Nielsen, Mogens and Engberg, Uffe},
acronym = {{FoSSaCS}'02},
booktitle = {{P}roceedings of the 5th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'02)},
author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and
Schnoebelen, {\relax Ph}ilippe},
title = {On Model Checking Durational {K}ripke Structures
(Extended Abstract)},
pages = {264-279},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMS-fossacs2002.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LMS-fossacs2002.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMS-fossacs2002.pdf},
abstract = {We consider quantitative model checking in \emph{durational
Kripke structures} (Kripke structures where transitions have integer
durations) with timed temporal logics where subscripts put quantitative
constraints on the time it takes before a property is satisfied.
We investigate the conditions that allow polynomial-time model
checking algorithms for timed versions of CTL and exhibit an
important gap
between logics where subscripts of the form {"}\(= c\){"} (exact duration) are
allowed, and simpler logics that only allow subscripts of the form {"}\(\leq c\){"}
or {"}\(\geq c\){"} (bounded duration).\par
A surprising outcome of this study is that it provides the second example
of a \(\Delta_2^P\)-complete model checking problem.}
}
@inproceedings{LMS-lics2002,
address = {Copenhagen, Denmark},
month = jul,
year = 2002,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'02},
booktitle = {{P}roceedings of the 17th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'02)},
author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and
Schnoebelen, {\relax Ph}ilippe},
title = {Temporal Logic with Forgettable Past},
pages = {383-392},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMS-lics2002.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LMS-lics2002.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMS-lics2002.pdf},
doi = {10.1109/LICS.2002.1029846},
abstract = {We investigate NLTL, a linear-time temporal logic with
forgettable past. NLTL can be exponentially more succinct
than LTL + Past (which in turn can be more succinct
than LTL). We study satisfiability and model checking for
NLTL and provide optimal automata-theoretic algorithms
for these EXPSPACE-complete problems.}
}
@article{LabSch-NJC2002,
journal = {Nordic Journal of Computing},
author = {Labroue, Anne and Schnoebelen, {\relax Ph}ilippe},
title = {An Automata-Theoretic Approach to the Reachability
Analysis of {RPPS} Systems},
volume = {9},
number = {2},
pages = {118-144},
year = {2002},
month = jul,
missingmonth = {dans DBLP, c'est summer},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LS-NJC.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LS-NJC.ps},
abstract = {We show how the reachability
analysis of RPPS systems can be tackled with the
tree-automata techniques proposed by Lugiez and
Schnoebelen for PA. This approach requires that
we express the states of RPPS systems in RPA, a
tailor-made process rewrite system where
reachability is a relation recognizable by
finite tree-automata. Two outcomes of this study
are (1)~an NP algorithm for reachability in RPPS
systems, and (2)~a simple decision procedure for
a large class of reachability problems in RPA
systems.}
}
@inproceedings{LabSch-express2001,
address = {Aalborg, Denmark},
month = feb,
year = 2002,
number = 1,
volume = 52,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Aceto, Luca and Panangaden, Prakash},
acronym = {{EXPRESS}'01},
booktitle = {{P}roceedings of the 8th {I}nternational
{W}orkshop on {E}xpressiveness in
{C}oncurrency
({EXPRESS}'01)},
author = {Labroue, Anne and Schnoebelen, {\relax Ph}ilippe},
title = {An Automata-Theoretic Approach to the Reachability
Analysis of {RPPS} Systems},
pages = {1-20},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LabSch-express2001.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LabSch-express2001.ps},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LabSch-express2001.pdf},
doi = {10.1016/S1571-0661(04)00213-0}
}
@article{LugSch-tcs,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Lugiez, Denis and Schnoebelen, {\relax Ph}ilippe},
title = {The Regular Viewpoint on {PA}-Processes},
volume = {274},
number = {1-2},
pages = {89-115},
year = {2002},
month = mar,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LugSch-TCS99.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LugSch-TCS99.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LugSch-TCS99.pdf},
doi = {10.1016/S0304-3975(00)00306-6},
abstract = {PA is the process algebra allowing
non-determinism, sequential and parallel
compositions, and recursion. We suggest viewing
PA-processes as trees, and using tree-automata
techniques for verification problems on PA.\par
Our main result is that the set of iterated
predecessors of a regular set of PA-processes is a
regular tree language, and similarly for iterated
successors. Furthermore, the corresponding
tree-automata can be built effectively in
polynomial-time. This has many immediate
applications to verification problems for
PA-processes, among which a simple and general
model-checking algorithm.}
}
@inproceedings{MS-mfcs2002,
address = {Warsaw, Poland},
month = aug,
year = 2002,
volume = 2420,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Diks, Krzysztof and Rytter, Wojciech},
acronym = {{MFCS}'02},
booktitle = {{P}roceedings of the 27th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'02)},
author = {Masson, Beno{\^\i}t and Schnoebelen, {\relax Ph}ilippe},
title = {On Verifying Fair Lossy Channel Systems},
pages = {543-555},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MS-mfcs2002-long.pdf},
abstract = {Lossy channel systems are systems
of finite state automata that communicate via
unreliable unbounded fifo channels. They are an
important computational model because of the
role they play in the algorithmic verification
of communication protocols.\par
In this paper, we show that fair termination is
decidable for a large class of these systems.}
}
@techreport{VPQ:AS22:final,
author = {Halbwachs, Nicolas and Schnoebelen, {\relax Ph}ilippe},
title = {{V}{\'e}rification de propri{\'e}t{\'e}s quantitatives},
year = {2002},
month = dec,
type = {Final Report},
institution = {Action Sp\'ecifique~22 du D\'epartement
STIC du CNRS},
oldhowpublished = {Rapport final de l'Action Sp\'ecifique 22 du D\'ept.\
STIC du CNRS}
}
@article{phs-IPL2002,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Verifying Lossy Channel Systems has Nonprimitive
Recursive Complexity},
volume = {83},
number = {5},
pages = {251-261},
year = {2002},
month = sep,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-IPL2002.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Sch-IPL2002.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-IPL2002.pdf},
doi = {10.1016/S0020-0190(01)00337-4},
abstract = {Lossy channel systems are systems of
finite state automata that communicate via unreliable
unbounded fifo channels. It is known that
reachability, termination and a few other verification
problems are decidable for these systems. In this
article we show that these problems cannot be solved
in primitive recursive time.}
}
@misc{phs-movep2002,
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Temporal Logic and Verification},
year = 2002,
month = jun,
howpublished = {Invited tutorial, 5th {S}ummer {S}chool on
{M}odelling and {V}erifying {P}arallel {P}rocesses
({MOVEP}'02), Nantes, France}
}
@techreport{BFNS-edf6,
author = {Bardin, S{\'e}bastien and Finkel, Alain and
Nowak, David and
Schnoebelen, {\relax Ph}ilippe},
title = {Note de synth{\`e}se {\`a} 6 mois},
year = {2003},
month = jul,
type = {Contract Report},
number = {P11L03/F01304/0 + 50.0241},
institution = {collaboration entre EDF et le LSV},
oldhowpublished = {Contrat P11L03/F01304/0 et 50.0241 de collaboration
entre EDF et le LSV},
note = {43~pages}
}
@inproceedings{BerSch-fossacs2003,
address = {Warsaw, Poland},
month = apr,
year = 2003,
volume = 2620,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gordon, Andrew D.},
acronym = {{FoSSaCS}'03},
booktitle = {{P}roceedings of the 6th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'03)},
author = {Bertrand, Nathalie and
Schnoebelen, {\relax Ph}ilippe},
title = {Model Checking Lossy Channels Systems Is Probably
Decidable},
pages = {120-135},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BerSch-fossacs2003.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BerSch-fossacs2003.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BerSch-fossacs2003.pdf},
abstract = {Lossy channel systems (LCS's) are systems of
finite state automata that communicate via unreliable
unbounded fifo channels. We propose a new probabilistic
model for these systems, where losses of messages are seen
as faults occurring with some given probability, and where
the internal behavior of the system remains
nondeterministic, giving rise to a reactive Markov chains
semantics. We then investigate the verification of
linear-time properties on this new model.}
}
@inproceedings{MarSch-concur2003,
address = {Marseilles, France},
month = aug,
year = 2003,
volume = 2761,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Amadio, Roberto M. and Lugiez, Denis},
acronym = {{CONCUR}'03},
booktitle = {{P}roceedings of the 14th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'03)},
author = {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
title = {Model Checking a Path (Preliminary Report)},
pages = {251-265},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MarSch-concur03.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MarSch-concur03.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MarSch-concur03.pdf},
doi = {10.1007/b11938},
abstract = {We consider the problem of checking whether a finite (or
ultimately periodic) run satisfies a temporal logic formula. This problem
is at the heart of {"}runtime verification{"} but it also appears in many other
situations. By considering several extended temporal logics, we show that
the problem of model checking a path can usually be solved efficiently,
and profit from specialized algorithms. We further show it is possible to
efficiently check paths given in compressed form.}
}
@inproceedings{Sch-icalp2003,
address = {Eindhoven, The Netherlands},
month = jun,
year = 2003,
volume = 2719,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baeten, Jos C. M. and Lenstra, Jan Karel and
Parrow, Joachim and Woeginger, Gerhard J.},
acronym = {{ICALP}'03},
booktitle = {{P}roceedings of the 30th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming
({ICALP}'03)},
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Oracle circuits for branching-time model checking},
pages = {790-801},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-icalp03-long.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Sch-icalp03-long.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-icalp03-long.pdf},
abstract = {A special class of oracle
circuits with tree-vector form is introduced.
It is shown that they can be evaluated in
deterministic polynomial-time with a polylog
number of adaptive queries to an NP oracle.
This framework allows us to evaluate the
precise computational complexity of model
checking for some branching-time logics where
it was known that the problem is NP-hard and
coNP-hard.}
}
@misc{TSMVv1.0,
author = {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
title = {{TSMV}~v1.0},
year = {2003},
month = oct,
howpublished = {Available at
\url{http://www.lsv.ens-cachan.fr/~markey/TSMV/}},
note = {See description in~\cite{MS-formats2004}. Written in C
(about 4000~lines on top of NuSMV v2.1.2)},
note-fr = {Voir la description dans~\cite{MS-formats2004}. \'Ecrit en C
(environ 4000~lignes \`ajout\'ees \`a NuSMV~v2.1.2)},
url = {http://www.lsv.ens-cachan.fr/~markey/TSMV/}
}
@article{lst-TCS2001,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Laroussinie, Fran{\c{c}}ois and
Schnoebelen, {\relax Ph}ilippe and
Turuani, Mathieu},
title = {On the Expressivity and Complexity of Quantitative
Branching-Time Temporal Logics},
volume = {297},
number = {1-3},
pages = {297-315},
year = {2003},
month = mar,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LST-TCS01.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LST-TCS01.ps},
doi = {10.1016/S0304-3975(02)00644-8},
abstract = {We investigate extensions of
CTL allowing to express quantitative
requirements about an abstract notion of time
in a simple discrete-time framework, and
study the expressive power of several
relevant logics.\par
When only subscripted modalities are used,
polynomial-time model checking is possible
even for the largest logic we consider, while
the introduction of freeze quantifiers leads
to a complexity blow-up.}
}
@inproceedings{phs-aiml02,
address = {Toulouse, France},
unsure-month = sep,
unsure-nmonth = 9,
year = 2003,
optaddress = {London, UK},
publisher = {King's College Publication},
editor = {Balbiani, {\relax Ph}ilippe and Suzuki, Nobu-Yuki
and Wolter, Frank and Zakharyaschev, Michael},
acronym = {{AiML}'02},
booktitle = {{S}elected {P}apers from the 4th
{W}orkshop on {A}dvances in {M}odal {L}ogics
({AiML}'02)},
author = {Schnoebelen, {\relax Ph}ilippe},
title = {The Complexity of Temporal Logic Model Checking},
chapter = {19},
pages = {393-436},
note = {Invited paper},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-aiml02.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Sch-aiml02.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-aiml02.pdf}
}
@misc{phs-svhss2003,
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Model Checking Branching-Time Temporal Logics},
year = {2003},
month = may,
howpublished = {Invited talk, Franco-Israeli Workshop on Semantics and
Verification of Hardware and Software Systems,
Tel-Aviv, Israel}
}
@inproceedings{BerSch-avis2004,
address = {Barcelona, Spain},
month = apr,
year = 2004,
editor = {Bharadwaj, Ramesh},
acronym = {{AVIS}'04},
booktitle = {{P}roceedings of the 3rd {I}nternational
{W}orkshop on {A}utomated {V}erification
of {I}nfinite-{S}tate {S}ystems
({AVIS}'04)},
author = {Bertrand, Nathalie and
Schnoebelen, {\relax Ph}ilippe},
title = {Verifying Nondeterministic Channel Systems With
Probabilistic Message Losses},
nopages = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BerSch-avis04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BerSch-avis04.pdf},
abstract = {Lossy channel systems (LCS's) are
systems of finite state automata that communicate
via unreliable unbounded fifo channels. In order to
circumvent the undecidability of model checking for
nondeterministic LCS's, probabilistic models have
been introduced, where it can be decided whether a
linear-time property holds almost surely. However,
such fully probabilistic systems are not a faithful
model of nondeterministic protocols.\par
We study a hybrid model for LCS's where losses of
messages are seen as faults occurring with some
given probability, and where the internal behavior
of the system remains nondeterministic. Thus the
semantics is in terms of infinite-state reactive
Markov chains (equivalently, Markovian decision
processes). A similar model was introduced in the
second part of (Bertrand \& Schnoebelen,
FOSSACS'2003, LNCS 2620, pp.~120-135): we continue
this work and give a complete picture of the
decidability of qualitative model checking for
MSO-definable properties and some relevant
subcases.}
}
@inproceedings{KucSch2004,
address = {London, UK},
month = aug,
year = 2004,
volume = 3170,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gardner, {\relax Ph}ilippa and Yoshida, Nobuko},
acronym = {{CONCUR}'04},
booktitle = {{P}roceedings of the 15th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'04)},
author = {Ku{\v c}era, Anton{\'\i}n and
Schnoebelen, {\relax Ph}ilippe},
title = {A General Approach to Comparing Infinite-State Systems
with Their Finite-State Specifications},
pages = {372-386},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KS-concur2004.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KS-concur2004.pdf},
doi = {10.1007/978-3-540-28644-8_24},
abstract = {We introduce a generic family of behavioral relations for
which the
problem of comparing an arbitrary transition system to some
finite-state specification can be reduced to a model checking problem
against simple modal formulae. As an application, we derive
decidability of several regular equivalence problems for well-known
families of infinite-state systems.}
}
@inproceedings{LMS-concur2004,
address = {London, UK},
month = aug,
year = 2004,
volume = 3170,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gardner, {\relax Ph}ilippa and Yoshida, Nobuko},
acronym = {{CONCUR}'04},
booktitle = {{P}roceedings of the 15th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'04)},
author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and
Schnoebelen, {\relax Ph}ilippe},
title = {Model Checking Timed Automata with One or Two Clocks},
pages = {387-401},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMS-concur2004.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LMS-concur2004.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMS-concur2004.pdf},
doi = {10.1007/978-3-540-28644-8_25},
abstract = {In this paper, we study model checking of timed automata
(TAs), and more precisely we aim at finding efficient model checking
for subclasses of TAs. For this, we consider model checking TCTL and
TCTL, over TAs with one clock or two clocks.\par
First we show that the reachability problem is NLOGSPACE-complete
for one clock TAs (i.e. as complex as reachability in classical graphs)
and we give a polynomial time algorithm for model checking TCTL,
over this class of TAs. Secondly we show that model checking becomes
PSPACE-complete for full TCTL over one clock TAs. We also show that
model checking CTL (without any timing constraint) over two clock TAs
is PSPACE-complete and that reachability is NP-hard.}
}
@inproceedings{MS-formats2004,
address = {Grenoble, France},
month = sep,
year = 2004,
volume = {3253},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Lakhnech, Yassine and Yovine, Sergio},
acronym = {{FORMATS}'04/{FTRTFT}'04},
booktitle = {{P}roceedings of the {J}oint {C}onferences
{F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'04) and
{F}ormal {T}echniques in {R}eal-{T}ime and
{F}ault-{T}olerant {S}ystems ({FTRTFT}'04)},
author = {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
title = {Symbolic Model Checking for Simply-Timed Systems},
pages = {102-117},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MS-formats2004.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MS-formats2004.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MS-formats2004.pdf},
abstract = {We describe OBDD-based symbolic model checking algorithms for
simply-timed systems, i.e. finite state graphs where transitions
carry a duration. These durations can be arbitrary natural numbers. A
simple and natural semantics for these systems opens the way for
improved efficiency. Our algorithms have been implemented in NuSMV
and perform well in practice (on standard case studies).}
}
@inproceedings{MS-qest2004,
address = {Enschede, The Netherlands},
month = sep,
year = 2004,
publisher = {{IEEE} Computer Society Press},
acronym = {{QEST}'04},
booktitle = {{P}roceedings of the 1st {I}nternational
{C}onference on {Q}uantitative
{E}valuation of {S}ystems
({QEST}'04)},
author = {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
title = {{TSMV}: {A} Symbolic Model Checker for Quantitative
Analysis of Systems},
pages = {330-331},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MS-qest2004.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MS-qest2004.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MS-qest2004.pdf},
doi = {10.1109/QEST.2004.10028},
abstract = {TSMV is an extension of NuSMV, the open-source
symbolic model checker, aimed at dealing with timed versions
of (models of) circuits, PLC controllers, protocols, etc. The
underlying model is an extension of Kripke structures, where
every transition carries an integer duration (possibly zero). This
simple model supports efficient symbolic algorithms for RTCTL
formulae.}
}
@incollection{Sch-voss,
year = 2004,
volume = 2925,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baier, {\relax Ch}ristel and Haverkort, Boudewijn R.
and Hermanns, Holger and Katoen, Joost-Pieter and
Siegle, Markus and Vaandrager, Frits},
acronym = {{V}alidation of {S}tochastic {S}ystems},
booktitle = {{V}alidation of {S}tochastic {S}ystems: {A} {G}uide
to {C}urrent {R}esearch},
author = {Schnoebelen, {\relax Ph}ilippe},
title = {The Verification of Probabilistic Lossy Channel
Systems},
pages = {445-465},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-voss.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Sch-voss.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-voss.pdf},
abstract = {Lossy channel systems (LCS's) are
systems of finite state automata that
communicate via unreliable unbounded fifo
channels. Several probabilistic versions of
these systems have been proposed in recent
years, with the two aims of modeling more
faithfully the losses of messages, and
circumventing undecidabilities by some kind of
randomization. We survey these proposals and
the verification techniques they support.}
}
@article{ms-IPL2004,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
title = {A {PTIME}-Complete Matching Problem for
{SLP}-Compressed Words},
volume = {90},
number = {1},
pages = {3-6},
year = {2004},
month = jan,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MarSch-IPL2004.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MarSch-IPL2004.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MarSch-IPL2004.pdf},
doi = {10.1016/j.ipl.2004.01.002},
abstract = {SLP-compressed words are words
given by simple deterministic grammars called
{"}straight-line programs{"}. We prove that the
problem of deciding whether an SLP-compressed
word is recognized by a FSA is complete for
polynomial-time.}
}
@article{ABRS-lossy,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Abdulla, Parosh Aziz and Bertrand, Nathalie and
Rabinovich, Alexander and Schnoebelen, {\relax Ph}ilippe},
title = {Verification of Probabilistic Systems with Faulty
Communication},
year = 2005,
month = nov,
volume = 202,
number = 2,
pages = {141-165},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/InfComp-ABRS.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/InfComp-ABRS.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/InfComp-ABRS.ps},
doi = {10.1016/j.ic.2005.05.008},
abstract = {Many protocols are designed to
operate correctly even in the case where the
underlying communication medium is faulty. To
capture the behavior of such protocols,
\emph{Lossy Channel Systems}~(LCS's) have been
proposed. In an LCS the communication channels
are modeled as unbounded FIFO buffers which are
unreliable in the sense that they can
nondeterministically lose messages. \par
Recently, several attempts have been made to
study \emph{Probabilistic Lossy Channel
Systems}~(PLCS's) in which the probability of
losing messages is taken into account. In this
article, we consider a variant of PLCS's which
is more realistic than those studied
previously. More precisely, we assume that
during each step in the execution of the
system, each message may be lost with a certain
predefined probability. We show that for such
systems the following model-checking problem is
decidable: to verify whether a linear-time
property definable by a finite-state
\(\omega\)-automaton holds with probability one.
We also consider other types of faulty
behavior, such as corruption and duplication of
messages, and insertion of new messages, and
show that the decidability results extend to
these models.}
}
@inproceedings{BFLS05-atva,
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 = {Bardin, S{\'e}bastien and Finkel, Alain and
Leroux, J{\'e}r{\^o}me and Schnoebelen, {\relax Ph}ilippe},
title = {Flat acceleration in symbolic model checking},
pages = {474-488},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLS05-atva.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLS05-atva.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BFLS05-atva.ps},
doi = {10.1007/11562948_35},
abstract = {Symbolic model checking provides partially
effective verification procedures that can handle systems
with an infinite state space. So-called {"}acceleration
techniques{"} enhance the convergence of fixpoint
computations by computing the transitive closure of some
transitions. In this paper we develop a new framework for
symbolic model checking with accelerations. We also propose
and analyze new symbolic algorithms using accelerations to
compute reachability sets.}
}
@article{LugSch-IC,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Lugiez, Denis and Schnoebelen, {\relax Ph}ilippe},
title = {Decidable first-order transition logics for
{PA}-processes},
year = 2005,
month = nov,
volume = 203,
number = 1,
pages = {75-113},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/InfComp-C2707.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/InfComp-C2707.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/InfComp-C2707.ps},
doi = {10.1016/j.ic.2005.02.003},
abstract = {We show the decidability of
model checking PA-processes against
several first-order logics
based upon the reachability predicate.
The main tool for this result is the
recognizability by tree automata of the
reachability relation. The tree
automata approach and the transition
logics we use allow a smooth and
general treatment of parameterized model
checking for PA. This approach is
extended to handle a quite general notion
of costs of PA-steps.
In particular, when costs are Parikh
images of traces, we show decidability
of a transition logic extended by some
form of first-order reasoning over
costs.}
}
@misc{persee-miparcours05,
author = {Schnoebelen, {\relax Ph}ilippe and others},
title = {{ACI} {S}{\'e}curit{\'e} {I}nformatique {PERS{\'E}E}~---
Rapport {\`a} mi-parcours},
year = 2005,
month = nov,
type = {Contract Report},
note = {8~pages}
}
@inproceedings{BBS-forte06,
address = {Paris, France},
month = sep,
year = 2006,
volume = 4229,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Najm, Elie and Pradat{-}Peyre, Jean-Fran{\c{c}}ois and
Vigui{\'e} Donzeau-Gouge, V{\'e}ronique},
acronym = {{FORTE}'06},
booktitle = {{P}roceedings of 26th {IFIP} {WG6.1}
{I}nternational {C}onference on {F}ormal
{T}echniques for {N}etworked and {D}istributed {S}ystems
({FORTE}'06)},
author = {Baier, Christel and Bertrand, Nathalie and Schnoebelen, {\relax Ph}ilippe},
title = {Symbolic verification of communicating systems with
probabilistic message losses: liveness and fairness},
pages = {212-227},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-forte06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-forte06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBS-forte06.ps},
doi = {10.1007/11888116_17},
abstract = {NPLCS's are a new model for nondeterministic channel systems
where unreliable communication is modeled by probabilistic message losses.
We~show that, for \(\omega\)-regular linear-time properties and finite-memory
schedulers, qualitative model-checking is decidable. The~techniques extend
smoothly to questions where fairness restrictions are imposed on the
schedulers. The~symbolic procedure underlying our decidability proofs has been
implemented and used to study a simple protocol handling two-way transfers in
an unreliable setting.}
}
@inproceedings{BBS-lpar06,
address = {Phnom Penh, Cambodia},
month = nov,
year = 2006,
volume = 4246,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Hermann, Miki and Voronkov, Andrei},
acronym = {{LPAR}'06},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onference on {L}ogic for {P}rogramming,
{A}rtificial {I}ntelligence, and {R}easoning
({LPAR}'06)},
author = {Baier, Christel and Bertrand, Nathalie and
Schnoebelen, {\relax Ph}ilippe},
title = {On Computing Fixpoints in Well-Structured Regular Model
Checking, with Applications to Lossy Channel Systems},
pages = {347-361},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-lpar06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-lpar06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBS-lpar06.ps},
doi = {10.1007/11916277_24},
abstract = {We prove a general finite convergence theorem for
{"}upward-guarded{"} fixpoint expressions over a well-quasi-ordered~set. This
has immediate applications in regular model checking of well-structured
systems, where a main issue is the eventual convergence of fixpoint
computations. In~particular, we are able to directly obtain several new
decidability results on lossy channel systems.}
}
@article{BBS-ipl05,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Baier, Christel and Bertrand, Nathalie and
Schnoebelen, {\relax Ph}ilippe},
title = {A note on the attractor-property of infinite-state {M}arkov chains},
year = 2006,
month = jan,
number = 2,
volume = 97,
pages = {58-63},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/IPL-BBS.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/IPL-BBS.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IPL-BBS.ps},
doi = {10.1016/j.ipl.2005.09.011},
abstract = {In the past five years, a series of verification algorithms
has been proposed for infinite Markov chains that have a
finite attractor, \emph{i.e.}, a set that will be visited
infinitely often almost surely starting from any state. \par
In this paper, we establish a sufficient criterion for
the existence of an attractor. We show that if the states
of a Markov chain can be given levels (positive integers)
such that the expected next level for states at some
level \(n > 0\) is less than \(n-\Delta\) for some positive
\(\Delta\), then the states at level~\(0\) constitute an
attractor for the chain. As an application, we obtain a
direct proof that some probabilistic channel systems
combining message losses with duplication and insertion
errors have a finite attractor.}
}
@inproceedings{BS05-express,
address = {San Francisco, California, USA},
month = jul,
year = 2006,
number = 3,
volume = 154,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Baeten, Jos and Phillips, Iain},
acronym = {{EXPRESS}'05},
booktitle = {{P}roceedings of the 12th {I}nternational
{W}orkshop on {E}xpressiveness in
{C}oncurrency
({EXPRESS}'05)},
author = {Bertrand, Nathalie and Schnoebelen, {\relax Ph}ilippe},
title = {A short visit to the {STS} hierarchy},
pages = {59-69},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BS05-express.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BS05-express.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BS05-express.ps},
doi = {10.1016/j.entcs.2006.05.007},
abstract = {The hierarchy of Symbolic
Transition Systems, introduced by Henzinger,
Majumdar and Raskin, is an elegant
classification
tool for some families of infinite-state
operational models that support some variants of
a symbolic {"}backward closure{"}
verification algorithm. It was first used and
illustrated with families of hybrid
systems.\par
In this paper we investigate whether the STS
hierarchy can account for classical
families of infinite-state systems outside of
timed or hybrid systems.}
}
@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.}
}
@article{KucSch-TCS,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Ku{\v c}era, Anton{\'\i}n and
Schnoebelen, {\relax Ph}ilippe},
title = {A General Approach to Comparing Infinite-State Systems
with Their Finite-State Specifications},
number = {2-3},
volume = {358},
pages = {315-333},
month = aug,
year = 2006,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KucSch-TCS.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KucSch-TCS.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/KucSch-TCS.ps},
doi = {10.1016/j.tcs.2006.01.021},
abstract = {We introduce a generic family of
behavioral relations for which the regular
equivalence problem (\emph{i.e.}, comparing an arbitrary
transition system to some finite-state
specification) can be reduced to the model
checking problem against simple modal formulae.
As an application, we derive decidability of
several regular equivalence problems for
well-known families of infinite-state systems. }
}
@article{LMS-tcs05,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas
and Schnoebelen, {\relax Ph}ilippe},
title = {Efficient Timed Model Checking for Discrete-Time
Systems},
volume = 353,
number = {1-3},
pages = {249-271},
month = mar,
year = 2006,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMS-TCS05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMS-TCS05.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LMS-TCS05.ps},
doi = {10.1016/j.tcs.2005.11.020},
abstract = {We consider model checking of timed
temporal formulae in \emph{durational transition
graphs} (DTGs), \emph{i.e.}, Kripke structures where
transitions have integer durations. Two semantics for
DTGs are presented and motivated. We consider timed
versions of CTL where subscripts put quantitative
constraints on the time it takes before a property is
satisfied. \par
We exhibit an important gap between logics where
subscripts of the form {"}\(= c\){"} (exact duration) are
allowed, and simpler logics that only allow subscripts
of the form {"}\(\leq c\){"} or {"}\(\geq c\){"} (bounded
duration).\par
Without exact durations, model checking can be done in
polynomial time, but with exact durations, it becomes
\(\Delta_{2}^{P}\)-complete or PSPACE-complete
depending on the considered semantics.}
}
@article{MS05-IPL,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
title = {Mu-Calculus Path Checking},
volume = 97,
number = 6,
month = mar,
year = 2006,
pages = {225-230},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MS05-IPL.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MS05-IPL.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MS05-IPL.ps},
doi = {10.1016/j.ipl.2005.11.010},
abstract = {We investigate the path model
checking problem for the \(\mu\)-calculus.
Surprisingly, restricting to deterministic
structures does not allow for more efficient model
checking algorithm, as we prove that it can encode
any instance of the standard model checking problem
for the \(\mu\)-calculus. }
}
@article{RS-btl2,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Rabinovich, Alexander and
Schnoebelen, {\relax Ph}ilippe},
title = {{\(\mathit{\MakeUppercase{BTL}}_2\)} and the expressive
power of {\(\mathit{\MakeUppercase{ECTL}}^+\)}},
year = 2006,
month = jul,
volume = 204,
number = 7,
pages = {1023-1044},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BTL2-InfComp.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BTL2-InfComp.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BTL2-InfComp.ps},
doi = {10.1016/j.ic.2005.07.006},
abstract = {We show that \(\mathit{ECTL}^+\), the
classical extension of \(\mathit{CTL}\) with fairness
properties, is expressively equivalent to
\(\mathit{BTL}_2\), a natural fragment of the monadic
logic of order. \(\mathit{BTL}_2\)~is the branching-time
logic with arbitrary quantification over paths, and
where path formulae are restricted to quantifier
depth~\(2\) first-order formulae in the monadic logic of
order. This result, linking \(\mathit{ECTL}^+\) to a
natural fragment of the monadic logic of order, provides
a characterization that other branching-time logics,
\emph{e.g.}, \(\mathit{CTL}\), lack. \par
We then go on to show that \(\mathit{ECTL}^+\) and
\(\mathit{BTL}_2\) are not finitely based (\emph{i.e.},
they cannot be defined by a finite set of temporal
modalities) and that their model-checking problems are
of the same complexity. }
}
@misc{phs-lipn2006,
author = {Schnoebelen, {\relax Ph}ilippe},
title = {De nouvelles applications pour le model-checking},
year = {2006},
month = nov,
howpublished = {Invited lecture, Journ{\'e}es {\`a} l'occasion des
20~ans du~LIPN, Villetaneuse, France}
}
@inproceedings{CS-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 = {Chambart, Pierre and Schnoebelen, {\relax Ph}ilippe},
title = {The \(\omega\)-Regular {P}ost Embedding Problem},
pages = {97-111},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-fossacs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-fossacs08.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CS-fossacs08.ps},
doi = {10.1007/978-3-540-78499-9_8},
abstract = {Post's Embedding Problem is a new variant of Post's
Correspondence Problem where words are compared with embedding rather than
equality. It~has been shown recently that adding regular constraints on
the form of admissible solutions makes the problem highly non-trivial, and
relevant to the study of lossy channel systems. Here we consider the
infinitary version and its application to recurrent reachability in lossy
channel systems.}
}
@inproceedings{BMOSW-stacs08,
address = {Bordeaux, France},
month = feb,
year = 2008,
volume = 1,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Albers, Susanne and Weil, Pascal},
acronym = {{STACS}'08},
booktitle = {{P}roceedings of the 25th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'08)},
author = {Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo{\"e}l
and Schnoebelen, {\relax Ph}ilippe and Worrell, James},
title = {On Termination for Faulty Channel Machines},
pages = {121-132},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bmosw-stacs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bmosw-stacs08.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/bmosw-stacs08.ps},
abstract = {A channel machine consists of a finite controller together with
several fifo channels; the controller can read messages from the head of a
channel and write messages to the tail of a channel. In this paper, we
focus on channel machines with \emph{insertion errors}, \textit{i.e.},
machines in whose channels messages can spontaneously appear. Such devices
have been previously introduced in the study of Metric Temporal Logic.
We~consider the termination problem: are all the computations of a given
insertion channel machine finite? We~show that this problem has
non-elementary, yet primitive recursive complexity.}
}
@inproceedings{CS-fsttcs07,
address = {New~Delhi, India},
month = dec,
year = 2007,
volume = 4855,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Arvind, V. and Prasad, Sanjiva},
acronym = {{FSTTCS}'07},
booktitle = {{P}roceedings of the 27th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'07)},
author = {Chambart, Pierre and Schnoebelen, {\relax Ph}ilippe},
title = {{P}ost Embedding Problem is not Primitive Recursive,
with Applications to Channel Systems},
pages = {265-276},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-fsttcs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-fsttcs07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CS-fsttcs07.ps},
doi = {10.1007/978-3-540-77050-3_22},
abstract = {We introduce \textsf{PEP}, the Post Embedding Problem, a variant
of \textsf{PCP} where one compares strings with the subword relation, and
\textsf{PEP}\textsuperscript{reg}, a further variant where solutions are
constrained and must belong to a given regular language.
\textsf{PEP}\textsuperscript{reg} is decidable but not primitive
recursive. This entails the decidability of reachability for
unidirectional systems with one reliable and one lossy channel. }
}
@inproceedings{phs-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 = {Schnoebelen, {\relax Ph}ilippe},
title = {Model Checking Branching-Time Logics},
pages = {5},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/phs-time07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/phs-time07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/phs-time07.ps},
doi = {10.1109/TIME.2007.52}
}
@misc{persee-final,
author = {Schnoebelen, {\relax Ph}ilippe and Bouajjani, Ahmed and Sutre, Gr{\'e}goire},
title = {{ACI} {S}{\'e}curit{\'e} {I}nformatique {PERS{\'E}E}~---
Rapport final},
year = 2006,
month = nov,
type = {Contract Report},
note = {12~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Persee-final.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Persee-final.pdf}
}
@article{BBS-arxiv05,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Baier, Christel and Bertrand, Nathalie and
Schnoebelen, {\relax Ph}ilippe},
title = {Verifying nondeterministic probabilistic channel
systems against {{\(\omega\)}}-regular linear-time
properties},
year = 2007,
volume = 9,
number = 1,
nopages = {},
month = dec,
url = {http://arxiv.org/abs/cs.LO/0511023},
pdf = {http://arxiv.org/pdf/cs.LO/0511023},
ps = {http://arxiv.org/ps/cs.LO/0511023},
doi = {10.1145/1297658.1297663},
abstract = {Lossy channel systems (LCS's) are systems of finite state processes that
communicate via unreliable unbounded fifo channels. We introduce NPLCS's,
a variant of LCS's where message losses have a probabilistic behavior
while the component processes behave nondeterministically, and study the
decidability of qualitative verification problems for \(\omega\)-regular
linear-time properties.\par
We show that ---in contrast to finite-state Markov decision processes---
the satisfaction relation for linear-time formulas depends on the type of
schedulers that resolve the nondeterminism. While the qualitative model
checking problems for the full class of history-dependent schedulers is
undecidable, the same questions for finite-memory schedulers can be
solved algorithmically. Additionally, some special kinds of reachability,
or recurrent reachability, qualitative properties yield decidable
verification problems for the full class of schedulers, which ---for this
restricted class of problems--- are as powerful as finite-memory
schedulers, or even a subclass of them.}
}
@misc{PhS-AV2008,
author = {Schnoebelen, {\relax Ph}ilippe},
title = {The complexity of lossy channel systems},
year = 2008,
month = aug,
noslides = {},
howpublished = {Invited talk, Workshop {A}utomata and {V}erification
({AV}'08), Mons, Belgium}
}
@inproceedings{CS-concur08,
address = {Toronto, Canada},
month = aug,
year = 2008,
volume = 5201,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {van Breugel, Franck and Chechik, Marsha},
acronym = {{CONCUR}'08},
booktitle = {{P}roceedings of the 19th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'08)},
author = {Chambart, Pierre and Schnoebelen, {\relax Ph}ilippe},
title = {Mixing Lossy and Perfect Fifo Channels},
pages = {340-355},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-concur08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-concur08.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CS-concur08.ps},
doi = {10.1007/978-3-540-85361-9_28},
abstract = {We~consider asynchronous networks of finite-state systems
communicating \emph{via} a combination of reliable and lossy fifo channels.
Depending on the topology, the~reachability problem for such networks may
be decidable. We~provide a complete classification of network topologies
according to whether they lead to a decidable reachability problem.
Furthermore, this classification can be decided in polynomial-time.}
}
@inproceedings{CS-lics08,
address = {Pittsburgh, Pennsylvania, USA},
month = jun,
year = 2008,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'08},
booktitle = {{P}roceedings of the 23rd
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'08)},
author = {Chambart, Pierre and Schnoebelen, {\relax Ph}ilippe},
title = {The Ordinal Recursive Complexity of Lossy Channel Systems},
pages = {205-216},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-lics08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-lics08.pdf},
doi = {10.1109/LICS.2008.47},
abstract = {We show that reachability and termination for lossy channel
systems is exactly at level \(\mathcal{F}_{\omega^{\omega}}\) in the
Fast-Growing Hierarchy of recursive functions, the first level that
dominates all multiply-recursive functions.}
}
@inproceedings{CS-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 = {Chambart, Pierre and Schnoebelen, {\relax Ph}ilippe},
title = {Toward a compositional theory of leftist grammars and
transformations},
pages = {237-251},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-fossacs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-fossacs10.pdf},
doi = {10.1007/978-3-642-12032-9_17},
abstract = {Leftist grammars [Motwani \textit{et~al.}, STOC~2000] are
special semi-Thue systems where symbols can only insert or erase to their
left. We~develop a theory of leftist grammars seen as word transformers as
a tool toward rigorous analyses of their computational power. Our~main
contributions in this first paper are (1)~constructions proving that
leftist transformations are closed under compositions and transitive
closures, and (2)~a~proof that bounded reachability is NP-complete even
for leftist grammars with acyclic rules.}
}
@inproceedings{phs-rp10,
address = {Brno, Czech Republic},
month = aug,
year = 2010,
volume = 6227,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ku{\v c}era, Anton{\'\i}n and Potapov, Igor},
acronym = {{RP}'10},
booktitle = {{P}roceedings of the 4th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'10)},
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Lossy Counter Machines Decidability Cheat Sheet},
pages = {51-75},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/phs-rp10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/phs-rp10.pdf},
doi = {10.1007/978-3-642-15349-5_4},
abstract = {Lossy counter machines (LCM's) are a variant of Minsky counter
machines based on weak (or~unreliable) counters in the sense that they can
decrease nondeterministically and without notification. This model,
introduced by R.~Mayr [TCS~297:337-354 (2003)], is not yet very
well known, even though it has already proven useful for establishing
hardness results.\par
In this paper we survey the basic theory of LCM's and their verification
problems, with a focus on the decidability/undecidability divide. }
}
@inproceedings{PhS-mfcs10,
address = {Brno, Czech Republic},
month = aug,
year = 2010,
volume = 6281,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hlin{\v e}n{\'y}, Petr and Ku{\v c}era, Anton{\'\i}n},
acronym = {{MFCS}'10},
booktitle = {{P}roceedings of the 35th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'10)},
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Revisiting {A}ckermann-Hardness for Lossy Counter Machines
and Reset {P}etri Nets},
pages = {616-628},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/phs-mfcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/phs-mfcs10.pdf},
doi = {10.1007/978-3-642-15155-2_54},
abstract = {We prove that coverability and termination are not
primitive-recursive for lossy counter machines and for Reset Petri nets.}
}
@inproceedings{CS-dlt2010,
address = {London, Ontario, Canada},
month = aug,
year = 2010,
volume = {6224},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gao, Yuan and Lu, Hanlin and Seki, Shinnosuke and Yu, Sheng},
acronym = {{DLT}'10},
booktitle = {{P}roceedings of the 14th {I}nternational
{C}onference on {D}evelopments in {L}anguage {T}heory
({DLT}'10)},
author = {Chambart, Pierre and Schnoebelen, {\relax Ph}ilippe},
title = {Computing blocker sets for the Regular {P}ost Embedding
Problem},
pages = {136-147},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-dlt10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-dlt10.pdf},
doi = {10.1007/978-3-642-14455-4_14},
abstract = {Blocker and coblocker sets are regular languages involved in the
algorithmic solution of the Regular Post Embedding Problem.
We investigate the computability of these languages and
related decision problems.}
}
@inproceedings{CS-icalp10,
address = {Bordeaux, France},
month = jul,
year = 2010,
volume = 6199,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abramsky, Samson and Meyer{ }auf{ }der{ }Heide, Friedhelm
and Spirakis, Paul},
acronym = {{ICALP}'10},
booktitle = {{P}roceedings of the 37th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'10)~-- {P}art~{II}},
author = {Chambart, Pierre and Schnoebelen, {\relax Ph}ilippe},
title = {Pumping and Counting on the Regular {P}ost Embedding Problem},
pages = {64-75},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-icalp10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-icalp10.pdf},
doi = {10.1007/978-3-642-14162-1_6},
abstract = {The Regular Post Embedding Problem is a variant of Post's
Correspondence Problem where one compares strings with the subword
relation and imposes additional regular constraints on admissible
solutions. It is known that this problem is decidable, albeit with very
high complexity.\par
We consider and solve variant problems where the set of solutions is
compared to regular constraint sets and where one counts the number of
solutions. Our positive results rely on two non-trivial pumping lemmas for
Post-embedding languages and their complements.}
}
@inproceedings{SS-icalp11,
address = {Z{\"u}rich, Switzerland},
month = jul,
year = 2011,
volume = 6756,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Aceto, Luca and Henzinger, Monika and Sgall, Jir{\'\i}},
acronym = {{ICALP}'11},
booktitle = {{P}roceedings of the 38th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'11)~-- {P}art~{II}},
author = {Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe},
title = {Multiply-Recursive Upper Bounds with {H}igman's Lemma},
pages = {441-452},
url = {http://arxiv.org/abs/1103.4399},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SS-icalp11.pdf},
doi = {10.1007/978-3-642-22012-8_35},
abstract = {We develop a new analysis for the length of controlled
bad sequences in well-quasi-orderings based on
Higman's Lemma. This leads to tight
multiply-recursive upper bounds that readily apply
to several verification algorithms for
well-structured systems.}
}
@inproceedings{FFSS-lics2011,
address = {Toronto, Canada},
month = jun,
year = 2011,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'11},
booktitle = {{P}roceedings of the 26th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'11)},
author = {Figueira, Diego and Figueira, Santiago and Schmitz, Sylvain and
Schnoebelen, {\relax Ph}ilippe},
title = {{A}ckermannian and Primitive-Recursive Bounds with {D}ickson's Lemma},
pages = {269-278},
url = {http://arxiv.org/abs/1007.2989},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FFSS-lics11.pdf},
doi = {10.1109/LICS.2011.39},
abstract = {Dickson's Lemma is a simple yet powerful tool widely used in
decidability proofs, especially when dealing with counters or related data
structures in algorithmics, verification and model-checking, constraint
solving, logic, etc. While Dickson's Lemma is well-known, most computer
scientists are not aware of the complexity upper bounds that are entailed
by its use. This is mainly because, on this issue, the existing literature
is not very accessible.\par
We propose a new analysis of the length of bad sequences over
\((\mathbb{N}^{k},\leq)\), improving on earlier results and providing
upper bounds that are essentially tight. This analysis is complemented by
a {"}user guide{"} explaining through practical examples how to easily
derive complexity upper bounds from Dickson's Lemma.}
}
@unpublished{aawqot,
author = {Sylvain Schmitz and {\relax Ph}ilippe Schnoebelen},
title = {Algorithmic Aspects of {WQO} Theory},
month = aug,
year = 2012,
note = {Lecture Notes},
url = {http://cel.archives-ouvertes.fr/cel-00727025},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SS-esslli12.pdf}
}
@article{BS-fmsd2012,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Bertrand, Nathalie and Schnoebelen, {\relax Ph}ilippe},
title = {Computable fixpoints in well-structured symbolic model
checking},
pages = {233-267},
volume = 43,
number = 2,
month = oct,
year = 2013,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-fmsd12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-fmsd12.pdf},
doi = {10.1007/s10703-012-0168-y},
abstract = {We prove a general finite-time convergence theorem for fixpoint
expressions over a well-quasi-ordered set. This has immediate applications
for the verification of well-structured systems, where a main issue is the
computability of fixpoint expressions, and in particular for
game-theoretical properties and probabilistic systems where nesting and
alternation of least and greatest fixpoints are common.}
}
@inproceedings{HSS-lics2012,
address = {Dubrovnik, Croatia},
month = jun,
year = 2012,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'12},
booktitle = {{P}roceedings of the 27th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'12)},
author = {Haddad, Serge and Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe},
title = {The Ordinal-Recursive Complexity of Timed-Arc {P}etri
Nets, Data Nets, and Other Enriched Nets},
pages = {355-364},
url = {http://hal.archives-ouvertes.fr/hal-00793811},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HSS-lics12.pdf},
doi = {10.1109/LICS.2012.46},
abstract = {We show how to reliably compute fast-growing functions
with timed-arc Petri nets and data nets. This
construction provides ordinal-recursive lower bounds
on the complexity of the main decidable properties
(safety, termination, regular simulation,~etc.) of
these models. Since these new lower bounds match the
upper bounds that one can derive from wqo theory,
they precisely characterise the computational power
of these so-called {"}enriched{"} nets.}
}
@article{BMOSW-fac12,
publisher = {Springer},
journal = {Formal Aspects of Computing},
author = {Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo{\"e}l
and Schnoebelen, {\relax Ph}ilippe and Worrell, James},
title = {On Termination and Invariance for Faulty Channel Systems},
year = 2012,
month = jul,
volume = 24,
number = {4-6},
pages = {595-607},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMOSU-fac12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMOSU-fac12.pdf},
doi = {10.1007/s00165-012-0234-7},
abstract = {A~\emph{channel machine} consists of a finite controller
together with several fifo channels; the controller can read messages from
the head of a channel and write messages to the tail of a channel. In this
paper we focus on channel machines with \emph{insertion errors}, i.e.,
machines in whose channels messages can spontaneously appear. We consider
the invariance problem: does a given insertion channel machine have an
infinite computation all of whose configurations satisfy a given
predicate? We show that this problem is primitive-recursive if the
predicate is closed under message losses. We also give a non-elementary
lower bound for the invariance problem under this restriction. Finally,
using the previous result, we show that the satisfiability problem for the
safety fragment of Metric Temporal Logic is non-elementary.}
}
@inproceedings{KS-csr12,
address = {Nizhni Novgorod, Russia},
month = jul,
year = 2012,
volume = {7353},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hirsch, Edward A. and Karhum{\"a}ki, Juhani and Lepist{\"o},
Arto and Prilutskii, Michail},
acronym = {{CSR}'12},
booktitle = {{P}roceedings of the 7th {I}nternational {C}omputer {S}cience
{S}ymposium in {R}ussia ({CSR}'12)},
author = {Karandikar, Prateek and Schnoebelen, {\relax Ph}ilippe},
title = {Cutting Through Regular {P}ost Embedding Problems},
pages = {229-240},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-csr12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-csr12.pdf},
doi = {10.1007/978-3-642-30642-6_22},
abstract = {The Regular Post Embedding Problem extended with partial
(co)directness is shown decidable. This extends to universal and{\slash}or
counting versions. It is also shown that combining directness and
codirectness in Post Embedding problems leads to undecidability.}
}
@inproceedings{SS-concur13,
address = {Buenos Aires, Argentina},
month = aug,
year = 2013,
volume = 8052,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {D'Argenio, Pedro R. and Melgratti, Hern{\'a}n)},
acronym = {{CONCUR}'13},
booktitle = {{P}roceedings of the 24th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'13)},
author = {Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe},
title = {The Power of Well-Structured Systems},
pages = {5-24},
url = {http://arxiv.org/abs/1402.2908},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SS-concur13.pdf},
doi = {10.1007/978-3-642-40184-8_2},
abstract = {Well-structured systems, aka WSTS, are computational models
where the set of possible configurations is equipped with a
well-quasi-ordering which is compatible with the transition relation
between configurations. This structure supports generic decidability
results that are important in verification and several other fields. This
paper recalls the basic theory underlying well-structured systems and
shows how two classic decision algorithms can be formulated as an
exhaustive search for some {"}bad{"} sequences. This lets us describe new
powerful techniques for the complexity analysis of WSTS algorithms.
Recently, these techniques have been successful in precisely
characterizing the power, in a complexity-theoretical sense, of several
important WSTS models like unreliable channel systems, monotonic counter
machines, or networks of timed systems.}
}
@inproceedings{BS-qapl2013,
address = {Rome, Italy},
volume = {117},
series = {Electronic Proceedings in Theoretical Computer Science},
month = jun,
year = 2013,
editor = {Bortolussi, Luca and Wiklicky, Herbert},
acronym = {{QAPL}'13},
booktitle = {{P}roceedings of the 11th {I}nternational
{W}orkshop on {Q}uantitative {A}spects of
{P}rogramming {L}anguages ({QAPl}'13)},
author = {Bertrand, Nathalie and Schnoebelen, {\relax Ph}ilippe},
title = {Solving stochastic B{\"u}chi games on infinite arenas with a
finite attractor},
pages = {116-131},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-qapl2013.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-qapl2013.pdf},
doi = {10.4204/EPTCS.117.8},
abstract = {We consider games played on an infinite probabilistic arena
where the first player aims at satisfying generalized B{\"u}chi objectives
almost surely, i.e., with probability one. We provide a fixpoint
characterization of the winning sets and associated winning strategies in
the case where the arena satisfies the finite-attractor property. From
this we directly deduce the decidability of these games on probabilistic
lossy channel systems.}
}
@article{JKS-lmcs14,
journal = {Logical Methods in Computer Science},
author = {Jancar, Petr and Karandikar, Prateek and Schnoebelen, {\relax Ph}ilippe},
title = {On Reachability for Unidirectional Channel Systems Extended
with Regular Tests},
year = {2015},
volume = 11,
number = {{2:2}},
month = apr,
nopages = {},
url = {http://arxiv.org/abs/1406.5067},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JKS-lmcs14.pdf},
doi = {10.2168/LMCS-11(2:2)2015},
abstract = {{"}Unidirectional channel systems{"} (Chambart~\& Schnoebelen,
CONCUR~2008) are finite-state systems where one-way communication from a
Sender to a Receiver goes via one reliable and one unreliable unbounded
fifo channel. While reachability is decidable for these systems, equipping
them with the possibility of testing regular properties on the contents of
channels makes it undecidable. Decidability is preserved when only
emptiness and nonemptiness tests are considered: the proof relies on an
elaborate reduction to a generalized version of Post's Embedding Problem.}
}
@article{KKS-ipl14,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Karandikar, Prateek and Kufleitner, Manfred and Schnoebelen, {\relax Ph}ilippe},
title = {On the index of {S}imon's congruence for piecewise testability},
year = {2015},
month = apr,
volume = {15},
number = {4},
pages = {515-519},
url = {http://arxiv.org/abs/1310.1278},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KKS-ipl14.pdf},
doi = {10.1016/j.ipl.2014.11.008},
abstract = {Simon's congruence, denoted \(\sim_{n}\), relates words having
the same subwords of length up to~\(n\). We~show that, over a
\(k\)-letter alphabet, the~number of words modulo~\(\sim_{n}\) is in
\(2^{\Theta(n^{k-1}\cdot\log n)}\).}
}
@article{HSS-lmcs14,
journal = {Logical Methods in Computer Science},
author = {Haase, Christoph and Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe},
title = {The Power of Priority Channel Systems},
year = {2014},
month = dec,
volume = 10,
number = {4:4},
nopages = {},
url = {http://arxiv.org/abs/1301.5500},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HSS-lmcs14.pdf},
doi = {10.2168/LMCS-10(4:4)2014},
abstract = {We introduce Priority Channel Systems, a new class of channel
systems where messages carry a numeric priority and where higher-priority
messages can supersede lower-priority messages preceding them in the fifo
communication buffers. The decidability of safety and inevitability
properties is shown via the introduction of a priority embedding, a
well-quasi-ordering that has not previously been used in well-structured
systems. We then show how Priority Channel Systems can compute
Fast-Growing functions and prove that the aforementioned verification
problems are \(\mathbf{F}_{\epsilon_{0}}\)-complete.}
}
@inproceedings{LS-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 = {Leroux, J{\'e}r{\^o}me and Schnoebelen, {\relax Ph}ilippe},
title = {On Functions Weakly Computable by {P}etri Nets and Vector
Addition Systems},
pages = {190-202},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-rp14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-rp14.pdf},
doi = { 10.1007/978-3-319-11439-2_15},
abstract = {We show that any unbounded function weakly computable by a Petri
net or a VASS cannot be sublinear. This answers a long-standing folklore
conjecture about weakly computing the inverses of some fast-growing
functions. The proof relies on a pumping lemma for sets of runs in Petri
nets or VASSes.}
}
@inproceedings{KS-dcfs2014,
address = {Turku, Finland},
month = aug,
year = 2014,
volume = {8614},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {J{\"u}rgensen, Helmut and Karhum{\"a}ki, Juhani and Okhotin, Alexander},
acronym = {{DCFS}'14},
booktitle = {{P}roceedings of the 16th {W}orkshop on {D}escriptional
{C}omplexity of {F}ormal {S}ystems ({DCFS}'14)},
author = {Karandikar, Prateek and Schnoebelen, {\relax Ph}ilippe},
title = {On the state complexity of closures and interiors of regular
languages with subwords},
pages = {234-245},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-dcfs2014.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-dcfs2014.pdf},
doi = {10.1007/978-3-319-09704-6_21},
abstract = {We study the state complexity of the set of subwords and
superwords of regular languages, and provide new lower bounds in the case
of languages over a two-letter alphabet. We also consider the dual
interior sets, for which the nondeterministic state complexity has a
doubly-exponential upper bound. We prove a matching doubly-exponential
lower bound for downward interiors in the case of an unbounded alphabet.}
}
@article{KS-msttocs14,
publisher = {Springer},
journal = {Theory of Computing Systems},
author = {Karandikar, Prateek and Schnoebelen, {\relax Ph}ilippe},
title = {Generalized {P}ost Embedding Problems},
year = {2015},
volume = 56,
number = 4,
pages = {697-716},
month = may,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-msttocs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-msttocs14.pdf},
doi = {10.1007/s00224-014-9561-9},
abstract = {The Regular Post Embedding Problem extended with partial
(co)directness is shown decidable. This extends to universal and\slash or
counting versions. It is also shown that combining directness and
codirectness in Post Embedding problems leads to undecidability.}
}
@inproceedings{KS-fsttcs15,
address = {Bangalore, India},
month = dec,
year = 2015,
volume = {45},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Harsha, Prahladh and Ramalingam, G.},
acronym = {{FSTTCS}'15},
booktitle = {{P}roceedings of the 35th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'15)},
author = {Karandikar, Prateek and Schnoebelen, {\relax Ph}ilippe},
title = {Decidability in the logic of subsequences and supersequences},
pages = {84-97},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-fsttcs15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-fsttcs15.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2015.84},
abstract = {We consider first-order logics of sequences ordered by the
subsequence ordering, aka sequence embedding. We show that the
\(\Sigma_{2}\)-theory is undecidable, answering a question left open by
Kuske. Regarding fragments with a bounded number of variables, we show
that the \(\textsf{FO}^{2}\)-theory is decidable while the
\(\textsf{FO}^{3}\)-theory is undecidable.}
}
@techreport{KNS-arxiv14,
author = {Karandikar, Prateek and Niewerth, Matthias and Schnoebelen, {\relax Ph}ilippe},
title = {On the state complexity of closures and interiors of regular languages with subwords},
institution = {Computing Research Repository},
number = {1406.0690},
year = {2014},
month = nov,
type = {Research Report},
url = {http://arxiv.org/abs/1406.0690},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KNS-arxiv14.pdf},
note = {24~pages},
abstract = {We study the state complexity of the set of subwords and
superwords of regular languages, and provide new lower bounds in the case
of languages over a two-letter alphabet. We also consider the dual
interior sets, for which the nondeterministic state complexity has a
doubly-exponential upper bound. We prove a matching doubly-exponential
lower bound for downward interiors in the case of an unbounded alphabet.}
}
@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.",
}}
@inproceedings{PhS-mfcs17,
address = {Aalborg, Denmark},
month = aug,
year = 2017,
volume = {83},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Fran{\c{c}}ois},
acronym = {{MFCS}'17},
booktitle = {{P}roceedings of the 42nd
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'17)},
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Ideal-Based Algorithms for the Symbolic Verification of Well-Structured Systems (Invited Talk)},
pages = {85:1-85:4},
url = {http://drops.dagstuhl.de/opus/volltexte/2017/8139/},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/8139/pdf/LIPIcs-MFCS-2017-85.pdf},
doi = {10.4230/LIPIcs.MFCS.2017.85},
abstract = {We explain how the downward-closed subsets of a well-quasi-ordering (\(X,\leq\)) can be represented via the ideals of \(X\) and how this leads to simple and efficient algorithms for the verification of well-structured systems.}
}
@inproceedings{HSZ-lics17,
address = {Reykjavik, Iceland},
month = jun,
publisher = {{IEEE} Press},
editor = {Ouaknine, Jo{\"e}l},
acronym = {{LICS}'17},
booktitle = {{P}roceedings of the 32nd {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'17)},
author = {Halfon, Simon and Schnoebelen, {\relax Ph}ilippe and Zetzsche, Georg},
title = {Decidability, complexity, and expressiveness of first-order logic over the subword ordering},
pages = {1-12},
year = {2017},
doi = {10.1109/LICS.2017.8005141},
url = {https://arxiv.org/abs/1701.07470},
abstract = {We consider first-order logic over the subword ordering on finite words, where each word is available as a constant. Our first result is that the \(\Sigma_1\) theory is undecidable (already over two letters).\par
We investigate the decidability border by considering fragments where all but a certain number of variables are alternation bounded, meaning that the variable must always be quantified over languages with a bounded number of letter alternations. We prove that when at most two variables are not alternation bounded, the \(\Sigma_1\) fragment is decidable, and that it becomes undecidable when three variables are not alternation bounded. Regarding higher quantifier alternation depths, we prove that the \(\Sigma_2\) fragment is undecidable already for one variable without alternation bound and that when all variables are alternation bounded, the entire first-order theory is decidable.}
}
@article{KS-lmcs19,
journal = {Logical Methods in Computer Science},
author = {P. Karandikar and Schnoebelen, {\relax Ph}ilippe},
title = {The height of piecewise-testable languages and the complexity of the logic of subwords},
volume = {15},
number = {2},
pages = {6:1-6:27},
year = {2019},
month = apr,
pdf = {https://lmcs.episciences.org/5409/pdf},
url = {https://lmcs.episciences.org/5409},
abstract = {The height of a piecewise-testable language \(L\) is the maximum length of the words needed to define \(L\) by excluding and requiring given subwords. The height of \(L\) is an important descriptive complexity measure that has not yet been investigated in a systematic way. This paper develops a series of new techniques for bounding the height of finite languages and of languages obtained by taking closures by subwords, superwords and related operations. As an application of these results, we show that \(FO^2(A^*,\sqsubseteq)\), the two-variable fragment of the first-order logic of sequences with the subword ordering, can only express piecewise-testable properties and has elementary complexity.}
}
@article{HS-ipl19,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Halfon, Simon and Schnoebelen, {\relax Ph}ilippe},
title = {On shuffle products, acyclic automata and piecewise-testable languages},
volume = {145},
pages = {68-73},
year = 2019,
doi = {10.1016/j.ipl.2019.01.012},
abstract = {We show that the shuffle $L\unicode{x29E2} F$ of a
piecewise-testable language $L$ and a finite language $F$ is
piecewise-testable. The proof relies on a classic but little-used
automata-theoretic characterization of piecewise-testable languages. We
also discuss some mild generalizations of the main result, and provide
bounds on the piecewise complexity of $L\unicode{x29E2} F$.}
}
@inproceedings{Schnoebelen-csl21,
address = {Ljubljana, Slovenia},
month = jan,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Baier, Christel and Goubault{-}Larrecq, Jean},
acronym = {{CSL}'21},
booktitle = {{P}roceedings of the 29th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'21)},
author = {{\relax Ph}ilippe Schnoebelen},
title = {On flat lossy channel machines},
pages = {37:1-37:22},
year = {2021},
doi = {10.4230/LIPIcs.CSL.2021.37},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2021/13471/},
url = {https://drops.dagstuhl.de/opus/volltexte/2021/13471/}
}
@incollection{GHKNS-til2020,
volume = 53,
series = {Trends In Logic},
publisher = {Springer},
booktitle = {Well-Quasi Orders in Computation, Logic, Language and Reasoning},
editor = {Schuster, Peter M. and Seisenberger, Monika and Weiermann, Andreas},
author = {Jean Goubault{-}Larrecq and Simon Halfon and P. Karandikar and K. {Narayan Kumar} and {\relax Ph}ilippe Schnoebelen},
title = {The Ideal Approach to Computing Closed Subsets in Well-Quasi-Orderings},
pages = {55-105},
year = 2020,
doi = {10.1007/978-3-030-30229-0_3}
}
@incollection{DSS-til2020,
volume = 53,
series = {Trends In Logic},
publisher = {Springer},
booktitle = {Well-Quasi Orders in Computation, Logic, Language and Reasoning},
editor = {Schuster, Peter M. and Seisenberger, Monika and Weiermann, Andreas},
author = {D{\v{z}}amonja, Mirna and Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe},
title = {On Ordinal Invariants in Well Quasi Orders and Finite Antichain Orders},
pages = {2-54},
year = 2020,
doi = {10.1007/978-3-030-30229-0_2}
}
@article{LPSS-lmcs2020,
journal = {Logical Methods in Computer Science},
author = {J{\'e}r{\^o}me Leroux and M. Praveen and Gr{\'e}goire Sutre and Schnoebelen, {\relax Ph}ilippe},
title = {On Functions Weakly Computable by Pushdown {Petri} Nets and Related Systems},
volume = {15},
number = {4},
year = 2019,
doi = {10.23638/LMCS-15(4:15)2019},
pdf = {https://arxiv.org/pdf/1904.04090.pdf}
}
This file was generated by bibtex2html 1.98.