@inproceedings{BCFL-gdv04,
address = {Boston, Massachusetts, USA},
month = feb,
year = {2005},
number = 1,
volume = 119,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {De Alfaro, Luca},
acronym = {{GDV}'04},
booktitle = {{P}roceedings of the {W}orkshop on
{G}ames in {D}esign and {V}erification
({GDV}'04)},
author = {Bouyer, Patricia and Cassez, Franck and
Fleury, Emmanuel and
Larsen, Kim G.},
title = {Synthesis of Optimal Strategies Using {HyTech}},
pages = {11-31},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFL-gdv04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFL-gdv04.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCFL-gdv04.ps},
doi = {10.1016/j.entcs.2004.07.006},
abstract = {Priced timed (game) automata extend timed
(game) automata with costs on both locations and
transitions. The problem of synthesizing an optimal
winning strategy for a priced timed game under some
hypotheses has been shown decidable in~[BCFL04]. In this
paper, we present an algorithm for computing the optimal
cost and for synthesizing an optimal strategy in case
there exists one. We also describe the implementation of
this algorithm with the tool HyTech and present an
example. }
}
@article{ComonCortier-TCS1,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Comon, Hubert and Cortier, V{\'e}ronique},
title = {Tree Automata with One Memory, Set Constraints and
Cryptographic Protocols},
year = {2005},
volume = 331,
number = 1,
pages = {143-214},
month = feb,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComonCortierTCS1.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComonCortierTCS1.ps},
doi = {10.1016/j.tcs.2004.09.036}
}
@inproceedings{DFH-avocs2004,
address = {London, UK},
month = may,
year = {2005},
number = 6,
volume = {128},
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Huth, Michael R. A.},
acronym = {{AVoCS}'04},
booktitle = {{P}roceedings of the 4th {I}nternational
{W}orkshop on {A}utomated {V}erification
of {C}ritical {S}ystems
({AVoCS}'04)},
author = {Duflot, Marie and Fribourg, Laurent and
H{\'e}rault, {\relax Th}omas and
Lassaigne, Richard and Magniette, Fr{\'e}d{\'e}ric
and Messika, St{\'e}phane and
Peyronnet, Sylvain and Picaronny, Claudine},
title = {Probabilistic Model Checking of the {CSMA/CD} Protocol
Using {PRISM} and {APMC}},
pages = {195-214},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFH-avocs2004.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFH-avocs2004.pdf},
doi = {10.1016/j.entcs.2005.04.012}
}
@inproceedings{DFV-avocs04,
address = {London, UK},
month = may,
year = {2005},
number = 6,
volume = {128},
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Huth, Michael R. A.},
acronym = {{AVoCS}'04},
booktitle = {{P}roceedings of the 4th {I}nternational
{W}orkshop on {A}utomated {V}erification
of {C}ritical {S}ystems
({AVoCS}'04)},
author = {Darlot, {\relax Ch}ristophe and Finkel, Alain and Van{~}Begin, Laurent},
title = {About {F}ast and {TReX} Accelerations},
pages = {87-103},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFV-avocs04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFV-avocs04.pdf},
doi = {10.1016/j.entcs.2005.04.006}
}
@inproceedings{FGRV-express04,
address = {London, UK},
month = apr,
year = 2005,
number = 2,
volume = 128,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Baeten, Jos and Corradini, Flavio},
acronym = {{EXPRESS}'04},
booktitle = {{P}roceedings of the 11th {I}nternational
{W}orkshop on {E}xpressiveness in
{C}oncurrency
({EXPRESS}'04)},
author = {Finkel, Alain and Geeraerts, Gilles and Raskin, Jean-Fran{\c{c}}ois and
Van{~}Begin, Laurent},
title = {On the Omega-Language Expressive Power of Extended
{P}etri Nets},
pages = {87-101},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGRV-express04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGRV-express04.pdf},
doi = {10.1016/j.entcs.2004.11.030}
}
@article{FL-IPL04,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me},
title = {The Convex Hull of a Regular Set of Integer Vectors is
Polyhedral and Effectively Computable},
year = {2005},
month = oct,
volume = 96,
number = 1,
pages = {30-35},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FL-ipl05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FL-ipl05.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FL-ipl05.ps},
doi = {10.1016/j.ipl.2005.04.004},
abstract = {Number Decision Diagrams (NDD)
provide a natural finite symbolic representation
for regular set of integer vectors encoded as
strings of digit vectors (least or most
significant digit first). The convex hull of the
set of vectors represented by a~NDD is proved to
be an effectively computable convex
polyhedron.}
}
@article{GLRV:acm,
publisher = {Elsevier Science Publishers},
journal = {Journal of Logic and Algebraic Programming},
author = {Goubault{-}Larrecq, Jean and Roger, Muriel and
Verma, Kumar N.},
title = {Abstraction and Resolution Modulo~{AC}: {H}ow to
Verify
{D}iffie-{H}ellman-like Protocols Automatically},
volume = 64,
number = 2,
pages = {219-251},
year = {2005},
month = aug,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GLRV-acm.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GLRV-acm.ps},
doi = {10.1016/j.jlap.2004.09.004}
}
@article{JGL:val:ext,
publisher = {Cambridge University Press},
journal = {Mathematical Structures in Computer Science},
author = {Goubault{-}Larrecq, Jean},
title = {Extensions of Valuations},
year = {2005},
volume = 15,
number = 2,
pages = {271-297},
month = apr,
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2002-17.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2002-17.rr.ps},
doi = {10.1017/S096012950400461X}
}
@inproceedings{KremerRyan2004,
address = {London, UK},
month = may,
year = 2005,
number = 5,
volume = {128},
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Focardi, Riccardo and Zavattaro, Gianluigi},
acronym = {{SecCo}'04},
booktitle = {{P}roceedings of the 2nd {I}nternational
{W}orkshop on {S}ecurity {I}ssues in
{C}oordination {M}odels, {L}anguages and
{S}ystems ({SecCo}'04)},
author = {Kremer, Steve and Ryan, Mark D.},
title = {Analysing the Vulnerability of Protocols to Produce
Known-pair and Chosen-text Attacks},
pages = {84-107},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Kremer-secco04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Kremer-secco04.pdf},
doi = {10.1016/j.entcs.2004.11.043},
abstract = {In this paper we report on an analysis
for finding known-pair and chosen-text attacks in
protocols. As these attacks are at the level of
blocks, we extend the attacker by special capabilities
related to block chaining techniques. The analysis is
automated using Blanchet's protocol verifier and
illustrated on two well-known protocols, the
Needham-Schroeder-Lowe public-key protocol as well as
the Needham-Schroeder symmetric-key protocol. On the
first protocol, we show how the special intruder
capabilities related to chaining may compromise the
secrecy of nonces and that chosen-ciphertext attacks
are possible. We propose two modified versions of the
protocol which strengthen its security. We then
illustrate known-pair and chosen-plaintext attacks on
the second protocol.}
}
@inproceedings{couvreur-ciaa04,
address = {Kingston, Ontario, Canada},
month = jan,
year = 2005,
volume = 3317,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Domaratzki, Michael and Okhotin, Alexander and
Salomaa, Kai and Yu, Sheng},
acronym = {{CIAA}'04},
booktitle = {{R}evised {S}elected {P}apers of the 9th {I}nternational
{C}onference on {I}mplementation and
{A}pplication of {A}utomata
({CIAA}'04)},
author = {Couvreur, Jean-Michel},
title = {A {BDD}-like Implementation of an Automata Package},
pages = {310-311},
doi = {10.1007/b105090}
}
@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{baudet-ccs2005,
address = {Alexandria, Virginia, USA},
month = nov,
year = 2005,
publisher = {ACM Press},
acronym = {{CCS}'05},
booktitle = {{P}roceedings of the 12th {ACM} {C}onference
on {C}omputer and {C}ommunications {S}ecurity
({CCS}'05)},
author = {Baudet, Mathieu},
title = {Deciding Security of Protocols against Off-line Guessing
Attacks},
pages = {16-25},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Baudet_CCS05revised.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Baudet_CCS05revised.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Baudet_CCS05revised.ps},
doi = {10.1145/1102120.1102125},
abstract = {We provide an effective procedure for
deciding the existence of off-line guessing attacks
on security protocols, for a bounded number of
sessions.\par
The procedure consists of a constraint solving
algorithm for determining satisfiability and
equivalence of a class of second-order E-unification
problems, where the equational theory~E is presented
by a convergent subterm rewriting system.\par
To the best of our knowledge, this is the first
decidability result to use the generic definition of
off-line guessing attacks due to Corin~\emph{et al.}
based on static equivalence in the applied
pi-calculus.}
}
@inproceedings{BCM05-fsttcs,
address = {Hyderabad, India},
month = dec,
year = 2005,
volume = 3821,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ramanujam, R. and Sen, Sandeep},
acronym = {{FSTTCS}'05},
booktitle = {{P}roceedings of the 25th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'05)},
author = {Bouyer, Patricia and Chevalier, Fabrice and
Markey, Nicolas},
title = {On the Expressiveness of {TPTL} and~{MTL}},
pages = {432-443},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCM-fsttcs05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCM-fsttcs05.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCM-fsttcs05.ps},
doi = {10.1007/11590156_35},
abstract = {TPTL and MTL are two classical timed extensions of LTL.
In this paper, we positively answer a 15-year-old conjecture that TPTL
is strictly more expressive than MTL. But we show that, surprisingly,
the TPTL formula proposed by Alur and Henzinger for witnessing
this conjecture can be expressed in MTL. More generally, we show that
TPTL formulae using only the F modality can be translated into MTL.}
}
@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.}
}
@inproceedings{BBGRS-ETFA05,
address = {Catania, Italy},
month = sep,
year = 2005,
publisher = {{IEEE} Industrial Electronics Society},
editor = {Lo Bello, Lucia and Sauter, Thilo},
acronym = {{ETFA}'05},
booktitle = {{P}roceedings of the 10th {IEEE} {I}nternational
{C}onference on {E}merging {T}echnologies and {F}actory
{A}utomation ({ETFA}'05)},
author = {Bel{ }mokadem, Houda and B{\'e}rard, B{\'e}atrice and
Gourcuff, Vincent and Roussel, Jean-Marc and
De{~}Smet, Olivier},
title = {Verification of a timed multitask system with {U}ppaal},
pages = {347-354},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ETFA05-FV.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ETFA05-FV.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ETFA05-FV.ps},
abstract = {Since it is an important issue for users and system designers,
verification of PLC programs has already been studied in various
contexts, mostly for untimed programs. More recently, timed features
were introduced and modeled with timed automata. In this case study,
we consider a part of the so-called MSS (Mecatronic Standard System)
platform from Bosh Group, a framework where time aspects are
combined with multitask programming. Our model for station~2 of the
MSS platform is a network of timed automata, including automata for
the operative part and for the control program, written in
\emph{Ladder Diagram}. This model is constrained with atomicity
hypotheses concerning program execution and model
checking of a reaction time property is performed with the
tool~{\scshape Uppaal}.}
}
@inproceedings{BC-icmtd05,
address = {Giens, France},
nmnote = {Informal proceedings. Selected papers to appear in a journal},
month = may,
year = 2005,
acronym = {{ICMTD}'05},
booktitle = {Proceedings of the 1st {I}nternational {C}onference on
{M}emory {T}echnology and {D}esign
({ICMTD}'05)},
author = {Baclet, Manuel and Chevallier, R{\'e}my},
title = {Timed Verification of the {SPSMALL} Memory},
pages = {89-92},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC05-spsmall.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC05-spsmall.pdf},
abstract = {The aim of the paper is to verify a small
synchronous memory component with the real-time
model checker Uppaal, taking into account the
electrical propagation delays through gates and
along wires.},
missingdoi = {}
}
@inproceedings{BH-ICTAC05,
address = {Hanoi, Vietnam},
month = oct,
year = 2005,
volume = 3722,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hung, Dang Van and Wirsing, Martin},
acronym = {{ICTAC}'05},
booktitle = {{P}roceedings of the 2nd {I}nternational {C}olloquium on
{T}heoretical {A}spects of {C}omputing ({ICTAC}'05)},
author = {Bidoit, Michel and Hennicker, Rolf},
title = {Externalized and Internalized Notions of Behavioral
Refinement},
pages = {334-350},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ictac05-ID128.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ictac05-ID128.pdf},
doi = {10.1007/11560647_22},
abstract = {Many different behavioral refinement notions for algebraic
specifications have been proposed in the literature but the relationship
between the various concepts is still unclear. In this paper we provide a
classification and a comparative study of behavioral refinements according
to two directions, the externalized approach which uses an explicit
behavioral abstraction operator that is applied to the specification to
be implemented, and the internalized approach which uses a built-in
behavioral semantics of specifications. We show that both concepts are
equivalent under suitable conditions. The formal basis of our study is
provided by the COL institution (constructor-based observational logic).
Hence, as a side-effect of our study on internalized behavioral refinements,
we introduce also a novel concept of behavioral refinement for
COL-specifications.}
}
@misc{bouyer-jsi05,
author = {Bouyer, Patricia},
title = {Timed Automata and Extensions: Decidability Limits},
year = 2005,
month = mar,
howpublished = {Invited talk, 5{\`e}mes Journ{\'e}es Syst{\`e}mes Infinis ({JSI}'05),
Cachan, France}
}
@misc{bouyer-games05,
author = {Bouyer, Patricia},
title = {Synthesis of Timed Systems},
year = 2005,
month = mar,
howpublished = {Invited lecture, Spring School on Infinite Games and
Their Applications, Bonn, Germany}
}
@misc{bouyer-gdv05,
author = {Bouyer, Patricia},
title = {Partial Observation of Timed Systems},
year = 2005,
month = jul,
howpublished = {Invited talk, 2nd Workshop on Games in Design and
Verification, Edinburgh, Scotland}
}
@misc{gastin-wpv05,
author = {Gastin, Paul},
title = {On the synthesis of distributed controllers},
year = 2005,
month = nov,
howpublished = {Invited talk, Workshop Perspectives in
Verification, in honor of Wolfgang Thomas on the occasion of his
Doctorate Honoris Causa, Cachan, France}
}
@inproceedings{BCD-fossacs05,
address = {Edinburgh, Scotland, UK},
month = apr,
year = 2005,
volume = 3441,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Sassone, Vladimiro},
acronym = {{FoSSaCS}'05},
booktitle = {{P}roceedings of the 8th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'05)},
author = {Bouyer, Patricia and Chevalier, Fabrice and D'Souza, Deepak},
title = {Fault Diagnosis Using Timed Automata},
pages = {219-233},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/fossacs05-BCD.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/fossacs05-BCD.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/fossacs05-BCD.pdf},
doi = {10.1007/b106850},
abstract = {Fault diagnosis consists in
observing behaviours of systems, and in detecting
online whether an error has occurred or not. In the
context of discrete event systems this problem has
been well-studied, but much less work has been done
in the timed framework. In this paper, we consider
the problem of diagnosing faults in behaviours of
timed plants. We focus on the problem of
synthesizing fault diagnosers which are realizable
as deterministic timed automata, with the
motivation that such diagnosers would function as
efficient online fault detectors. We study two
classes of such mechanisms, the class of
deterministic timed automata~(DTA) and the class of
event-recording timed automata~(ERA). We show that
the problem of synthesizing diagnosers in each of
these classes is decidable, provided we are given a
bound on the resources available to the diagnoser.
We prove that under this assumption diagnosability
is 2EXPTIME-complete in the case of DTA's whereas
it becomes PSPACE-complete for ERA's.}
}
@inproceedings{BBBL-concur2005,
address = {San Francisco, California, USA},
month = aug,
year = 2005,
volume = 3653,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abadi, Mart{\'\i}n and de Alfaro, Luca},
acronym = {{CONCUR}'05},
booktitle = {{P}roceedings of the 16th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'05)},
author = {Bel{ }mokadem, Houda and B{\'e}rard, B{\'e}atrice and
Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois},
title = {A New Modality for Almost Everywhere Properties in
Timed Automata},
pages = {110-124},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBL05-concur.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBL05-concur.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBBL05-concur.ps},
doi = {10.1007/11539452_12},
abstract = {The context of this study is timed temporal logics
for timed automata. In this paper, we propose an extension of the
classical logic TCTL with a new Until modality, called {"}Until
almost everywhere{"}. In the extended logic, it is possible, for
instance, to express that a property is true at all positions of
all runs, except on a negligible set of positions. Such
properties are very convenient, for example in the framework of
boolean program verification, where transitions result from
changing variable values. We investigate the expressive power of
this modality and in particular, we prove that it cannot be
expressed with classical TCTL modalities. However, we show that
model-checking the extended logic remains PSPACE-complete as
for~TCTL.}
}
@inproceedings{BCL-concur2005,
address = {San Francisco, California, USA},
month = aug,
year = 2005,
volume = 3653,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abadi, Mart{\'\i}n and de Alfaro, Luca},
acronym = {{CONCUR}'05},
booktitle = {{P}roceedings of the 16th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'05)},
author = {Bouyer, Patricia and Cassez, Franck and Laroussinie,
Fran{\c{c}}ois},
title = {Modal Logics for Timed Control},
pages = {81-94},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCL05-concur.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCL05-concur.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCL05-concur.ps},
doi = {10.1007/11539452_10},
abstract = {In this paper we use the timed
modal logic \(L_{\nu}\) to specify control
objectives for timed plants. We show that the
control problem for a large class of objectives
can be reduced to a model-checking problem for
an extension (\(L_{\nu}^{\mathrm{\small cont}}\))
of the logic \(L_{\nu}\) with a new modality.
\par
More precisely we define a fragment of~\(L_{\nu}\),
namely \(L_{\nu}^{\mathrm{\small det}}\),
such that any control objective
of~\(L_{\nu}^{\mathrm{\small det}}\)
can be translated into an \(L_{\nu}^{\mathrm{\small cont}}\)
formula that holds for the plant if and only if
there is a controller that can enforce the
control objective.
\par
We also show that the new modality
of~\(L_{\nu}^{\mathrm{\small cont}}\)
strictly increases the expressive power
of~\(L_{\nu}\), while model-checking
of~\(L_{\nu}^{\mathrm{\small cont}}\) remains
EXPTIME-complete. }
}
@inproceedings{BLR-formats2005,
address = {Uppsala, Sweden},
month = nov,
year = 2005,
volume = 3829,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Pettersson, Paul and Yi, Wang},
acronym = {{FORMATS}'05},
booktitle = {{P}roceedings of the 3rd {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'05)},
author = {Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois and
Reynier, Pierre-Alain},
title = {Diagonal Constraints in Timed Automata: Forward
Analysis of Timed Systems},
pages = {112-126},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLR05-DBM.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLR05-DBM.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BLR05-DBM.ps},
doi = {10.1007/11603009_10},
abstract = {Timed automata (TA) are a
widely used model for real-time systems. Several
tools are dedicated to this model, and they mostly
implement a forward analysis for checking
reachability properties. Though diagonal
constraints do not add expressive power to
classical~TA, the standard forward analysis
algorithm is not correct for this model. In this
paper we survey several approaches to handle
diagonal constraints and propose a
refinement-based method for patching the usual
algorithm: erroneous traces found by the classical
algorithm are analyzed, and used for refining the
model.}
}
@inproceedings{BCK-ICALP2005,
address = {Lisboa, Portugal},
month = jul,
year = 2005,
volume = {3580},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Caires, Lu{\'\i}s and Italiano, Giuseppe F. and
Monteiro, Lu{\'\i}s and Palamidessi, Catuscia and Yung, Moti},
acronym = {{ICALP}'05},
booktitle = {{P}roceedings of the 32nd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming
({ICALP}'05)},
author = {Baudet, Mathieu and Cortier, V{\'e}ronique and Kremer,Steve},
title = {Computationally Sound Implementations of Equational
Theories against Passive Adversaries},
pages = {652-663},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCK-icalp05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCK-icalp05.pdf},
doi = {10.1007/11523468_53},
abstract = {In this paper we study the link between formal and
cryptographic models for security protocols in the presence of a passive
adversary. In contrast to other works, we do not consider a fixed set of
primitives but aim at results for an arbitrary equational theory. We
define a framework for comparing a cryptographic implementation and its
idealization w.r.t.\ various security notions. In particular, we
concentrate on the computationnal soundness of static equivalence, a
standard tool in cryptographic \(\pi\)-calculi. We present a soundness
criterion, which for many theories is not only sufficient but also
necessary. Finally, we establish new soundness results for the Exclusive
Or, as well as a theory of ciphers and lists.}
}
@book{lncs3426,
editor = {Bouyssonouse, Bruno and Sifakis, Joseph},
title = {Embedded Systems Design: The {ARTIST} Roadmap for Research and
Development},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
volume = 3436,
year = 2005,
url = {http://www.springer.com/978-3-540-25107-3},
olderurl = {http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-25107-3},
isbn = {3-540-25107-3},
doi = {10.1007/b106761}
}
@inproceedings{ComDel-rta2005,
address = {Nara, Japan},
month = apr,
year = 2005,
volume = 3467,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Giesl, J{\"u}rgen},
acronym = {{RTA}'05},
booktitle = {{P}roceedings of the 16th {I}nternational
{C}onference on {R}ewriting {T}echniques
and {A}pplications
({RTA}'05)},
author = {Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie},
title = {The finite variant property: {H}ow to get rid of some
algebraic properties},
pages = {294-307},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/rta05-CD.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/rta05-CD.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/rta05-CD.pdf},
doi = {10.1007/b135673},
abstract = {We consider the following problem: Given a term
\(t\), a rewrite system \(\mathcal{R}\), a finite set
of equations \(E'\) such that \(\mathcal{R}\) is
convergent modulo~\(E'\), compute finitely many
instances of~\(t\): \(t_1,\ldots,t_n\) such that, for
every substitution~\(\sigma\), there is an index
\(i\) and a substitution~\(\theta\) such that \(
t\sigma\mathord{\downarrow}=_{E'} t_i\theta\) (where
\(t\sigma\mathord{\downarrow}\) is the normal form of
\(t\sigma\) w.r.t.~\(\mathcal{R}/E'\)). \par
The goal of this paper is to give equivalent (resp.
sufficient) conditions for the finite variant
property and to systematically investigate this
property for equational theories, which are relevant
to security protocols verification. For instance, we
prove that the finite variant property holds for
Abelian Groups, and a theory of modular
exponentiation and does not hold for the
theory~\textit{ACUNh} (Associativity, Commutativity,
Unit, Nilpotence, homomorphism).}
}
@article{CF-icomp05,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {C{\'e}c{\'e}, G{\'e}rard and Finkel, Alain},
title = {Verification of Programs with Half-Duplex Communication},
year = 2005,
month = nov,
volume = 202,
number = 2,
pages = {166-190},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CF-icomp05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CF-icomp05.pdf},
doi = {10.1016/j.ic.2005.05.006},
abstract = {We consider the analysis of infinite
\emph{half-duplex systems} made of finite state machines
that communicate over unbounded channels. The
half-duplex property for two machines and two
channels (one in each direction) says that each
reachable configuration has at most one channel
non-empty. We prove in this paper that such
half-duplex systems have a recognizable
reachability set. We show how to compute, in
polynomial time, a symbolic representation of this
reachability set and how to use that description to
solve several verification problems. Furthermore,
though the model of communicating finite state
machines is Turing-powerful, we prove that
membership of the class of half-duplex systems is
decidable. Unfortunately, the natural
generalization to systems with more than two
machines is Turing-powerful. We also prove that the
model-checking of those systems against PLTL
(Propositional Linear Temporal Logic) or CTL
(Computational Tree Logic) is undecidable. Finally,
we show how to apply the previous decidability
results to the Regular Model Checking. We propose a
new symbolic reachability semi-algorithm with
accelerations which successfully terminates on
half-duplex systems of two machines and some
interesting non-half-duplex systems.}
}
@misc{cortos05,
author = {Bouyer, Patricia and others},
title = {{ACI} {S}{\'e}curit{\'e} {I}nformatique {CORTOS}
<<~{C}ontrol and {O}bservation of {R}eal-{T}ime {O}pen
{S}ystems~>>~--- Rapport {\`a} mi-parcours},
year = 2005,
month = apr,
type = {Contract Report},
note = {6~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/cortos-MP.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/cortos-MP.pdf},
missingdoi = {}
}
@inproceedings{Cortos-MSR05-impl,
address = {Autrans, France},
month = oct,
year = 2005,
publisher = {Herm{\`e}s},
editor = {Alla, Hassane and Rutten, {\'E}ric},
acronym = {{MSR}'05},
booktitle = {{A}ctes du 5{\`e}me {C}olloque sur la
{M}od{\'e}lisation des {S}yst{\`e}mes
{R}{\'e}actifs
({MSR}'05)},
author = {Altisen, Karine and Markey, Nicolas and Reynier, Pierre-Alain and
Tripakis, Stavros},
title = {Impl{\'e}mentabilit{\'e} des automates temporis{\'e}s},
pages = {395-406},
nonote = {Invited paper},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-impl.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-impl.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MSR05-impl.ps},
abstract = {In this paper, we present the problem
of the implementability of timed automata. The
theoretical semantics of timed automata can not be
exactly implemented in practice, because computers
are digital and more or less precise; the properties
verified on a timed automaton are not necessarily
preserved when implementing it. We deal with two
approaches: the first one is based on the modeling of
the execution platform and the second studies an
enlarged semantics for timed automata that takes the
imprecision into account.}
}
@inproceedings{Cortos-MSR05-obs,
address = {Autrans, France},
month = oct,
year = 2005,
publisher = {Herm{\`e}s},
editor = {Alla, Hassane and Rutten, {\'E}ric},
acronym = {{MSR}'05},
booktitle = {{A}ctes du 5{\`e}me {C}olloque sur la
{M}od{\'e}lisation des {S}yst{\`e}mes
{R}{\'e}actifs
({MSR}'05)},
author = {Bouyer, Patricia and Chevalier, Fabrice and Krichen, Moez and
Tripakis, Stavros},
title = {Observation partielle des syst{\`e}mes temporis{\'e}s},
pages = {381-393},
nonote = {Invited paper},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-obs.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-obs.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MSR05-obs.ps},
abstract = {In this paper, we present the partial
observability constraint, which naturally appears when
modeling real-time systems. We have selected three
problems in which this hypothesis is fundamental but
leads to more difficult problems: control of timed
systems, fault diagnosis, and conformance testing. We
describe methods which can be used for solving such
problems. }
}
@inproceedings{Cortos-MSR05-control,
address = {Autrans, France},
month = oct,
year = 2005,
publisher = {Herm{\`e}s},
editor = {Alla, Hassane and Rutten, {\'E}ric},
acronym = {{MSR}'05},
booktitle = {{A}ctes du 5{\`e}me {C}olloque sur la
{M}od{\'e}lisation des {S}yst{\`e}mes
{R}{\'e}actifs
({MSR}'05)},
author = {Altisen, Karine and Bouyer, Patricia and Cachat, Thierry and
Cassez, Franck and Gardey, Guillaume},
title = {Introduction au contr{\^o}le des syst{\`e}mes temps-r{\'e}el},
pages = {367-380},
nonote = {Invited paper},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-control.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-control.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MSR05-control.ps},
abstract = {In this paper we give a quick overview
of the area of control of real-time systems.}
}
@misc{demri-RSFDGrC05,
author = {Demri, St{\'e}phane},
title = {On the complexity of information logics},
year = 2005,
month = aug,
howpublished = {Invited talk, Workshop on Logical and Algebraic
Foundations of Rough Sets, Regina, Canada}
}
@article{demri-JLC05,
publisher = {Oxford University Press},
journal = {Journal of Logic and Computation},
author = {Demri, St{\'e}phane},
title = {A reduction from {DLP} to~{PDL}},
year = 2005,
month = oct,
volume = 15,
number = 5,
pages = {767-785},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-jlc05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-jlc05.pdf},
doi = {10.1093/logcom/exi043},
abstract = {We present a reduction from a new logic extending van der Meyden's
dynamic logic of permission~(DLP) into propositional dynamic logic (PDL),
providing a 2EXPTIME decision procedure and showing that all the machinery
for~PDL can be reused for reasoning about dynamic policies. As a
side-effect, we establish that DLP is EXPTIME-complete. The logic we introduce
extends the logic~DLP so that the policy set can be updated depending on its
current value and such an update corresponds to add\slash delete transitions
in the model, showing similarities with van Benthem's sabotage modal logic.}
}
@article{ddn-jlli05,
publisher = {Kluwer Academic Publishers},
journal = {Journal of Logic, Language and Information},
author = {Demri, St{\'e}phane and de Nivelle, Hans},
title = {Deciding Regular Grammar Logics with Converse through
First-Order Logic},
volume = 14,
number = 3,
pages = {289-319},
year = {2005},
month = jun,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ddn-gf-issue.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ddn-gf-issue.pdf},
oldnote = {special issue dedicated to guarded logics.},
doi = {10.1007/s10849-005-5788-9},
abstract = {We provide a simple translation of the satisfiability problem for regular
grammar logics with converse into GF2 , which is the intersection of the guarded
fragment and the 2-variable fragment of first-order logic. The translation is theoretically
interesting because it translates modal logics with certain frame conditions into
first-order logic, without explicitly expressing the frame conditions. It is practically
relevant because it makes it possible to use a decision procedure for the guarded
fragment in order to decide regular grammar logics with converse. The class of
regular grammar logics includes numerous logics from various application domains.\par
A consequence of the translation is that the general satisfiability problem for
every regular grammar logics with converse is in~EXPTIME. This extends a previous
result of the first author for grammar logics without converse. Other logics that
can be translated into GF2 include nominal tense logics and intuitionistic logic.
In our view, the results in this paper show that the natural first-order fragment
corresponding to regular grammar logics is simply GF2 without extra machinery
such as fixed point-operators.}
}
@inproceedings{DZG05-aplas,
address = {Tsukuba, Japan},
month = nov,
year = 2005,
volume = 3780,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Yi, Kwangkeun},
acronym = {{APLAS}'05},
booktitle = {{P}roceedings of the 3rd {A}sian {S}ymposium
on {P}rogramming {L}anguages and {S}ystems
({APLAS}'05)},
author = {Dal Zilio, Silvano and Gascon, R{\'e}gis},
title = {Resource Bound Certification for a Tail-Recursive
Virtual Machine},
pages = {247-263},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DZG-APLAS05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DZG-APLAS05.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DZG-APLAS05.ps},
doi = {10.1007/11575467_17},
abstract = {We define a method to statically bound the size of values
computed during the execution of a program as a function of the size
of its parameters. More precisely, we consider bytecode programs that
should be executed on a simple stack machine with support for algebraic
data types, pattern-matching and tail-recursion. Our size verification
method is expressed as a static analysis, performed at the level
of the bytecode, that relies on machine-checkable certificates. We follow
here the usual assumption that code and certificates may be forged and
should be checked before execution.\par
Our approach extends a system of static analyses based on the notion
of quasi-interpretations that has already been used to enforce resource
bounds on first-order functional programs. This paper makes two additional
contributions. First, we are able to check optimized programs,
containing instructions for unconditional jumps and tail-recursive calls,
and remove restrictions on the structure of the bytecode that was imposed
in previous works. Second, we propose a direct algorithm that
depends only on solving a set of arithmetical constraints.}
}
@inproceedings{DG-concur2005,
address = {San Francisco, California, USA},
month = aug,
year = 2005,
volume = 3653,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abadi, Mart{\'\i}n and de Alfaro, Luca},
acronym = {{CONCUR}'05},
booktitle = {{P}roceedings of the 16th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'05)},
author = {Demri, St{\'e}phane and Gascon, R{\'e}gis},
title = {Verification of Qualitative
{\(\mathbb{\MakeUppercase{Z}}\)}-Constraints},
pages = {518-532},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-Concur05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-Concur05.pdf},
doi = {10.1007/11539452_39},
abstract = {We introduce an LTL-like logic with atomic formulae built
over a constraint language interpreting variables in~\(\mathbb{Z}\). The constraint
language includes periodicity constraints, comparison constraints of the
form \(x = y\) and \(x < y\), it is closed under Boolean operations and it
admits a restricted form of existential quantification. This is the largest
set of qualitative constraints over~\(\mathbb{Z}\) known so far, shown to admit a
decidable LTL extension. Such constraints are those used for instance
in calendar formalisms or in abstractions of counter automata by using
congruences modulo some power of two. Indeed, various programming
languages perform arithmetic operators modulo some integer. We show
that the satisfiability and model-checking problems (with respect to an
appropriate class of constraint automata) for this logic are decidable in
polynomial space improving significantly known results about its strict
fragments. As a by-product, LTL model-checking over integral relational
automata is proved complete for polynomial space which contrasts with
the known undecidability of its CTL counterpart.}
}
@inproceedings{DKR-FEE2005,
address = {Milan, Italy},
month = sep,
year = 2005,
optaddress = {},
acronym = {{FEE} 2005},
booktitle = {{P}roceedings of the {W}orkshop {F}rontiers in {E}lectronic
{E}lections ({FEE} 2005)},
author = {Delaune, St{\'e}phanie and Kremer, Steve and
Ryan, Mark D.},
title = {Receipt-Freeness: Formal Definition and Fault
Attacks (Extended Abstract)},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-fee05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-fee05.pdf},
preliminary-version-of = {DKR-csfw06}
}
@inproceedings{DLN-time05,
address = {Burlington, Vermont, USA},
month = jun,
year = 2005,
publisher = {{IEEE} Computer Society Press},
acronym = {{TIME}'05},
booktitle = {{P}roceedings of the 12th {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'05)},
author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko and
Nowak, David},
title = {On the Freeze Quantifier in Constraint {LTL}:
Decidability and Complexity},
pages = {113-121},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-03.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2005-03.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-03.pdf},
doi = {10.1109/TIME.2005.28},
abstract = {Constraint LTL, a generalization of LTL over Presburger
constraints, is often used as a formal language to specify the
behavior of operational models with constraints. The freeze
quantifier can be part of the language, as in some real-time
logics, but this variable-binding mechanism is quite general
and ubiquitous in many logical languages (first-order temporal
logics, hybrid logics, logics for sequence diagrams,
navigation logics, etc.). We show that Constraint LTL over
the simple domain \(\langle \mathbb{N}, = \rangle\) augmented
with the freeze operator is undecidable which is a
surprising result regarding the
poor language for constraints (only equality tests). Many
versions of freeze-free Constraint LTL are decidable over
domains with qualitative predicates and our undecidability
result actually establishes \(\Sigma_{1}^{1}\)-completeness.
On the positive side, we provide complexity results when the domain is
finite (EXPSPACE-completeness) or when the formulae are
flat in a sense introduced in the paper. Our undecidability
results are quite sharp (\emph{i.e.}~with restrictions on the
number of variables) and all our complexity characterizations
insure completeness with respect to some complexity class
(mainly PSPACE and~EXPSPACE).}
}
@inproceedings{DN-atva05,
address = {Taipei, Taiwan},
month = oct,
year = {2005},
volume = 3707,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Peled, Doron A. and Tsay, Yih-Kuen},
acronym = {{ATVA}'05},
booktitle = {{P}roceedings of the 3rd {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'05)},
author = {Demri, St{\'e}phane and Nowak, David},
title = {Reasoning about transfinite sequences (extended abstract)},
pages = {248-262},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DN-atva2005.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DN-atva2005.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DN-atva2005.ps},
doi = {10.1007/11562948_20},
abstract = {We introduce a family of temporal logics to specify the
behavior of systems with Zeno behaviors. We extend linear-time temporal
logic LTL to authorize models admitting Zeno sequences of actions and
quantitative temporal operators indexed by ordinals replace the standard
next-time and until future-time operators. Our aim is to control
such systems by designing controllers that safely work on \(\omega\)-sequences
but interact synchronously with the system in order to restrict their behaviors.
We show that the satisfiability problem for the logics working
on \(\omega^{k}\)-sequences is EXPSPACE-complete when the integers are represented
in binary, and PSPACE-complete with a unary representation. To do so,
we substantially extend standard results about LTL by introducing a
new class of succinct ordinal automata that can encode the interaction
between the different quantitative temporal operators.}
}
@inproceedings{FM-podc05,
address = {Las Vegas, Nevada, USA},
month = jul,
year = 2005,
publisher = {ACM Press},
editor = {Aguilera, Marcos Kawazoe and Aspnes, James},
acronym = {{PODC}'05},
booktitle = {{P}roceedings of the {T}wenty-{F}ourth {A}nnual
{ACM} {SIGACT}-{SIGOPS} {S}ymposium
on {P}rinciples of {D}istributed {C}omputing
({PODC}'05)},
author = {Fribourg, Laurent and Messika, St{\'e}phane},
title = {Brief Announcement: Coupling for {M}arkov Decision
Processes~--- {A}pplication to Self-Stabilization with Arbitrary
Schedulers},
pages = {322},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ba173-messika.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ba173-messika.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ba173-messika.ps},
doi = {10.1145/1073814.1073875}
}
@inproceedings{Gascon-m4m2005,
address = {Berlin, Germany},
month = dec,
year = 2005,
volume = 194,
series = {Informatik Bericht},
publisher = {Humboldt Universit{\"a}t zu Berlin},
editor = {Schlingloff, Holger},
acronym = {{M4M-4}},
booktitle = {{P}roceedings of the 4th
{W}orkshop on {M}ethods for {M}odalities
({M4M-4})},
author = {Gascon, R{\'e}gis},
title = {Verifying qualitative and quantitative properties with~{LTL}
over concrete domains},
pages = {54-61},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Gascon-M4M05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Gascon-M4M05.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Gascon-M4M05.ps},
abstract = {We introduce different
extensions of LTL where propositional
variables are replaced by constraints
interpreted in~\(\mathbb{Z}\). We show
different decidability and complexity results
for the satisfiability and model checking
problems of these logics. The extension of
LTL over a wide set of qualitative
constraints is shown to be PSPACE-complete.
When introducing some quantitative
constraints, we must consider strong
restrictions to regain decidability.}
}
@inproceedings{Gastin-ICALP2005,
address = {Lisboa, Portugal},
month = jul,
year = 2005,
volume = {3580},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Caires, Lu{\'\i}s and Italiano, Giuseppe F. and
Monteiro, Lu{\'\i}s and Palamidessi, Catuscia and Yung, Moti},
acronym = {{ICALP}'05},
booktitle = {{P}roceedings of the 32nd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming
({ICALP}'05)},
author = {Droste, Manfred and Gastin, Paul},
title = {Weighted Automata and Weighted Logics},
pages = {513-525},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/icalp05dg-final.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/icalp05dg-final.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/icalp05dg-final.pdf},
doi = {10.1007/11523468_42},
abstract = {Weighted automata are used to
describe quantitative properties in various
areas such as probabilistic systems, image
compression, speech-to-text processing. The
behaviour of such an automaton is a mapping,
called a formal power series, assigning to
each word a weight in some semiring. We
generalize B{\"{u}}chi's and Elgot's
fundamental theorems to this quantitative
setting. We introduce a weighted version of
MSO~logic and prove that, for commutative
semirings, the behaviours of weighted
automata are precisely the formal power
series definable with our weighted logic. We
also consider weighted first-order logic and
show that aperiodic series coincide with the
first-order definable ones, if the semiring
is locally finite, commutative and has some
aperiodicity property.}
}
@inproceedings{GLP:VMCAI,
address = {Paris, France},
month = jan,
year = 2005,
volume = 3385,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cousot, Radhia},
acronym = {{VMCAI}'05},
booktitle = {{P}roceedings of the 6th {I}nternational {C}onference on
{V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation
({VMCAI}'05)},
author = {Goubault{-}Larrecq, Jean and Parrennes, Fabrice},
title = {Cryptographic Protocol Analysis on Real {C}~Code},
pages = {363-379},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GouPar-VMCAI2005.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GouPar-VMCAI2005.pdf},
doi = {10.1007/b105073},
abstract = {Implementations of
cryptographic protocols, such as OpenSSL for
example, contain bugs affecting security,
which cannot be detected by just analyzing
abstract protocols (e.g., SSL or TLS). We
describe how cryptographic protocol
verification techniques based on solving
clause sets can be applied to detect
vulnerabilities of C programs in the
Dolev-Yao model, statically. This involves
integrating fairly simple pointer analysis
techniques with an analysis of which messages
an external intruder may collect and forge.
This also involves relating concrete run-time
data with abstract, logical terms
representing messages. To this end, we make
use of so-called trust assertions.
The output of the analysis is a set of
clauses in the decidable class H1, which can
then be solved independently. This can be
used to establish secrecy properties, and to
detect some other bugs. }
}
@article{JGL-ipl2005,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Goubault{-}Larrecq, Jean},
title = {Deciding {\(\mathcal{\MakeUppercase{H}}_1\)}
by Resolution},
year = {2005},
volume = 95,
number = 3,
pages = {401-408},
month = aug,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Goubault-h1.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Goubault-h1.pdf},
doi = {10.1016/j.ipl.2005.04.007},
abstract = {Nielson, Nielson and Seidl's
class \(\mathcal{H}_1\) is a decidable class
of first-order Horn clause sets, describing
strongly regular relations. We give
another proof of decidability, and of the
regularity of the defined languages, based
on fairly standard automated deduction
techniques. }
}
@article{VGL-dmtcs05,
journal = {Discrete Mathematics \& Theoretical Computer Science},
author = {Verma, Kumar N. and Goubault{-}Larrecq, Jean},
title = {{K}arp-{M}iller Trees for a Branching Extension of~{VASS}},
volume = 7,
number = 1,
pages = {217-230},
year = 2005,
month = nov,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/VGL-dmtcs05.pdf},
secondurl = {http://www.dmtcs.org/volumes/abstracts/dm070113.abs.html},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/VGL-dmtcs05.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/VGL-dmtcs05.ps},
abstract = {We study BVASS (Branching VASS)
which extend VASS (Vector Addition Systems with
States) by allowing addition transitions that
merge two configurations. Runs in BVASS are
tree-like structures instead of linear ones as
for VASS. We show that the construction of
Karp-Miller trees for VASS can be extended to
BVASS. This entails that the coverability set
for BVASS is computable. This allows us to
obtain decidability results for certain classes
of equational tree automata with an
associative-commutative symbol. Recent
independent work by de Groote \emph{et al.} implies
that decidability of reachability in BVASS is
equivalent to decidability of provability in
MELL (multiplicative exponential linear logic),
which is still an open problem. Hence our
results are also a step towards answering this
question in the affirmative.}
}
@inproceedings{MukhamedovKremerRitter2005,
address = {Roseau, The Commonwealth Of Dominica},
month = aug,
year = 2005,
volume = 3570,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Patrick, Andrew S. and Yung, Moti},
acronym = {{FC}'05},
booktitle = {{R}evised {P}apers from the 9th {I}nternational {C}onference
on {F}inancial {C}ryptography and {D}ata {S}ecurity
({FC}'05)},
author = {Mukhamedov, Aybek and Kremer, Steve and
Ritter, Eike},
title = {Analysis of a Multi-Party Fair Exchange Protocol and
Formal Proof of Correctness in the Strand Space
Model},
pages = {255-269},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MKR-fcrypto05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MKR-fcrypto05.pdf},
doi = {10.1007/11507840_23},
abstract = {A multi-party fair
exchange protocol is a cryptographic
protocol allowing several parties to
exchange commodities in such a way that
everyone gives an item away if and only
if it receives an item in return. In this
paper we discuss a multi-party fair
exchange protocol originally proposed by
Franklin and Tsudik, and subsequently
shown to have flaws and fixed by Gonz\'alez
and Markowitch. We identify flaws in the
fixed version of the protocol, propose a
corrected version, and give a formal
proof of correctness in the strand space
model.}
}
@inproceedings{KremerRyan2005,
address = {Edinburgh, Scotland, UK},
month = apr,
year = 2005,
volume = 3444,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Sagiv, Mooly},
acronym = {{ESOP}'05},
booktitle = {{P}rogramming {L}anguages and {S}ystems~---
{P}roceedings of the 14th
{E}uropean {S}ymposium on {P}rogramming
({ESOP}'05)},
author = {Kremer, Steve and Ryan, Mark D.},
title = {Analysis of an Electronic Voting Protocol in the
Applied Pi-Calculus},
pages = {186-200},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Kremer-esop05.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Kremer-esop05.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Kremer-esop05.pdf},
doi = {10.1007/b107380},
abstract = {Electronic voting promises the
possibility of a convenient, efficient and
secure facility for recording and tallying votes
in an election. Recently highlighted
inadequacies of implemented systems have
demonstrated the importance of formally
verifying the underlying voting protocols. The
applied pi calculus is a formalism for modelling
such protocols, and allows us to verify
properties by using automatic tools, and to rely
on manual proof techniques for cases that
automatic tools are unable to handle. We model
a known protocol for elections known as FOO~92
in the applied pi calculus, and we formalise
three of its expected properties, namely
fairness, eligibility, and privacy. We use the
ProVerif tool to prove that the first two
properties are satisfied. In the case of the
third property, ProVerif is unable to prove it
directly, because its ability to prove
observational equivalence between processes is
not complete. We provide a manual proof of the
required equivalence.}
}
@inproceedings{GK-concur05,
address = {San Francisco, California, USA},
month = aug,
year = 2005,
volume = 3653,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abadi, Mart{\'\i}n and de Alfaro, Luca},
acronym = {{CONCUR}'05},
booktitle = {{P}roceedings of the 16th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'05)},
author = {Gastin, Paul and Kuske, Dietrich},
title = {Uniform Satisfiability Problem for Local Temporal Logics
over {M}azurkiewicz Traces},
pages = {533-547},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/concur05gk-final.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/concur05gk-final.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/concur05gk-final.ps},
doi = {10.1007/11539452_40},
abstract = {We continue our study of the complexity
of temporal logics over concurrent systems that can be
described by Mazurkiewicz traces. In a previous paper
(CONCUR~2003), we investigated the class of local and
MSO definable temporal logics that capture all known
temporal logics and we showed that the satisfiability
problem for any such logic is in PSPACE (provided the
dependence alphabet is fixed). In this paper, we
concentrate on the uniform satisfiability problem: we
consider the dependence alphabet (\emph{i.e.}, the
architecture of the distributed system) as part of the
input. We prove lower and upper bounds for the uniform
satisfiability problem that depend on the number of
monadic quantifier alternations present in the chosen
MSO-modalities.}
}
@inproceedings{LLT-rta2005,
address = {Nara, Japan},
month = apr,
year = 2005,
volume = 3467,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Giesl, J{\"u}rgen},
acronym = {{RTA}'05},
booktitle = {{P}roceedings of the 16th {I}nternational
{C}onference on {R}ewriting {T}echniques
and {A}pplications
({RTA}'05)},
author = {Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf},
title = {Intruder Deduction for {AC}-like Equational Theories
with Homomorphisms},
pages = {308-322},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/rta05-LLT.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/rta05-LLT.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/rta05-LLT.ps},
doi = {10.1007/b135673},
abstract = {Cryptographic protocols are
small programs which involve a high level
of concurrency and which are difficult to
analyze by hand. The most successful
methods to verify such protocols rely on
rewriting techniques and automated
deduction in order to implement or mimic
the process calculus describing the
protocol execution. \par
We focus on the
intruder deduction problem, that is the
vulnerability to passive attacks, in
presence of several variants of
\textit{AC}-like axioms (from \textit{AC}
to Abelian groups, including the theory
of \emph{exclusive or}) and homomorphism
which are the most frequent axioms
arising in cryptographic protocols.
Solutions are known for the cases of
\emph{exclusive or}, of Abelian groups,
and of homomorphism alone. In this paper
we address the combination of these
\textit{AC}-like theories with the law of
homomorphism which leads to much more
complex decision problems.\par
We prove
decidability of the intruder deduction
problem in all cases considered. Our
decision procedure is in EXPTIME, except
for a restricted case in which we have
been able to get a PTIME decision
procedure using a property of one-counter
and pushdown automata.}
}
@inproceedings{Laroussinie-m4m05,
address = {Berlin, Germany},
month = dec,
year = 2005,
volume = 194,
series = {Informatik Bericht},
publisher = {Humboldt Universit{\"a}t zu Berlin},
editor = {Schlingloff, Holger},
acronym = {{M4M-4}},
booktitle = {{P}roceedings of the 4th
{W}orkshop on {M}ethods for {M}odalities
({M4M-4})},
author = {Laroussinie, Fran{\c{c}}ois},
title = {Timed modal logics for the verification of real-time systems},
pages = {293-305},
nonote = {Invited paper},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Lar-M4M05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Lar-M4M05.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Lar-M4M05.ps},
abstract = {The timed modal logic \(L_{\nu}\) has
been proposed in order to express timed properties
over real-time systems modeled as (compositions of)
timed automata. In this paper, we present a short
survey of results about~\(L_{\nu}\): complexity of
model checking, expressivity, compositional methods,
relationship with strong timed bisimulation etc. We
also show how \(L_{\nu}\) can be extended in order to
express new properties. }
}
@inproceedings{LS-fossacs05,
address = {Edinburgh, Scotland, UK},
month = apr,
year = 2005,
volume = 3441,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Sassone, Vladimiro},
acronym = {{FoSSaCS}'05},
booktitle = {{P}roceedings of the 8th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'05)},
author = {Laroussinie, Fran{\c{c}}ois and Sproston, Jeremy},
title = {Model Checking Durational Probabilistic Systems},
pages = {140-154},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/fossacs05-FS.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/fossacs05-FS.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/fossacs05-FS.ps},
doi = {10.1007/b106850},
abstract = {We consider model-checking algorithms for durational probabilistic
systems, which are systems exhibiting nondeterministic, probabilistic and
discrete-timed behaviour. We present two semantics for durational probabilistic
systems, and show how formulae of the probabilistic and timed temporal logic
PTCTL can be verified on such systems. We also address complexity issues, in
particular identifying the cases in which model checking durational probabilistic
systems is harder than verifying non-probabilistic durational systems.}
}
@inproceedings{LNZ-appsem05,
address = {Frauenchiemsee, Germany},
month = sep,
year = 2005,
editor = {Hofmann, Martin and Loidl, Hans-Wolfgang},
acronym = {{APPSEM}'05},
booktitle = {{P}roceedings of the 3rd {APPSEM~II} Workshop
({APPSEM}'05)},
author = {Lasota, S{\l}awomir and Nowak, David and
Zhang, Yu},
title = {On completeness of logical relations for monadic types},
nopages = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LNZ-monad-complete.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LNZ-monad-complete.pdf},
abstract = {Interesting properties of programs can be expressed using
contextual equivalence. The latter is difficult to prove directly, hence
(pre-)logical relations are often used as a tool to prove it.
Whereas pre-logical relations are complete at all types, logical
relations are only complete up to first-order types. We propose a
notion of contextual equivalence for Moggi's computational lambda calculus,
and define pre-logical and logical relations for this calculus. Monads
introduce new difficulties: in particular the usual proofs of completeness
up to first-order types do not go through. We prove completeness up to
first order for several of Moggi's monads. In the case of the non-determinism
monad we obtain, as a corollary, completness of strong bisimulation
w.r.t.~contextual equivalence in lambda calculus with monadic non-determinism.}
}
@techreport{rr-LSV:05:11,
author = {Bouhoula, Adel and Jacquemard, Florent},
title = {Automated Induction for Complex Data Structures},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2005},
month = jul,
type = {Research Report},
number = {LSV-05-11},
note = {24~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-11.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-11.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2005-11.ps},
abstract = {We develop a new approach for mechanizing induction
on complex data structures (like sets, sorted lists,
trees, powerlists...). The key idea is to compute a
tree grammar with constraints which describes exactly
the initial model of the given specification, unlike
test sets or cover sets which are approximative
induction schemes when the constructors are not free.
This grammar is used for the generation of subgoals
during the proof by induction. Our procedure is sound
and refutationally complete even with constrained
axioms for constructors. it subsumes all test set
induction techniques, and yields very natural proofs
for several examples on which other approaches
failed.}
}
@techreport{rr-LSV:05:17,
author = {Bouhoula, Adel and Jacquemard, Florent},
title = {Automatic Verification of Sufficient Completeness for Specifications
of Complex Data Structures},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = 2005,
month = aug,
type = {Research Report},
number = {LSV-05-17},
note = {14~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-17.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-17.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2005-17.ps},
abstract = {We present a new procedure for testing sufficient
completeness for conditional and constrained term
rewriting systems in presence of constrained axioms
for constructors. Such axioms allow to specify
complex data structures like e.g. sets or sorted lists.
Our approach is based on tree grammars with
constraints, a formalism which permits an exact
representation of languages of ground constructor
terms in normal form. The procedure is sound and
complete and has been successfully used for checking
the sufficient completeness of several
specifications where related former techniques fail.}
}
@techreport{LSV:05:19,
author = {Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf},
title = {Intruder Deduction for the Equational Theory of Exclusive-or
with Distributive Encryption},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = 2005,
month = oct,
type = {Research Report},
number = {LSV-05-19},
note = {39~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-19.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-19.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2005-19.ps},
abstract = {Cryptographic protocols are small programs which involve a high
level of concurrency and which are difficult to analyze by hand. The
most successful methods to verify such protocols are based on
rewriting techniques and automated deduction in order to implement
or mimic the process calculus describing the execution of a
protocol.\par
We are interested in the intruder deduction problem, that is the
vulnerability to passive attacks, in presence of the theory of an
encryption
operator which distributes over the \emph{exclusive-or}. This
equational
theory describes very common properties of cryptographic primitives.
Solutions to the intruder deduction problem modulo an equational theory
are known for the cases of \emph{exclusive-or}, of Abelian groups, of a
homomorphism symbol alone, and of combinations of these theories. In
this paper we consider the case where the encryption distributes over
\emph{exclusive-or}. The interaction of the distributive law of the
encryption with the cancellation law of \emph{exclusive-or} leads to a
much more complex decision problem. We prove decidability of the intruder
deduction problem for an encryption which distributes over
\emph{exclusive-or} with an EXPTIME procedure and we give a PTIME
decision
procedure relying on prefix rewrite systems for a restricted case, the
\emph{binary} case.}
}
@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.}
}
@inproceedings{Orchids-cav05,
address = {Edinburgh, Scotland, UK},
month = jul,
year = 2005,
volume = 3576,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Etessami, Kousha and Rajamani, Sriram},
acronym = {{CAV}'05},
booktitle = {{P}roceedings of the 17th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'05)},
author = {Olivain, Julien and Goubault{-}Larrecq, Jean},
title = {The {O}rchids Intrusion Detection Tool},
pages = {286-290},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/OG-cav05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/OG-cav05.pdf},
doi = {10.1007/11513988_28}
}
@misc{PERSEE-RC1,
author = {Bardin, S{\'e}bastien and Herbreteau, Fr{\'e}d{\'e}ric
and Sighireanu, Mihaela and Sutre, Gr{\'e}goire
and Vincent, Aymeric},
title = {Int{\'e}gration des outils {PERS\'EE} (Proposition
d'architecture)},
howpublished = {D\'elivrable~3.1~--- Partie~1 du Projet PERS\'EE de
l'ACI S\'ecurit\'e Informatique},
year = 2005,
month = jun,
url = {http://www.labri.fr/perso/herbrete/persee/downloads/integration/deliverable3.1.pdf},
pdf = {http://www.labri.fr/perso/herbrete/persee/downloads/integration/deliverable3.1.pdf},
note = {35~pages}
}
@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}
}
@techreport{Prouve:rap5,
author = {Bozga, Liana and Delaune, St{\'e}phanie and
Klay, Francis and Vigneron, Laurent},
title = {Retour d'exp{\'e}rience sur la validation du
porte-monnaie {\'e}lectronique},
institution = {projet RNTL PROUV{\'E}},
month = mar,
year = 2005,
type = {Technical Report},
number = 5,
note = {29~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/prouve-rap5.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/prouve-rap5.ps},
abstract = {Le domaine de la
mod{\'e}lisation et de la v{\'e}rification
est une activit{\'e} d{\'e}licate et
importante qui a connu une v{\'e}ritable
explosion dans les ann{\'e}es~1990. On
dispose {\`a} l'entr{\'e}e des
ann{\'e}es~2000 de toute une gamme de
mod{\`e}les et de m{\'e}thodes plus ou moins
avanc{\'e}s en ce qui concerne
l'expressivit{\'e} et l'automatisation.
\par
Afin de d{\'e}finir les besoins et les
priorit{\'e}s {\`a} mettre sur les outils
consacr{\'e}s {\`a} la v{\'e}rification de
protocoles cryptographiques qui seront
d{\'e}velopp{\'e}s au sein du projet RNTL
PROUV{\'E}, nous proposons de travailler en
situation r{\'e}elle, sur des protocoles
plut{\^o}t <<~durs~>>, en effectuant le cycle
suivant: mod{\'e}lisation, formalisation puis
validation dans des outils existants. Ce
travail est effectu{\'e} ici pour deux
versions d'un protocole de porte-monnaie
{\'e}lectronique, dont l'une a {\'e}t{\'e}
d{\'e}velopp{\'e}e r{\'e}cemment par une
{\'e}quipe de France T{\'e}l{\'e}com. Les
outils retenus pour la r{\'e}alisation de
cette {\'e}tude sont ProVerif, Hermes et
Casrul, en raison de leurs
caract{\'e}ristiques tr{\`e}s
diff{\'e}rentes.}
}
@techreport{Prouve:rap6,
author = {Delaune, St{\'e}phanie and
Klay, Francis and Kremer, Steve},
title = {Sp{\'e}cification du protocole de vote
{\'e}lectronique},
institution = {projet RNTL PROUV{\'E}},
month = nov,
year = 2005,
type = {Technical Report},
number = 6,
note = {19~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Prouve-rap6.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Prouve-rap6.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Prouve-rap6.ps},
abstract = {Cette nouvelle \'etude de cas a pour
but de tester les limites du
langage~{\scshape Prouv\'e}. En effet, le
protocole que nous avons choisi d'\'etudier est
volontairement complexe tant au niveau de la
mod\'elisation des propri\'et\'es de s\'ecurit\'e que de la
description du protocole lui-m\^eme en raison de la
manipulation de structures de donn\'ees telles que
les listes.\par
Notre \'etude de cas est un protocole de vote qui a
\'et\'e mis au point par J.~Traor\'e, ing\'enieur de
recherche chez France~T\'el\'ecom. Ce protocole est
bas\'e sur le m\'ecanisme de signature en aveugle et
peut \^etre consid\'er\'e comme un d\'eriv\'e du protocole
de Fujioka, Okamoto et~Ohta. Ce document
introduit dans un premier temps le probl\`eme du
vote \'electronique en g\'en\'eral avant de d\'ecrire le
protocole en lui-m\^eme et sa formalisation dans le
langage~{\scshape Prouv\'e}.}
}
@techreport{Prouve:rap7,
author = {Kremer, Steve and Lakhnech, Yassine and Treinen, Ralf},
title = {The {P}{\scshape rouv\'e} Manual: Specifications, Semantics, and Logics},
institution = {projet RNTL PROUV{\'E}},
month = dec,
year = 2005,
type = {Technical Report},
number = 7,
note = {49~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Prouve-rap7.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Prouve-rap7.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Prouve-rap7.ps},
abstract = { In this report we describe the {\scshape Prouv\'e}
specification language for cryptographic protocols. A main
feature of the language is that it separates the roles of a
protocol, which are defined in a simple imperative
programming language, from the scenario which defines how
instances of the roles are created.\par
We give a formal semantics of the protocol specification
language, and define both an expressive logics for safety
conditions of protocols and a more limited assertion
language.\par
This version of the report~(2.0.x) describes version~2.0 of
the {\scshape Prouv\'e} language.}
}
@inproceedings{PinchinatRiedweg05,
address = {Portland, Oregon, USA},
month = jun,
year = 2005,
publisher = {IEEECSP},
editor = {Balakrishnan, S. N.},
acronym = {{ACC}'05},
booktitle = {{P}roceedings of the 24th {A}merican {C}ontrol
{C}onference ({ACC}'05)},
author = {Pinchinat, Sophie and Riedweg, St{\'e}phane},
title = {You Can Always Compute Maximally Permissive
Controllers Under Partial Observation When They Exist},
pages = {2287-2292},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PR-ACC05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PR-ACC05.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/PR-ACC05.ps},
abstract = {The maximal permissivity property of controllers
is an optimal criterion that is often taken for granted as the
result of synthesis algorithms: the algorithms are designed
for frameworks where the existence and the uniqueness of
a maximal permissive controller is demonstrated apart, as
it fulfills sufficient hypotheses; these algorithms precisely
compute this object. Still, maximally permissive solutions
might exist in circumstances which do not fall into such
identified frameworks, but there is no way to ensure that
the algorithms deliver an optimal solution. In this paper, we
propose a general synthesis procedure which always computes
a maximal permissive controller when it exists.}
}
@inproceedings{PR-cdc05,
address = {Seville, Spain},
month = dec,
year = 2005,
publisher = {{IEEE} Control System Society},
acronym = {{CDC-ECC}'05},
booktitle = {{P}roceedings of the 44th {IEEE} {C}onference on Decision
and Control and European Control Conference
({CDC-ECC}'05)},
author = {Pinchinat, Sophie and Riedweg, St{\'e}phane},
title = {On the Architectures in Decentralized Supervisory
Control},
pages = {12-17},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PR-cdc05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PR-cdc05.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/PR-cdc05.ps},
abstract = {In this paper, we clarify the notion of architecture in
decentralized control, in order to investigate the realizability problem:
given a discrete-event system, a desired behavior and an architecture for
a decentralized control, can the desired behavior be achieved by
decentralized controllers in accordance with the given architecture? We
consider the problem for any mu-calculus definable behavior and for
classic architectures from the literature. The method consists in
compiling in a single formula both the desired behavior and the
architecture. Applications of this approach are a single synthesis
algorithm of decentralized controllers (with full observation) for the
whole considered family of architectures, and the development of a
convenient mathematical framework for a theory of decentralized control
architectures.}
}
@article{PR-IPL05,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Pinchinat, Sophie and Riedweg, St{\'e}phane},
title = {A Decidable Class of Problems for Control under Partial Observation},
year = 2005,
month = aug,
volume = 95,
number = 4,
pages = {454-465},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PR-IPL05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PR-IPL05.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/PR-IPL05.ps},
doi = {10.1016/j.ipl.2005.04.011}
}
@phdthesis{THESE-bardin05,
author = {Bardin, S{\'e}bastien},
title = {Vers un model checking avec acc{\'e}l{\'e}ration plate
de syst{\`e}mes h{\'e}t{\'e}rog{\`e}nes},
year = 2005,
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/PDF/bardin-THESE.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bardin-THESE.pdf}
}
@phdthesis{THESE-zhang05,
author = {Zhang, Yu},
title = {Cryptographic logical relations~-- What is the
contextual equivalence for
cryptographic protocols and how to prove~it?},
year = 2005,
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/PDF/zy-thesis.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/zy-thesis.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/zy-thesis.ps}
}
@phdthesis{THESE-baclet05,
author = {Baclet, Manuel},
title = {Applications du model-checking {\`a} des probl{\`e}mes de
v{\'e}rification de syst{\`e}mes sur puce},
year = 2005,
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/PDF/these-baclet.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-baclet.pdf}
}
@phdthesis{treinen-hab2005,
author = {Treinen, Ralf},
title = {R{\'e}solution symbolique de contraintes},
year = 2005,
month = nov,
type = {M{\'e}moire d'habilitation},
school = {Universit{\'e} Paris-Sud~11, Orsay, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/RT-habil.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/RT-habil.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/RT-habil.ps}
}
@phdthesis{FL-hab2005,
author = {Laroussinie, Fran{\c{c}}ois},
title = {Model checking temporis{\'e}~--- Algorithmes efficaces et complexit{\'e}},
year = 2005,
month = dec,
type = {M{\'e}moire d'habilitation},
school = {Universit{\'e} Paris~7, Paris, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FL-habil.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FL-habil.pdf}
}
@mastersthesis{pinot-master,
author = {Pinot, Simon},
title = {Analyse de stabilit{\'e} d'algorithme
distribu{\'e}s probabilistes},
school = {{M}aster de {L}ogique {M}ath{\'e}matique
et {F}ondements de l'{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = 2005,
month = sep,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Pinot-M2.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Pinot-M2.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Pinot-M2.ps}
}
@mastersthesis{sznajder-master,
author = {Sznajder, Nathalie},
title = {Synth{\`e}se de contr{\^o}leur pour les
syst{\`e}mes distribu{\'e}s synchrones},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = 2005,
month = sep,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sznajder-M2.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sznajder-M2.pdf}
}
@article{FL-ACMtecs05,
publisher = {ACM Press},
journal = {ACM Transactions in Embedded Computing Systems},
author = {{The Artist Education Group}},
fullauthor = {Caspi, Paul and
Sangiovanni-Vincentelli, Alberto L. and
Almeida Lu{\'\i}s and
Benveniste, Albert and
Bouyssounouse, Bruno and
Buttazzo, Giorgio C. and
Crnkovic, Ivica and
Damm, Werner and
Engblom, Jakob and
Fohler, Gerhard and
Garc{\'\i}a-Valls, Marisol and
Kopetz, hermann and
Lakhnech, Yassine and
Laroussinie, Fran{\c{c}}ois and
Lavagno, Luciano and
Lipari, Guiseppe and
Maraninchi, Florence and
Peti, Philipp and
Antonio de la Puente, Juan and
Scaife, Norman and
Sifakis, Joseph and
de{ }Simone, Robert and
T{\"o}rngren, Martin and
Ver{\'\i}ssimo, Paulo and
Wellings, Andy J. and
Wilhelm, Reinhard and
Willemse, Tim A. C. and
Yi, Wang},
title = {Guidelines for a graduate curriculum on embedded software
and systems},
volume = 4,
number = 3,
year = 2005,
month = aug,
pages = {587-611},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Artist-tecs05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Artist-tecs05.pdf},
doi = {10.1145/1086519.1086526},
abstract = {The design of embedded real-time systems requires skills from
multiple specific disciplines, including, but not limited to, control,
computer science, and electronics. This often involves experts from differing
backgrounds, who do not recognize that they address similar, if not identical,
issues from complementary angles. Design methodologies are lacking in rigor
and discipline so that demonstrating correctness of an embedded design, if at
all possible, is a very expensive proposition that may delay significantly the
introduction of a critical product. While the economic importance of embedded
systems is widely acknowledged, academia has not paid enough attention to the
education of a community of high-quality embedded system designers, an obvious
difficulty being the need of interdisciplinarity in a period where
specialization has been the target of most education systems. This paper
presents the reflections that took place in the European Network of Excellence
Artist leading us to propose principles and structured contents for building
curricula on embedded software and systems.}
}
@techreport{FGRV-ulb05,
author = {Finkel, Alain and Geeraerts, Gilles and Raskin, Jean-Fran{\c{c}}ois and
Van{~}Begin, Laurent},
title = {A counter-example the the minimal coverability tree algorithm},
institution = {Universit\'e Libre de Bruxelles, Belgium},
year = {2005},
number = {535},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FGRV-ulb05.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FGRV-ulb05.pdf},
abstract = {In [Finkel, 1993], an~algorithm to compute a minimal
coverability tree for Petri nets has been presented. This document
demonstrates, thanks to a simple counter-example, that this algorithm may
compute an under-approximation of a coverability tree, i.e., a~tree whose
set of nodes is not sufficient to cover all the reachable markings.}
}
@article{BC-JALC2005,
journal = {Journal of Automata, Languages and Combinatorics},
author = {Bouyer, Patricia and Chevalier, Fabrice},
title = {On Conciseness of Extensions of Timed Automata},
year = 2005,
volume = 10,
number = 4,
pages = {393-405},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC05-jalc.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC05-jalc.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BC05-jalc.ps},
abstract = {In this paper we study conciseness of
various extensions of timed automata, and prove
that several features like diagonal constraints or
updates lead to exponentially more concise timed
models.}
}
@misc{bouyer-cortos06,
author = {Bouyer, Patricia},
title = {Weighted Timed Automata: Model-Checking and Games},
year = {2005},
month = aug,
howpublished = {Invited talk, Workshop CORTOS'06, Bonn, Germany}
}
@misc{bouyer-avocs05,
author = {Bouyer, Patricia},
title = {Optimal Timed Games},
year = {2005},
month = sep,
howpublished = {Invited talk, 5th {I}nternational {W}orkshop
on {A}utomated {V}erification of {C}ritical {S}ystems
({AVoCS}'05), Warwick, UK}
}
@misc{bouyer-infinity05,
author = {Bouyer, Patricia},
title = {Optimal Reachability Timed Games},
year = {2005},
month = aug,
howpublished = {Invited talk, 7th {I}nternational {W}orkshop
on {V}erification of {I}nfinite {S}tate {S}ystems
({INFINITY}'05), San Francisco, USA}
}
@inproceedings{bouyer-etr05,
address = {Nancy, France},
month = sep,
year = 2005,
noeditor = {},
acronym = {{ETR}'05},
booktitle = {{A}ctes de la 4{\`e}me {\'E}cole {T}emps-{R}{\'e}el ({ETR}'05)},
author = {Bouyer, Patricia},
title = {An Introduction to Timed Automata},
pages = {111-123},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-etr05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-etr05.pdf}
}
@inproceedings{bouyer-artist2-05,
author = {Bouyer, Patricia},
title = {Foundations of Timed Systems},
booktitle = {Proc. of the ARTIST2 Summer School on Component \&
Modelling, Testing \& Verification, and Statical Analysis of Embedded
Systems},
address = {N{\"a}sslingen, Sweden},
month = sep # {-} # oct,
year = {2005},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-nasslingen.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-nasslingen.pdf}
}
@misc{Demri0506,
author = {Demri, St{\'e}phane},
title = {Temporal logics},
year = {2005},
note = {Course notes, {M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri-2.8-TL.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri-2.8-TL.pdf}
}
@mastersthesis{bouchy-master,
author = {Bouchy, Florent},
title = {Biblioth{\`e}que de m{\'e}thodes pour la
classification},
school = {{M}aster {R}echerche
{I}nformatique, Tours, France},
type = {Rapport de {M}aster},
year = 2005,
month = sep
}
@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.