@article{BP-JALC2002,
journal = {Journal of Automata, Languages and Combinatorics},
author = {Bouyer, Patricia and Petit, Antoine},
title = {A {K}leene{\slash}B{\"u}chi-like Theorem for Clock Languages},
volume = {7},
number = {2},
pages = {167-186},
year = {2002},
missingmonth = {},
missingnmonth = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BP-JALC2001.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BP-JALC2001.ps},
abstract = {We propose in this paper a
generalization of the famous Kleene\slash B{\"u}chi's
theorem on formal languages, one of the
cornerstones of theoretical
computer science, to the timed model of clock
languages. These
languages extend the now classical timed
languages introduced by Alur
and Dill as a suitable model of real-time
systems. As a corollary of
our main result, we get a simple algebraic
characterization of timed
languages recognized by (updatable) timed
automata.}
}
@article{BST-FAC2002,
publisher = {Springer},
journal = {Formal Aspects of Computing},
author = {Bidoit, Michel and Sannella, Donald and
Tarlecki, Andrzej},
title = {Architectural Specifications in {CASL}},
volume = {13},
number = {3-5},
pages = {252-273},
year = {2002},
month = jul,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BST-FAC2002.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BST-FAC2002.ps},
doi = {10.1007/s001650200012}
}
@inproceedings{BST-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 = {Bidoit, Michel and Sannella, Donald and
Tarlecki, Andrzej},
title = {Global Development via Local Observational
Construction Steps},
pages = {1-24},
note = {Invited paper},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BST-MFCS02.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BST-MFCS02.ps}
}
@mastersthesis{Baclet-dea,
author = {Baclet, Manuel},
title = {Langages de donn{\'e}es},
type = {Rapport de {DEA}},
year = {2002},
month = sep,
school = {{DEA} Algorithmique, Paris, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Baclet-dea02.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Baclet-dea02.ps}
}
@mastersthesis{Bernat-dea,
author = {Bernat, Vincent},
title = {Transformation de l'authentification en secret},
type = {Rapport de {DEA}},
year = {2002},
month = sep,
school = {{DEA} Algorithmique, Paris, France}
}
@article{Bou-IPL2002,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Bouyer, Patricia},
title = {A Logical Characterization of Data Languages},
volume = {84},
number = {2},
pages = {75-85},
year = {2002},
month = oct,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bou-IPL2002.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bou-IPL2002.ps}
}
@inproceedings{DD-fsttcs2002,
address = {Kanpur, India},
month = dec,
year = 2002,
volume = 2556,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Agrawal, Manindra and Seth, Anil},
acronym = {{FSTTCS}'02},
booktitle = {{P}roceedings of the 22nd {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'02)},
author = {Demri, St{\'e}phane and D'Souza, Deepak},
title = {An Automata-Theoretic Approach to Constraint {LTL}},
pages = {121-132},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DemDsou-fsttcs02.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DemDsou-fsttcs02.ps}
}
@inproceedings{DFP-tcs2002,
address = {Montr{\'e}al, Qu{\'e}bec, Canada},
month = aug,
year = 2002,
volume = 223,
series = {IFIP Conference Proceedings},
publisher = {Kluwer Academic Publishers},
editor = {Baeza-Yates, Ricardo A. and Montanari, Ugo and
Santoro, Nicolas},
acronym = {{IFIP~TCS}'02},
booktitle = {{P}roceedings of the 2nd {IFIP} {I}nternational
{C}onference on {T}heoretical {C}omputer
{S}cience
({IFIP~TCS}'02)},
author = {Duflot, Marie and Fribourg, Laurent and
Picaronny, Claudine},
title = {Randomized Dining Philosophers without Fairness
Assumption},
pages = {169-180},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DFP-tcs02.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DFP-tcs02.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.}
}
@book{Demri::Orlowska02,
author = {Demri, St{\'e}phane and Or{\l}owska, Ewa},
title = {Incomplete Information: Structure, Inference,
Complexity},
series = {EATCS Monographs},
year = {2002},
missingnumber = {},
missingmonth = {},
missingnmonth = {},
publisher = {Springer},
isbn = {3-540-41904-7},
url = {http://www.springer.com/978-3-540-41904-7},
olderurl = {http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-41904-7}
}
@article{Demri::Sattler02,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {Demri, St{\'e}phane and Sattler, Ulrike},
title = {Automata-Theoretic Decision Procedures for Information
Logics},
volume = {53},
number = {1},
pages = {1-22},
year = {2002},
missingmonth = {},
missingnmonth = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ds-fund-02.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ds-fund-02.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ds-fund-02.pdf}
}
@inproceedings{FRSV-infinity2002,
address = {Brno, Czech Republic},
month = aug,
year = 2002,
number = 6,
volume = 68,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Ku{\v c}era, Anton{\'\i}n and Mayr, Richard},
acronym = {{INFINITY}'02},
booktitle = {{P}roceedings of the 4th {I}nternational
{W}orkshop on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'02)},
author = {Finkel, Alain and Raskin, Jean-Fran{\c{c}}ois and
Samuelides, Mathias and Van{~}Begin, Laurent},
title = {Monotonic Extensions of {P}etri Nets: Forward and
Backward Search Revisited},
pages = {121-144},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FRSVB-infinity2002.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FRSVB-infinity2002.ps}
}
@inproceedings{FinLer-fsttcs2002,
address = {Kanpur, India},
month = dec,
year = 2002,
volume = 2556,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Agrawal, Manindra and Seth, Anil},
acronym = {{FSTTCS}'02},
booktitle = {{P}roceedings of the 22nd {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'02)},
author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me},
title = {How To Compose {P}resburger-Accelerations:
Applications to Broadcast Protocols},
pages = {145-156},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2002-14.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2002-14.rr.ps}
}
@inproceedings{GLLN-csl2002,
address = {Edinburgh, Scotland, UK},
month = sep,
year = 2002,
volume = 2471,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Bradfield, Julian C.},
acronym = {{CSL}'02},
booktitle = {{P}roceedings of the 16th {I}nternational
{W}orkshop on {C}omputer {S}cience {L}ogic
({CSL}'02)},
author = {Goubault{-}Larrecq, Jean and Lasota, S{\l}awomir and
Nowak, David},
title = {Logical Relations for Monadic Types},
pages = {553-568},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GLLN-csl2002.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GLLN-csl2002.ps}
}
@inproceedings{HCFRS-latin2002,
address = {Cancun, Mexico},
month = apr,
year = 2002,
volume = 2286,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Rajsbaum, Sergio},
acronym = {{LATIN}'02},
booktitle = {{P}roceedings of the 5th {L}atin {A}merican
{S}ymposium on {T}heoretical {I}nformatics
({LATIN}'02)},
author = {Herbreteau, Fr{\'e}d{\'e}ric and Cassez, Franck and
Finkel, Alain and Roux, Olivier F.
and Sutre, Gr{\'e}goire},
title = {Verification of Embedded Reactive Fiffo Systems},
pages = {400-414},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HCFRS-latin2002.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HCFRS-latin2002.ps}
}
@incollection{HHB-OCL,
missingnmonth = {},
missingmonth = {},
year = 2002,
volume = 2263,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Clark, Tony and Warmer, Jos},
booktitle = {{O}bject {M}odeling with the {OCL}~---
{T}he {R}ationale behind the {O}bject {C}onstraint {L}anguage},
author = {Hennicker, Rolf and Hu{\ss}mann, Heinrich and
Bidoit, Michel},
title = {On the Precise Meaning of {OCL} Constraints},
pages = {69-84},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HBB-oclBook.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HBB-oclBook.ps}
}
@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{JGL-csl2002,
address = {Edinburgh, Scotland, UK},
month = sep,
year = 2002,
volume = 2471,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Bradfield, Julian C.},
acronym = {{CSL}'02},
booktitle = {{P}roceedings of the 16th {I}nternational
{W}orkshop on {C}omputer {S}cience {L}ogic
({CSL}'02)},
author = {Goubault{-}Larrecq, Jean},
title = {Higher-Order Positive Set Constraints},
pages = {473-489},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2002-6.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2002-6.rr.ps}
}
@techreport{JGL:EVA:CPV/2,
author = {Goubault{-}Larrecq, Jean},
title = {Outils {CPV} et {CPV2}},
year = {2002},
month = may,
type = {Contract Report},
number = 8,
institution = {Projet RNTL~EVA},
oldhowpublished = {Rapport num{\'e}ro 8 du projet RNTL EVA},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EVA-TR8.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EVA-TR8.pdf},
note = {7 pages}
}
@article{JGL:JTIT,
address = {Warsaw, Poland},
publisher = {Instytut {\L}{\k a}csno{\'s}ci},
journal = {Journal of Telecommunications and
Information Technology},
author = {Goubault{-}Larrecq, Jean},
editor = {Goubault{-}Larrecq, Jean},
title = {Special Issue on Models and Methods for Cryptographic
Protocol Verification},
volume = {4/2002},
year = {2002},
missingmonth = {},
missingnmonth = {},
url = {http://www.nit.eu/archive?view=kwartalrok&rok=2002&kwartal=4}
}
@proceedings{JGL:SECI,
title = {{A}ctes du 1er {W}orkshop {I}nternational
sur la {S}{\'e}curit{\'e} des {C}ommunications
sur {I}nternet
({SECI}'02)},
booktitle = {{A}ctes du 1er {W}orkshop {I}nternational
sur la {S}{\'e}curit{\'e} des {C}ommunications
sur {I}nternet
({SECI}'02)},
editor = {Goubault{-}Larrecq, Jean},
publisher = {INRIA},
year = 2002,
month = sep,
address = {Tunis, Tunisia},
url = {http://www.lsv.ens-cachan.fr/~goubault/SECI-02/Final/actes-seci02/index.html}
}
@inproceedings{JGL:SECI:pirates,
address = {Tunis, Tunisia},
month = sep,
year = 2002,
publisher = {INRIA},
editor = {Goubault{-}Larrecq, Jean},
acronym = {{SECI}'02},
booktitle = {{A}ctes du 1er {W}orkshop {I}nternational
sur la {S}{\'e}curit{\'e} des {C}ommunications
sur {I}nternet
({SECI}'02)},
author = {Goubault{-}Larrecq, Jean},
title = {{V}{\'e}rification de protocoles cryptographiques: la
logique {\`a} la rescousse!},
pages = {119-152},
note = {Invited paper},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/JGL-seci.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/JGL-seci.ps}
}
@article{JGL:crypto:modeles,
address = {Bordeaux, France},
publisher = {Groupe Pr{\'e}ventique},
journal = {Ph{\oe}bus, la revue de la s{\^u}ret{\'e} de
fonctionnement},
author = {Goubault{-}Larrecq, Jean},
title = {{S}{\'e}curit{\'e}, mod{\'e}lisation et analyse de
protocoles cryptographiques},
missingpages = {??},
volume = {20},
year = {2002},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/DOC/GL-Phoebus2002.doc}
}
@techreport{JGL:dico:3.1,
author = {Goubault{-}Larrecq, Jean and
Pouzol, Jean-{\relax Ph}ilippe and Demri, St{\'e}phane
and M{\'e}, Ludovic and Carle, P.},
missingauthor = {},
title = {Langages de d{\'e}tection d'attaques par signatures},
year = {2002},
month = jun,
type = {Contract Report},
number = {(Sous-projet~3, livrable~1)},
institution = {Projet RNTL DICO},
oldhowpublished = {Sous-projet 3, livrable 1 du projet RNTL DICO. Version
1},
note = {30 pages}
}
@inproceedings{LK-JB-LP-ZQ-RK-DASC-02,
address = {Irvine, California, USA},
month = oct,
year = 2002,
volume = 1,
publisher = {{IEEE} Aerospace and Electronic Systems Society},
acronym = {{DASC}'02},
booktitle = {{P}roceedings of the 21st {IEEE}
{D}igital {A}vionics {S}ystems
{C}onference ({DASC}'02)},
author = {Kristensen, Lars M. and Billington, Jonathan and
Petrucci, Laure and
Qureshi, Zahid H. and Kiefer, R.},
missingauthor = {},
title = {Formal specification and analysis of airborne mission
systems},
pages = {4.D.4.1-4.D.4.13},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/KBPQK-DASC-02.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/KBPQK-DASC-02.ps}
}
@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.}
}
@inproceedings{LP-LK-JB-ZQ-CRPIT-02,
address = {Adelaide, Australia},
month = jun,
year = 2002,
volume = 12,
series = {Conferences in Research and Practice in Information
Technology},
publisher = {Australian Computer Society},
editor = {Lakos, Charles and Esser, Robert and
Kristensen, Lars M. and Billington, Jonathan},
booktitle = {{P}roceedings of the {W}orkshops on
{S}oftware {I}ngineering and {F}ormal
{M}ethods and
{F}ormal {M}ethods {A}pplied to
{D}efence {S}ystems},
author = {Petrucci, Laure and Kristensen, Lars M. and
Billington, Jonathan and
Qureshi, Zahid H.},
title = {Towards Formal Specification and Analysis of Avionics
Mission Systems},
pages = {95-104},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/PKBQ-CRPIT02.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/PKBQ-CRPIT02.ps}
}
@techreport{LSV:02:11,
author = {Goubault{-}Larrecq, Jean and Verma, Kumar N.},
title = {Alternating Two-Way {AC}-Tree Automata},
type = {Research Report},
number = {LSV-02-11},
year = {2002},
month = sep,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {21 pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2002-11.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2002-11.rr.ps}
}
@techreport{LSV:02:12,
author = {Fribourg, Laurent and Messika, St{\'e}phane and
Picaronny, Claudine},
title = {Traces of Randomized Distributed Algorithms as {G}ibbs
Fields},
type = {Research Report},
number = {LSV-02-12},
year = {2002},
month = sep,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {16 pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2002-12.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2002-12.rr.ps}
}
@techreport{LSV:02:13,
author = {Lasota, S{\l}awomir},
title = {A Polynomial-Time Algorithm for Deciding True
Concurrency Equivalences of {B}asic {P}arallel
{P}rocesses},
type = {Research Report},
number = {LSV-02-13},
year = {2002},
month = sep,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {16 pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2002-13.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2002-13.rr.ps}
}
@techreport{LSV:02:18,
author = {Goubault{-}Larrecq, Jean},
title = {Un algorithme pour l'analyse de logs},
type = {Research Report},
number = {LSV-02-18},
year = {2002},
month = nov,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {33 pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2002-18.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2002-18.rr.ps}
}
@techreport{LSV:02:3,
author = {Cortier, V{\'e}ronique},
title = {Observational Equivalence and Trace Equivalence in an
Extension of {S}pi-calculus. {A}pplication to
Cryptographic Protocols Analysis. {E}xtended Version},
type = {Research Report},
number = {LSV-02-3},
year = {2002},
month = mar,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {33 pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2002-3.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2002-3.rr.ps}
}
@techreport{LSV:02:4,
author = {Boisseau, Alexandre},
title = {Signatures {\'e}lectroniques de contrats},
type = {Research Report},
number = {LSV-02-4},
year = {2002},
month = apr,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {22 pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2002-4.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2002-4.rr.ps}
}
@techreport{LSV:02:7,
author = {Goubault{-}Larrecq, Jean},
title = {{SKInT} Labels},
type = {Research Report},
number = {LSV-02-7},
year = {2002},
month = jul,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {15 pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2002-7.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2002-7.rr.ps}
}
@techreport{LSV:02:8,
author = {Goubault{-}Larrecq, Jean},
title = {A Note on the Completeness of Certain Refinements of
Resolution},
type = {Research Report},
number = {LSV-02-8},
year = {2002},
month = jul,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {16 pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2002-8.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2002-8.rr.ps}
}
@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.}
}
@inproceedings{NM-express2002,
address = {Brno, Czech Republic},
month = aug,
year = 2002,
number = 2,
volume = 68,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Nestmann, Uwe and Panagaden, Prakash},
acronym = {{EXPRESS}'02},
booktitle = {{P}roceedings of the 9th {I}nternational
{W}orkshop on {E}xpressiveness in
{C}oncurrency
({EXPRESS}'02)},
author = {Markey, Nicolas},
title = {Past is for Free: {O}n the Complexity of Verifying
Linear Temporal Properties with Past},
pages = {87-104},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/NM-express2002.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/NM-express2002.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/NM-express2002.pdf},
doi = {10.1016/S1571-0661(05)80366-4},
abstract = {We study the complexity of satisfiability and model-checking of the linear-time
temporal logic with past~(PLTL). More precisely, we consider several fragments of PLTL,
depending on the allowed set of temporal modalities, the use of negations or the nesting
of future formulae into past formulae. Our~results show that {"}past is for free{"},
that is
it does not bring additional theoretical complexity, even for small fragments, and even
when nesting future formulae into past formulae. We~also remark that existential and
universal model-checking can have different complexity for certain fragments.}
}
@techreport{NowakDJJ:semddi2,
author = {Lazi{\'c}, Ranko and Nowak, David},
title = {On a Semantic Definition of Data Independence},
type = {Research Report},
number = {CS-RR-392},
year = {2002},
month = dec,
institution = {Department of Computer Science, University of
Warwick, UK},
note = {19 pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/RR-LazNow.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/RR-LazNow.ps}
}
@techreport{PKB-DSTO-02,
author = {Petrucci, Laure and Kristensen, Lars M. and
Billington, Jonathan},
title = {Modelling and Analysis of Airborne Mission Systems},
oldtitle = {[.]{F}inal report for phase 4 - {DSTO/UniSA} contract},
year = {2002},
month = oct,
type = {Final Report},
institution = {phase~4, {DSTO/UniSA} contract},
nmnote = {Voir ce que ca donne en sortie...},
note = {68 pages}
}
@techreport{PKGEDBA-DSTO-02,
author = {Petrucci, Laure and Kristensen, Lars M. and
Gallasch, Guy E. and
Elliot, M. and Dauchy, Pierre and
Billington, Jonathan and Aziz, M.},
missingauthor = {},
title = {Modelling and Analysis of Airborne Mission Systems},
oldtitle = {{F}inal report for phase 3 - {DSTO/UniSA} contract},
year = {2002},
month = aug,
type = {Contract Report},
number = {Final report for phase~3},
institution = {{DSTO/UniSA} contract},
note = {79 pages}
}
@phdthesis{THESE-BLANC-2002,
author = {Blanc, Benjamin},
title = {Prise en compte de principes architecturaux lors de la
formalisation des besoins},
year = {2002},
month = dec,
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/Blanc-these.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Blanc-these.ps}
}
@phdthesis{THESE-BOUYER-2002,
author = {Bouyer, Patricia},
title = {Mod{\`e}les et algorithmes pour la v{\'e}rification des
syst{\`e}mes temporis{\'e}s},
year = {2002},
month = apr,
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/PDF/Bouyer-these.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bouyer-these.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bouyer-these.ps}
}
@phdthesis{THESE-FLEURY-2002,
author = {Fleury, Emmanuel},
title = {Automates temporis{\'e}s avec mises {\`a} jour},
year = {2002},
month = dec,
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/Fleury-these.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Fleury-these.ps}
}
@phdthesis{THESE-LABROUE-2002,
author = {Labroue, Anne},
title = {{M}{\'e}thodes alg{\'e}briques pour la v{\'e}rification
des
syst{\`e}mes infinis},
year = {2002},
month = jan,
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/Labroue-these.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Labroue-these.ps}
}
@phdthesis{THESE-MAGNIETTE-2001,
author = {Magniette, Fr{\'e}d{\'e}ric},
title = {Preuves d'algorithmes auto-stabilisants},
year = {2002},
month = jun,
type = {Th{\`e}se de doctorat},
school = {Universit{\'e} Paris-Sud~11, Orsay, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/These-magniette.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/These-magniette.ps}
}
@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{acefl-JLAP,
publisher = {Elsevier Science Publishers},
journal = {Journal of Logic and Algebraic Programming},
author = {Aceto, Luca and Laroussinie, Fran{\c{c}}ois},
title = {Is Your Model Checker on Time? {O}n the Complexity of
Model Checking for Timed Modal Logics},
volume = {52-53},
pages = {7-51},
year = {2002},
month = aug,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/AceLar-JLAP.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/AceLar-JLAP.ps},
doi = {10.1016/S1567-8326(02)00022-X}
}
@mastersthesis{baudet02DEA,
author = {Baudet, Mathieu},
title = {Contr\^{o}le de ressource et {\'e}vitement des
interblocages sur la m{\'e}moire},
year = {2002},
month = sep,
type = {Rapport de {DEA}},
school = {{DEA} Programmation, Paris, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Baudet-dea02.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Baudet-dea02.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Baudet-dea02.pdf}
}
@inproceedings{bbp-rttools02,
address = {Copenhagen, Denmark},
month = aug,
year = 2002,
howpublished = {Technical Report 2002-025,
Department of Information Technology,
Uppsala University, Sweden},
publisher = {Uppsala University},
editor = {Petterson, Paul and Yi, Wang},
acronym = {{RT-TOOLS}'02},
booktitle = {{P}roceedings of the 2nd {W}orkshop
on {R}eal-{T}ime {T}ools
({RT-TOOLS}'02)},
author = {B{\'e}rard, B{\'e}atrice and Bouyer, Patricia and
Petit, Antoine},
title = {Analysing the {PGM} Protocol with {UPPAAL}},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/pgmfin.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/pgmfin.ps},
abstract = {Pragmatic General Multicast (PGM)
is a reliable multicast protocol,
designed to minimize both the probability of
negative acknowledgements
(NAK) implosion and the loading of the network
due to retransmissions
of lost packets. This protocol was presented to
the Internet
Engineering Task Force as an open reference
specification. \par
In this paper, we focus on the main reliability
property which PGM
intends to guarantee: a receiver either receives
all data packets from
transmissions and repairs or is able to detect
unrecoverable data
packet loss.\par
To this purpose, we propose a modelization of (a
simplified version
of) PGM via a network of timed automata. Using
Uppaal model-checker,
we then study the validity of the reliability
property above, which
turns out to not be always verified but to
depend of the values of
several parameters that we underscore.}
}
@phdthesis{berard-hab-02,
author = {B{\'e}rard, B{\'e}atrice},
title = {{V}{\'e}rification de mod{\`e}les temporis{\'e}s},
year = {2002},
month = apr,
type = {M{\'e}moire d'habilitation},
school = {Universit{\'e} Paris~7, Paris, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BB-habile.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BB-habile.ps}
}
@mastersthesis{bertrand2002,
author = {Bertrand, Nathalie},
title = {{V}{\'e}rification de canaux {\`a} pertes
stochastiques},
year = {2002},
month = sep,
type = {Rapport de {DEA}},
school = {{DEA} Algorithmique, Paris, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/NB-dea02.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/NB-dea02.ps}
}
@inproceedings{bh-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 = {Bidoit, Michel and Hennicker, Rolf},
title = {On the Integration of Observability and Reachability
Concepts},
pages = {21-36},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BidHenFossacs02SHORT.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/
BidHenFossacs02SHORT.ps}
}
@article{bid-etalias-casl-tcs,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Astesiano, Egidio and Bidoit, Michel and
Kirchner, H{\'e}l{\`e}ne
and Krieg-Br{\"u}ckner, Bernd and Mosses, Peter D. and
Sannella, Donald and Tarlecki, Andrzej},
title = {{CASL}: {T}he {C}ommon {A}lgebraic {S}pecification
{L}anguage},
volume = {286},
number = {2},
pages = {153-196},
year = {2002},
month = sep,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CASL-TCS01.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CASL-TCS01.ps}
}
@article{comon02jtit,
address = {Warsaw, Poland},
publisher = {Instytut {\L}{\k a}csno{\'s}ci},
journal = {Journal of Telecommunications and
Information Technology},
author = {Comon, Hubert and Shmatikov, Vitaly},
title = {Is it Possible to Decide whether a Cryptographic
Protocol is Secure or not?},
volume = {4/2002},
year = {2002},
pages = {5-15},
missingmonth = {},
missingnmonth = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JTIT-CS.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JTIT-CS.pdf}
}
@article{cor-ITA,
journal = {Informatique Th\'eorique et Applications},
author = {Cortier, V{\'e}ronique},
title = {About the Decision of Reachability for Register
Machines},
volume = {36},
number = {4},
pages = {341-358},
year = {2002},
month = oct # {-} # dec,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Cor-ITA.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Cor-ITA.ps}
}
@techreport{cortier-securify-eva7,
author = {Cortier, V{\'e}ronique},
title = {Outil de v{\'e}rification {SECURIFY}},
year = {2002},
month = may,
type = {Contract Report},
number = 7,
institution = {projet RNTL~EVA},
note = {6 pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EVA-TR7.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EVA-TR7.pdf}
}
@inproceedings{lasota-concur2002,
address = {Brno, Czech Republic},
month = aug,
year = 2002,
volume = 2421,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Brim, Lubos and Jan{\v c}ar, Petr and
K{\v{r}}et{\'i}nsk{\'y}, Mojm{\'i}r and Ku{\v c}era, Anton{\'\i}n},
acronym = {{CONCUR}'02},
booktitle = {{P}roceedings of the 13th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'02)},
author = {Lasota, S{\l}awomir},
title = {Decidability of Strong Bisimilarity for Timed {BPP}},
pages = {562-578},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Las-concur2002.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Las-concur2002.ps}
}
@mastersthesis{messika-dea,
author = {Messika, St{\'e}phane},
title = {{V}{\'e}rification param{\'e}tr{\'e}e de r{\'e}seaux
{\`a} processus
probabiliste. {A}pplication du th{\'e}or{\`e}me de
{H}ammersley
et {C}lifford aux algorithmes distribu{\'e}s},
year = {2002},
month = sep,
type = {Rapport de {DEA}},
school = {{DEA} Logique et Fondements de l'Informatique, Paris,
France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Messika-dea02.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Messika-dea02.ps}
}
@phdthesis{petrucci-hab-02,
author = {Petrucci, Laure},
title = {Mod{\'e}lisation, v{\'e}rification et applications},
year = {2002},
month = dec,
type = {M{\'e}moire d'habilitation},
school = {Universit{\'e} d'{\'E}vry, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LP-habile.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LP-habile.ps}
}
@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}
}
@misc{securify1,
author = {Cortier, V{\'e}ronique},
title = {{Securify} version 1},
year = {2002},
howpublished = {Available at
\url{http://www.lsv.ens-cachan.fr/~cortier/EVA/securify.tar.gz}},
note = {Started 2001. See~\cite{cortier-securify-eva7} for
description. Written in Caml (about 3200 lines)}
}
@mastersthesis{zhang2002,
author = {Zhang, Yu},
title = {Logical Relations For Names},
year = {2002},
month = sep,
type = {Rapport de {DEA}},
school = {{DEA} Programmation, Paris, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ZY-dea02.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ZY-dea02.ps}
}
@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.