@inproceedings{AF-GS-STACS-2000,
address = {Lille, France},
month = feb,
year = 2000,
volume = 1770,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Reichel, Horst and Tison, Sophie},
acronym = {{STACS} 2000},
booktitle = {{P}roceedings of the 17th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS} 2000)},
author = {Finkel, Alain and Sutre, Gr{\'e}goire},
title = {Decidability of Reachability Problems for Classes
of Two-Counter Automata},
pages = {346-357},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FinSut-stacs2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FinSut-stacs2000.ps},
doi = {10.1007/3-540-46541-3_29}
}
@inproceedings{BDFP-mfcs-2000,
address = {Bratislava, Slovakia},
month = aug,
year = 2000,
volume = 1893,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Nielsen, Mogens and Rovan, Branislav},
acronym = {{MFCS} 2000},
booktitle = {{P}roceedings of the 25th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS} 2000)},
author = {Bouyer, Patricia and Dufourd, Catherine and
Fleury, Emmanuel and Petit, Antoine},
title = {Expressiveness of Updatable Timed Automata},
pages = {232-242},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDFP-mfcs2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDFP-mfcs2000.ps},
abstract = {Since their introduction by Alur
and Dill, timed automata have been
one of the most widely studied models for
real-time systems. The
syntactic extension of so-called updatable timed
automata allows more
powerful updates of clocks than the reset
operation proposed in the
original model.\par
We prove that any language accepted by an
updatable timed automaton
(from classes where emptiness is decidable) is
also accepted by a
{"}classical{"} timed automaton. We propose even
more precise results on
bisimilarity between updatable and classical
timed automata.}
}
@article{BEFMRWW-ipl2000,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Bouajjani, Ahmed and Esparza, Javier and
Finkel, Alain and Maler, Oded
and Rossmanith, Peter and Willems, Bernard and
Wolper, Pierre},
title = {An Efficient Automata Approach to some Problems on
Context-Free Grammars},
volume = {74},
number = {5-6},
pages = {221-227},
year = {2000},
month = jun,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BEFMRWW-IPL2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BEFMRWW-IPL2000.ps}
}
@article{BerDuf-IPL2000,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {B{\'e}rard, B{\'e}atrice and Dufourd, Catherine},
title = {Timed Automata and Additive Clock Constraints},
volume = {75},
number = {1-2},
pages = {1-7},
year = {2000},
month = jul,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BerDuf-IPL2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BerDuf-IPL2000.ps}
}
@article{BerPic-ACTA2000,
publisher = {Springer},
journal = {Acta Informatica},
author = {B{\'e}rard, B{\'e}atrice and Picaronny, Claudine},
title = {Accepting {Z}eno Words: {A} Way Toward Timed
Refinements},
volume = {37},
number = {1},
pages = {45-81},
year = {2000},
missingmonth = {},
missingnmonth = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BerPic-ACTA2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BerPic-ACTA2000.ps}
}
@misc{Calife-1.1,
author = {B{\'e}rard, B{\'e}atrice and Cast{\'e}ran, Pierre
and Fleury, Emmanuel and
Fribourg, Laurent and Monin, Jean-Fran{\c{c}}ois
and Paulin, {\relax Ch}ristine and Petit, Antoine and
Rouillard, Davy},
title = {Document de sp{\'e}cification du mod{\`e}le
commun},
year = {2000},
month = apr,
howpublished = {Fourniture~1.1 du projet RNRT Calife},
lsv-lang = {FR}
}
@misc{Calife-4.1,
author = {Fribourg, Laurent},
title = {Document de synth{\`e}se sur les techniques
d'abstraction},
year = {2000},
month = jan,
howpublished = {Fourniture~4.1 du projet RNRT Calife},
lsv-lang = {FR}
}
@misc{Calife-4.2,
author = {Bouyer, Patricia and Fleury, Emmanuel and
Petit, Antoine},
title = {Document de synth{\`e}se sur les proc{\'e}dures de
v{\'e}rification des syst{\`e}mes temps r{\'e}el :
Les automates temporis{\'e}s},
year = {2000},
month = jan,
howpublished = {Fourniture~4.2 du projet RNRT Calife},
lsv-lang = {FR}
}
@inproceedings{CasLar-cav2000,
address = {Chicago, Illinois, USA},
month = jul,
year = 2000,
volume = 1855,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Emerson, E. Allen and Sistla, A. Prasad},
acronym = {{CAV} 2000},
booktitle = {{P}roceedings of the 12th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV} 2000)},
author = {Cassez, Franck and Laroussinie, Fran{\c{c}}ois},
title = {Model-Checking for Hybrid Systems by Quotienting
and Constraints Solving},
pages = {373-388},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CasLar-cav2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CasLar-cav2000.ps}
}
@article{FB-MB-LP-IGPL-00,
publisher = {Oxford University Press},
journal = {Logic Journal of the IGPL},
author = {Belala, F. and Bettaz, Mohamed and
Petrucci{-}Dauchy, Laure},
title = {Concurrent systems analysis using {ECATNets}},
volume = {8},
number = {2},
pages = {149-164},
year = {2000},
month = mar,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/belala00concurrent.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/belala00concurrent.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/belala00concurrent.ps},
doi = {10.1093/jigpal/8.2.149}
}
@inproceedings{FPS-concur-2000,
address = {Pennsylvania State University, Pennsylvania, USA},
month = aug,
year = 2000,
volume = 1877,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Palamidessi, Catuscia},
acronym = {{CONCUR} 2000},
booktitle = {{P}roceedings of the 11th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR} 2000)},
author = {Finkel, Alain and Purushothaman{ }Iyer, S. and
Sutre, Gr{\'e}goire},
title = {Well-Abstracted Transition Systems},
pages = {566-580},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2000-6.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2000-6.rr.ps}
}
@inproceedings{FS-mfcs-2000,
address = {Bratislava, Slovakia},
month = aug,
year = 2000,
volume = 1893,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Nielsen, Mogens and Rovan, Branislav},
acronym = {{MFCS} 2000},
booktitle = {{P}roceedings of the 25th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS} 2000)},
author = {Finkel, Alain and Sutre, Gr{\'e}goire},
title = {An Algorithm Constructing the Semilinear {P}ost*
for
2-Dim {R}eset{{\slash}}{T}ransfer {VASS}},
pages = {353-362},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FinSut-mfcs2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FinSut-mfcs2000.ps}
}
@inproceedings{GB-LP-HLPN-00,
address = {\AA rhus, Denmark},
month = jun,
year = 2000,
howpublished = {Research Report DAIMI PB-547},
optaddress = {\AA rhus, Denmark},
optpublisher = {DAIMI},
editor = {Jensen, Kurt},
booktitle = {{P}roceedings of the {W}orkshop on
{P}ractical {U}se of {H}igh-{L}evel
{P}etri {N}ets},
author = {Berthelot, G{\'e}rard and Petrucci, Laure},
title = {Specification and Validation of a Concurrent
System:
{A}n Educational Project},
pages = {55-72},
url = {http://www.daimi.au.dk/designCPN/exam/Other/Trains/index.html},
secondurl = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/BerPet-hlpn2000.ps}
}
@misc{GL:ASPROM,
author = {Goubault{-}Larrecq, Jean},
title = {Analyse de protocoles cryptographiques},
year = {2000},
month = oct,
howpublished = {Invited lecture, Journ{\'e}es {ASPROM}, Paris,
France},
lsv-lang = {FR}
}
@inproceedings{JGL:crypto:orPTA,
address = {Cancun, Mexico},
month = may,
year = 2000,
volume = 1800,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Rolim, Jos{\'e} D. P.},
booktitle = {{P}roceedings of the Workshops of the 15th {I}nternational
{P}arallel and {D}istributed {P}rocessing {S}ymposium},
author = {Goubault{-}Larrecq, Jean},
title = {A Method for Automatic Cryptographic Protocol
Verification (Extended Abstract)},
pages = {977-984},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Gou-fmppta2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Gou-fmppta2000.ps}
}
@inproceedings{LF-LOPSTR-99,
address = {Venezia, Italy},
year = 2000,
volume = 1817,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Bossi, Annalisa},
acronym = {{LOPSTR}'99},
booktitle = {{P}roceedings of the 9th {I}nternational
{W}orkshop on {L}ogic {P}rogram {S}ynthesis
and {T}ransformation
({LOPSTR}'99)},
author = {Laurent Fribourg},
title = {Constraint Logic Programming Applied to Model
Checking},
pages = {31-42},
note = {Invited tutorial},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Fri-lopstr99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Fri-lopstr99.ps}
}
@inproceedings{LF-WFPL-99,
address = {Benicassim, Spain},
month = sep,
year = 2000,
optaddress = {Valencia, Spain},
publisher = {Universidad Polit{\'e}cnica de Valencia, Spain},
editor = {Alpuente, Mar{\'i}a},
acronym = {{WFLP} 2000},
booktitle = {{P}roceedings of the 9th {I}nternational
{W}orkshop on {F}unctional and {L}ogic
{P}rogramming
({WFLP} 2000)},
author = {Laurent Fribourg},
title = {{P}etri Nets, Flat Languages and Linear Arithmetic},
pages = {344-365},
note = {Invited lecture},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Fri-wflp00.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Fri-wflp00.ps}
}
@inproceedings{LP-SCI-00,
address = {Orlando, Florida, USA},
month = jul,
year = 2000,
acronym = {{SCI} 2000},
booktitle = {{P}roceedings of the 4th {W}orld
{M}ulticonference on {S}ystemics,
{C}ybernetics and {I}nformatics
({SCI} 2000)},
author = {Petrucci, Laure},
title = {Design and Validation of a Controller},
pages = {684-688},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Pet-sci2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Pet-sci2000.ps}
}
@techreport{LSV:00:2,
author = {B{\'e}rard, B{\'e}atrice and Sierra, Luis},
title = {Comparing Verification with {H}y{T}ech, {K}ronos
and
{U}ppaal on the Railroad Crossing Example},
type = {Research Report},
number = {LSV-00-2},
year = {2000},
month = jan,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2000-2.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2000-2.rr.ps}
}
@inproceedings{PB-CD-EF-AP-cav2000,
address = {Chicago, Illinois, USA},
month = jul,
year = 2000,
volume = 1855,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Emerson, E. Allen and Sistla, A. Prasad},
acronym = {{CAV} 2000},
booktitle = {{P}roceedings of the 12th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV} 2000)},
author = {Bouyer, Patricia and Dufourd, Catherine and
Fleury, Emmanuel and Petit, Antoine},
title = {Are Timed Automata Updatable?},
pages = {464-479},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDEP-cav2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDEP-cav2000.ps},
abstract = {In classical timed automata, as
defined by Alur and Dill and since
widely studied, the only operation allowed to
modify the clocks is the
reset operation. For instance, a clock can
neither be set to a
non-null constant value, nor be set to the value
of another clock nor,
in a non-deterministic way, to some value lower
or higher than a given
constant. In this paper we study in details such
updates.\par
We characterize in a thin way the frontier
between decidability and
undecidability. Our main contributions are the
following:\par
1)~We exhibit many classes of updates for which
emptiness is
undecidable. These classes depend on the clock
constraints that are
used ---~diagonal-free or not~--- whereas it is
well-known that these
two kinds of constraints are equivalent for
classical timed
automata.\par
2)~We propose a generalization of the region
automaton proposed by Alur
and Dill, allowing to handle larger classes of
updates. The
complexity of the decision procedure remains
PSPACE-complete.}
}
@article{SC-LP-CJ-00,
publisher = {Oxford University Press},
journal = {The Computer Journal},
author = {Christensen, S{\o}ren and Petrucci, Laure},
title = {Modular Analysis of {P}etri Nets},
volume = {43},
number = {3},
pages = {224-242},
year = {2000},
missingmonth = {},
missingnmonth = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CP-COMPJ00.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CP-COMPJ00.ps}
}
@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}
}
@phdthesis{THESE-SUTRE-2000,
author = {Sutre, Gr{\'e}goire},
title = {Abstraction et acc{\'e}l{\'e}ration de syst{\`e}mes
infinis},
year = {2000},
month = oct,
type = {Th{\`e}se de doctorat},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Sutre-these.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Sutre-these.ps},
lsv-lang = {FR}
}
@inproceedings{VGLPAK:BDDinCoq,
address = {Penang, Malaysia},
month = nov,
year = 2000,
volume = 1961,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {He, Jifeng and Sato, Masahito},
acronym = {{ASIAN} 2000},
booktitle = {{P}roceedings of the 6th {A}sian
{C}omputing {S}cience {C}onference
({ASIAN} 2000)},
author = {Verma, Kumar N. and Goubault{-}Larrecq, Jean and
Prasad, Sanjiva and Arun{-}Kumar, S.},
title = {Reflecting {BDD}s in {C}oq},
pages = {162-181},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/VGPA-asian2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/VGPA-asian2000.ps}
}
@article{VP-fourth-99,
publisher = {Cambridge University Press},
journal = {Mathematical Structures in Computer Science},
author = {Padovani, Vincent},
title = {Decidability of Fourth-Order Matching},
volume = {10},
number = {3},
pages = {361-372},
year = {2000},
month = jun
}
@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}
}
@mastersthesis{boisseau-dea,
author = {Boisseau, Alexandre},
title = {V{\'e}rification de protocoles cryptographiques},
year = {2000},
month = sep,
type = {Rapport de {DEA}},
school = {{DEA} Programmation, Paris, France},
lsv-lang = {FR}
}
@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{comon00ic2,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Comon, Hubert and Nieuwenhuis, Robert},
title = {Inductive Proofs = {I}-Axiomatization + First-Order
Consistency},
volume = {159},
number = {1-2},
pages = {151-186},
year = {2000},
month = may # {-} # jun,
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-1998-9.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-1998-9.rr.ps}
}
@inproceedings{comon2000csl,
address = {Fischbachau, Germany},
month = aug,
year = 2000,
volume = 1862,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Clote, Peter and Schwichtenberg, Helmut},
acronym = {{CSL} 2000},
booktitle = {{P}roceedings of the 14th {I}nternational
{W}orkshop on {C}omputer {S}cience {L}ogic
({CSL} 2000)},
author = {Comon, Hubert and Cortier, V{\'e}ronique},
title = {Flatness is not a Weakness},
pages = {262-276},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComCor-csl2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComCor-csl2000.ps}
}
@article{comon97ic,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Comon, Hubert},
title = {Sequentiality, Monadic Second Order Logic and Tree
Automata},
volume = {157},
number = {1-2},
pages = {25-51},
year = {2000},
month = feb # {-} # mar,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-sequentiality-ic.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/
Com-sequentiality-ic.ps}
}
@mastersthesis{duflot-dea,
author = {Duflot, Marie},
title = {Configurations r{\'e}currentes pour les anneaux de
processus --- {A}pplication {\`a}
l'auto-stabilisation},
year = {2000},
month = sep,
type = {Rapport de {DEA}},
school = {{DEA} Algorithmique, Paris, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Duflot-dea.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Duflot-dea.ps},
lsv-lang = {FR}
}
@inproceedings{finkel-leroux-vcl2000,
address = {London, UK},
month = jul,
year = 2000,
publisher = {University of Southampton, Southampton, UK},
editor = {Leuschel, Michael and Podelski, Andreas and
Ramakrishnan, C. R. and Ultes{-}Nitsche, Ulrich},
acronym = {{VCL} 2000},
booktitle = {{P}roceedings of the {I}nternational
{W}orkshop on {V}erification and
{C}omputational {L}ogic
({VCL} 2000)},
author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me},
title = {A Finite Covering Tree for Analysing Entropic
Broadcast Protocols},
nopages = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FinLer-vcl2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FinLer-vcl2000.ps}
}
@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}
}
@mastersthesis{markey-dea,
author = {Markey, Nicolas},
title = {Complexit{\'e} de la logique temporelle avec
pass{\'e}},
year = {2000},
month = jun,
type = {Rapport de {DEA}},
school = {{DEA} Algorithmique, Paris, France},
nops = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2000-11.rr.ps},
nopsgz = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PSGZ/
rr-lsv-2000-11.rr.ps.gz},
lsv-lang = {FR}
}
@misc{note-EVA-nov-2000,
author = {Boisseau, Alexandre and Jacquemard, Florent and
Le{ }M{\'e}tayer, Daniel},
title = {Exemple de mod{\'e}lisation de protocoles
cryptographiques},
year = {2000},
month = nov,
howpublished = {Projet EVA, note interne},
lsv-lang = {FR}
}
@phdthesis{preston-these-2000,
author = {Nicky Williams},
missingauthor = {on met pas son nom complet ?},
title = {Application des sp{\'e}cifications alg{\'e}briques
{\`a} la
r{\'e}tro-ing{\'e}nierie de codes {F}ortran},
year = {2000},
month = feb,
type = {Th{\`e}se de doctorat},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Williams-these.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Williams-these.ps},
lsv-lang = {FR}
}
@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{fl:hcmc,
author = {Laroussinie, Fran{\c{c}}ois},
title = {{HCMC}: {A}n Extension of {CMC} for
Hybrid Systems},
year = {2000},
howpublished = {Available at
\url{http://www.lsv.ens-cachan.fr/~fl/cmcweb.html}},
url = {http://www.lsv.ens-cachan.fr/~fl/cmcweb.html},
note = {See~\cite{CasLar-cav2000} for description.
Written in C++ (about 26000 lines)}
}
@misc{stabilo,
author = {Nilsson, Ulf and Duflot, Marie and Fribourg, Laurent},
title = {{STABILO}, a tool computing inevitable configurations
in distributed protocols},
year = {2000},
month = nov,
note = {See description in~\cite{DFN-concur-2001}.
Written in PROLOG (about 500 lines on top of
Gertjan van Noord's finite automata package)}
}
@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}
}
@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.",
}}
This file was generated by bibtex2html 1.98.