@techreport{Averroes-4.2.2,
author = {Duflot, Marie and Fribourg, Laurent and
H{\'e}rault, {\relax Th}omas and
Lassaigne, Richard and
Magniette, Fr{\'e}d{\'e}ric and
Messika, St{\'e}phane and
Peyronnet, Sylvain and Picaronny, Claudine},
title = {Probabilistic Model Checking of the {CSMA/CD} Protocol
Using {PRISM} and {APMC}},
year = {2004},
month = jun,
type = {Contract Report},
number = {(Lot 4.2 fourniture 2)},
institution = {projet RNTL Averroes},
oldhowpublished = {Lot 4.2 fourniture 2, du projet RNTL Averroes},
note = {22~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Averroes-4.2.2.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Averroes-4.2.2.ps}
}
@inproceedings{B04sasyft,
address = {Orl{\'e}ans, France},
howpublished = {LIFO Technical Report 2004-11, Laboratoire d'Informatique Fondamentale d'Orl{\'e}ans,
France},
month = jun,
year = 2004,
editor = {Anantharaman, Siva},
acronym = {{SASYFT}'04},
booktitle = {{P}roceedings of the {W}orkshop on {S}ecurity
of {S}ystems: {F}ormalism and {T}ools
({SASYFT}'04)},
author = {Baudet, Mathieu},
title = {Random Polynomial-Time Attacks and {D}olev-{Y}ao
Models},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/B04sasyft.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/B04sasyft.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/B04sasyft.pdf},
preliminary-version-of = {Baudet05jalc},
abstract = {For several decades two different
communities have been working on the formal security of
cryptographic protocols. Many efforts have been made
recently to take benefit of both approaches, in brief: the
comprehensiveness of computational models and the
automatizability of formal methods. The purpose of this
paper is to investigate an original approach to relate the
two views, that is: to extend existing Dolev-Yao models to
account for random polynomial-time (Las Vegas)
computability. This is done first by noticing 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 sufficient realistic assumptions the extended models
are equivalent to standard Dolev-Yao models as far as
security is concerned. Thus our work enlarges the scope of
existing decision procedures.}
}
@misc{bouyer-movep2004,
author = {Bouyer, Patricia},
title = {Timed Automata~--- {F}rom Theory to Implementation},
year = 2004,
month = dec,
note = {27~pages},
howpublished = {Invited tutorial, 6th {W}inter {S}chool on
{M}odelling and {V}erifying {P}arallel {P}rocesses
({MOVEP}'04), Brussels, Belgium}
}
@misc{gastin-movep2004,
author = {Gastin, Paul},
title = {Basics of model checking},
year = 2004,
month = dec,
nonote = {-- pages},
howpublished = {Invited tutorial, 6th {W}inter {S}chool on
{M}odelling and {V}erifying {P}arallel {P}rocesses
({MOVEP}'04), Brussels, Belgium}
}
@misc{bouyer-epit32,
author = {Bouyer, Patricia},
title = {Timed Models for Concurrent Systems},
year = 2004,
month = apr,
howpublished = {Invited lecture, 32nd {S}pring {S}chool on
{T}heoretical {C}omputer {S}cience ({C}oncurrency {T}heory),
Luminy, France}
}
@misc{gastin-epit32,
author = {Gastin, Paul},
title = {Specifications for distributed systems},
year = 2004,
month = apr,
howpublished = {Invited lecture, 32nd {S}pring {S}chool on
{T}heoretical {C}omputer {S}cience ({C}oncurrency {T}heory),
Luminy, France}
}
@misc{bouyer-qest04,
author = {Bouyer, Patricia},
title = {Timed Automata~--- {F}rom Theory to Implementation},
year = 2004,
month = sep,
howpublished = {Invited tutorial, 1st International Conference on the
Quantitative Evaluation of System (QEST'04),
Twente, The Netherlands}
}
@inproceedings{BBL-hscc2004,
address = {Philadelphia, Pennsylvania, USA},
month = mar,
year = 2004,
volume = 2993,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Alur, Rajeev and Pappas, George J.},
acronym = {{HSCC}'04},
booktitle = {{P}roceedings of the 7th {I}nternational {C}onference
on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
({HSCC}'04)},
author = {Bouyer, Patricia and Brinksma, Ed and
Larsen, Kim G.},
title = {Staying Alive As Cheaply As Possible},
pages = {203-218},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBL-hscc04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBL-hscc04.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBL-hscc04.ps},
abstract = {This paper is concerned with the
derivation of infinite schedules for timed automata
that are in some sense optimal. To cover a wide class
of optimality criteria we start out by introducing an
extension of the (priced) timed automata model that
includes both costs and rewards as separate modelling
features. A precise definition is then given of what
constitutes optimal infinite behaviours for this class
of models. We subsequently show that the derivation of
optimal non-terminating schedules for such
double-priced timed automata is computable. This is
done by a reduction of the problem to the determination
of optimal mean-cycles in finite graphs with weighted
edges. This reduction is obtained by introducing the
so-called corner-point abstraction, a powerful
abstraction technique of which we show that it
preserves optimal schedules. }
}
@inproceedings{BBLP-tacas04,
address = {Barcelona, Spain},
month = mar,
year = 2004,
volume = 2988,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Jensen, Kurt and Podelski, Andreas},
acronym = {{TACAS}'04},
booktitle = {{P}roceedings of the 10th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'04)},
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},
pages = {312-326},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBLP-tacas04.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBLP-tacas04.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBLP-tacas04.pdf},
abstract = {Timed automata have an infinite
semantics. 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{BBP-IJPR04,
publisher = {Taylor \& Francis},
journal = {International Journal of Production Research},
author = {B{\'e}rard, B{\'e}atrice and Bouyer, Patricia and
Antoine Petit},
title = {Analysing the {PGM} Protocol with {U}ppaal},
volume = {42},
number = {14},
pages = {2773-2791},
year = {2004},
month = jul,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBP-IJPR04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBP-IJPR04.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBP-IJPR04.ps},
abstract = {Pragmatic General Multicast (PGM)
is a reliable multicast protocol, designed to
minimize both the probability of negative
acknowledgements~(NAK) implosion and the load
of the network due to retransmissions of lost
packets. This protocol was presented to the
Internet Engineering Task Force as an open
reference specification.\par
In this paper, we focus on the main
reliability property which PGM intends to
guarantee: a receiver either receives all data
packets from transmissions and repairs or is
able to detect unrecoverable data packet loss.
\par
We first propose a modelization of (a
simplified version of) PGM via a network of
timed automata. Using Uppaal model-checker, we
then study the validity of the reliability
property above, which turns out not to be
always verified but to depend on the values of
several parameters that we underscore.}
}
@inproceedings{BBS-afadl2004,
address = {Besan{\c{c}}on, France},
month = jun,
year = 2004,
editor = {Julliand, Jacques},
acronym = {{AFADL}'04},
booktitle = {{A}ctes du 6{\`e}me {A}telier sur les {A}pproches {F}ormelles
dans l'{A}ssistance au {D}{\'e}veloppement de {L}ogiciels
({AFADL}'04)},
author = {Ben{ }Gaid, Mongi and B{\'e}rard, B{\'e}atrice and
De{~}Smet, Olivier},
title = {Mod{\'e}lisation et v{\'e}rification d'un
{\'e}vaporateur en {Uppaal}},
pages = {223-238},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-afadl04.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBS-afadl04.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-afadl04.pdf}
}
@inproceedings{BDF-afadl2004,
address = {Besan{\c{c}}on, France},
month = jun,
year = 2004,
editor = {Julliand, Jacques},
acronym = {{AFADL}'04},
booktitle = {{A}ctes du 6{\`e}me {A}telier sur les {A}pproches {F}ormelles
dans l'{A}ssistance au {D}{\'e}veloppement de {L}ogiciels
({AFADL}'04)},
author = {Bardin, S{\'e}bastien and
Darlot, {\relax Ch}ristophe and Finkel, Alain},
title = {{FAST}: un model-checker pour syst{\`e}mes {\`a}
compteurs},
pages = {377-380},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDF-afadl04.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDF-afadl04.ps},
abstract = {FAST est un outil pour la
v\'erification de propri\'et\'es de s\^uret\'e
pour des syst\`emes \`a compteurs.
L'originalit\'e de l'outil tient dans
l'utilisation de repr\'esentations symboliques
pour repr\'esenter des ensembles infinis et de
techniques d'acc\'el\'eration pour augmenter
les chances de convergence. FAST a \'et\'e
appliqu\'e avec succ\`es \`a un grand nombre de
cas non triviaux.}
}
@article{BDFP04,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Bouyer, Patricia and Dufourd, Catherine and
Fleury, Emmanuel and Petit, Antoine},
title = {Updatable Timed Automata},
volume = {321},
number = {2-3},
pages = {291-345},
year = {2004},
month = aug,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/uta-BDFP04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/uta-BDFP04.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/uta-BDFP04.ps},
doi = {10.1016/j.tcs.2004.04.003},
abstract = {We investigate extensions of Alur and
Dill's timed automata, based on the possibility to
update the clocks in a more elaborate way than simply
reset them to zero. We call these automata updatable
timed automata. They form an undecidable class of
models, in the sense that emptiness checking is not
decidable. However, using an extension of the region
graph construction, we exhibit interesting decidable
subclasses. In a surprising way, decidability depends
on the nature of the clock constraints which are
used, diagonal-free or not, whereas these constraints
play identical roles in timed automata. We thus
describe in a quite precise way the thin frontier
between decidable and undecidable classes of
updatable timed automata. \par
We also study the
expressive power of updatable timed automata. It
turns out that any updatable automaton belonging to
some decidable subclass can be effectively
transformed into an equivalent timed automaton
without updates but with silent transitions. The
transformation suffers from an enormous combinatorics
blow-up which seems unavoidable. Therefore, updatable
timed automata appear to be a concise model for
representing and analyzing large classes of timed
systems. }
}
@inproceedings{BF-atva04,
address = {Taipei, Taiwan},
month = oct # {-} # nov,
year = {2004},
volume = {3299},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Wang, Farn},
acronym = {{ATVA}'04},
booktitle = {{P}roceedings of the 2nd {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'04)},
author = {Bardin, S{\'e}bastien and Finkel, Alain},
title = {Composition of accelerations to verify infinite
heterogeneous systems},
pages = {248-262},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BF-atva04.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BF-atva04.ps},
abstract = {Symbolic representations and
acceleration algorithms are emerging methods to
extend model-checking to infinite state space
systems. However until now, there is no general
theory of acceleration, and designing
acceleration algorithms for new data types is a
complex task. On the other hand, protocols
rarely manipulate new data types, rather new
combinations of well-studied data types. For
this reason, in this paper we focus on the
automatic construction of symbolic
representations and acceleration algorithms
from existing ones.}
}
@inproceedings{BFL-tacas04,
address = {Barcelona, Spain},
month = mar,
year = 2004,
volume = 2988,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Jensen, Kurt and Podelski, Andreas},
acronym = {{TACAS}'04},
booktitle = {{P}roceedings of the 10th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'04)},
author = {Bardin, S{\'e}bastien and Finkel, Alain and
Leroux, J{\'e}r{\^o}me},
title = {{FAST}er Acceleration of Counter Automata in
Practice},
pages = {576-590},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BFL-tacas04.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BFL-tacas04.ps},
abstract = {We compute reachability sets of
counter automata. Even if the reachability set
is not necessarily recursive, we use symbolic
representation and acceleration to increase
convergence. For functions defined by
translations over a polyhedral domain, we give
a new acceleration algorithm which is
polynomial in the size of the function and
exponential in its dimension, while the more
generic algorithm is exponential in both the
size of the function and its dimension. This
algorithm has been implemented in the tool
FAST. We apply it to a complex industrial
protocol, the TTP membership algorithm. This
protocol has been widely studied. For the first
time, the protocol is automatically proved to
be correct for \(1\)~fault and \(N\)~stations,
and using abstraction we prove the correctness
for \(2\)~faults and \(N\)~stations also.}
}
@inproceedings{BFN-avis2004,
address = {Barcelona, Spain},
month = apr,
year = 2004,
editor = {Bharadwaj, Ramesh},
acronym = {{AVIS}'04},
booktitle = {{P}roceedings of the 3rd {I}nternational
{W}orkshop on {A}utomated {V}erification
of {I}nfinite-{S}tate {S}ystems
({AVIS}'04)},
author = {Bardin, S{\'e}bastien and Finkel, Alain and
Nowak, David},
title = {Toward Symbolic Verification of Programs Handling
Pointers},
nopages = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BFN-avis2004.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BFN-avis2004.ps},
abstract = {We aim at checking safety
properties on systems with pointers which are
naturally infinite state systems. In this
paper, we introduce Symbolic Memory States, a
new symbolic representation well suited to the
verification of systems with pointers. We show
SMS enjoys all the good properties needed to
check safety properties, such as closure under
union, canonicity of the representation and
decidable inclusion. We also introduce pointer
automata, a model for programs using dynamic
allocation of memory. We define the properties
we want to check in this model and we give
undecidability results. The verification part
is still work in progress.}
}
@inproceedings{BP-coast04,
address = {Besan{\c{c}}on, France},
month = jun,
year = 2004,
editor = {Julliand, Jacques},
acronym = {{AFADL}'04},
booktitle = {{A}ctes du 6{\`e}me {A}telier sur les {A}pproches {F}ormelles
dans l'{A}ssistance au {D}{\'e}veloppement de {L}ogiciels
({AFADL}'04)},
author = {Bardin, S{\'e}bastien and Petrucci, Laure},
title = {{COAST}: des r{\'e}seaux de {P}etri {\`a} la
planification assist{\'e}e},
pages = {285-298},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BP-afadl04.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BP-afadl04.ps},
abstract = {COAST est un outil d'assistance
\`a la planification militaire. Son
architecture distribu\'ee comprend un serveur
constitu\'e d'un moteur d'analyse de r\'eseaux
de Petri tandis que l'interface graphique
fournie par le client permet de masquer
l'utilisation des m\'ethodes formelles. Les
synchronisations entre t\^aches \`a planifier
sont un aspect essentiel de COAST. Dans cet
article, apr\`es une pr\'esentation
g\'en\'erale de la probl\'ematique et de
l'outil, nous d\'ecrivons les synchronisations,
montrons comment elles sont mod\'elis\'ees et
implant\'ees.}
}
@inproceedings{BP-pnml2004,
address = {Bologna, Italy},
month = jun,
year = {2004},
editor = {Kindler, Ekkart},
booktitle = {{P}roceedings of the {W}orkshop on
{I}nterchange {F}ormat for {P}etri {N}ets},
author = {Bardin, S{\'e}bastien and Petrucci, Laure},
title = {From {PNML} to Counter Systems for Accelerating
{P}etri Nets with~{FAST}},
pages = {26-40},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BP-pnml04.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BP-pnml04.ps},
abstract = {We use the tool FAST to check
parameterized safety properties on Petri nets
with a large or infinite state space. Although
this tool is not dedicated to Petri nets, it
can be used for these as place\slash transition
nets (and some of their extensions) are
subcases of FAST input model. The originality
of the tool lies in the use of acceleration
techniques in order to compute the exact
reachability set for infinite systems.\par
In this paper, we present the automatic
transformation of Petri nets written in PNML
(Petri Net Markup Language) into counter
systems. Then, FAST provides a simple but very
powerful language to express complex properties
and check these.}
}
@inproceedings{BCFL-fsttcs04,
address = {Chennai, India},
month = dec,
year = 2004,
volume = 3328,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Lodaya, Kamal and Mahajan, Meena},
acronym = {{FSTTCS}'04},
booktitle = {{P}roceedings of the 24th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'04)},
author = {Bouyer, Patricia and Cassez, Franck and
Fleury, Emmanuel and
Larsen, Kim G.},
title = {Optimal Strategies in Priced Timed Game Automata},
pages = {148-160},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFL-fsttcs04.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/
BCFL-fsttcs04.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFL-fsttcs04.pdf},
abstract = {Priced timed (game) automata extend
timed (game) automata with costs on both locations
and transitions. In this paper we focus on
reachability priced timed game automata and prove
that the optimal cost for winning such a game is
computable under conditions concerning the
non-zenoness of cost. Under stronger conditions
(strictness of constraints) we prove that in case an
optimal strategy exists, we can compute a
state-based winning optimal strategy.}
}
@inproceedings{BerSch-avis2004,
address = {Barcelona, Spain},
month = apr,
year = 2004,
editor = {Bharadwaj, Ramesh},
acronym = {{AVIS}'04},
booktitle = {{P}roceedings of the 3rd {I}nternational
{W}orkshop on {A}utomated {V}erification
of {I}nfinite-{S}tate {S}ystems
({AVIS}'04)},
author = {Bertrand, Nathalie and
Schnoebelen, {\relax Ph}ilippe},
title = {Verifying Nondeterministic Channel Systems With
Probabilistic Message Losses},
nopages = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BerSch-avis04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BerSch-avis04.pdf},
abstract = {Lossy channel systems (LCS's) are
systems of finite state automata that communicate
via unreliable unbounded fifo channels. In order to
circumvent the undecidability of model checking for
nondeterministic LCS's, probabilistic models have
been introduced, where it can be decided whether a
linear-time property holds almost surely. However,
such fully probabilistic systems are not a faithful
model of nondeterministic protocols.\par
We study a hybrid model for LCS's where losses of
messages are seen as faults occurring with some
given probability, and where the internal behavior
of the system remains nondeterministic. Thus the
semantics is in terms of infinite-state reactive
Markov chains (equivalently, Markovian decision
processes). A similar model was introduced in the
second part of (Bertrand \& Schnoebelen,
FOSSACS'2003, LNCS 2620, pp.~120-135): we continue
this work and give a complete picture of the
decidability of qualitative model checking for
MSO-definable properties and some relevant
subcases.}
}
@book{CASL-LNCS,
author = {Bidoit, Michel and Mosses, Peter D.},
title = {{CASL} User Manual~--- Introduction to Using the
Common
Algebraic Specification Language},
volume = {2900},
series = {Lecture Notes in Computer Science},
year = {2004},
publisher = {Springer},
isbn10 = {3-540-20766-X},
isbn = {978-3-540-20766-5},
doi = {10.1007/b11968},
url = {http://www.springer.com/978-3-540-20766-X},
oldurl = {http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-20766-X}
}
@mastersthesis{Chevalier-dea,
author = {Chevalier, Fabrice},
title = {D{\'e}tection d'erreurs dans les syst{\`e}mes
temporis{\'e}s},
year = {2004},
month = sep,
type = {Rapport de {DEA}},
school = {{DEA} Algorithmique, Paris, France},
note = {59~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FC-dea2004.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FC-dea2004.ps}
}
@article{ComonCortier04scp,
publisher = {Elsevier Science Publishers},
journal = {Science of Computer Programming},
author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique},
title = {Security Properties: {T}wo Agents are Sufficient},
volume = {50},
number = {1-3},
pages = {51-71},
year = {2004},
month = mar,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComonCortier-step2.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComonCortier-step2.ps}
}
@inproceedings{DCMM-hscc2004,
address = {Philadelphia, Pennsylvania, USA},
month = mar,
year = 2004,
volume = 2993,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Alur, Rajeev and Pappas, George J.},
acronym = {{HSCC}'04},
booktitle = {{P}roceedings of the 7th {I}nternational {C}onference
on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
({HSCC}'04)},
author = {Davoren, Jennifer M. and Coulthard, Vaughan and
Markey, Nicolas and
Moor, {\relax Th}omas},
title = {Non-deterministic Temporal Logics for General Flow
Systems},
pages = {280-295},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HSCC04-DCMM.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HSCC04-DCMM.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HSCC04-DCMM.pdf},
abstract = {In this paper, we use the constructs of branching temporal logic to
formalize reasoning about a class of general flow systems, including
discrete-time transition systems, continuous-time differential
inclusions,
and hybrid-time
systems such as hybrid automata. We introduce Full General Flow Logic,
GFL\(^*\),
which has essentially the same syntax as the well-known Full Computation Tree
Logic, CTL\(^*\),
but generalizes the semantics to general flow systems over arbitrary
time-lines. We propose an axiomatic proof system for GFL\(^*\) and establish its
soundness w.r.t. the general flow semantics.}
}
@inproceedings{DDMR-formats2004,
address = {Grenoble, France},
month = sep,
year = 2004,
volume = {3253},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Lakhnech, Yassine and Yovine, Sergio},
acronym = {{FORMATS}'04/{FTRTFT}'04},
booktitle = {{P}roceedings of the {J}oint {C}onferences
{F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'04) and
{F}ormal {T}echniques in {R}eal-{T}ime and
{F}ault-{T}olerant {S}ystems ({FTRTFT}'04)},
author = {De{~}Wulf, Martin and Doyen, Laurent and
Markey, Nicolas and
Raskin, Jean-Fran{\c{c}}ois},
title = {Robustness and Implementability of Timed Automata},
pages = {118-133},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDMR-formats2004.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DDMR-formats2004.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDMR-formats2004.pdf},
abstract = {In a former paper, we defined a new semantics for timed
automata, the Almost ASAP semantics, which is parameterized by
\(\Delta\)
to cope with the reaction delay of the controller. We showed that this
semantics is implementable provided there exists a strictly positive value
for the parameter \(\Delta\) for which the strategy is correct. In this paper, we
define the implementability problem to be the question of existence of
such a \(\Delta\). We show that this question is closely related to a notion of
robustness for timed automata defined in [Pur98] and prove that the
implementability problem is decidable.}
}
@article{DFP-DISTCOMP,
publisher = {Springer},
journal = {Distributed Computing},
author = {Duflot, Marie and Fribourg, Laurent and
Picaronny, Claudine},
title = {Randomized Dining Philosophers Without Fairness
Assumption},
volume = {17},
number = {1},
pages = {65-76},
year = {2004},
month = feb,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DFP-DISCOMP.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DFP-DISCOMP.ps},
doi = {10.1007/s00446-003-0102-z}
}
@article{icomp-DG2004,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Diekert, Volker and Gastin, Paul},
title = {Local temporal logic is expressively complete for
cograph dependence alphabets},
volume = {195},
number = {1-2},
pages = {30-52},
year = 2004,
month = nov,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG04-icomp.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DG04-icomp.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG04-icomp.pdf},
doi = {10.1016/j.ic.2004.08.001},
abstract = {Recently, local logics for Mazurkiewicz
traces are of increasing interest. This is mainly
due to the fact that the satisfiability problem has
the same complexity as in the word case. If we focus
on a purely local interpretation of formulae at
vertices (or events) of a trace, then the
satisfiability problem of linear temporal logics
over traces turns out to be PSPACE-complete. But
now the difficult problem is to obtain expressive
completeness results with respect to first order
logic. \par
The main result of the paper shows such an
expressive completeness result, if the underlying
dependence alphabet is a cograph, \emph{i.e.}
if all
traces are series parallel posets. Moreover, we show
that this is the best we can expect in our setting:
If the dependence alphabet is not a cograph, then we
cannot express all first order properties.}
}
@inproceedings{Dem-fossacs2004,
address = {Barcelona, Spain},
month = mar,
year = 2004,
volume = 2987,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Walukiewicz, Igor},
acronym = {{FoSSaCS}'04},
booktitle = {{P}roceedings of the 7th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'04)},
author = {Demri, St{\'e}phane},
title = {{LTL} over Integer Periodicity Constraints},
pages = {121-135},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri-fossacs04.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Demri-fossacs04.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri-fossacs04.pdf}
}
@misc{FAST-v1.5,
author = {Bardin, S{\'e}bastien and Darlot, {\relax Ch}ristophe and
Finkel, Alain and Leroux, J{\'e}r{\^o}me and Van{~}Begin, Laurent},
futureauthor = {Il en manque ? Plus maintenant...},
title = {{FAST}~v1.5: {F}ast {A}cceleration of {S}ymbolic
{T}ransition Systems},
year = {2004},
month = jun,
howpublished = {Available at \url{http://www.lsv.ens-cachan.fr/fast/}},
url = {http://www.lsv.ens-cachan.fr/fast/}
}
@inproceedings{FL-cav04,
address = {Boston, Massachusetts, USA},
month = jul,
year = 2004,
volume = 3114,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Alur, Rajeev and Peled, Doron A.},
acronym = {{CAV}'04},
booktitle = {{P}roceedings of the 16th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'04)},
author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me},
title = {Image Computation in Infinite State Model Checking},
pages = {361-371},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FL-cav04.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FL-cav04.ps}
}
@inproceedings{FL-spin04,
address = {Barcelona, Spain},
month = apr,
year = 2004,
volume = 2989,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Graf, Susanne and Mounier, Laurent},
acronym = {{SPIN}'04},
booktitle = {{P}roceedings of the 11th {I}nternational
{SPIN} {W}orkshop on {M}odel {C}hecking {S}oftware
({SPIN}'04)},
author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me},
title = {Polynomial Time Image Computation With
Interval-Definable Counters Systems},
pages = {182-197},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FL-spin04.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FL-spin04.ps}
}
@inproceedings{FMP-disc04,
address = {Amsterdam, The Netherlands},
month = oct,
year = 2004,
volume = 3274,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Guerraoui, Rachid},
acronym = {{DISC}'04},
booktitle = {{P}roceedings of the 18th {I}nternational
{S}ymposium on {D}istributed {C}omputing
({DISC}'04)},
author = {Fribourg, Laurent and Messika, St{\'e}phane and
Picaronny, Claudine},
title = {Coupling and Self-Stabilization},
pages = {201-215},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FMP-disc04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FMP-disc04.pdf}
}
@article{FMP-wstsPN-icomp,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Finkel, Alain and McKenzie, Pierre and Picaronny, Claudine},
title = {A Well-Structured Framework for Analysing {P}etri Net
Extensions},
volume = {195},
number = {1-2},
pages = {1-29},
year = {2004},
month = nov,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FMP-wstsPN-icomp.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FMP-wstsPN-icomp.ps},
doi = {10.1016/j.ic.2004.01.005}
}
@inproceedings{GLNZ-csl2004,
address = {Karpacz, Poland},
month = sep,
year = 2004,
volume = {3210},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Marcinkowski, Jerzy and Tarlecki, Andrzej},
acronym = {{CSL}'04},
booktitle = {{P}roceedings the 18th {I}nternational
{W}orkshop on {C}omputer {S}cience {L}ogic
({CSL}'04)},
author = {Goubault{-}Larrecq, Jean and Lasota, S{\l}awomir
and Nowak, David and
Zhang, Yu},
title = {Complete Lax Logical Relations for Cryptographic
Lambda-Calculi},
pages = {400-414},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GLLNZ-csl04.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GLLNZ-csl04.ps}
}
@inproceedings{KucSch2004,
address = {London, UK},
month = aug,
year = 2004,
volume = 3170,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gardner, {\relax Ph}ilippa and Yoshida, Nobuko},
acronym = {{CONCUR}'04},
booktitle = {{P}roceedings of the 15th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'04)},
author = {Ku{\v c}era, Anton{\'\i}n and
Schnoebelen, {\relax Ph}ilippe},
title = {A General Approach to Comparing Infinite-State Systems
with Their Finite-State Specifications},
pages = {372-386},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KS-concur2004.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KS-concur2004.pdf},
doi = {10.1007/978-3-540-28644-8_24},
abstract = {We introduce a generic family of behavioral relations for
which the
problem of comparing an arbitrary transition system to some
finite-state specification can be reduced to a model checking problem
against simple modal formulae. As an application, we derive
decidability of several regular equivalence problems for well-known
families of infinite-state systems.}
}
@inproceedings{LMS-concur2004,
address = {London, UK},
month = aug,
year = 2004,
volume = 3170,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gardner, {\relax Ph}ilippa and Yoshida, Nobuko},
acronym = {{CONCUR}'04},
booktitle = {{P}roceedings of the 15th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'04)},
author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and
Schnoebelen, {\relax Ph}ilippe},
title = {Model Checking Timed Automata with One or Two Clocks},
pages = {387-401},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMS-concur2004.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LMS-concur2004.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMS-concur2004.pdf},
doi = {10.1007/978-3-540-28644-8_25},
abstract = {In this paper, we study model checking of timed automata
(TAs), and more precisely we aim at finding efficient model checking
for subclasses of TAs. For this, we consider model checking TCTL and
TCTL, over TAs with one clock or two clocks.\par
First we show that the reachability problem is NLOGSPACE-complete
for one clock TAs (i.e. as complex as reachability in classical graphs)
and we give a polynomial time algorithm for model checking TCTL,
over this class of TAs. Secondly we show that model checking becomes
PSPACE-complete for full TCTL over one clock TAs. We also show that
model checking CTL (without any timing constraint) over two clock TAs
is PSPACE-complete and that reachability is NP-hard.}
}
@inproceedings{LS-concur04,
address = {London, UK},
month = aug,
year = 2004,
volume = 3170,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gardner, {\relax Ph}ilippa and Yoshida, Nobuko},
acronym = {{CONCUR}'04},
booktitle = {{P}roceedings of the 15th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'04)},
author = {Leroux, J{\'e}r{\^o}me and Sutre, Gr{\'e}goire},
title = {On Flatness for 2-dimensional Vector Addition Systems
with States},
pages = {402-416},
nmnote = {Partially while J. Leroux was at LSV},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LS-concur04.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LS-concur04.ps},
doi = {10.1007/978-3-540-28644-8_26}
}
@techreport{LSV:04:10,
author = {Baclet, Manuel and Pacalet, Renaud and
Petit, Antoine},
title = {Register Transfer Level Simulation},
type = {Research Report},
number = {LSV-04-10},
year = {2004},
month = may,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {15~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2004-10.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2004-10.rr.ps}
}
@techreport{LSV:04:11,
author = {Baclet, Manuel and Chevallier, R{\'e}my},
title = {Using {UPPAAL} to Verify an On-Chip Memory},
type = {Research Report},
number = {LSV-04-11},
year = {2004},
month = may,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {12~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2004-11.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2004-11.rr.ps}
}
@techreport{LSV:04:12,
author = {Fribourg, Laurent and Messika, St{\'e}phane and
Picaronny, Claudine},
title = {Mixing Time of the Asymmetric Simple Exclusion Problem
on a Ring with Two Particles},
type = {Research Report},
number = {LSV-04-12},
year = {2004},
month = jun,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {15~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2004-12.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2004-12.rr.ps}
}
@inproceedings{Ler-atva04,
address = {Taipei, Taiwan},
month = oct # {-} # nov,
year = {2004},
volume = {3299},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Wang, Farn},
acronym = {{ATVA}'04},
booktitle = {{P}roceedings of the 2nd {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'04)},
author = {Leroux, J{\'e}r{\^o}me},
title = {Disjunctive Invariants for Numerical Systems},
pages = {93-107},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Ler-atva04.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Ler-atva04.ps}
}
@inproceedings{Ler-inf03,
address = {Marseilles, France},
month = aug,
year = 2004,
volume = 98,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Schnoebelen, {\relax Ph}ilippe},
acronym = {{INFINITY}'03},
booktitle = {{P}roceedings of the 5th {I}nternational
{W}orkshop on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'03)},
author = { Leroux, J{\'e}r{\^o}me},
title = {The Affine Hull of a Binary Automaton is Computable in
Polynomial Time},
pages = {89-104},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Ler-inf03.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Ler-inf03.ps}
}
@phdthesis{messika-these2004,
author = {Messika, St{\'e}phane},
title = {M{\'e}thodes probabilistes pour la v{\'e}rification des
syst{\`e}mes distribu{\'e}s},
year = 2004,
month = dec,
type = {Th{\`e}se de doctorat},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/messika-these.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/messika-these.pdf}
}
@inproceedings{MR-concur2004,
address = {London, UK},
month = aug,
year = 2004,
volume = 3170,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gardner, {\relax Ph}ilippa and Yoshida, Nobuko},
acronym = {{CONCUR}'04},
booktitle = {{P}roceedings of the 15th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'04)},
author = {Markey, Nicolas and Raskin, Jean-Fran{\c{c}}ois},
title = {Model Checking Restricted Sets of Timed Paths},
pages = {432-447},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MR-concur2004.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MR-concur2004.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MR-concur2004.pdf},
doi = {10.1007/978-3-540-28644-8_28},
abstract = {In this paper, we study the complexity of model-checking
formulas of three important real-time logics (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)} a infinite set of finite (or infinite) timed paths
defined by a finite
(or ultimately periodic) path in a region graph, \textit{(iii)} a
infinite set of finite
(or infinite) timed paths defined by a finite (or ultimately periodic) path
in a zone graph.}
}
@inproceedings{MS-formats2004,
address = {Grenoble, France},
month = sep,
year = 2004,
volume = {3253},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Lakhnech, Yassine and Yovine, Sergio},
acronym = {{FORMATS}'04/{FTRTFT}'04},
booktitle = {{P}roceedings of the {J}oint {C}onferences
{F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'04) and
{F}ormal {T}echniques in {R}eal-{T}ime and
{F}ault-{T}olerant {S}ystems ({FTRTFT}'04)},
author = {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
title = {Symbolic Model Checking for Simply-Timed Systems},
pages = {102-117},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MS-formats2004.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MS-formats2004.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MS-formats2004.pdf},
abstract = {We describe OBDD-based symbolic model checking algorithms for
simply-timed systems, i.e. finite state graphs where transitions
carry a duration. These durations can be arbitrary natural numbers. A
simple and natural semantics for these systems opens the way for
improved efficiency. Our algorithms have been implemented in NuSMV
and perform well in practice (on standard case studies).}
}
@inproceedings{MS-qest2004,
address = {Enschede, The Netherlands},
month = sep,
year = 2004,
publisher = {{IEEE} Computer Society Press},
acronym = {{QEST}'04},
booktitle = {{P}roceedings of the 1st {I}nternational
{C}onference on {Q}uantitative
{E}valuation of {S}ystems
({QEST}'04)},
author = {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
title = {{TSMV}: {A} Symbolic Model Checker for Quantitative
Analysis of Systems},
pages = {330-331},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MS-qest2004.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MS-qest2004.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MS-qest2004.pdf},
doi = {10.1109/QEST.2004.10028},
abstract = {TSMV is an extension of NuSMV, the open-source
symbolic model checker, aimed at dealing with timed versions
of (models of) circuits, PLC controllers, protocols, etc. The
underlying model is an extension of Kripke structures, where
every transition carries an integer duration (possibly zero). This
simple model supports efficient symbolic algorithms for RTCTL
formulae.}
}
@inproceedings{Mar-afadl2004,
address = {Besan{\c{c}}on, France},
month = jun,
year = 2004,
editor = {Julliand, Jacques},
acronym = {{AFADL}'04},
booktitle = {{A}ctes du 6{\`e}me {A}telier sur les {A}pproches {F}ormelles
dans l'{A}ssistance au {D}{\'e}veloppement de {L}ogiciels
({AFADL}'04)},
author = {Markey, Nicolas},
title = {{TSMV}: model-checking symbolique de syst{\`e}mes
simplement temporis{\'e}s},
pages = {349-352},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Mar-afadl04.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Mar-afadl04.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Mar-afadl04.pdf}
}
@proceedings{PHS:INFINITY2003,
title = {{P}roceedings of the 5th {I}nternational
{W}orkshop on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'03)},
booktitle = {{P}roceedings of the 5th {I}nternational
{W}orkshop on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'03)},
editor = {Schnoebelen, {\relax Ph}ilippe},
volume = {98},
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
year = 2004,
month = aug,
doi = {10.1016/j.entcs.2003.10.001},
address = {Marseilles, France},
oldurl = {http://www.sciencedirect.com/science?_ob=IssueURL&
_tockey=%23TOC%2313109%232004%23999019999%23512226%23FLP%23
Volume_98,_(2_August_2004)%2BMProceedings_of_INFINITY_2003,
_the_5th_International_Workshop_on_Verification_of_Infinite-State
_Systems,_a_satellite_workshop_of_CONCUR_2003%2BMMarseille,_France,
_2_September_2003%2BMEdited_by_P._Schnoebelen&_auth=y&view=c&
_acct=C000051058&_version=1&_urlVersion=0&
_userid=1052425&md5=c6eb616ae1aec31a577ad19b058bc540}
}
@techreport{Prouve:rap1,
author = {Bozga, Liana and Delaune, St{\'e}phanie and
Klay, Francis and
Treinen, Ralf},
title = {Sp{\'e}cification du protocole de porte-monnaie
{\'e}lectronique},
year = {2004},
month = jun,
type = {Technical Report},
number = 1,
institution = {projet RNTL PROUV{\'E}},
oldhowpublished = {Rapport Technique 1 du projet RNTL PROUV\'E},
note = {12~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/prouve-rap1.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/prouve-rap1.ps},
abstract = {Cette \'etude de cas a pour but de contribuer \`a une
premi\`ere \'evaluation des besoins pour l'aspect description formelle
des protocoles cryptographiques. Cet aspect est un pr\'ealable oblig\'e
avant d'aborder des points tels que la s\'emantique et la
v\'erification. Le r\'esultat de ce travail a guid\'e la d\'efinition de
la syntaxe du langage de sp\'ecification d\'evelopp\'e dans la t\^ache~1 du
projet~: <<~S\'emantique des protocoles et des propri\'et\'es~>>.\par
Parmi la multitude de protocoles existants celui qui a \'et\'e \'etudi\'e
est un porte-monnaie \'electronique \`a cl\'e publique d\'evelopp\'e
r\'ecemment par France T\'el\'ecom R\&D car il refl\`ete fid\`element les
ambitions du projet. Ce protocole, sortant sans surprise du
spectre de tous les outils d\'evelopp\'es \`a l'heure actuelle, notre
travail a consist\'e \`a mod\'eliser au mieux le porte-monnaie
\'electronique dans un sous ensemble repr\'esentatif d'outils
existants. Cette \'etude met \'evidence, sur un cas r\'eel, les carences
et les faiblesses des outils actuels et permet ainsi d'affiner et
de valider les objectifs du projet. D'un autre c\^ot\'e, ce travail
montre que des lacunes importantes peuvent parfois \^etre
raisonnablement contourn\'ees modulo un codage adapt\'e.}
}
@techreport{Prouve:rap2,
author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie
and Lafourcade, Pascal},
title = {A Survey of Algebraic Properties Used in Cryptographic
Protocols},
year = {2004},
month = jun,
type = {Technical Report},
number = 2,
institution = {projet RNTL PROUV{\'E}},
oldhowpublished = {Rapport Technique 2 du projet RNTL PROUV\'E},
note = {19~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/prouve-rap2.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/prouve-rap2.ps},
abstract = {Using the \emph{perfect encryption
assumption}, cryptographic primitives are often
represented by free function symbols. However some attacks
and even honest runs may use algebraic properties of the
operators like the exclusive or, the modular
exponentiation, the addition, etc.\par
We give here a survey of protocols and attacks using such
algebraic properties.}
}
@techreport{Prouve:rap3,
author = {Treinen, Ralf},
title = {The {PROUV\'E} Specification Language},
year = {2004},
month = aug,
number = 3,
type = {Technical Report},
institution = {Projet RNTL PROUV{\'E}},
oldhowpublished = {Rapport Technique 3 du projet RNTL PROUV\'E},
note = {10~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/prouve-rap3.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/prouve-rap3.ps}
}
@techreport{Prouve:rap4,
author = {Bernat, Vincent and Comon{-}Lundh, Hubert and
Cortier, V{\'e}ronique and Delaune, St{\'e}phanie and
Jacquemard, Florent and Lafourcade, Pascal and
Lakhnech, Yassine and Mazar{\'e}, Laurent},
title = {Sufficient conditions on properties for an automated
verification: theoretical report on the verification of
protocols for an extended model of the intruder },
year = {2004},
month = dec,
type = {Technical Report},
number = 4,
institution = {projet RNTL PROUV{\'E}},
oldhowpublished = {Rapport Technique 4 du projet RNTL PROUV\'E},
note = {33~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/prouve-rap4.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/prouve-rap4.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 first give an
overview of the existing methods in formal
approaches for analyzing cryptographic
protocols. Then we describe more precisely
the results obtained by the partners of the
RNTL project PROUV\'E.}
}
@mastersthesis{Ratti-dea,
author = {Ratti, Benjamin},
title = {Automates d'arbre d'ordre~deux},
year = 2004,
month = sep,
type = {Rapport de {DEA}},
school = {{DEA} Programmation, Paris, France},
note = {45~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BRatti-dea2004.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BRatti-dea2004.ps}
}
@mastersthesis{Reynier-dea,
author = {Reynier, Pierre-Alain},
title = {Analyse en avant des automates temporis{\'e}s},
year = {2004},
month = sep,
type = {Rapport de {DEA}},
school = {{DEA} Algorithmique, Paris, France},
note = {68~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/PAR-dea2004.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/PAR-dea2004.ps}
}
@incollection{Sch-voss,
year = 2004,
volume = 2925,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baier, {\relax Ch}ristel and Haverkort, Boudewijn R.
and Hermanns, Holger and Katoen, Joost-Pieter and
Siegle, Markus and Vaandrager, Frits},
acronym = {{V}alidation of {S}tochastic {S}ystems},
booktitle = {{V}alidation of {S}tochastic {S}ystems: {A} {G}uide
to {C}urrent {R}esearch},
author = {Schnoebelen, {\relax Ph}ilippe},
title = {The Verification of Probabilistic Lossy Channel
Systems},
pages = {445-465},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-voss.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Sch-voss.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-voss.pdf},
abstract = {Lossy channel systems (LCS's) are
systems of finite state automata that
communicate via unreliable unbounded fifo
channels. Several probabilistic versions of
these systems have been proposed in recent
years, with the two aims of modeling more
faithfully the losses of messages, and
circumventing undecidabilities by some kind of
randomization. We survey these proposals and
the verification techniques they support.}
}
@inproceedings{bh-amast2004,
address = {Stirling, UK},
month = jul,
year = 2004,
volume = 3116,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Rattray, Charles and Maharaj, Savitri and Shankland, Carron},
acronym = {{AMAST}'04},
booktitle = {{P}roceedings of the 10th {I}nternational
{C}onference on {A}lgebraic {M}ethodology and
{S}oftware {T}echnology
({AMAST}'04)},
author = {Bidoit, Michel and Hennicker, Rolf},
title = {Glass Box and Black Box Views of State-Based System
Specifications},
pages = {19},
note = {Invited talk}
}
@inproceedings{bhkb-sefm2004,
address = {Beijing, China},
month = sep,
year = 2004,
publisher = {{IEEE} Computer Society Press},
acronym = {{SEFM}'04},
booktitle = {{P}roceedings of the 2nd {IEEE} {I}nternational
{C}onference on {S}oftware {E}ngineering and
{F}ormal {M}ethods
({SEFM}'04)},
author = {Bidoit, Michel and Hennicker, Rolf and
Knapp, Alexander
and Baumeister, Hubert},
title = {Glass-Box and Black-Box Views on Object-Oriented
Specifications},
pages = {208-217},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bhkb-sefm2004.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bhkb-sefm2004.pdf},
doi = {10.1109/SEFM.2004.10014}
}
@inproceedings{bj-strategies2004,
address = {Cork, Ireland},
month = jul,
year = 2004,
editor = {Bonacina, Maria Paola and
Boy{ }de{~}la{~}Tour, {\relax Th}ierry},
acronym = {{STRATEGIES}'04},
booktitle = {{P}roceedings of the 5th {W}orkshop
on {S}trategies in {A}utomated {D}eduction
({STRATEGIES}'04)},
author = {Bouhoula, Adel and Jacquemard, Florent},
title = {Constrained Tree Grammars to Pilot Automated Proof
by
Induction},
pages = {64-78},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BJ-strategies04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BJ-strategies04.pdf}
}
@techreport{blueberries-TR1.3.2,
author = {Baclet, Manuel and Chevallier, R{\'e}my},
title = {Using {UPPAAL} to verify an on-chip memory},
year = {2004},
month = may,
type = {Contract Report},
number = {(Work Package~3.2 Fourniture~1)},
institution = {projet T126 MEDEA+ Blueberries},
oldhowpublished = {Fourniture 1 du Work Package 3.2 du projet T126 MEDEA+
Blueberries},
note = {12~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2004-11.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2004-11.rr.ps}
}
@article{bouyer-fmsd-2004,
publisher = {Kluwer Academic Publishers},
journal = {Formal Methods in System Design},
author = {Bouyer, Patricia},
title = {Forward Analysis of Updatable Timed Automata},
volume = {24},
number = {3},
pages = {281-320},
year = {2004},
month = may,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bou-FMSD2004.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bou-FMSD2004.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bou-FMSD2004.ps},
doi = {10.1023/B:FORM.0000026093.21513.31},
abstract = {Timed automata are a widely studied
model. Its decidability has been proved using the
so-called region automaton construction. This
construction provides a correct abstraction for
the behaviours of timed automata, but it suffers
from a state explosion and is thus not used in
practice. Instead, algorithms based on the notion
of zones are implemented using adapted data
structures like~DBMs. When we focus on forward
analysis algorithms, the exact computation of all
the successors of the initial configurations does
not always terminate. Thus, some abstractions are
often used to ensure termination, among which, a
widening operator on zones.\par
In this paper, we study in detail this widening
operator and the corresponding forward analysis
algorithm. This algorithm is most used and
implemented in tools like KRONOS and UPPAAL. One
of our main results is that it is hopeless to
find a forward analysis algorithm for general
timed automata, that uses such a widening
operator, and which is correct. This goes really
against what one could think. We then study in
detail this algorithm in the more general
framework of updatable timed automata, a model
which has been introduced as a natural syntactic
extension of classical timed automata. We
describe subclasses of this model for which a
correct widening operator can be found. }
}
@inproceedings{bst-monterey,
address = {Venice, Italy},
year = 2004,
volume = 2941,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Wirsing, Martin and Knapp, Alexander and
Balsamo, Simonetta},
acronym = {{RISSEF}'02},
booktitle = {{R}evised {P}apers of the 9th {I}nternational
{W}orkshop on {R}adical {I}nnovations of {S}oftware
and {S}ystems {E}ngineering in the {F}uture
({RISSEF}'02)},
author = {Bidoit, Michel and Sannella, Donald and
Tarlecki, Andrzej},
title = {Toward Component-Oriented Formal Software
Development:
{A}n Algebraic Approach},
pages = {75-90},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BST-monterey.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BST-monterey.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BST-monterey.pdf}
}
@inproceedings{comon04fossacs,
address = {Barcelona, Spain},
month = mar,
year = 2004,
volume = 2987,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Walukiewicz, Igor},
acronym = {{FoSSaCS}'04},
booktitle = {{P}roceedings of the 7th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'04)},
author = {Comon{-}Lundh, Hubert },
title = {Intruder Theories (Ongoing Work)},
pages = {1-4},
note = {Invited talk}
}
@incollection{couvreur-chap04,
author = {Br{\'e}ant, F. and Couvreur, Jean-Michel and
Gilliers, Fr{\'e}d{\'e}ric and
Kordon, Fabrice and Mounier, Isabelle and
Paviot{-}Adet, Emmanuel and
Poitrenaud, Denis and
Regep, Dan M. and Sutre, Gr{\'e}goire},
title = {Modeling and Verifying Behavioral Aspects},
chapter = {6},
editor = {Kordon, Fabrice and Lemoine, Michel},
booktitle = {Formal Methods for Embedded Distributed Systems: {H}ow
to Master the Complexity},
pages = {171-211},
year = {2004},
month = jun,
publisher = {Kluwer Academic Publishers}
}
@inproceedings{dj-ccs-2004,
address = {Washington, D.C., USA},
month = oct,
year = 2004,
publisher = {ACM Press},
editor = {Atluri, Vijayalakshmi and Pfitzmann, Birgit and
McDaniel, Patrick},
acronym = {{CCS}'04},
booktitle = {{P}roceedings of the 11th {ACM} {C}onference
on {C}omputer and {C}ommunications {S}ecurity
({CCS}'04)},
author = {Delaune, St{\'e}phanie and Jacquemard, Florent},
title = {A Decision Procedure for the Verification of Security
Protocols with Explicit Destructors},
pages = {278-287},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DJ-ccs-2004.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DJ-ccs-2004.ps},
abstract = {We present a non-deterministic polynomial
time procedure to decide the problem of insecurity, in the
presence of a bounded number of sessions, for
cryptographic protocols containing explicit destructor
symbols, like decryption and projection. These operators
are axiomatized by an arbitrary convergent rewrite system
satisfying some syntactic restrictions. This approach,
with parameterized semantics, allows us to weaken the
security hypotheses for verification, \emph{i.e.} to
address a larger class of attacks than for models based on
free algebra. Our procedure is defined by an inference
system based on basic narrowing techniques for deciding
satisfiability of combinations of first-order equations
and intruder deduction constraints.}
}
@inproceedings{dj-csfw2004,
address = {Asilomar, Pacific Grove, California, USA},
month = jun,
year = 2004,
publisher = {{IEEE} Computer Society Press},
acronym = {{CSFW}'04},
booktitle = {{P}roceedings of the
17th {IEEE} {C}omputer {S}ecurity {F}oundations
{W}orkshop ({CSFW}'04)},
author = {Delaune, St{\'e}phanie and Jacquemard, Florent},
title = {A Theory of Dictionary Attacks and its Complexity},
pages = {2-15},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DJ-csfw2004.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DJ-csfw2004.ps},
abstract = {We consider the problem of automating
proofs of cryptographic protocols when some data, like
poorly chosen passwords, can be guessed by dictionary
attacks. First, we define a theory of these attacks: we
introduce an inference system modeling the guessing
capabilities of an intruder. This system extends the
classical Dolev-Yao rules. Using proof rewriting
techniques, we show a locality lemma for our inference
system which yields the PTIME-completeness of the
deduction problem.\par
This result is lifted to the simultaneous solving of
intruder deduction constraints with variables.
Constraint solving is the basis of a NP algorithm for
the protocol insecurity problem in the presence of
dictionary attacks, assuming a bounded number of
sessions. This extends the classical NP-completeness
result for the Dolev-Yao model.\par
We illustrate the procedure with examples of published
protocols. The model and decision algorithm have been
validated on some examples in a prototype
implementation.}
}
@inproceedings{dk-jdir-2004,
address = {Lannion, France},
month = nov,
year = 2004,
acronym = {{JDIR}'04},
booktitle = {{A}ctes des 6{\`e}mes {J}ourn{\'e}es {D}octorales
{I}nformatique et {R}{\'e}seau
({JDIR}'04)},
author = {Delaune, St{\'e}phanie and Klay, Francis},
title = {V{\'e}rification automatique appliqu{\'e}e {\`a} un
protocole de commerce {\'e}lectronique},
pages = {260-269},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DK-jdir-2004.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DK-jdir-2004.pdf},
abstract = {Le domaine de la mod{\'e}lisation et de la
v{\'e}rification est une activit{\'e} d{\'e}licate et importante qui a
connu une v{\'e}ritable explosion dans les ann{\'e}es 1990. On
dispose {\`a} l'entr{\'e}e des ann{\'e}es 2000 de toute une gamme de
mod{\`e}les et de m{\'e}thodes plus ou moins avanc{\'e}s en ce qui
concerne l'expressivit{\'e} et l'automatisation.\par
Afin de d{\'e}finir les besoins et les priorit{\'e}s {\`a} mettre sur
les outils consacr{\'e}s {\`a} la v{\'e}rification de protocoles
cryptographiques qui seront d{\'e}velopp{\'e}s au sein du projet
RNTL PROUV{\'E}, nous proposons de travailler en situation
r{\'e}elle, sur des protocoles plut{\^o}t <<~durs~>>, en effectuant le
cycle suivant~: mod{\'e}lisation, formalisation puis validation
dans des outils existants. Ce travail est effectu{\'e} ici pour
un protocole de porte-monnaie {\'e}lectronique, d{\'e}velopp{\'e}
r{\'e}cemment par une {\'e}quipe de France T{\'e}l{\'e}com. }
}
@misc{dn-fms04,
author = {Nowak, David},
title = {Logical Relations for Monadic Types},
year = 2004,
month = may,
howpublished = {Invited talk, {I}nternational
{W}orkshop on {F}ormal {M}ethods
and {S}ecurity ({IWFMS}'04), Nanjing, China}
}
@misc{evtgen-v1.0,
author = {Olivain, Julien},
title = {{EVTGEN} v1.0: {A} Programmable Generic Generator of
Event Sequences},
year = {2004},
month = jul,
note = {Written in C (about 5000 lines)},
note-fr = {{\'E}crit en~C (environ 5000 lignes)},
url = {http://www.lsv.ens-cachan.fr/~olivain/evtgen/}
}
@misc{netentropy-v1.0,
author = {Olivain, Julien},
title = {Net-entropy v1.0: {A}n entropy checker for
ciphered network connections},
year = {2004},
month = sep,
url = {http://www.lsv.ens-cachan.fr/~olivain/net-entropy/}
}
@inproceedings{GaLeZe04fsttcs,
address = {Chennai, India},
month = dec,
year = 2004,
volume = 3328,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Lodaya, Kamal and Mahajan, Meena},
acronym = {{FSTTCS}'04},
booktitle = {{P}roceedings of the 24th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'04)},
author = {Gastin, Paul and Lerman, Benjamin and Zeitoun, Marc},
title = {Distributed games with causal memory are decidable for
series-parallel systems},
pages = {275-286},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GLZ-fsttcs04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GLZ-fsttcs04.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GLZ-fsttcs04.ps},
abstract = {This paper deals with distributed
control problems by means of distributed games
played on Mazurkiewicz traces. The main difference
with other notions of distributed games recently
introduced is that, instead of having a \emph{local} view,
strategies and controllers are able to use a more
accurate memory, based on their \emph{causal} view. Our
main result states that using the causal view makes
the control synthesis problem decidable for
series-parallel systems for \emph{all} recognizable winning
conditions on finite behaviors, while this problem
with local view was proved undecidable even for
reachability conditions.}
}
@phdthesis{jmc-hab-04,
author = {Couvreur, Jean-Michel},
title = {Contribution {\`a} l'algorithmique de la v{\'e}rification},
year = {2004},
month = jul,
type = {M{\'e}moire d'habilitation},
school = {Universit{\'e} de Bordeaux~I, Bordeaux, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/jmc-habile.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/jmc-habile.pdf}
}
@article{mar-ACTA2004,
publisher = {Springer},
journal = {Acta Informatica},
author = {Markey, Nicolas},
title = {Past is for Free: {O}n the Complexity of Verifying
Linear Temporal Properties with Past},
volume = {40},
number = {6-7},
pages = {431-458},
year = {2004},
month = may,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Mar-ACTA2004.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Mar-ACTA2004.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Mar-ACTA2004.pdf},
doi = {10.1007/s00236-003-0136-5},
abstract = {We study the complexity of satisfiability
and model checking problems for fragments of
linear-time temporal logic with past (PLTL).
We consider many fragments of PLTL, obtained by restricting
the set of allowed temporal modalities, the use of negations or the
nesting of future formulas into past formulas. Our results strengthen
the widely accepted fact that {"}past is for free{"}, in the sense that
allowing symmetric past-time modalities does not bring additional
theoretical complexity. This result holds even for small fragments and
even when nesting future formulas into past formulas.}
}
@inproceedings{mj-wmc2004,
address = {Milano, Italy},
month = jun,
year = 2004,
editor = {Paun, {\relax Gh}eorghe},
acronym = {{WMC}'04},
booktitle = {{P}roceedings of the 5th {W}orkshop
on {M}embrane {C}omputing
({WMC}'04)},
author = {Michel, Olivier and Jacquemard, Florent},
title = {An Analysis of the {N}eedham-{S}chroeder Public-Key
Protocol with~{MGS}},
pages = {295-315},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/mj-wmc05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/mj-wmc05.pdf},
phsnote = {est prevu un lncs avec certains papiers revises},
nmnote = {C'est LNCS3365, mais le papier n'est pas selectionne}
}
@article{ms-IPL2004,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
title = {A {PTIME}-Complete Matching Problem for
{SLP}-Compressed Words},
volume = {90},
number = {1},
pages = {3-6},
year = {2004},
month = jan,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MarSch-IPL2004.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MarSch-IPL2004.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MarSch-IPL2004.pdf},
doi = {10.1016/j.ipl.2004.01.002},
abstract = {SLP-compressed words are words
given by simple deterministic grammars called
{"}straight-line programs{"}. We prove that the
problem of deciding whether an SLP-compressed
word is recognized by a FSA is complete for
polynomial-time.}
}
@mastersthesis{robin-dea,
author = {Robin, Agn{\`e}s},
title = {Aux fronti{\`e}res de la d{\'e}cidabilit{\'e}...},
year = {2004},
month = jul,
type = {Rapport de {DEA}},
school = {{DEA} Algorithmique, Paris, France},
note = {33~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Robin-dea2004.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Robin-dea2004.ps}
}
@misc{rtaloop,
author = {Treinen, Ralf},
title = {{RTALOOP}: {T}he {RTA} List of Open Problems},
year = {2004},
howpublished = {Web site at \url{http://www.lsv.ens-cachan.fr/rtaloop/},
started 1997},
note = {Size as of July 2004: 100 problems, 90 pages, 432
references},
note-fr = {En juillet~2004: 100 probl{\`e}mes, 90~pages, 432
r{\'e}f{\'e}rences},
url = {http://www.lsv.ens-cachan.fr/rtaloop/}
}
@misc{ssp,
author = {Hugel, {\relax Th}omas},
title = {{SSP}: {S}tochastic Shortest Paths},
year = {2004},
month = jul,
note = {Written in Caml (about 500 lines)},
note-fr = {{\'E}crit en Caml (environ 500 lignes)}
}
@misc{bouyer-fac04,
author = {Bouyer, Patricia},
title = {Automates temporis{\'e}s, de la th{\'e}orie {\`a} l'impl{\'e}mentation},
year = {2004},
month = mar,
howpublished = {Invited talk, Journ\'ees Formalisation des Activit?s
Concurrentes (FAC'04), Toulouse, France}
}
@misc{Demri0304,
author = {Demri, St{\'e}phane},
title = {Complexit{\'e} algorithmique de variantes de {LTL} pour la v{\'e}rification},
year = {2004},
note = {Course notes, {DEA} Algorithmique, Paris, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri-coursLTL.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri-coursLTL.pdf}
}
@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.