@article{CL-tsi06,
publisher = {Herm{\`e}s},
journal = {Technique et Science Informatiques},
author = {Cassez, Franck and Laroussinie, Fran{\c{c}}ois},
editor = {Cassez, Franck and Laroussinie, Fran{\c{c}}ois},
title = {Contr{\^o}le des applications temps-r{\'e}el~: mod{\`e}les
temporis{\'e}s et hybrides},
volume = 25,
number = 3,
year = 2006,
url = {http://www.lavoisier.fr/notice/fr2746214830.html}
}
@incollection{jgl-encyc06,
author = {Goubault{-}Larrecq, Jean},
title = {Preuve et v{\'e}rification pour la s{\'e}curit{\'e}
et la s{\^u}ret{\'e}},
booktitle = {Encyclop{\'e}die de l'informatique et des syst{\`e}mes
d'information},
editor = {Akoka, Jacky and Comyn-Wattiau, Isabelle},
pages = {683-703},
publisher = {Vuibert},
year = 2006,
month = dec,
chapter = {I.6},
url = {http://www.vuibert.com/livre12401.html},
abstract = {La s\^uret\'e, comme la s\'ecurit\'e, \'enonce qu'un mal n'arrive
jamais. Le but de cet article est de d\'efinir la notion de propri\'et\'e
de s\^uret\'e, et d'en d\'ecrire quelques techniques de v\'erification et de
preuve~: model-checking, interpr\'etation abstraite notamment. Apr\`es
avoir remarqu\'e qu'il n'y avait pas de s\'ecurit\'e sans s\^uret\'e, il est
expliqu\'e que l'analyse de s\'ecurit\'e d'un syst\`eme repose sur un
mod\`ele, des hypoth\`eses, des propri\'et\'es \`a v\'erifier, et une
architecture de s\'ecurit\'e. Finalement, il est donn\'e un aper\c{c}u de
quelques mod\`eles et m\'ethodes de preuve de protocoles
cryptographiques.}
}
@inproceedings{BJ-secret06,
address = {Venice, Italy},
month = jul,
year = 2006,
editor = {Fern{\'a}ndez, Maribel and Kirchner, Claude},
acronym = {{SecReT}'06},
booktitle = {{P}reliminary {P}roceedings of the 1st
{I}nternational {W}orkshop on {S}ecurity and {R}ewriting {T}echniques
({SecReT}'06)},
author = {Bouhoula, Adel and Jacquemard, Florent},
title = {Security Protocols Verification with Implicit Induction and
Explicit Destructors},
pages = {37-44},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BJ-secret06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BJ-secret06.pdf},
abstract = {We present a new method for automatic implicit induction theorem
proving, and its application for the verification of a key distribution
cryptographic protocol. The~method can handle axioms between constructor
terms, a~feature generally not supported by other induction procedure. We~use
such axioms in order to specify explicit destructors representing
cryptographic operators.}
}
@inproceedings{BBS-forte06,
address = {Paris, France},
month = sep,
year = 2006,
volume = 4229,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Najm, Elie and Pradat{-}Peyre, Jean-Fran{\c{c}}ois and
Vigui{\'e} Donzeau-Gouge, V{\'e}ronique},
acronym = {{FORTE}'06},
booktitle = {{P}roceedings of 26th {IFIP} {WG6.1}
{I}nternational {C}onference on {F}ormal
{T}echniques for {N}etworked and {D}istributed {S}ystems
({FORTE}'06)},
author = {Baier, Christel and Bertrand, Nathalie and Schnoebelen, {\relax Ph}ilippe},
title = {Symbolic verification of communicating systems with
probabilistic message losses: liveness and fairness},
pages = {212-227},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-forte06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-forte06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBS-forte06.ps},
doi = {10.1007/11888116_17},
abstract = {NPLCS's are a new model for nondeterministic channel systems
where unreliable communication is modeled by probabilistic message losses.
We~show that, for \(\omega\)-regular linear-time properties and finite-memory
schedulers, qualitative model-checking is decidable. The~techniques extend
smoothly to questions where fairness restrictions are imposed on the
schedulers. The~symbolic procedure underlying our decidability proofs has been
implemented and used to study a simple protocol handling two-way transfers in
an unreliable setting.}
}
@inproceedings{BP06,
address = {Taipei, Taiwan},
month = aug,
year = 2006,
volume = 4094,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Ibarra, Oscar H. and Yen, Hsu-Chun},
acronym = {{CIAA}'06},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}onference on {I}mplementation and
{A}pplication of {A}utomata
({CIAA}'06)},
author = {Baclet, Manuel and Pagetti, Claire},
title = {Around {H}opcroft's Algorithm},
pages = {114-125},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BP-ciaa06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BP-ciaa06.pdf},
doi = {10.1007/11812128_12},
abstract = {In this paper, a reflection is made on an indeterminism inherent
to Hopcroft's minimization algorithm: the splitter choice. We have implemented
two natural policies (FIFO and~FILO) for managing the set of splitters for
which we obtain the following practical results: the FILO strategy performs
better than the FIFO strategy, in the case of a one letter alphabet, the FILO
practical complexity never exceeds a linear one and our implementation is more
efficient than the minimization algorithm of the FSM tool. This implementation
is being integrated in a finite automata library, the Dash library. Thus, we
present an efficient manner to manipulate automata by using canonical minimal
automata.}
}
@inproceedings{abw-fossacs2006,
address = {Vienna, Austria},
month = mar,
year = 2006,
volume = 3921,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Aceto, Luca and Ing{\'o}lfsd{\'o}ttir, Anna},
acronym = {{FoSSaCS}'06},
booktitle = {{P}roceedings of the 9th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'06)},
author = {Abadi, Mart{\'\i}n and Baudet, Mathieu and
Warinschi, Bogdan},
title = {Guessing Attacks and the Computational Soundness of
Static Equivalence},
pages = {398-412},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABW_Fossacs06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABW_Fossacs06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ABW_Fossacs06.ps},
doi = {10.1007/11690634_27},
abstract = {The indistinguishability of two pieces of
data (or two lists of pieces of data) can be
represented formally in terms of a relation called
static equivalence. Static equivalence depends on an
underlying equational theory. The choice of an
inappropriate equational theory can lead to overly
pessimistic or overly optimistic notions of
indistinguishability, and in turn to security criteria
that require protection against impossible attacks
or ---worse yet--- that ignore feasible ones. In this
paper, we define and justify an equational theory for
standard, fundamental cryptographic operations. This
equational theory yields a notion of static equivalence
that implies computational indistinguishability. Static
equivalence remains liberal enough for use in
applications. In particular, we develop and analyze a
principled formal account of guessing attacks in terms
of static equivalence.}
}
@inproceedings{BKRS-fsttcs2006,
address = {Kolkata, India},
month = dec,
year = 2006,
volume = 4337,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Garg, Naveen and Arun-Kumar, S.},
acronym = {{FSTTCS}'06},
booktitle = {{P}roceedings of the 26th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'06)},
author = {Bozzelli, Laura and K{\v{r}}et{\'\i}nsk{\'y}, Mojm{\'\i}r and
{\v{R}}eh{\'a}k, Vojt{\v{e}}ch and Strej{\v c}ek, Jan},
title = {On Decidability of {LTL} Model Checking for Process Rewrite Systems},
pages = {248-259},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKRS-fsttcs06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKRS-fsttcs06.pdf},
doi = {10.1007/11944836_24}
}
@inproceedings{BLMR-fsttcs2006,
address = {Kolkata, India},
month = dec,
year = 2006,
volume = 4337,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Garg, Naveen and Arun-Kumar, S.},
acronym = {{FSTTCS}'06},
booktitle = {{P}roceedings of the 26th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'06)},
author = {Bouyer, Patricia and Larsen, Kim G. and Markey, Nicolas and
Rasmussen, Jacob Illum},
title = {Almost Optimal Strategies in One-Clock Priced Timed Automata},
pages = {345-356},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLMR-fsttcs06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLMR-fsttcs06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BLMR-fsttcs06.ps},
doi = {10.1007/11944836_32},
abstract = {We consider timed games extended with cost information, and
prove computability of the optimal cost and of \(\epsilon\)-optimal memoryless
strategies in timed games with one~clock. In~contrast, this problem has
recently been proved undecidable for timed games with three clocks.}
}
@proceedings{GDV06,
editor = {Bouyer, Patricia and Madhusudan, P.},
title = {Proceedings of the 3rd Workshop on Games in Design and Verification
({GDV}'06)},
booktitle = {Proceedings of the 3rd Workshop on Games in Design and Verification
({GDV}'06)},
address = {Seattle, Washington, USA},
year = 2006,
month = aug
}
@inproceedings{BBBL-atva06,
address = {Beijing, China},
month = oct,
year = {2006},
volume = 4218,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Graf, Susanne and Zhang, Wenhui},
acronym = {{ATVA}'06},
booktitle = {{P}roceedings of the 4th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'06)},
author = {Bel{ }mokadem, Houda and B{\'e}rard, B{\'e}atrice and Bouyer, Patricia
and Laroussinie, Fran{\c{c}}ois},
title = {Timed temporal logics for abstracting transient states},
pages = {337-351},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBL-atva06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBL-atva06.pdf},
doi = {10.1007/11901914_26},
abstract = {In previous work, the timed logic TCTL was extended with an
{"}almost everywhere{"} Until modality which abstracts negligible sets of
positions (i.e.,~with a null duration) along a run of a timed automaton.
We~propose here an extension of this logic with more powerful modalities, in
order to specify properties abstracting transient states, which are events
that last for less than k time units. Our main result is that modelchecking
is still decidable and PSPACE-complete for this extension. On the other
hand, a second semantics is defined, in which we consider the total duration
where the property does not hold along a run. In~this case, we prove that
model-checking is undecidable.}
}
@inproceedings{BBC-concur06,
address = {Bonn, Germany},
month = aug,
year = 2006,
volume = 4137,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baier, Christel and Hermanns, Holger},
acronym = {{CONCUR}'06},
booktitle = {{P}roceedings of the 17th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'06)},
author = {Bouyer, Patricia and Bozzelli, Laura and Chevalier, Fabrice},
title = {Controller Synthesis for {MTL} Specifications},
pages = {450-464},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-concur06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-concur06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBC-concur06.ps},
doi = {10.1007/11817949_30},
abstract = {We consider the control problem for timed automata
against specifications given as MTL formulas. The logic MTL is a
linear-time timed temporal logic which extends LTL with timing
constraints on modalities, and recently, its model-checking has been
proved decidable in several cases. We investigate these decidable
fragments of MTL (full MTL when interpreted over finite timed
words, and SafetyMTL when interpreted over infinite timed words),
and prove two kinds of results. (1)~We first prove that,
contrary to model-checking, the control problem is
undecidable. Roughly, the computation of a lossy channel system
could be encoded as a model-checking problem, and we prove here that
a perfect channel system can be encoded as a control
problem. (2)~We then prove that if we fix the resources
of the controller (by resources we mean clocks and constants that
the controller can use), the control problem becomes decidable. This
decidability result relies on properties of well (and better)
quasi-orderings.}
}
@article{BBLP-STTT05,
publisher = {Springer},
journal = {International Journal on Software Tools
for Technology Transfer},
author = {Behrmann, Gerd and Bouyer, Patricia and Larsen, Kim G.
and Pel{\'a}nek, Radek},
title = {Lower and Upper Bounds in Zone-Based Abstractions of
Timed Automata},
year = 2006,
month = jun,
pages = {204-215},
number = 3,
volume = 8,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBLP-STTT05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBLP-STTT05.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBLP-STTT05.ps},
doi = {10.1007/s10009-005-0190-0},
abstract = {The semantics of timed automata is
defined using an infinite-state transition system.
For verification purposes, one usually uses zone
based abstractions w.r.t.~the maximal constants to
which clocks of the timed automaton are compared.
We show that by distinguishing maximal lower and
upper bounds, significantly coarser abstractions
can be obtained. We show soundness and
completeness of the new abstractions
w.r.t.~reachability. We demonstrate how
information about lower and upper bounds can be
used to optimise the algorithm for bringing a
difference bound matrix into normal form. Finally,
we experimentally demonstrate that the new
techniques dramatically increases the scalability
of the real-time model checker~{\scshape
Uppaal}.}
}
@article{BC06-beatcs,
publisher = {European Association for
Theoretical Computer Science},
journal = {EATCS Bulletin},
author = {Bouyer, Patricia and Chevalier, Fabrice},
title = {On the Control of Timed and Hybrid Systems},
volume = 89,
year = {2006},
month = jun,
pages = {79-96},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC-beatcs89.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC-beatcs89.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BC-beatcs89.ps},
abstract = {In this paper, we survey some of the results which have
been obtained the last ten years on the control of hybrid and timed
systems.}
}
@inproceedings{BBC-lics2006,
address = {Seattle, Washington, USA},
month = aug,
year = 2006,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'06},
booktitle = {{P}roceedings of the 21st
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'06)},
author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and
Chevalier, Fabrice},
title = {Control in o-Minimal Hybrid Systems},
pages = {367-378},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-lics06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-lics06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBC-lics06.ps},
doi = {10.1109/LICS.2006.22},
abstract = {In this paper, we consider
the control of general hybrid systems. In
this context we show that time-abstract
bisimulation is not adequate for solving
such a problem. That is why we consider
an other equivalence, namely the suffix
equivalence based on the encoding of
trajectories through words. We show that
this suffix equivalence is in general a
correct abstraction for control problems.
We apply this result to o-minimal hybrid
systems, and get decidability and
computability results in this framework.}
}
@inproceedings{BLP-cav06,
address = {Seattle, Washington, USA},
month = aug,
year = 2006,
volume = 4144,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ball, {\relax Th}omas and Jones, Robert B.},
acronym = {{CAV}'06},
booktitle = {{P}roceedings of the 18th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'06)},
author = {Bardin, S{\'e}bastien and Leroux, J{\'e}r{\^o}me and Point, G{\'e}rald},
title = {{FAST} {E}xtended {R}elease},
pages = {63-66},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLP-cav06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLP-cav06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BLP-cav06.ps},
doi = {10.1007/11817963_9},
abstract = {{\scshape Fast} is a tool designed for the analysis of
counter systems, \emph{i.e.}~automata extended with unbounded integer variables.
Despite the reachability set is not recursive in general, Fast implements
several innovative techniques such as acceleration and circuit selection to
solve this problem in practice. In its latest version, the tool is built upon
an open architecture: the Presburger library is manipulated through a clear
and convenient interface, thus any Presburger arithmetics package can be
plugged to the tool. We provide four implementations of the interface using
Lash, Mona, Omega and a new shared automata package with computation cache.
Finally new features are available, like different acceleration algorithms.}
}
@inproceedings{BFLS-avis06,
address = {Vienna, Austria},
month = apr,
year = 2006,
editor = {Bharadwaj, Ramesh},
acronym = {{AVIS}'06},
booktitle = {{P}roceedings of the 5th {I}nternational
{W}orkshop on {A}utomated {V}erification
of {I}nfinite-{S}tate {S}ystems
({AVIS}'06)},
author = {Bardin, S{\'e}bastien and Finkel, Alain and Lozes, {\'E}tienne
and Sangnier, Arnaud},
title = {From Pointer Systems to Counter Systems Using Shape Analysis},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLS-AVIS-06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLS-AVIS-06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BFLS-AVIS-06.ps},
abstract = {We aim at checking safety properties on systems
manipulating dynamic linked lists. First we prove that every
pointer system is bisimilar to an effectively constructible
counter system. We then deduce a two-step analysis procedure.
We first build an over-approximation of the reachability set
of the pointer system. If this over-approximation is too
coarse to conclude, we then extract from it a bisimilar
counter system which is analyzed via efficient symbolic
techniques developed for general counter systems.}
}
@inproceedings{edos2006wsl,
address = {Porto Allegre, Brazil},
month = apr,
year = 2006,
editor = {Berger, Olivier},
acronym = {{IWFS}'06},
booktitle = {{P}roceedings of the {I}nternational
{W}orkshop on {F}ree {S}oftware
({IWFS}'06)},
author = {Boender, Jaap and Di Cosmo, Roberto and Durak, Berke and Leroy, Xavier
and Mancinelli, Fabio and Morgado, Mario and Pinheiro, David and
Treinen, Ralf and Trezentos, Paulo and Vouillon, J{\'e}r{\^o}me},
title = {News from the {EDOS} project: improving the maintenance of free
software distributions},
pages = {199-207},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/wsl06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/wsl06.pdf},
abstract = {The EDOS research project aims
at contributing to the quality assurance of free software
distributions. This is a major technical and engineering
challenge, due to the size and complexity of these
distributions (tens of thousands of software packages). We
present here some of the challenges that we have tackled so
far, and some of the advanced tools that are already
available to the community as an outcome of the first year
of work. }
}
@inproceedings{edos2006ase,
address = {Tokyo, Japan},
month = sep,
year = 2006,
publisher = {{IEEE} Computer Society Press},
acronym = {{ASE}'06},
booktitle = {{P}roceedings of the 21st {IEEE}/{ACM} {I}nternational
{C}onference on {A}utomated {S}oftware {E}ngineering
({ASE}'06)},
author = {Mancinelli, Fabio and Boender, Jaap and Di Cosmo, Roberto and
Vouillon, J{\'e}r{\^o}me and Durak, Berke and Leroy, Xavier
and Treinen, Ralf},
title = {Managing the Complexity of Large Free and Open Source
Package-Based Software Distributions},
pages = {199-208},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/edos-ase06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/edos-ase06.pdf},
doi = {10.1109/ASE.2006.49},
abstract = {The widespread adoption of Free and Open Source Software~(FOSS)
in many strategic contexts of the information technology society has drawn the
attention on the issues regarding how to handle the complexity of assembling
and managing a huge number of (packaged) components in a consistent and
effective~way. FOSS~distributions (and~in particular GNU\slash Linux-based~ones)
have always provided tools for managing the tasks of installing, removing and
upgrading the (packaged) components they were made~of. While these tools
provide a (not always effective) way to handle these tasks on the client side,
there is still a lack of tools that could help the distribution editors to
maintain, on the server side, large and high-quality distributions. In~this
paper we present our research whose main goal is to fill this gap: we~show our
approach, the tools we have developed and their application with experimental
results. Our~contribution provides an effective and automatic way to support
distribution editors in handling those issues that were, until now, mostly
addressed using ad-hoc tools and manual techniques.}
}
@inproceedings{BKSS-tacas06,
address = {Vienna, Austria},
month = mar,
year = 2006,
volume = {3920},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hermanns, Holger and Palsberg, Jens},
acronym = {{TACAS}'06},
booktitle = {{P}roceedings of the 12th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'06)},
author = {Bollig, Benedikt and Kern, Carsten and
Schl{\"u}tter, Markus and Stolz, Volker},
title = {{MSC}an: A Tool for Analyzing {MSC} Specifications},
pages = {455-458},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSCan.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSCan.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MSCan.ps},
doi = {10.1007/11691372_32},
abstract = {We present the tool MSCan, which supports MSC-based
system development. In particular, it automatically checks
high-level MSC specifications for implementability.}
}
@article{BBM-ipl06,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and
Markey, Nicolas},
title = {Improved Undecidability Results on Weighted Timed
Automata},
year = 2006,
month = jun,
volume = 98,
number = 5,
pages = {188-194},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/IPL-BBM06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/IPL-BBM06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IPL-BBM06.ps},
doi = {10.1016/j.ipl.2006.01.012},
abstract = {In this paper, we improve two recent undecidability
results of Brihaye, Bruy{\`e}re and Raskin about
weighted timed automata, an extension of timed automata with a
cost variable. Our results rely on a new encoding of the two
counters of a Minsky machine that only require three clocks and
one stopwatch cost, while previous reductions required five clocks
and one stopwatch cost.}
}
@inproceedings{BBS-lpar06,
address = {Phnom Penh, Cambodia},
month = nov,
year = 2006,
volume = 4246,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Hermann, Miki and Voronkov, Andrei},
acronym = {{LPAR}'06},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onference on {L}ogic for {P}rogramming,
{A}rtificial {I}ntelligence, and {R}easoning
({LPAR}'06)},
author = {Baier, Christel and Bertrand, Nathalie and
Schnoebelen, {\relax Ph}ilippe},
title = {On Computing Fixpoints in Well-Structured Regular Model
Checking, with Applications to Lossy Channel Systems},
pages = {347-361},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-lpar06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-lpar06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBS-lpar06.ps},
doi = {10.1007/11916277_24},
abstract = {We prove a general finite convergence theorem for
{"}upward-guarded{"} fixpoint expressions over a well-quasi-ordered~set. This
has immediate applications in regular model checking of well-structured
systems, where a main issue is the eventual convergence of fixpoint
computations. In~particular, we are able to directly obtain several new
decidability results on lossy channel systems.}
}
@article{BBS-ipl05,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Baier, Christel and Bertrand, Nathalie and
Schnoebelen, {\relax Ph}ilippe},
title = {A note on the attractor-property of infinite-state {M}arkov chains},
year = 2006,
month = jan,
number = 2,
volume = 97,
pages = {58-63},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/IPL-BBS.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/IPL-BBS.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IPL-BBS.ps},
doi = {10.1016/j.ipl.2005.09.011},
abstract = {In the past five years, a series of verification algorithms
has been proposed for infinite Markov chains that have a
finite attractor, \emph{i.e.}, a set that will be visited
infinitely often almost surely starting from any state. \par
In this paper, we establish a sufficient criterion for
the existence of an attractor. We show that if the states
of a Markov chain can be given levels (positive integers)
such that the expected next level for states at some
level \(n > 0\) is less than \(n-\Delta\) for some positive
\(\Delta\), then the states at level~\(0\) constitute an
attractor for the chain. As an application, we obtain a
direct proof that some probabilistic channel systems
combining message losses with duplication and insertion
errors have a finite attractor.}
}
@inproceedings{BG-lpar06,
address = {Phnom Penh, Cambodia},
month = nov,
year = 2006,
volume = 4246,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Hermann, Miki and Voronkov, Andrei},
acronym = {{LPAR}'06},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onference on {L}ogic for {P}rogramming,
{A}rtificial {I}ntelligence, and {R}easoning
({LPAR}'06)},
author = {Bozzelli, Laura and Gascon, R{\'e}gis},
title = {Branching Time Temporal Logic Extended with {P}resburger Constraints},
pages = {197-211},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BG-LPAR06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BG-LPAR06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BG-LPAR06.ps},
doi = {10.1007/11916277_14},
abstract = {Recently, \(\mathrm{LTL}\) extended with atomic formulas built
over a constraint language interpreting variables in~\(\mathbb{Z}\) has been
shown to have a decidable satisfiability and model-checking problem.
This~language allows to compare the variables at different states of the model
and include periodicity constraints, comparison constraints, and a restricted
form of quantification. On the other hand, the \(\mathrm{CTL}\) counterpart of
this logic (and hence also its \(\mathrm{CTL}^{*}\) counterpart which subsumes
both \(\mathrm{LTL}\) and~\(\mathrm{CTL}\)) has an undecidable model-checking
problem. In~this paper, we substantially extend the decidability border, by
considering a meaningful fragment of \(\mathrm{CTL}^{*}\) extended with such
constraints (which subsumes both the universal and existential fragments, as
well as the \(\mathrm{EF}\)-like fragment) and show that satisfiability and
model-checking over relational automata that are abstraction of counter
machines are decidable. The~correctness and the termination of our algorithm
rely on a suitable well quasi-ordering defined over the set of variable
valuations.}
}
@misc{chevalier-prefsttcs06,
author = {Chevalier, Fabrice},
title = {Decision procedures for timed logics},
year = 2006,
month = dec,
howpublished = {Invited talk, Advances and Issues in Timed Systems,
Kolkata, India}
}
@misc{gastin-prefsttcs06,
author = {Gastin, Paul},
title = {Refinements and Abstractions of Signal-Event (Timed) Languages},
year = 2006,
month = dec,
howpublished = {Invited talk, Advances and Issues in Timed Systems,
Kolkata, India}
}
@misc{gastin-wata06,
author = {Gastin, Paul},
title = {Weigthed logics and weighted automata},
year = 2006,
month = mar,
howpublished = {Invited talk, Workshop Weighted Automata: Theory and Applications,
Leipzig, Germany}
}
@misc{gastin-epit06,
author = {Gastin, Paul},
title = {Distributed synthesis: synchronous and asynchronous semantics},
year = 2006,
month = may,
howpublished = {Invited talk, 34{\`e}me {\'E}cole de Printemps en
Informatique Th{\'e}orique, Ile de R{\'e}, France}
}
@misc{gastin-mfps22,
author = {Gastin, Paul},
title = {Refinements and Abstractions of Signal-Event (Timed) Languages},
year = 2006,
month = may,
howpublished = {Invited talk, 22nd {C}onference on
{M}athematical {F}oundations of {P}rogramming
{S}emantics ({MFPS}'06)}
}
@inproceedings{Bouyer-MFPS22,
address = {Genova, Italy},
month = may,
year = 2006,
volume = 158,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Brookes, Steve and Mislove, Michael},
acronym = {{MFPS}'06},
booktitle = {{P}roceedings of the 22nd {C}onference on
{M}athematical {F}oundations of {P}rogramming
{S}emantics ({MFPS}'06)},
author = {Bouyer, Patricia},
title = {Weighted Timed Automata: {M}odel-Checking and Games},
pages = {3-17},
note = {Invited paper},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-mfps06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-mfps06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/bouyer-mfps06.ps},
doi = {10.1016/j.entcs.2006.04.002},
abstract = {In this paper, we present weighted\slash priced
timed automata, an extension of timed automaton with
costs, and solve several interesting problems on that model.}
}
@article{bid-hen-JLAP-2005,
publisher = {Elsevier Science Publishers},
journal = {Journal of Logic and Algebraic Programming},
author = {Bidoit, Michel and Hennicker, Rolf},
title = {Constructor-Based Observational Logic},
year = {2006},
month = apr # {-} # may,
number = {1-2},
volume = 67,
pages = {3-51},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BID-HEN-JLAP.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BID-HEN-JLAP.pdf},
doi = {10.1016/j.jlap.2005.09.002},
abstract = {This paper focuses on the integration of reachability and
observability concepts within an algebraic,
institution-based framework. In the first part of this work,
we develop the essential ingredients that are needed to define the
constructor-based observational logic institution, called
COL, which takes into account both
the generation- and observation-oriented aspects of software systems. The
underlying paradigm of our approach is that the semantics of a specification should be as
loose as possible to capture all its correct realizations. We also consider the {"}black
box{"} semantics of a specification which is useful to study the behavioral properties
a user can observe when he\slash she is experimenting with the system.\par
In the second part of this work, we develop proof techniques for structured
COL-specifications. For this purpose we introduce an
institution encoding from the COL
institution to the institution of many-sorted first-order logic with equality
and sort-generation constraints. Using this institution
encoding, we can then reduce proofs of
consequences of structured specifications built over COL to proofs of consequences
of structured specifications written in a simple subset of the algebraic specification
language {\scshape Casl}. This means, in particular, that any inductive theorem prover, such
as \emph{e.g.} the Larch Prover or PVS, can be used to prove theorems over structured
COL-specifications.}
}
@inproceedings{BH-Goguen06,
address = {San Diego, California, USA},
month = jun,
year = 2006,
volume = 4060,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Futatsugi, Kokichi and Jouannaud, Jean-Pierre and
Meseguer, Jos{\'e}},
acronym = {{A}lgebra, {M}eaning and {C}omputation},
booktitle = {{A}lgebra, {M}eaning and {C}omputation~--- Essays dedicated to
Joseph~A.~Goguen on the Occasion of His 65th~Birthday},
author = {Bidoit, Michel and Hennicker, Rolf},
title = {Proving Behavioral Refinements of {COL}-Specifications},
pages = {333-354},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BH-Goguen06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BH-Goguen06.pdf},
doi = {10.1007/11780274_18},
abstract = {The COL institution (constructor-based
observational logic) has been introduced as a formal
framework to specify both generation- and
observation-oriented properties of software systems. In
this paper we consider behavioral refinement relations
between COL-specifications taking into account
implementation constructions. We propose a general
strategy for proving the correctness of such
refinements by reduction to (standard) first-order
theorem proving with induction. Technically our
strategy relies on appropriate proof rules and on a
lifting construction to encode the reachability and
observability notions of the COL institution.}
}
@inproceedings{BHR06-acsd,
address = {Turku, Finland},
month = jun,
year = 2006,
publisher = {{IEEE} Computer Society Press},
editor = {Goossens, Kees and Petrucci, Laure},
acronym = {{ACSD}'06},
booktitle = {{P}roceedings of the 6th {I}nternational
{C}onference on {A}pplication of {C}oncurrency
to {S}ystem {D}esign
({ACSD}'06)},
author = {Bouyer, Patricia and Haddad, Serge and
Reynier, Pierre-Alain},
title = {Extended Timed Automata and Time {P}etri Nets},
pages = {91-100},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-01.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-01.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2006-01.ps},
doi = {10.1109/ACSD.2006.6},
abstract = {Timed Automata (TA) and Time Petri Nets (TPN) are two
well-established formal models for real-time systems. Recently, a
linear transformation of TA to TPNs preserving reachability
properties and timed languages has been proposed, which does however
not extend to larger classes of TA which would allow diagonal
constraints or more general resets of clocks. Though these features
do not add expressiveness, they yield exponentially more concise
models. \par
In this work, we propose two translations: one from extended TA to
TPNs whose size is either linear or quadratic in the size of the
original TA, depending on the features which are allowed; another
one from a parallel composition of TA to TPNs, which is also linear.
As a consequence, we get that TPNs are exponentially more concise
than~TA.}
}
@inproceedings{BHR-ICALP2006,
address = {Venice, Italy},
month = jul,
year = 2006,
volume = 4052,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Buglesi, Michele and Preneel, Bart and Sassone, Vladimiro and Wegener, Ingo},
acronym = {{ICALP}'06},
booktitle = {{P}roceedings of the 33rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'06)~--- {P}art~{II}},
author = {Bouyer, Patricia and Haddad, Serge and Reynier, Pierre-Alain},
title = {Timed {P}etri Nets and Timed Automata: On the Discriminating Power of
{Z}eno Sequences},
pages = {420-431},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-icalp06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-icalp06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHR-icalp06.ps},
doi = {10.1007/11787006_36},
abstract = {Timed Petri nets and timed
automata are two standard models for the
analysis of real-time systems. In this
paper, we prove that they are incomparable
for the timed language equivalence. Thus we
propose an extension of timed Petri nets
with read-arcs~(RA-TdPN), whose coverability
problem is decidable. We also show that this
model unifies timed Petri nets and timed
automata. Then, we establish numerous
expressiveness results and prove that Zeno
behaviours discriminate between several
sub-classes of RA-TdPNs. This has surprising
consequences on timed automata,
\emph{e.g.}~on the power of
non-deterministic clock resets.}
}
@inproceedings{BHR-atva06,
address = {Beijing, China},
month = oct,
year = {2006},
volume = 4218,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Graf, Susanne and Zhang, Wenhui},
acronym = {{ATVA}'06},
booktitle = {{P}roceedings of the 4th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'06)},
author = {Bouyer, Patricia and Haddad, Serge and Reynier, Pierre-Alain},
title = {Timed Unfoldings for Networks of Timed Automata},
pages = {292-306},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-atva06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-atva06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHR-atva06.ps},
doi = {10.1007/11901914_23},
abstract = {Whereas partial order methods have proved their efficiency for
the analysis of discrete-event systems, their application to
timed systems remains a challenging research topic. Here, we
design a verification algorithm for networks of timed automata
with invariants. Based on the unfolding technique, our method
produces a branching process as an acyclic Petri net extended
with read arcs. These arcs verify conditions on tokens without
consuming them, thus expressing concurrency between conditions
checks. They are useful for avoiding the explosion of the size
of the unfolding due to clocks which are compared with constants
but not reset. Furthermore, we attach zones to events, in addition
to markings. We~then compute a complete finite prefix of the
unfolding. The~presence of invariants goes against the concurrency
since it entails a global synchronization on time. The use of read
arcs and the analysis of the clock constraints appearing in
invariants will help increasing the concurrency relation between
events. Finally, the finite prefix we compute can be used to decide
reachability properties, and transition enabling.}
}
@incollection{BL-VAT06,
author = {Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois},
title = {V{\'e}rification par automates temporis{\'e}s},
booktitle = {Syst{\`e}mes temps-r{\'e}el~1~: techniques de description
et de v{\'e}rification},
editor = {Navet, Nicolas},
publisher = {Herm{\`e}s},
year = 2006,
month = jun,
pages = {121-150},
url = {http://www.lavoisier.fr/fr/livres/index.asp?texte=2746213030&select=isbn&from=Hermes},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BL-VAT06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BL-VAT06.ps},
isbn = {2-7462-1303-6}
}
@inproceedings{BMR-latin06,
address = {Valdivia, Chile},
month = mar,
year = 2006,
volume = 3887,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Correa, Jose R. and Hevia, Alejandro and Kiwi, Marcos},
acronym = {{LATIN}'06},
booktitle = {{P}roceedings of the 7th {L}atin {A}merican
{S}ymposium on {T}heoretical {I}nformatics
({LATIN}'06)},
author = {Bouyer, Patricia and Markey, Nicolas and Reynier, Pierre-Alain},
title = {Robust Model-Checking of Linear-Time Properties in Timed Automata},
pages = {238-249},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMR-latin06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMR-latin06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BMR-latin06.ps},
doi = {10.1007/11682462_25},
abstract = {Formal verification of timed systems
is well understood, but their
\emph{implementation} is still challenging. Recent
works by Raskin \emph{et al.} have brought out a
model of parameterized timed automata that can be
used to prove \emph{implementability} of timed
systems for safety properties. We define here a
more general notion of robust model-checking for
linear-time properties, which consists in
verifying whether a property still holds even if
the transitions are slightly delayed or expedited.
We provide PSPACE algorithms for the robust
model-checking of B{\"u}chi-like and LTL
properties. We also verify bounded-response-time
properties. }
}
@book{Bollig06,
author = {Bollig, Benedikt},
title = {Formal Models of Communicating Systems~--- Languages, Automata,
and Monadic Second-Order Logic},
year = {2006},
month = jun,
publisher = {Springer},
isbn = {3-540-32922-6},
otherurl = {http://www.springer.com/978-3-540-32922-6},
url = {http://www.lsv.ens-cachan.fr/~bollig/fmcs/},
abstract = {This book studies the relationship between automata and
monadic second-order logic, focusing on classes of automata that
describe the concurrent behavior of distributed systems.\par
It provides a unifying theory of communicating automata and their
logical properties. Based on Hanf's Theorem and Thomas's graph
acceptors, it develops a result that allows us to characterize many
popular models of distributed computation in terms of the existential
fragment of monadic second-order logic. In particular, the book covers
finite automata, asynchronous (cellular) automata, communicating
finite-state machines, and lossy channel systems. Model behavior is
described using graphs and partial orders, leading to the notions of
Mazurkiewicz traces, message sequence charts, and live sequence
charts.\par
This book is suitable for senior undergraduate and graduate courses on
advanced automata theory, concurrency and communication issues. It can
also be used as a reference by researchers concerned with the formal
modeling of concurrent systems. Some knowledge of automata theory is a
prerequisite. Numerous exercises, chapter summaries, and suggested
reading allow for self-study, while the book is supported with a website
containing course material and solutions.}
}
@inproceedings{BS05-express,
address = {San Francisco, California, USA},
month = jul,
year = 2006,
number = 3,
volume = 154,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Baeten, Jos and Phillips, Iain},
acronym = {{EXPRESS}'05},
booktitle = {{P}roceedings of the 12th {I}nternational
{W}orkshop on {E}xpressiveness in
{C}oncurrency
({EXPRESS}'05)},
author = {Bertrand, Nathalie and Schnoebelen, {\relax Ph}ilippe},
title = {A short visit to the {STS} hierarchy},
pages = {59-69},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BS05-express.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BS05-express.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BS05-express.ps},
doi = {10.1016/j.entcs.2006.05.007},
abstract = {The hierarchy of Symbolic
Transition Systems, introduced by Henzinger,
Majumdar and Raskin, is an elegant
classification
tool for some families of infinite-state
operational models that support some variants of
a symbolic {"}backward closure{"}
verification algorithm. It was first used and
illustrated with families of hybrid
systems.\par
In this paper we investigate whether the STS
hierarchy can account for classical
families of infinite-state systems outside of
timed or hybrid systems.}
}
@inproceedings{TED-hldvt06,
address = {Monterey, California, USA},
month = nov,
year = 2006,
publisher = {{IEEE} Computer Society Press},
acronym = {{HLDVT}'06},
booktitle = {{P}roceedings of the {IEEE} {H}igh {L}evel {D}esign
{V}erification and {T}est Workshop ({HLDVT}'06)},
author = {Taktak, Sami and Encrenaz, Emmanuelle and Desbarbieux, Jean-Lou},
title = {A Tool for Automatic Detection of Deadlock in Wormhole Networks
on Chip},
pages = {203-210},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/TED-hldvt06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/TED-hldvt06.pdf},
doi = {10.1109/HLDVT.2006.319992},
abstract = {We present an extension of Duato's necessary and
sufficient condition a routing function must satisfy in order to
be deadlock-free, to support environment constraints inducing
extra-dependencies between messages. We also present an original
algorithm to automatically check the deadlock-freeness of a
network with a given routing function. A~prototype tool has
been developed and automatic deadlock checking of large scale
networks with various routing functions have been successfully
achieved.}
}
@inproceedings{BE-rsp06,
address = {Chania, Crete},
month = jun,
year = 2006,
publisher = {{IEEE} Computer Society Press},
acronym = {{RSP}'06},
booktitle = {{P}roceedings of the 17th {I}nternational {W}orkshop
on {R}apid {S}ystem {P}rototyping ({RSP}'06)},
author = {Braunstein, C{\'e}cile and Encrenaz, Emmanuelle},
title = {Formalizing the incremental design and verification process of
a pipelined protocol converter},
pages = {103-109},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BE-rsp06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BE-rsp06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BE-rsp06.ps},
doi = {10.1109/RSP.2006.19},
abstract = {This work studies the relations between pipeline
architectures and their specification expressed in~CTL. We
propose a method to build pipeline structures incrementally
from a simple one (already verified) to a more complex one.
Moreover, we show how each increment can be integrated
in a CTL specification. We define increments to model
treatment delay and treatment abortion of a pipeline flow, and
we formalize the composition of the different increments. In
order to represent the increments added to an architecture,
we derive a set of CTL formulae transformations. Finally
we model a control flow of a protocol converter by
composition of these increments. We show how CTL properties
of the complex architecture are built by applying automatic
transformations on the set of CTL properties of the simplest
architecture.}
}
@inproceedings{GSZ-fsttcs2006,
address = {Kolkata, India},
month = dec,
year = 2006,
volume = 4337,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Garg, Naveen and Arun-Kumar, S.},
acronym = {{FSTTCS}'06},
booktitle = {{P}roceedings of the 26th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'06)},
author = {Gastin, Paul and Sznajder, Nathalie and Zeitoun, Marc},
title = {Distributed synthesis for well-connected architectures},
pages = {321-332},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GSZ-fsttcs2006.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GSZ-fsttcs2006.pdf},
doi = {10.1007/11944836_30},
abstract = {We study the synthesis problem for external linear or branching
specifications and distributed, synchronous architectures with arbitrary
delays on processes. External means that the specification only relates input
and output variables. We~introduce the subclass of uniformly
well-connected~(UWC) architectures for which there exists a routing allowing
each output process to get the values of all inputs it is connected to, as
soon as possible. We~prove that the distributed synthesis problem is decidable
on UWC architectures if and only if the set of all sets of input variables
visible by output variables is totally ordered, under set inclusion. We~also
show that if we extend this class by letting the routing depend on the output
process, then the previous decidability result fails. Finally, we provide a
natural restriction on specifications under which the whole class of~UWC
architectures is decidable.}
}
@proceedings{AB-lncs4202,
title = {{P}roceedings of the 4th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'06)},
booktitle = {{P}roceedings of the 4th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'06)},
editor = {Asarin, Eug{\`e}ne and Bouyer, Patricia},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 4202,
year = 2006,
month = sep,
address = {Paris, France},
isbn = {3-540-45026-2},
url = {http://www.springer.com/978-3-540-45026-2},
doi = {10.1007/11867340}
}
@inproceedings{BGP1-formats06,
address = {Paris, France},
month = sep,
year = 2006,
volume = 4202,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Asarin, Eug{\`e}ne and Bouyer, Patricia},
acronym = {{FORMATS}'06},
booktitle = {{P}roceedings of the 4th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'06)},
author = {B{\'e}rard, B{\'e}atrice and Gastin, Paul and Petit, Antoine},
title = {Refinements and abstractions of signal-event (timed) languages},
pages = {67-81},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP1-formats06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP1-formats06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BGP1-formats06.ps},
doi = {10.1007/11867340_6},
abstract = {In the classical framework of formal languages, a refinement
operation is modeled by a substitution and an abstraction by an inverse
substitution. These mechanisms have been widely studied, because they describe
a change in the specification level, from an abstract view to a more concrete
one, or conversely. For~timed systems, there is up to now no uniform notion of
substitutions. In~this paper, we study the timed substitutions in the general
framework of signal-event languages, where both signals and events are taken
into account. We~prove that regular signal-event languages are closed under
substitutions and inverse substitutions. }
}
@inproceedings{BGP2-formats06,
address = {Paris, France},
month = sep,
year = 2006,
volume = 4202,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Asarin, Eug{\`e}ne and Bouyer, Patricia},
acronym = {{FORMATS}'06},
booktitle = {{P}roceedings of the 4th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'06)},
author = {B{\'e}rard, B{\'e}atrice and Gastin, Paul and Petit, Antoine},
title = {Intersection of regular signal-event (timed) languages},
pages = {52-66},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP2-formats06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP2-formats06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BGP2-formats06.ps},
doi = {10.1007/11867340_5},
abstract = {We propose in this paper a construction for a {"}well known{"}
result: regular signal-event languages are closed by intersection. In~fact,
while this result is indeed trivial for languages defined by Alur and Dill's
timed automata (the proof is an immediate extension of the one in the untimed
case), it turns out that the construction is much more tricky when considering
the most involved model of signal-event automata. While several constructions
have been proposed in particular cases, it is the first time, up to our
knowledge, that a construction working on finite and infinite signal-event
words and taking into account signal stuttering, unobservability of
zero-duration \(\tau\)-signals and Zeno runs is proposed.}
}
@inproceedings{CDP-fsttcs2006,
address = {Kolkata, India},
month = dec,
year = 2006,
volume = 4337,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Garg, Naveen and Arun-Kumar, S.},
acronym = {{FSTTCS}'06},
booktitle = {{P}roceedings of the 26th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'06)},
author = {Chevalier, Fabrice and D'Souza, Deepak and Prabhakar, Pavithra},
title = {On continuous timed automata with input-determined guards},
pages = {369-380},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDP-fsttcs06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDP-fsttcs06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CDP-fsttcs06.ps},
doi = {10.1007/11944836_34},
abstract = {We consider a general class of timed automata parameterized by a
set of {"}input-determined{"} operators, in a continuous time setting. We show
that for any such set of operators, we have a monadic second order logic
characterization of the class of timed languages accepted by the corresponding
class of automata. Further, we consider natural timed temporal logics based on
these operators, and show that they are expressively equivalent to the
first-order fragment of the corresponding MSO logics. As~a~corollary of these
general results we obtain an expressive completeness result for the continuous
version of MTL.}
}
@inproceedings{CKKW-fsttcs2006,
address = {Kolkata, India},
month = dec,
year = 2006,
volume = 4337,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Garg, Naveen and Arun-Kumar, S.},
acronym = {{FSTTCS}'06},
booktitle = {{P}roceedings of the 26th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'06)},
author = {Cortier, V{\'e}ronique and Kremer, Steve and
K{\"u}sters, Ralf and Warinschi, Bogdan},
title = {Computationally Sound Symbolic Secrecy in the Presence of Hash Functions},
pages = {176-187},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CKKW-fsttcs06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CKKW-fsttcs06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CKKW-fsttcs06.ps},
doi = {10.1007/11944836_18},
abstract = {The standard symbolic, deducibility-based notions of secrecy are
in general insufficient from a cryptographic point of view, especially in
presence of hash functions. In~this paper we devise and motivate a more
appropriate secrecy criterion which exactly captures a standard cryptographic
notion of secrecy for protocols involving public-key enryption and hash
functions: protocols that satisfy it are computationally secure while any
violation of our criterion directly leads to an attack. Furthermore, we prove
that our criterion is decidable via an NP decision procedure. Our~results hold
for standard security notions for encryption and hash functions modeled as
random oracles.}
}
@article{CDL05-survey,
publisher = {{IOS} Press},
journal = {Journal of Computer Security},
author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie
and Lafourcade, Pascal},
title = {A Survey of Algebraic Properties Used in Cryptographic
Protocols},
year = {2006},
volume = 14,
number = 1,
pages = {1-43},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/surveyCDL.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/surveyCDL.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/surveyCDL.ps},
abstract = {Cryptographic protocols are
successfully analyzed using formal methods.
However, formal approaches usually consider the
encryption schemes as black boxes and assume that
an adversary cannot learn anything from an
encrypted message except if he has the key. Such an
assumption is too strong in general since some
attacks exploit in a clever way the interaction
between protocol rules and properties of
cryptographic operators. Moreover, the executability of some
protocols relies explicitly on some algebraic
properties of cryptographic primitives such as
commutative encryption. We give a list of some
relevant algebraic properties of cryptographic
operators, and for each of them, we provide
examples of protocols or attacks using these
properties. We also give an overview of the
existing methods in formal approaches for analyzing
cryptographic protocols.}
}
@inproceedings{CEFX-formats06,
address = {Paris, France},
month = sep,
year = 2006,
volume = 4202,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Asarin, Eug{\`e}ne and Bouyer, Patricia},
acronym = {{FORMATS}'06},
booktitle = {{P}roceedings of the 4th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'06)},
author = {Chevallier, R{\'e}my and Encrenaz{-}Tiph{\`e}ne, Emmanuelle and
Fribourg, Laurent and Xu, Weiwen},
title = {Verification of the Generic Architecture of a Memory Circuit Using
Parametric Timed Automata},
pages = {113-127},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-formats06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-formats06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CEFX-formats06.ps},
econtrat = {MEDEA+ Blueberries},
doi = {10.1007/11867340_9},
abstract = {Using a variant of Clariso-Cortadella's parametric method
for verifying asynchronous circuits, we formally derive a set of linear
constraints that ensure the correctness of some crucial timing behaviours
of the architecture of SPSMALL memory. This allows us to check two
different implementations of this architecture.}
}
@article{CEFX-wseas06,
publisher = {World Scientific and Engineering Academy and Society},
journal = {WSEAS Transactions on Circuits and Systems},
author = {Chevallier, R{\'e}my and Encrenaz{-}Tiph{\`e}ne, Emmanuelle and
Fribourg, Laurent and Xu, Weiwen},
title = {Timing analysis of an embedded memory: {SPSMALL}},
pages = {973-978},
volume = 5,
number = 7,
year = 2006,
month = jul,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-wseas06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-wseas06.pdf},
abstract = {This paper proposes a high-level formalism, called
Abstract Functional and Timing Graph~(AFTG), for describing a memory
architecture, which combines logical functionality and timing. After
translation of the~AFTG into the form a timed automaton, we are able to
compute the response times of the modeled memory, and check their consistency
with the values specified in the datasheet. We also address the problem of
finding optimal values of setup timings.}
}
@inproceedings{DDFG-atva06,
address = {Beijing, China},
month = oct,
year = {2006},
volume = 4218,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Graf, Susanne and Zhang, Wenhui},
acronym = {{ATVA}'06},
booktitle = {{P}roceedings of the 4th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'06)},
author = {Demri, St{\'e}phane and Finkel, Alain
and Goranko, Valentin and van Drimmelen, Govert},
title = {Towards a model-checker for counter systems},
pages = {493-507},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDFG-atva06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDFG-atva06.pdf},
doi = {10.1007/11901914_36},
abstract = {This paper deals with model-checking of fragments and extensions
of~\(\mathrm{CTL}^{*}\) on infinite-state Presburger counter systems, where
the states are vectors of integers and the transitions are determined by means
of relations definable within Presburger arithmetic. We have identified a
natural class of admissible counter systems~(ACS) for which we show that the
quantification over paths in~\(\mathrm{CTL}^{*}\) can be simulated by
quantification over tuples of natural numbers, eventually allowing translation
of the whole Presburger-\(\mathrm{CTL}^{*}\) into Presburger arithmetic,
thereby enabling effective model checking. We have provided evidence that our
results are close to optimal with respect to the class of counter systems
described above. Finally, we design a complete semi-algorithm to verify
first-order~\(\mathrm{LTL}\) properties over trace-flattable counter systems,
extending the previous underlying FAST semi-algorithm to verify reachability
questions over flattable counter systems. }
}
@inproceedings{DL-lics2006,
address = {Seattle, Washington, USA},
month = aug,
year = 2006,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'06},
booktitle = {{P}roceedings of the 21st
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'06)},
author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko},
title = {{LTL} with the freeze quantifier and register automata},
pages = {17-26},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DL-lics2006.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DL-lics2006.pdf},
doi = {10.1109/LICS.2006.31},
abstract = {Temporal logics, first-order logics, and automata over data
words have recently attracted considerable attention. A~data word is a word
over a finite alphabet, together with a datum (an element of an infinite
domain) at each position. Examples include timed words and XML documents. To
refer to the data, temporal logics are extended with the freeze quantifier,
first-order logics with predicates over the data domain, and automata with
registers or pebbles.\par
We investigate relative expressiveness and complexity of standard decision
problems for~\(\mathrm{LTL}\) with the freeze
quantifier~(\(\mathrm{LTL}^{\downarrow}\)), 2-variable first-order logic
(\(\mathrm{FO}^{2}\)) over data words, and register automata. The only
predicate available on data is equality. Previously undiscovered connections
among those formalisms, and to counter automata with in- crementing errors,
enable us to answer several questions left open in recent literature.\par
We show that the future-time fragment of~\(\mathrm{LTL}^{\downarrow}\)
which corresponds to \(\mathrm{FO}^{2}\) over finite data words can be
extended considerably while preserving decidability, but at the expense of
non-primitive recursive complexity, and that most of further extensions are
undecidable. We also prove that surprisingly, over infinite data words,
\(\mathrm{LTL}^{\downarrow}\) without the `until' operator, as well as
nonemptiness of one-way universal register automata, are undecidable even when
there is only one register.}
}
@inproceedings{DL-ijcar06,
address = {Seattle, Washington, USA},
month = aug,
year = 2006,
volume = 4130,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer-Verlag},
editor = {Furbach, Ulrich and Shankar, Natarajan},
acronym = {{IJCAR}'06},
booktitle = {{P}roceedings of the 3rd {I}nternational {J}oint
{C}onference on {A}utomated {R}easoning
({IJCAR}'06)},
author = {Demri, St{\'e}phane and Lugiez, Denis},
title = {{P}resburger Modal Logic is Only {PSPACE}-complete},
pages = {541-556},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-25.pdf},
doi = {10.1007/11814771_44},
abstract = {We introduce a Presburger modal logic PML with regularity
constraints and full Presburger constraints on the number of children that
generalize graded modalities, also known as number restrictions in description
logics. We~show that PML satisfiability is only PSPACE-complete by designing a
Ladner-like algorithm that can be turned into an analytic proof system
algorithm. This extends a well-known and non-trivial PSPACE upper bound for
graded modal logic. Furthermore, we provide a detailed comparison with logics
that contain Presburger constraints and that are dedicated to query XML
documents. As~an application, we show that satisfiability for Sheaves Logic SL
is PSPACE-complete, improving significantly its best known upper bound.}
}
@article{delaune-tcs06,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Delaune, St{\'e}phanie},
title = {An Undecidability Result for~{\textsf{\MakeUppercase{AG}h}}},
volume = 368,
number = {1-2},
pages = {161-167},
year = 2006,
month = dec,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/delaune-tcs06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/delaune-tcs06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/delaune-tcs06.ps},
doi = {10.1016/j.tcs.2006.08.018},
abstract = {We present an undecidability result for
the verification of security protocols. Since the
\emph{perfect cryptography assumption} is unrealistic
for cryptographic primitives with visible algebraic
properties, several recent works relax this assumption,
allowing the intruder to exploit these properties. We
are interested in the \emph{Abelian groups} theory in
combination with the homomorphism axiom. We show that
satisfaisability of symbolic deducibility constraints
is undecidable, obtaining in this way the first
undecidability result concerning a theory for which
unification is known to be decidable~[F.~Baader, Unification
in commutative theories, Hilbert's basis theorem, and
Gr{\"{o}}bner
bases, J.~ACM~40(3) (1993)~477-503].}
}
@inproceedings{DKR-wote06,
address = {Cambridge, UK},
month = jun,
year = 2006,
acronym = {{WOTE}'06},
booktitle = {{P}roceedings of the {IAVoSS} {W}orkshop {O}n {T}rustworthy {E}lections
({WOTE}'06)},
author = {Delaune, St{\'e}phanie and Kremer, Steve and
Ryan, Mark D.},
title = {Verifying Properties of Electronic Voting Protocols},
pages = {45-52},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-wote06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-wote06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DKR-wote06.ps},
abstract = {In this paper we report on some recent work to formally specify
and verify electronic voting protocols. In particular, we use the formalism of
the applied pi calculus: the applied pi calculus is a formal language
similar to the pi calculus but with useful extensions for modelling
cryptographic protocols. We model several important properties, namely
fairness, eligibility, privacy, receipt-freeness and coercion-resistance.
Verification of these properties is illustrated on two cases studies and has
been partially automated using the Blanchet's ProVerif tool.}
}
@inproceedings{DKR-csfw06,
address = {Venice, Italy},
month = jul,
year = 2006,
publisher = {{IEEE} Computer Society Press},
acronym = {{CSFW}'06},
booktitle = {{P}roceedings of the
19th {IEEE} {C}omputer {S}ecurity {F}oundations
{W}orkshop ({CSFW}'06)},
author = {Delaune, St{\'e}phanie and Kremer, Steve and
Ryan, Mark D.},
title = {Coercion-Resistance and Receipt-Freeness in
Electronic Voting},
pages = {28-39},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-csfw06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-csfw06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DKR-csfw06.ps},
doi = {10.1109/CSFW.2006.8},
abstract = {In this paper we formally study
important properties of electronic voting protocols.
In particular we are interested in
coercion-resistance and receipt-freeness.
Intuitively, an election protocol is
coercion-resistant if a voter \(A\) cannot prove to a
potential coercer~\(C\) that she voted in a particular
way. We assume that \(A\) cooperates with~\(C\) in an
interactive way. Receipt-freeness is a weaker
property, for which we assume that \(A\) and~\(C\)
cannot interact during the protocol, but \(A\) later
provides evidence (the receipt) of how she voted.
While receipt-freeness can be expressed using
observational equivalence from the applied pi
calculus, we need to introduce a new relation to
capture coercion-resistance. Our formalization of
coercion-resistance and receipt-freeness are quite
different. Nevertheless, we show in accordance with
intuition that coercion-resistance implies
receipt-freeness, which implies privacy, the basic
anonymity property of voting protocols, as defined
in previous work. Finally we illustrate the
definitions on a simplified version of the
Lee~\emph{et~al.}\ voting protocol.}
}
@inproceedings{DLLT-ICALP2006,
address = {Venice, Italy},
month = jul,
year = 2006,
volume = 4052,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Buglesi, Michele and Preneel, Bart and Sassone, Vladimiro and Wegener, Ingo},
acronym = {{ICALP}'06},
booktitle = {{P}roceedings of the 33rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'06)~--- {P}art~{II}},
author = {Delaune, St{\'e}phanie and Lafourcade, Pascal and
Lugiez, Denis and Treinen, Ralf},
title = {Symbolic Protocol Analysis in Presence of a Homomorphism
Operator and {\emph{Exclusive~Or}}},
pages = {132-143},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLLT-icalp06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLLT-icalp06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DLLT-icalp06.ps},
doi = {10.1007/11787006_12},
abstract = {Security of a cryptographic
protocol for a bounded number of sessions is
usually expressed as a symbolic trace
reachability problem. We show that symbolic
trace reachability for well-defined protocols
is decidable in presence of the exclusive or
theory in combination with the homomorphism
axiom. These theories allow us to model basic
properties of important cryptographic
operators. This trace reachability problem
can be expressed as a system of symbolic
deducibility constraints for a certain
inference system describing the capabilities
of the attacker. One main step of our proof
consists in reducing deducibility constraints
to constraints for deducibility in one step
of the inference system. This constraint
system, in turn, can be expressed as a system
of quadratic equations of a particular form
over \(\mathbb{Z}/2\mathbb{Z}[h]\), the ring
of polynomials in one indeterminate over the
finite field \(\mathbb{Z}/2\mathbb{Z}\). We
show that satisfiability of such systems is
decidable. }
}
@proceedings{CK-fcc2006,
editor = {Cortier, V{\'e}ronique and Kremer, Steve},
booktitle = {{P}roceedings of the 2nd {W}orkshop on {F}ormal and
{C}omputational {C}ryptography ({FCC}'06)},
title = {{P}roceedings of the 2nd {W}orkshop on {F}ormal and
{C}omputational {C}ryptography ({FCC}'06)},
address = {Venice, Italy},
year = 2006,
month = jul,
url = {http://hal.inria.fr/FCC2006/}
}
@article{CKS-jar2005,
publisher = {Springer},
journal = {Journal of Automated Reasoning},
author = {Chadha, Rohit and Kremer, Steve and Scedrov, Andre},
title = {Formal Analysis of Multi-Party Contract Signing},
volume = 36,
number = {1-2},
pages = {39-83},
year = 2006,
month = jan,
nmnote = {Special Issue on Automated Reasoning for Security Protocol Analysis},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/mpcs-CKS.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/mpcs-CKS.pdf},
doi = {10.1007/s10817-005-9019-5},
abstract = {We analyze the multi-party contract-signing protocols
of Garay and MacKenzie (GM) and of Baum and Waidner
(BW). We use a finite-state tool, {\scshape Mocha},
which allows specification of protocol properties in
a branching-time temporal logic with game semantics.
While our analysis does not reveal any errors in the
BW protocol, in the GM protocol we discover serious
problems with fairness for four signers and an
oversight regarding abuse-freeness for three signers.
We propose a complete revision of the GM subprotocols
in order to restore fairness.}
}
@article{dj-jar05,
publisher = {Springer},
journal = {Journal of Automated Reasoning},
author = {Delaune, St{\'e}phanie and Jacquemard, Florent},
title = {Decision Procedures for the Security of
Protocols with Probabilistic Encryption against
Offline Dictionary Attacks},
volume = 36,
number = {1-2},
year = 2006,
month = jan,
pages = {85-124},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DJ-jar05.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DJ-jar05.ps},
doi = {10.1007/s10817-005-9017-7},
abstract = {We consider the problem of formal
automatic verification of cryptographic protocols
when some data, like poorly chosen passwords, can
be guessed by dictionary attacks. First, we define
a theory of these attacks and propose an inference
system modeling the deduction capabilities of an
intruder. This system extends a set of well
studied deduction rules for symmetric and public
key encryption often called Dolev-Yao rules with
the introduction of a probabilistic encryption
operator and guessing abilities for the intruder.
Then, we show that the intruder deduction problem
in this extended model is decidable in~PTIME. The
proof is based on a locality lemma for our
inference system. This first result yields to an
NP decision procedure for the protocol insecurity
problem in presence of a passive intruder. In the
active case, the same problem is proved to be
NP-complete: we give a procedure for
simultaneously solving symbolic constraints with
variables which represent intruder deductions. We
illustrate the procedure with examples of
published protocols and compare our model to other
recent formal definitions of dictionary attacks.}
}
@article{SD-ipl05,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Delaune, St{\'e}phanie},
title = {Easy Intruder Deduction Problems with Homomorphisms},
volume = 97,
number = 6,
pages = {213-218},
month = mar,
year = 2006,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SD-ipl05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SD-ipl05.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/SD-ipl05.ps},
doi = {10.1016/j.ipl.2005.11.008},
abstract = {We present complexity results for
the verification of security protocols. Since
the perfect cryptography assumption is
unrealistic for cryptographic primitives with
visible algebraic properties, we extend the
classical \emph{Dolev-Yao} model by permitting
the intruder to exploit these properties. More
precisely, we are interested in theories such
as \emph{Exclusive or} and \emph{Abelian
groups} in combination with the homomorphism
axiom. We show that the intruder deduction
problem is in PTIME in both cases, improving
the EXPTIME complexity results presented
in~(Lafourcade, Lugiez, Treinen,~2005).}
}
@article{Demri06,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Demri, St{\'e}phane},
title = {{LTL} over integer periodicity constraints},
year = {2006},
volume = 360,
number = {1-3},
pages = {96-123},
month = aug,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-tcs06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-tcs06.pdf},
doi = {10.1016/j.tcs.2006.02.019},
abstract = {Periodicity constraints are used
in many logical formalisms, in fragments of Presburger~LTL,
in calendar logics, and in logics for access
control, to quote a few examples. In the paper, we
introduce the logic PLTL\(^{\mathrm{mod}}\), an
extension of Linear-Time Temporal Logic LTL with
past-time operators whose atomic formulae are defined
from a first-order constraint language dealing with
periodicity. Although the underlying constraint language
is a fragment of Presburger arithmetic shown to admit a
{\scshape pspace}-complete satisfiability problem, we establish
that PLTL\(^{\mathrm{mod}}\) model-checking and
satisfiability problems remain in {\scshape pspace} as plain~LTL
(full Presburger LTL is known to be highly undecidable).
This is particularly interesting for dealing with
periodicity constraints since the language of
PLTL\(^{\mathrm{mod}}\) has a language more concise than
existing languages and the temporalization of our
first-order language of periodicity constraints has the
same worst case complexity as the underlying constraint
language. Finally, we show examples of introduction the
quantification in the logical language that provide to
PLTL\(^{\mathrm{mod}}\), {\scshape expspace}-complete
problems. As another application, we establish that the
equivalence problem for extended single-string automata,
known to express the equality of time granularities, is
{\scshape pspace}-complete by designing a reduction from~QBF and by
using our results for PLTL\(^{\mathrm{mod}}\). }
}
@article{DLS-jcss-param,
publisher = {Elsevier Science Publishers},
journal = {Journal of Computer and System Sciences},
author = {Demri, St{\'e}phane and Laroussinie, Fran{\c{c}}ois
and Schnoebelen, {\relax Ph}ilippe},
title = {A Parametric Analysis of the State Explosion Problem in
Model Checking},
year = 2006,
month = jun,
volume = 72,
number = 4,
pages = {547-575},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLS-jcss-param.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLS-jcss-param.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DLS-jcss-param.ps},
doi = {10.1016/j.jcss.2005.11.003},
abstract = {In model checking, the
state-explosion problem occurs when one checks a
non-flat system, \emph{i.e.}, a system implicitly
described as a synchronized product of elementary
subsystems. In this paper, we investigate the
complexity of a wide variety of model checking
problems for non-flat systems under the light of
parameterized complexity, taking the number of
synchronized components as a parameter. We provide
precise complexity measures (in the parameterized
sense) for most of the problems we investigate, and
evidence that the results are robust.}
}
@article{FGRV-tcs05,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
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},
year = 2006,
month = may,
volume = 356,
number = 3,
pages = {374-386},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGRV-TCS04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGRV-TCS04.pdf},
doi = {10.1016/j.tcs.2006.02.008},
abstract = {In this paper, we study the expressive power of several
monotonic extensions of Petri
nets. We compare the expressive power of Petri nets, Petri nets extended
with \emph{non-blocking arcs} and Petri nets extended with \emph{transfer arcs},
in terms of \(\omega\)-languages.
We show that the hierarchy of expressive powers of those models is strict. To prove
these results, we propose \emph{original techniques} that rely on
well-quasi orderings and monotonicity properties.}
}
@article{FMP-dc05,
publisher = {Springer},
journal = {Distributed Computing},
author = {Fribourg, Laurent and Messika, St{\'e}phane and
Picaronny, Claudine},
title = {Coupling and Self-Stabilization},
year = 2006,
month = feb,
volume = 18,
number = 3,
pages = {221-232},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/dcmessika.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/dcmessika.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/dcmessika.pdf},
doi = {10.1007/s00446-005-0142-7},
abstract = {A randomized self-stabilizing algorithm~\(\mathcal{A}\)
is an algorithm that, whatever the initial configuration
is, reaches a set~\(\mathcal{L}\) of \emph{legal configurations} in finite time
with probability~1. The proof of convergence towards~\(\mathcal{L}\)
is generally done by exhibiting a potential function~\(\varphi\),
which measures the {"}vertical{"} distance of any configuration
to~\(\mathcal{L}\), such that \(\varphi\) decreases with non-null probability
at each step of~\(\mathcal{A}\). We propose here a method, based on
the notion of coupling, which makes use of a {"}horizontal{"}
distance~\(\delta\) between any pair of configurations, such that \(\delta\)
decreases in expectation at each step of~\(\mathcal{A}\). In contrast
with classical methods, our coupling method does not
require the knowledge of~\(\mathcal{L}\). In addition to the proof of
convergence, the method allows us to assess the convergence
rate according to two different measures. Proofs
produced by the method are often simpler or give better
upper bounds than their classical counterparts, as
examplified here on Herman's mutual exclusion and Iterated
Prisoner's Dilemma algorithms in the case of cyclic
graphs.}
}
@inproceedings{BGM-atva2006,
address = {Beijing, China},
month = oct,
year = {2006},
volume = 4218,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Graf, Susanne and Zhang, Wenhui},
acronym = {{ATVA}'06},
booktitle = {{P}roceedings of the 4th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'06)},
author = {Bhateja, Puneet and Gastin, Paul and Mukund, Madhavan},
title = {A fresh look at testing for asynchronous communication},
pages = {369-383},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGM-atva06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGM-atva06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BGM-atva06.ps},
doi = {10.1007/11901914_28},
abstract = {Testing is one of the fundamental techniques for verifying if a
computing system conforms to its specification. We~take a fresh look at the
theory of testing for message-passing systems based on a natural notion of
observability in terms of input-output relations. We~propose two notions of
test equivalence: one which corresponds to presenting all test inputs up front
and the other which corresponds to interactively feeding inputs to the system
under test. We compare our notions with those studied earlier, notably the
equivalence proposed by Tretmans. In~Tretmans' framework, asynchrony is
modelled using synchronous communication by augmenting the state space of the
system with queues. We~show that the first equivalence we consider is strictly
weaker than Tretmans' equivalence and undecidable, whereas the second notion
is incomparable. We~also establish (un)decidability results for these
equivalences.}
}
@article{DG-icomp2006,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Diekert, Volker and Gastin, Paul},
title = {Pure future local temporal logics are expressively complete for
{M}azurkiewicz traces},
pages = {1597-1619},
year = 2006,
month = nov,
volume = 204,
number = 11,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-icomp06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-icomp06.pdf},
doi = {10.1016/j.ic.2006.07.002},
abstract = {The paper settles a long standing problem for Mazurkiewicz
traces: the pure future local temporal logic defined with the basic modalities
exists-next and until is expressively complete. This means every first-order
definable language of Mazurkiewicz traces can be defined in a pure future
local temporal logic. The~analogous result with a global interpretation has
been known, but the treatment of a local interpretation turned out to be much
more involved. Local logics are interesting because both the satisfiability
problem and the model checking problem are solvable in PSPACE for these logics
whereas they are non-elementary for global logics. Both, the (previously
known) global and the (new) local results generalize Kamp's Theorem for words,
because for sequences local and global viewpoints coincide. }
}
@article{DG06-TCS,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Diekert, Volker and Gastin, Paul},
title = {From local to global temporal logics over {M}azurkiewicz traces},
year = 2006,
month = may,
volume = 356,
number = {1-2},
pages = {126-135},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG06-TCS.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG06-TCS.pdf},
doi = {10.1016/j.tcs.2006.01.035},
abstract = {We review some results on global and local temporal logic on
Mazurkiewicz traces. Our~main contribution is to show how to derive the
expressive completeness of global temporal logic with respect to first-order
logic [V.~Diekert, P.~Gastin, LTL~is expressively complete for Mazurkiewicz
traces, J.~Comput. System Sci.~64 (2002) 396-418] from the similar result on
local temporal logic [V.~Diekert, P.~Gastin, Pure future local temporal logics
are expressively complete for Mazurkiewicz traces, in: M.~Farach-Colton~(Ed.),
Proc.~LATIN'04, Lecture Notes in Computer Science, Vol.~2976, Springer,
Berlin, 2004, pp.~232-241, Full version available as Research Report
LSV-05-22, Laboratoire Sp\'ecification et V\'erification, ENS Cachan, France].}
}
@inproceedings{JRV-ijcar06,
address = {Seattle, Washington, USA},
month = aug,
year = 2006,
volume = 4130,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer-Verlag},
editor = {Furbach, Ulrich and Shankar, Natarajan},
acronym = {{IJCAR}'06},
booktitle = {{P}roceedings of the 3rd {I}nternational {J}oint
{C}onference on {A}utomated {R}easoning
({IJCAR}'06)},
author = {Jacquemard, Florent and Rusinowitch, Micha{\"e}l
and Vigneron, Laurent},
title = {Tree automata with equality constraints modulo equational
theories},
pages = {557-571},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-07.pdf},
doi = {10.1007/11814771_45},
abstract = {This paper presents new classes
of tree automata combining automata with
equality test and automata modulo equational
theories. We believe that this class has a
good potential for application in
\emph{e.g.}~software verification. These tree
automata are obtained by extending the
standard Horn clause representations with
equational conditions and rewrite systems.
We show in particular that a generalized
membership problem (extending the emptiness
problem) is decidable by proving that the
saturation of tree automata presentations
with suitable paramodulation strategies
terminates. Alternatively our results can be
viewed as new decidable classes of
first-order formula.}
}
@misc{markey-SynthVerif06,
author = {Markey, Nicolas},
title = {Verification of Multi-Agent Systems with~{ATL}},
year = 2006,
month = oct,
howpublished = {Invited talk, FNRS meeting on {"}Synthesis and
Verification{"}}
}
@article{KucSch-TCS,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Ku{\v c}era, Anton{\'\i}n and
Schnoebelen, {\relax Ph}ilippe},
title = {A General Approach to Comparing Infinite-State Systems
with Their Finite-State Specifications},
number = {2-3},
volume = {358},
pages = {315-333},
month = aug,
year = 2006,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KucSch-TCS.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KucSch-TCS.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/KucSch-TCS.ps},
doi = {10.1016/j.tcs.2006.01.021},
abstract = {We introduce a generic family of
behavioral relations for which the regular
equivalence problem (\emph{i.e.}, comparing an arbitrary
transition system to some finite-state
specification) can be reduced to the model
checking problem against simple modal formulae.
As an application, we derive decidability of
several regular equivalence problems for
well-known families of infinite-state systems. }
}
@inproceedings{LLT-unif2006,
address = {Seattle, Washington, USA},
month = aug,
year = 2006,
editor = {Levy, Jordi},
acronym = {{UNIF}'06},
booktitle = {{P}roceedings of the 20th {I}nternational
{W}orkshop on {U}nification
({UNIF}'06)},
author = {Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf},
title = {{ACUNh}: Unification and Disunification Using Automata Theory},
pages = {6-20},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LLT-unif06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LLT-unif06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LLT-unif06.ps},
abstract = {We show several results about unification problems in the
equational theory~ACUNh consisting of the theory of exclusive or with one
homomorphism. These results are shown using only techniques of automata and
combinations of unification problems. We~show how to construct a most-general
unifier for ACUNh-unification problems with constants using automata. We also
prove that the first-order theory of ground terms modulo~ACUNh is decidable if
the signature does not contain free non-constant function symbols, and that
the existential fragment is decidable in the general case. Furthermore, we
show a technical result about the set of most-general unifiers obtained for
general unification problems.}
}
@inproceedings{BJ-unif2006,
address = {Seattle, Washington, USA},
month = aug,
year = 2006,
editor = {Levy, Jordi},
acronym = {{UNIF}'06},
booktitle = {{P}roceedings of the 20th {I}nternational
{W}orkshop on {U}nification
({UNIF}'06)},
author = {Bouhoula, Adel and Jacquemard, Florent},
title = {Automating Sufficient Completeness Check for Conditional
and Constrained~{TRS}},
nopages = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BJ-unif06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BJ-unif06.pdf},
abstract = {We present a procedure for checking sufficient completeness for
conditional and constrained term rewriting systems containing axioms for
constructors which may be constrained (by~e.g.~equalities, disequalities,
ordering, membership...). Such axioms allow to specify complex data structures
like e.g.~sets, sorted lists or powerlists. Our approach is integrated in a
framework for inductive theorem proving based on tree grammars with
constraints, a formalism which permits an exact representation of languages of
ground constructor terms in normal form. The key technique used in the
procedure is a generalized form of narrowing where, given a term, instead of
unifying it with left members of rewrite rules, we instantiate it, at selected
variables, following the productions of a constrained tree grammar, and test
whether it can be rewritten. Our~procedure is sound and complete and has been
successfully applied to several examples, yielding very natural proofs and, in
case of negative answer, a counter example suggesting how to complete the
specification. Moreover, it is a decision procedure when the TRS is
unconditional but constrained, for a large class of constrained constructor
axioms.}
}
@inproceedings{LMO-formats06,
address = {Paris, France},
month = sep,
year = 2006,
volume = 4202,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Asarin, Eug{\`e}ne and Bouyer, Patricia},
acronym = {{FORMATS}'06},
booktitle = {{P}roceedings of the 4th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'06)},
author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and
Oreiby, Ghassan},
title = {Model Checking Timed {ATL} for Durational Concurrent
Game Structures},
pages = {245-259},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMO-formats06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMO-formats06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LMO-formats06.ps},
doi = {10.1007/11867340_18},
abstract = {We extend the framework of ATL model-checking to {"}simply
timed{"} concurrent game structures, i.e., multi-agent structures where
each transition carry an integral duration (or interval thereof). While
the case of single durations is easily handled from the semantics point of
view, intervals of durations raise several interesting questions. Moreover
subtle algorithmic problems have to be handled when dealing with model
checking. We propose a semantics for which we develop efficient (PTIME)
algorithms for timed ATL without equality constraints, while the general
case is shown to be EXPTIME-complete.}
}
@article{LMS-tcs05,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas
and Schnoebelen, {\relax Ph}ilippe},
title = {Efficient Timed Model Checking for Discrete-Time
Systems},
volume = 353,
number = {1-3},
pages = {249-271},
month = mar,
year = 2006,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMS-TCS05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMS-TCS05.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LMS-TCS05.ps},
doi = {10.1016/j.tcs.2005.11.020},
abstract = {We consider model checking of timed
temporal formulae in \emph{durational transition
graphs} (DTGs), \emph{i.e.}, Kripke structures where
transitions have integer durations. Two semantics for
DTGs are presented and motivated. We consider timed
versions of CTL where subscripts put quantitative
constraints on the time it takes before a property is
satisfied. \par
We exhibit an important gap between logics where
subscripts of the form {"}\(= c\){"} (exact duration) are
allowed, and simpler logics that only allow subscripts
of the form {"}\(\leq c\){"} or {"}\(\geq c\){"} (bounded
duration).\par
Without exact durations, model checking can be done in
polynomial time, but with exact durations, it becomes
\(\Delta_{2}^{P}\)-complete or PSPACE-complete
depending on the considered semantics.}
}
@inproceedings{MOJ-aisc2006,
address = {Beijing, China},
month = sep,
year = 2006,
volume = 4120,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Calmet, Jacques and Ida, Tetsuo and Wang, Dongming},
acronym = {{AISC}'06},
booktitle = {{P}roceedings of the 8th {I}nternational {C}onference
on {A}rtificial {I}ntelligence and {S}ymbolic {C}omputation
({AISC}'06)},
author = {Mitsuhashi, Ichiro and Oyamaguchi, Michio and Jacquemard, Florent},
title = {The Confluence Problem for Flat~{TRSs}},
pages = {68-81},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MOJ-aisc06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MOJ-aisc06.pdf},
doi = {10.1007/11856290_8},
abstract = {We prove that the properties of reachability, joinability and
confluence are undecidable for flat~TRSs. Here, a~TRS is flat if the heights
of the left and right-hand sides of each rewrite rule are at most one.}
}
@article{MR-TCS05,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Markey, Nicolas and Raskin, Jean-Fran{\c{c}}ois},
title = {Model Checking Restricted Sets of Timed Paths},
year = {2006},
month = aug,
volume = 358,
number = {2-3},
pages = {273-292},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Markey-Raskin-TCS05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Markey-Raskin-TCS05.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/
Markey-Raskin-TCS05.ps},
doi = {10.1016/j.tcs.2006.01.019},
abstract = {In this paper, we study the complexity of
model-checking formulas of four important real-time
logics (TPTL, MTL, MITL, and TCTL) over restricted sets
of timed paths. The classes of restricted sets of timed
paths that we consider are \textit{(i)}~a~single finite
(or ultimately periodic) timed path,
\textit{(ii)}~an~infinite set of finite (or infinite)
timed paths defined by a finite (or ultimately periodic)
path in a region graph, \textit{(iii)}~an~infinite set of
finite (or infinite) timed paths defined by a finite (or
ultimately periodic) path in a zone graph.
\par
Several results are quite negative: TPTL and MTL
remain undecidable along
region- and zone-paths. On the other hand,
we obtained PTIME algorithms for
model checking TCTL along a region path,
and for MTL along a single timed path.}
}
@article{MS05-IPL,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
title = {Mu-Calculus Path Checking},
volume = 97,
number = 6,
month = mar,
year = 2006,
pages = {225-230},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MS05-IPL.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MS05-IPL.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MS05-IPL.ps},
doi = {10.1016/j.ipl.2005.11.010},
abstract = {We investigate the path model
checking problem for the \(\mu\)-calculus.
Surprisingly, restricting to deterministic
structures does not allow for more efficient model
checking algorithm, as we prove that it can encode
any instance of the standard model checking problem
for the \(\mu\)-calculus. }
}
@article{RS-btl2,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Rabinovich, Alexander and
Schnoebelen, {\relax Ph}ilippe},
title = {{\(\mathit{\MakeUppercase{BTL}}_2\)} and the expressive
power of {\(\mathit{\MakeUppercase{ECTL}}^+\)}},
year = 2006,
month = jul,
volume = 204,
number = 7,
pages = {1023-1044},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BTL2-InfComp.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BTL2-InfComp.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BTL2-InfComp.ps},
doi = {10.1016/j.ic.2005.07.006},
abstract = {We show that \(\mathit{ECTL}^+\), the
classical extension of \(\mathit{CTL}\) with fairness
properties, is expressively equivalent to
\(\mathit{BTL}_2\), a natural fragment of the monadic
logic of order. \(\mathit{BTL}_2\)~is the branching-time
logic with arbitrary quantification over paths, and
where path formulae are restricted to quantifier
depth~\(2\) first-order formulae in the monadic logic of
order. This result, linking \(\mathit{ECTL}^+\) to a
natural fragment of the monadic logic of order, provides
a characterization that other branching-time logics,
\emph{e.g.}, \(\mathit{CTL}\), lack. \par
We then go on to show that \(\mathit{ECTL}^+\) and
\(\mathit{BTL}_2\) are not finitely based (\emph{i.e.},
they cannot be defined by a finite set of temporal
modalities) and that their model-checking problems are
of the same complexity. }
}
@misc{phs-lipn2006,
author = {Schnoebelen, {\relax Ph}ilippe},
title = {De nouvelles applications pour le model-checking},
year = {2006},
month = nov,
howpublished = {Invited lecture, Journ{\'e}es {\`a} l'occasion des
20~ans du~LIPN, Villetaneuse, France}
}
@phdthesis{THESE-bernat06,
author = {Bernat, Vincent},
title = {Th{\'e}ories de l'intrus pour la v{\'e}rification
des protocoles cryptographiques},
year = 2006,
month = jun,
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-bernat.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-bernat.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/these-bernat.ps}
}
@phdthesis{THESE-delaune06,
author = {Delaune, St{\'e}phanie},
title = {V{\'e}rification des protocoles cryptographiques
et propri{\'e}t{\'e}s alg{\'e}briques},
year = 2006,
month = jun,
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-delaune.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-delaune.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/these-delaune.ps},
abstract = {Cryptographic protocols are small concurrent programs designed
to guarantee the security of exchanges between participants using non-secure
medium. Establishing the correctness of these protocols is crucial given the
increasing number of applications, such as electronic commerce, that exchange
information on the Internet. Unfortunately, the existence of cryptographic
primitives such as encryption is not sufficient to ensure security. The
security of exchanges is ensured by cryptographic protocols which are
notoriously error-prone.\par
The formal verification of cryptographic protocols is a difficult problem that
can be seen as a particular model-checking problem in an hostile environment.
To verify such protocols, a line of research consists in considering
encryption as a black box and assuming that an adversary can't learn anything
from an encrypted message except if he has the key. This is called the
\emph{perfect cryptography} assumption. Many results have been obtained under
this assumption, but such an assumption is too strong in general. Some attacks
exploit in a clever way the interaction between protocol rules and properties
of cryptographic operators. \par
In this thesis, we relax the perfect cryptography assumption by taking into
account some algebraic properties of cryptographic primitives. We give
decision procedures for the security problem in presence of several algebraic
operators.}
}
@phdthesis{THESE-lafourcade06,
author = {Lafourcade, Pascal},
title = {V{\'e}rification des protocoles cryptographiques
en pr{\'e}sence de th{\'e}ories {\'e}quationnelles},
year = 2006,
month = sep,
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-lafourcade.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-lafourcade.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/these-lafourcade.ps},
note = {209~pages},
abstract = {The rise of the internet of new technologies has reinforced the
key role of computer science in communication technology. The recent progress
in these technologies has brought a dramatic change in the ways how we
communicate and consume. All these communication activities are subject to
complex communication protocols that a user does not control completely. Users
of communication protocols require that their communications are {"}secure{"}.
The developers of these communication protocols aim to secure communications
in a hostile environment by cryptographic means. Such an environment consists
of a dishonest communication participant, called an {"}intruder{"} or
{"}attacker{"}... We suppose that the intruder controls the network on which
the messages are exchanged.\par
The verification of a cryptographic protocol either ensures that no attack is
possible against the execution of the protocol in presence of a certain
intruder, or otherwise exhibits an attack. One important assumption in the
verification of cryptographic protocols is the so-called {"}perfect
cryptography assumption{"}, which states that the only way to obtain knowledge
about an encrypted message is to know its decryption key. This hypothesis is
not sufficient to guarantee security in reality. It is possible that certain
properties used in the protocol allow the intruder to obtain some
information.\par
One way to weaken this perfect cryptography assumption is to take into account
in the model certain algebraic properties. We develop a formal approach for
verifying the so-called secrecy property of cryptographic protocols in the
presence of equational theories and of homomorphism.}
}
@phdthesis{THESE-belmokadem06,
author = {Bel{ }mokadem, Houda},
title = {V{\'e}rification des propri{\'e}t{\'e}s temporis{\'e}es des
automates programmables industriels},
year = 2006,
month = sep,
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-mokadem.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-mokadem.pdf}
}
@phdthesis{THESE-bertrand06,
author = {Bertrand, Nathalie},
title = {Mod{\`e}les stochastiques pour les pertes de messages dans les
protocoles asynchrones et techniques de v{\'e}rification automatique},
year = 2006,
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/these-bertrand.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-bertrand.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/these-bertrand.ps}
}
@mastersthesis{naves-master,
author = {Naves, Guyslain},
title = {Accessibilit{\'e} dans les automates temporis{\'e}s {\`a} deux horloges},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = 2006,
month = sep,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/master-naves.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/master-naves.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/master-naves.ps}
}
@mastersthesis{akshay-master,
author = {Akshay, S.},
title = {Formal Specification and Verification of Timed Communicating Systems},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
month = sep,
year = 2006,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Akshay-M2.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Akshay-M2.pdf}
}
@mastersthesis{brochenin-master,
author = {Brochenin, R{\'e}mi},
title = {Techniques d'automates pour raisonner sur la m{\'e}moire},
school = {{M}aster {R}echerche {I}nformatique de {L}yon~---
{I}nformatique {F}ondamentale, Lyon, France},
type = {Rapport de {M}aster},
month = jun,
year = 2006,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Brochenin-M2.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Brochenin-M2.ps}
}
@mastersthesis{bursuc-master,
author = {Bursuc, Sergiu},
title = {Contraintes de d{\'e}ductibilit{\'e} modulo
Associativit{\'e}-Commutativit{\'e}},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
month = sep,
year = 2006,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bursuc-M2.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bursuc-M2.pdf}
}
@techreport{LSV:06:11,
author = {Bollig, Benedikt and Kuske, Dietrich},
title = {Distributed {M}uller Automata and Logics},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = 2006,
month = may,
type = {Research Report},
number = {LSV-06-11},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-11.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-11.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2006-11.ps},
note = {23~pages},
abstract = {We consider Muller asynchronous cellular automata running on
infinite dags over distributed alphabets. We show that they have the same
expressive power as the existential fragment of a monadic second-order logic
featuring a first-order quantifier to express that there are infinitely many
elements satisfying some property. Our result is based on an extension of the
classical Ehrenfeucht-Fra{\"\i}ss{\'e} game to cope with infinite structures
and the new first-order quantifier. As a byproduct, we obtain a logical
characterization of unbounded Muller message-passing automata running on
infinite message sequence charts.}
}
@techreport{LSV:06:13,
author = {Olivain, Julien and Goubault{-}Larrecq, Jean},
title = {Detecting Subverted Cryptographic Protocols by Entropy Checking},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = 2006,
month = jun,
type = {Research Report},
number = {LSV-06-13},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-13.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-13.pdf},
note = {19~pages},
abstract = {What happens when your implementation of SSL or some other
cryptographic protocol is subverted through a buffer overflow
attack? You have been hacked, right. Unfortunately, you may be
unaware of~it: since normal traffic is encrypted, most IDSs cannot
monitor~it. We propose a simple, yet efficient technique to detect
such attacks, by computing the entropy of the flow and comparing it
against known thresholds. This was implemented in the Net-Entropy
sensor.}
}
@techreport{Prouve:rap9,
author = {Klay, Francis and Bozga, Liana and Lakhnech, Yassine and
Mazar{\'e}, Laurent and Delaune, St{\'e}phanie and
Kremer, Steve},
title = {Retour d'exp{\'e}rience sur la validation du vote {\'e}lectronique},
institution = {projet RNTL PROUV{\'E}},
month = nov,
year = 2006,
type = {Technical Report},
number = 9,
note = {47~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/prouve-rap9.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/prouve-rap9.pdf},
abstract = {Dans ce rapport, nous pr{\'e}sentons le travail de
v{\'e}rification qui a {\'e}t{\'e} r{\'e}alis{\'e} sur le protocole de
vote {\'e}lectronique que nous avons introduit et formalis{\'e} dans le
rapport RNTL Prouv{\'e} num{\'e}ro~\(6\). Ce protocole a {\'e}t{\'e} mis au
point par J.~Traor{\'e}, ing{\'e}nieur de recherche chez France
T{\'e}l{\'e}com. Il est bas{\'e} sur le m{\'e}canisme de signature en
aveugle et peut {\^e}tre consid{\'e}r{\'e} comme un d{\'e}riv{\'e} du
protocole de Fujioka, Okamoto et~Ohta.\par
La formalisation de ce protocole {\`a} mis en {\'e}vidence une grande
complexit{\'e} due en particulier aux structures de donn{\'e}es et aux
primitives cryptographiques manipul{\'e}es. D'un autre c{\^o}t{\'e} ce
travail a {\'e}galement r{\'e}v{\'e}l{\'e} que les propri{\'e}t{\'e}s de
s{\^u}ret{\'e} {\`a} garantir sont particuli{\`e}rement subtiles.
Ce~document pr{\'e}sente les r{\'e}sultats qui ont {\'e}t{\'e} obtenus
lors de la v{\'e}rification de ce protocole. En particulier nous montrons
que certaines propri{\'e}t{\'e}s de s{\^u}ret{\'e} ont pu {\^e}tre
prouv{\'e}es automatiquement alors que pour d'autres une preuve manuelle
s'est av{\'e}r{\'e}e n{\'e}cessaire.}
}
@misc{versydis-final,
author = {Gastin, Paul and others},
title = {{ACI} {S}{\'e}curit{\'e} {I}nformatique {VERSYDIS}~---
Rapport final},
year = 2006,
month = oct,
type = {Contract Report},
note = {10~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Versydis-final.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Versydis-final.pdf}
}
@misc{cortos-final,
author = {Bouyer, Patricia and others},
title = {{ACI} {S}{\'e}curit{\'e} {I}nformatique {CORTOS}~---
Rapport final},
year = 2006,
month = nov,
type = {Contract Report},
note = {17~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Cortos-final.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Cortos-final.pdf}
}
@misc{persee-final,
author = {Schnoebelen, {\relax Ph}ilippe and Bouajjani, Ahmed and Sutre, Gr{\'e}goire},
title = {{ACI} {S}{\'e}curit{\'e} {I}nformatique {PERS{\'E}E}~---
Rapport final},
year = 2006,
month = nov,
type = {Contract Report},
note = {12~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Persee-final.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Persee-final.pdf}
}
@article{Baudet05jalc,
journal = {Journal of Automata, Languages and Combinatorics},
author = {Baudet, Mathieu},
title = {Random Polynomial-Time Attacks and {D}olev-{Y}ao Models},
year = 2006,
volume = 11,
number = 1,
pages = {7-21},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bau05-jalc.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bau05-jalc.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bau05-jalc.ps},
abstract = {In this paper we present an extension of
Dolev-Yao models for security protocols with a notion
of random polynomial-time (Las Vegas) computability.
First we notice that Dolev-Yao models can be seen as
transition systems, possibly infinite. We then extend
these transition systems with computation times and
probabilities. The extended models can account for
normal Dolev-Yao transitions as well as nonstandard
operations such as inverting a one-way function. Our
main contribution consists of showing that under
reasonable assumptions the extended models are
equivalent to standard Dolev-Yao models as far as
(safety) security properties are concerned.}
}
@article{Demri-jancl06,
publisher = {Taylor \& Francis},
journal = {Journal of Applied Non-Classical Logics},
author = {Demri, St{\'e}phane},
title = {Linear-Time Temporal Logics with {P}resburger Constraints: An~Overview},
year = 2006,
volume = 16,
number = {3-4},
pages = {311-347},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-jancl06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-jancl06.pdf},
abstract = {We present an overview of linear-time temporal logics with
Presburger constraints whose models are sequences of tuples of integers. Such
formal specification languages are well-designed to specify and verify systems
that can be modelled with counter systems. The paper recalls the general
framework of LTL over concrete domains and presents the main decidability and
complexity results related to fragments of Presburger~LTL. Related formalisms
are also briefly presented.}
}
@misc{NB-SuMo-2006,
author = {Bertrand, Nathalie},
title = {SuMo~-- Reachability analysis for lossy channels},
month = feb,
year = {2006},
note = {See~\cite{BBS-forte06} for a description. Written in~OCaml (3000~lines)},
note-fr = {Voir la description dans~\cite{BBS-forte06}. {\'E}crit
en~OCaml (3000~lignes)}
}
@misc{gastex-v2.8,
author = {Gastin, Paul},
title = {Gas{{\TeX}}: Graphs and Automata Simplified in~{{\TeX}} (v2.8)},
year = {2006},
month = nov,
nohowpublished = {Available at http://www.lsv.ens-cachan.fr/~gastin/gastex/gastex.html},
note = {Written in~\TeX (about 2000 lines)},
note-fr = {\'Ecrit en~\TeX (environ 2000 lignes)},
url = {http://www.lsv.ens-cachan.fr/~gastin/gastex/gastex.html}
}
@proceedings{AGHMR-sasyft04,
title = {Selected papers of the International Workshop on
Security Analysis of Systems: Formalisms and Tools
({SASYFT}'04)},
booktitle = {Selected papers of the International Workshop on
Security Analysis of Systems: Formalisms and Tools
({SASYFT}'04)},
editor = {Anantharaman, Siva and Gastin, Paul and Hains, Ga{\'e}tan and
Mullins, John and Rusinowitch, Micha{\"e}l},
year = 2006,
address = {Orl{\'e}ans, France},
journal = {jalc},
volume = 11,
number = 1
}
@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.