@inproceedings{BC-asian06,
address = {Tokyo, Japan},
month = jan,
year = 2008,
volume = 4435,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Okada, Mitsu and Satoh, Ichiro},
acronym = {{ASIAN}'06},
booktitle = {{R}evised {S}elected {P}apers of the 11th {A}sian
{C}omputing {S}cience {C}onference
({ASIAN}'06)},
author = {Bernat, Vincent and Comon{-}Lundh, Hubert},
title = {Normal proofs in intruder theories},
pages = {151-166},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC-asian06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC-asian06.pdf},
doi = {10.1007/978-3-540-77505-8_12},
abstract = {Given an arbitrary intruder deduction capability, modeled as an
inference system~\(\mathcal{S}\) and a protocol, we show how to
compute an inference system~\(\widehat{\mathcal{S}}\) such that
the security problem for an unbounded number of sessions is
equivalent to the deducibility of some message
in~\(\widehat{\mathcal{S}}\). Then, assuming that
\(\mathcal{S}\)~has some subformula property, we lift such a
property to~\(\widehat{\mathcal{S}}\), thanks to a proof
normalisation theorem. In~general, for an unbounded number of
sessions, this provides with a complete deduction strategy. In
case of a bounded number of sessions, our theorem implies that
the security problem is co-NP-complete. As an instance of our
result we get a decision algorithm for the theory of
blind-signatures, which, to our knowledge, was not known
before.}
}
@inproceedings{LNZ-asian06,
address = {Tokyo, Japan},
month = jan,
year = 2008,
volume = 4435,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Okada, Mitsu and Satoh, Ichiro},
acronym = {{ASIAN}'06},
booktitle = {{R}evised {S}elected {P}apers of the 11th {A}sian
{C}omputing {S}cience {C}onference
({ASIAN}'06)},
author = {Lasota, S{\l}awomir and Nowak, David and Yu, Zhang},
title = {On completeness of logical relations for monadic types},
pages = {223-230},
nmnote = {autc parce que c'est un short paper, pas ant pour Zhang Yu},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LNZ-monad-complete.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LNZ-monad-complete.pdf},
doi = {10.1007/978-3-540-77505-8_17},
abstract = {Software security can be ensured by specifying and verifying
security properties of software using formal methods with
strong theoretical bases. In~particular, programs can be
modeled in the framework of lambda-calculi, and interesting
properties can be expressed formally by contextual
equivalence (a.k.a.~observational equivalence). Furthermore,
imperative features, which exist in most real-life software,
can be nicely expressed in the so-called computational
lambda-calculus. Contextual equivalence is difficult to
prove directly, but we can often use logical relations as a
tool to establish it in lambda-calculi. We~have already
defined logical relations for the computational
lambda-calculus in previous work. We~devote this paper to
the study of their completeness w.r.t.~contextual
equivalence in the computational lambda-calculus.}
}
@inproceedings{DLS-fossacs08,
address = {Budapest, Hungary},
month = mar # {-} # apr,
year = 2008,
volume = 4962,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Amadio, Roberto},
acronym = {{FoSSaCS}'08},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'08)},
author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko and Sangnier, Arnaud},
title = {Model checking freeze {LTL} over one-counter automata},
pages = {490-504},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLS-fossacs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLS-fossacs08.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DLS-fossacs08.ps},
doi = {10.1007/978-3-540-78499-9_34},
abstract = {We study complexity issues related to the model-checking
problem for LTL with registers (a.k.a. freeze LTL) over
one-counter automata. We~consider several classes of one-counter
automata (mainly deterministic vs.~nondeterministic) and several
syntactic fragments (restriction on the number of registers and on
the use of propositional variables for control
locations). The~logic has the ability to store a counter value and
to test it later against the current counter value. By~introducing
a non-trivial abstraction on counter values, we~show that model
checking LTL with registers over deterministic one-counter
automata is PSPACE-complete with infinite accepting
runs. By~constrast, we prove that model checking LTL with
registers over nondeterministic one-counter automata is
\(\Sigma_{1}^{1}\)-complete [resp. \(\Sigma_{1}^{0}\)-complete] in
the infinitary [resp. finitary] case even if only one register is
used and with no propositional variable. This makes a difference
with the facts that several verification problems for one-counter
automata are known to be decidable with relatively low complexity,
and that finitary satisfiability for LTL with a unique register is
decidable. Our~results pave the way for model-checking LTL with
registers over other classes of operational models, such as
reversal-bounded counter machines and deterministic pushdown
systems.}
}
@inproceedings{HIV-fossacs08,
address = {Budapest, Hungary},
month = mar # {-} # apr,
year = 2008,
volume = 4962,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Amadio, Roberto},
acronym = {{FoSSaCS}'08},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'08)},
author = {Habermehl, Peter and Iosif, Radu and Vojnar, Tom{\'a}{\v{s}}},
title = {What else is decidable about arrays?},
pages = {474-489},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hiv07-TR.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hiv07-TR.pdf},
doi = {10.1007/978-3-540-78499-9_33},
abstract = {We introduce a new decidable logic for reasoning about infinite
arrays of integers. The logic is in the \(\exists^{*}\forall^{*}\)
first-order fragment and allows (1)~Presburger constraints on
existentially quantified variables, (2)~difference constraints as well as
periodicity constraints on universally quantified indices, and
(3)~difference constraints on values. In~particular, using our logic, one
can express constraints on consecutive elements of arrays
(\emph{e.g.}~\(\forall i.\ 0 \leq i < n \rightarrow a[i + 1] = a[i] - 1\))
as well as periodic facts (\emph{e.g.}~\(\forall i.\ i \equiv_2 0
\rightarrow a[i] = 0\)). The decision procedure follows the
automata-theoretic approach: we~translate formulae into a special class of
B{\"u}chi counter automata such that any model of a formula corresponds to
an accepting run of the automaton, and vice versa. The~emptiness problem
for this class of counter automata is shown to be decidable, as a
consequence of earlier results on counter automata with a flat control
structure and transitions based on difference constraints. We~show
interesting program properties expressible in our logic, and give an
example of invariant verification for programs that handle integer
arrays.}
}
@inproceedings{BMR-fossacs08,
address = {Budapest, Hungary},
month = mar # {-} # apr,
year = 2008,
volume = 4962,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Amadio, Roberto},
acronym = {{FoSSaCS}'08},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'08)},
author = {Bouyer, Patricia and Markey, Nicolas and Reynier, Pierre-Alain},
title = {Robust Analysis of Timed Automata {\em via} Channel Machines},
pages = {157-171},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMR-fossacs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMR-fossacs08.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BMR-fossacs08.ps},
doi = {10.1007/978-3-540-78499-9_12},
abstract = {Whereas formal verification of timed systems has become a very
active field of research, the idealised mathematical semantics of timed
automata cannot be faithfully implemented. Several works have thus focused
on a modified semantics of timed automata which ensures implementability,
and robust model-checking algorithms for safety, and later LTL properties
have been designed. Recently, a~new approach has been proposed, which
reduces (standard) model-checking of timed automata to other verification
problems on channel machines. Thanks to a new encoding of the modified
semantics as a network of timed systems, we propose an original
combination of both approaches, and prove that robust model-checking for
coFlat-MTL, a large fragment of~MTL, is EXPSPACE-Complete.}
}
@inproceedings{CS-fossacs08,
address = {Budapest, Hungary},
month = mar # {-} # apr,
year = 2008,
volume = 4962,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Amadio, Roberto},
acronym = {{FoSSaCS}'08},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'08)},
author = {Chambart, Pierre and Schnoebelen, {\relax Ph}ilippe},
title = {The \(\omega\)-Regular {P}ost Embedding Problem},
pages = {97-111},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-fossacs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-fossacs08.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CS-fossacs08.ps},
doi = {10.1007/978-3-540-78499-9_8},
abstract = {Post's Embedding Problem is a new variant of Post's
Correspondence Problem where words are compared with embedding rather than
equality. It~has been shown recently that adding regular constraints on
the form of admissible solutions makes the problem highly non-trivial, and
relevant to the study of lossy channel systems. Here we consider the
infinitary version and its application to recurrent reachability in lossy
channel systems.}
}
@inproceedings{Gou-fossacs08b,
address = {Budapest, Hungary},
month = mar # {-} # apr,
year = 2008,
volume = 4962,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Amadio, Roberto},
acronym = {{FoSSaCS}'08},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'08)},
author = {Goubault{-}Larrecq, Jean},
title = {Simulation Hemi-Metrics Between Infinite-State Stochastic Games},
pages = {50-65},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-34.pdf},
doi = {10.1007/978-3-540-78499-9_5},
abstract = {We investigate simulation hemi-metrics between certain forms
of turn-based \(2\frac{1}{2}\)-player games played on infinite
topological spaces. They have the desirable property of bounding the
difference in payoffs obtained by starting from one state or another.
All
constructions are described as the special case of a unique one, which we
call the Hutchinson hemi-metric on various spaces of continuous
previsions. We show a directed form of the Kantorovich-Rubinstein theorem,
stating that the Hutchinson hemi-metric on spaces of continuous
probability valuations coincides with a notion of trans-shipment
hemi-metric. We also identify the class of so-called sym-compact spaces as
the right class of topological spaces, where the theory works out as
nicely as possible.}
}
@inproceedings{Gou-fossacs08a,
address = {Budapest, Hungary},
month = mar # {-} # apr,
year = 2008,
volume = 4962,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Amadio, Roberto},
acronym = {{FoSSaCS}'08},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'08)},
author = {Goubault{-}Larrecq, Jean},
title = {Prevision Domains and Convex Powercones},
pages = {318-333},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-33.pdf},
doi = {10.1007/978-3-540-78499-9_23},
abstract = {Two recent semantic families of models for mixed
probabilistic and non-deterministic choice over a space~\(X\) are the
convex powercone models, due independently to Mislove, and to Tix,
Keimel, and Plotkin, and the continuous prevision model of the
author. We show that, up to some minor details, these models are
isomorphic whenever \(X\) is a continuous, coherent cpo, and whether
the particular brand of non-determinism we focus on is demonic,
angelic, or chaotic. The construction also exhibits domains of
continuous previsions as retracts of well-known continuous cpos,
providing simple bases for the various continuous cpos of continuous
previsions. This has practical relevance to computing approximations
of operations on previsions.}
}
@inproceedings{Kremer-tgc07,
address = {Sophia-Antipolis, France},
year = 2008,
volume = 4912,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Barthe, Gilles and Fournet, C{\'e}dric},
acronym = {{TGC}'07},
booktitle = {{R}evised {S}elected {P}apers from the 3rd {S}ymposium on {T}rustworthy {G}lobal
{C}omputing ({TGC}'07)},
author = {Kremer, Steve},
title = {Computational soundness of equational theories (Tutorial)},
pages = {363-382},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Kremer-tgc07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Kremer-tgc07.pdf},
doi = {10.1007/978-3-540-78663-4},
abstract = {We study the link between formal and cryptographic models for
security protocols in the presence of passive and adaptive adversaries. We
first describe the seminal result by Abadi and Rogaway and shortly discuss
some of its extensions. Then we describe a general model for reasoning
about the soundness of implementations of equational theories. We
illustrate this model on several examples of computationally sound
implementations of equational theories.}
}
@article{JRV-jlap07,
publisher = {Elsevier Science Publishers},
journal = {Journal of Logic and Algebraic Programming},
author = {Jacquemard, Florent and Rusinowitch, Micha{\"e}l and Vigneron, Laurent},
title = {Tree automata with equality constraints modulo equational
theories},
year = 2008,
month = apr,
volume = 75,
number = 2,
pages = {182-208},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JRV-jlap08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JRV-jlap08.pdf},
doi = {10.1016/j.jlap.2007.10.006},
abstract = {This paper presents new classes of tree automata combining
automata with equality test and automata modulo equational theories.
We believe that these classes have 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.}
}
@inproceedings{BMOSW-stacs08,
address = {Bordeaux, France},
month = feb,
year = 2008,
volume = 1,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Albers, Susanne and Weil, Pascal},
acronym = {{STACS}'08},
booktitle = {{P}roceedings of the 25th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'08)},
author = {Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo{\"e}l
and Schnoebelen, {\relax Ph}ilippe and Worrell, James},
title = {On Termination for Faulty Channel Machines},
pages = {121-132},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bmosw-stacs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bmosw-stacs08.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/bmosw-stacs08.ps},
abstract = {A channel machine consists of a finite controller together with
several fifo channels; the controller can read messages from the head of a
channel and write messages to the tail of a channel. In this paper, we
focus on channel machines with \emph{insertion errors}, \textit{i.e.},
machines in whose channels messages can spontaneously appear. Such devices
have been previously introduced in the study of Metric Temporal Logic.
We~consider the termination problem: are all the computations of a given
insertion channel machine finite? We~show that this problem has
non-elementary, yet primitive recursive complexity.}
}
@article{TED-todaes08,
publisher = {ACM Press},
journal = {ACM Transactions on Design Automation of Electronic Systems},
author = {Taktak, Sami and Encrenaz, Emmanuelle and Desbarbieux, Jean-Lou},
title = {A tool for automatic detection of deadlocks in wormhole networks on chip},
nopages = {},
volume = 13,
number = 1,
year = 2008,
month = jan,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/TED-todaes07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/TED-todaes07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/TED-todaes07.ps},
doi = {10.1145/1297666.1297672},
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 \emph{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.
We~provide comparative results with standard approach, highlighting the
benefits of our method.}
}
@article{BHR-ietc07,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
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},
year = {2008},
month = jan,
volume = 206,
number = 1,
pages = {73-107},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-ic07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-ic07.pdf},
doi = {10.1016/j.ic.2007.10.004},
abstract = {Timed Petri nets and timed automata are two standard models for
the analysis of real-time systems. We~study in this paper their
relationship, and prove in particular that they are incomparable w.r.t.
language equivalence. In~fact, we~study the more general model of timed
Petri nets with read-arcs (RA-TdPN), already introduced in~[Ji{\v{r}}{\'\i}~Srba,
\textit{Timed-arc petri nets vs. networks of timed
automata}, Proc.\ ICATPN'05, LNCS~3536, Springer], which
unifies both models of timed Petri nets and of timed automata, and prove
that the coverability problem remains decidable for this model. 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, for~instance on the power of
non-deterministic clock resets.}
}
@article{DLLT-IC07,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Delaune, St{\'e}phanie and Lafourcade, Pascal and
Lugiez, Denis and Treinen, Ralf},
title = {Symbolic protocol analysis for monoidal equational theories},
pages = {312-351},
volume = 206,
number = {2-4},
year = 2008,
month = feb # {-} # apr,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLLT-ic07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLLT-ic07.pdf},
doi = {10.1016/j.ic.2007.07.005},
abstract = {We are interested in the design of
automated procedures for analyzing the (in)security of
cryptographic protocols in the Dolev-Yao model for a
bounded number of sessions when we take into account some
algebraic properties satisfied by the operators involved
in the protocol. This~leads to a more realistic model
than what we get under the perfect cryptography
assumption, but it implies that protocol analysis deals
with terms modulo some equational theory instead of terms
in a free algebra. The main goal of this paper is to set
up a general approach that works for a whole class of
monoidal theories which contains many of the specific
cases that have been considered so far in an ad-hoc way
(e.g.~exclusive~or, Abelian groups, exclusive or in
combination with the homomorphism axiom). We~follow a
classical schema for cryptographic protocol analysis
which proves first a locality result and then reduces the
insecurity problem to a symbolic constraint solving
problem. This approach strongly relies on the
correspondence between a monoidal theory~{\(E\)} and a
semiring~{\(S_E\)} which we use to deal with the symbolic
constraints. We~show that the well-defined symbolic
constraints that are generated by reasonable protocols
can be solved provided that unification in the monoidal
theory satisfies some additional properties.
The~resolution process boils down to solving particular
quadratic Diophantine equations that are reduced to
linear Diophantine equations, thanks to linear algebra
results and the well-definedness of the problem. Examples
of theories that do not satisfy our additional properties
appear to be undecidable, which suggests that our
characterization is reasonably tight.}
}
@article{BBL-fmsd06,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Bouyer, Patricia and Brinksma, Ed and Larsen, Kim G.},
title = {Optimal Infinite Scheduling for Multi-Priced
Timed Automata},
volume = {32},
number = {1},
pages = {2-23},
year = 2008,
month = feb,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBL-FMSD04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBL-FMSD04.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBL-FMSD04.ps},
doi = {10.1007/s10703-007-0043-4},
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.}
}
@article{DrGa06tocsys,
publisher = {Springer},
journal = {Theory of Computing Systems},
author = {Droste, Manfred and Gastin, Paul},
title = {On aperiodic and star-free formal power series in
partially commuting variables},
year = 2008,
month = may,
volume = 42,
number = 4,
pages = {608-631},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-12.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-12.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2005-12.ps},
doi = {10.1007/s00224-007-9064-z},
abstract = {Formal power series over non-commuting variables have been
investigated as representations of the behavior of automata with
multiplicities. Here we introduce and investigate the concepts of
aperiodic and of star-free formal power series over semirings and
partially commuting variables. We prove that if the semiring~\(K\) is
idempotent and commutative, or if \(K\) is idempotent and the variables
are non-commuting, then the product of any two aperiodic series is again
aperiodic. We also show that if \(K\) is idempotent and the matrix monoids
over~\(K\) have a Burnside property (satisfied, \textit{e.g.}~by the
tropical semiring), then the aperiodic and the star-free series coincide.
This generalizes a classical result of Sch{\"u}tzenberger~(1961) for
aperiodic regular languages and subsumes a result of Guaiana, Restivo and
Salemi~(1992) on aperiodic trace languages. }
}
@inproceedings{AA+-pvldb08,
address = {Auckland, New Zealand},
month = aug,
year = 2008,
volume = 1,
series = {Proceedings of the {VLDB} Endowment},
publisher = {ACM Press},
editor = {Weber, Gerald},
acronym = {{VLDB}'08},
booktitle = {{P}roceedings of the 34th {I}nternational
{C}onference on {V}ery {L}arge {D}ata {B}ases
({VLDB}'08)},
author = {Abiteboul, Serge and Allard, Tristan and
Chatalic, {\relax Ph}ilippe and Gardarin, Georges and
Ghitescu, Anca and Goasdou{\'e}, Fran{\c{c}}ois and Manolescu,
Ioana and Nguyen, Benjamin and Ouazara, Mohamed and
Somani, Aditya and Travers, Nicolas and
Vasile, Gabriel and Zoupanos, Spyros},
title = {Web{C}ontent: efficient {P2P} warehousing of web data},
pages = {1428-1431},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/Aetal-pvldb08.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Aetal-pvldb08.pdf},
abstract = {We present the WebContent platform for managing distributed
repositories of XML and semantic Web data. The platform allows integrating
various data processing building blocks (crawling, translation, semantic
annotation, full-text search, structured XML querying, and semantic
querying), presented as Web services, into a large-scale efficient
platform. Calls to various services are combined inside ActiveXML
documents, which are XML documents including service calls. An ActiveXML
optimizer is used to: (i)~efficiently distribute computations among sites;
(ii)~perform XQuery-specific optimizations by leveraging an algebraic
XQuery optimizer; and (iii)~given an XML query, chose among several
distributed indices the most appropriate in order to answer the query.}
}
@article{ABM-vldb08,
publisher = {ACM Press},
journal = {The VLDB Journal},
author = {Abiteboul, Serge and Benjelloun, Omar and Milo, Tova},
title = {The Active~{XML} project: an~overview},
volume = 17,
number = 5,
pages = {1019-1040},
year = {2008},
month = aug,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABM-vldb08.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABM-vldb08.pdf},
doi = {10.1007/s00778-007-0049-y},
abstract = {This paper provides an overview of the Active XML
project developed at INRIA over the past five years. Active XML (AXML, for
short), is a declarative framework that harnesses Web services for
distributed data management, and is put to work in a peer-to-peer
architecture.\par
The model is based on AXML documents, which are XML documents that may
contain embedded calls to Web services, and on AXML services, which are
Web services capable of exchanging AXML documents. An AXML peer is a
repository of AXML documents that acts both as a client by invoking the
embedded service calls, and as a server by providing AXML services, which
are generally defined as queries or updates over the persistent AXML
documents.\par
The approach gracefully combines stored information with data defined in
an intensional manner as well as dynamic information. This simple, rather
classical idea leads to a number of technically challenging problems, both
theoretical and practical.\par
In this paper, we describe and motivate the AXML model and language,
overview the research results obtained in the course of the project, and
show how all the pieces come together in our implementation.}
}
@inproceedings{AMPPS-icde08,
address = {Cancun, Mexico},
month = apr,
year = 2008,
publisher = {{IEEE} Computer Society Press},
editor = {Alonso, Gustavo and Blakeley, Jos{\'e} A. and Chen, Arbee L. P.},
acronym = {{ICDE}'08},
booktitle = {{P}roceedings of the 24th {I}nternational {C}onference on
{D}ata {E}ngineering ({ICDE}'08)},
author = {Abiteboul, Serge and Manolescu, Ioana and
Polyzotis, Neoklis and Preda, Nicoleta and
Sun, Chong},
title = {{XML} processing in {DHT} networks},
pages = {606-615},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AMPPS-icde08.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AMPPS-icde08.pdf},
doi = {10.1109/ICDE.2008.4497469},
abstract = {We study the scalable management of XML data in P2P networks
based on distributed hash tables (DHTs). We identify performance
limitations in this context, and propose an array o ftechniques to lift
them. First, we adapt the DHT platform to the needs of massive data
processing. (This primarily consists of replacing the DHT store by an
efficient native store and in streaming the communications with the DHT.)
Second, we introduce a distributed hierarchical index and efficient
algorithms taking advantage of this index to speed up query processing.
Third, we present an innovative, XML-specific flavor of Bloom filters, to
reduce data transfers entailed by query processing. Our approach is fully
implemented in the KadoP DHT-based XML processing system, used in a
real-life software manufacturing application. We present experiments that
demonstrate the benefits of the proposed techniques.}
}
@inproceedings{AMZ-icde08,
address = {Cancun, Mexico},
month = apr,
year = 2008,
publisher = {{IEEE} Computer Society Press},
editor = {Alonso, Gustavo and Blakeley, Jos{\'e} A. and Chen, Arbee L. P.},
acronym = {{ICDE}'08},
booktitle = {{P}roceedings of the 24th {I}nternational {C}onference on
{D}ata {E}ngineering ({ICDE}'08)},
author = {Abiteboul, Serge and Manolescu, Ioana and
Zoupanos, Spyros},
title = {{O}ptim{AX}: efficient support for data-intensive mash-ups},
pages = {1564-1567},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AMZ-icde08.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AMZ-icde08.pdf},
doi = {10.1109/ICDE.2008.4497622},
abstract = {Mash-ups are being used in various Web-based applications of Web
2.0 which combine instantly information from different sources. Active XML
(AXML, in short) language is a tool for decentralized, data-centric Web
service integration. AXML document includes calls to services that may be
either simple request-responses either long running subscriptions. Being
fully composable and allowing resource sharing makes AXML ideal for
mash-up style integration. In this demo we present how AXML can be used as
a specification, optimization and distributed execution language for
dynamic distributed mash-ups in varied P2P settings. We also demonstrate
our AXML optimizer's (OptimAX) optimization rules and rewriting engine
with a help of GUI.}
}
@inproceedings{AMB-icde08,
address = {Cancun, Mexico},
month = apr,
year = 2008,
publisher = {{IEEE} Computer Society Press},
editor = {Alonso, Gustavo and Blakeley, Jos{\'e} A. and Chen, Arbee L. P.},
acronym = {{ICDE}'08},
booktitle = {{P}roceedings of the 24th {I}nternational {C}onference on
{D}ata {E}ngineering ({ICDE}'08)},
author = {Abiteboul, Serge and Marinoiu, Bogdan and
Bourhis, Pierre},
title = {Distributed Monitoring of Peer-to-Peer Systems},
pages = {1572-1575},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AMB-icde08.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AMB-icde08.pdf},
doi = {10.1109/ICDE.2008.4497624},
abstract = {Observing highly dynamic Peer-to-Peer systems is essential for
many applications such as fault management or business processing. We
demonstrate P2PMonitor, a P2P system for monitoring such systems. Alerters
deployed on the monitored peers are designed to detect particular kinds of
local events. They generate streams of XML data that form the primary
sources of information for P2PMonitor. The core of the system is composed
of processing components implementing the operators of an algebra over
data streams.\par
From a user viewpoint, monitoring a P2P system can be as simple as
querying an XML document. The document is an ActiveXML document that
aggregates a (possibly very large) number of streams generated by alerters
on the monitored peers. Behind the scene, P2PMonitor compiles the
monitoring query into a distributed monitoring plan, deploys alerters and
stream algebra processors and issues notifications that are sent to users.\par
The system functionalities are demonstrated by simulating the supply chain
of a large company.}
}
@inproceedings{AMZ-icwe08,
address = {Yorktown Heights, New York, USA},
month = jul,
year = 2008,
publisher = {{IEEE} Computer Society Press},
editor = {Schwabe, Daniel and Curbera, Francisco and Dantzig, Paul},
acronym = {{ICWE}'08},
booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on {W}eb {E}ngineering
({ICWE}'08)},
author = {Abiteboul, Serge and Manolescu, Ioana and
Zoupanos, Spyros},
title = {{O}ptim{AX}: Optimizing Distributed {A}ctive{XML} Applications},
pages = {299-310},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AMZ-icwe08.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AMZ-icwe08.pdf},
doi = {10.1109/ICWE.2008.11},
abstract = {The Web has become a platform of choice for the deployment of
complex applications involving several business partners. Typically, such
applications interoperate by means of Web services, exchanging XML
information.\par
We present OptimAX, an optimization Web service that applies at the static
level (prior to enacting an application) in order to rewrite it into one
whose execution will be more performant. OptimAX builds on the ActiveXML
(AXML) data-centric Web service composition language, and demonstrates how
database-style techniques can be efficiently integrated in a
loosely-coupled, distributed application based on Web services. OptimAX
has been fully implemented and we describe its experimental performance.}
}
@inproceedings{AGM-widm08,
address = {Napa Valley, California, USA},
month = oct,
year = 2008,
publisher = {ACM Press},
editor = {Chan, Chee Yong and Polyzotis, Neoklis},
acronym = {{WIDM}'08},
booktitle = {{P}roceedings of the 10th {ACM} {I}nternational {W}orkshop on {W}eb
{I}nformation and {D}ata {M}anagement ({WIDM}'08)},
author = {Abiteboul, Serge and Greenshpan, Ohad and Milo, Tova},
title = {Modeling the mashup space},
pages = {87-94},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGM-widm08.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGM-widm08.pdf},
doi = {10.1145/1458502.1458517},
abstract = {We introduce a formal model for capturing the notion of mashup
in its globality. The basic component in our model is the mashlet. A
mashlet may query data sources, import other mashlets, use external Web
services, and specify complex interaction patterns between its components.
A mashlet state is modeled by a set of relations and its logic specified
by datalog-style active rules. We are primarily concerned with changes in
a mashlet state relations and rules. The interactions with users and other
applications, as well as the consequent effects on the mashlets
composition and behavior, are captured by streams of changes. The model
facilitates dynamic mashlets composition, interaction and reuse, and
captures the fundamental behavioral aspects of mashups.}
}
@article{SAG-ercim08,
publisher = {European Research Consortium for Informatics and Mathematics},
journal = {ERCIM News},
author = {Senellart, Pierre and Abiteboul, Serge and Gilleron,
R{\'e}mi},
title = {Understanding the Hidden Web},
volume = 72,
pages = {32-33},
year = 2008,
month = jan,
url = {http://ercim-news.ercim.eu/en72/special/understanding-the-hidden-web}
}
@inproceedings{HCL-fsttcs08,
address = {Bangalore, India},
month = dec,
year = 2008,
volume = 2,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Hariharan, Ramesh and Mukund, Madhavan and Vinay, V.},
acronym = {{FSTTCS}'08},
booktitle = {{P}roceedings of the 28th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'08)},
author = {Comon{-}Lundh, Hubert},
title = {About models of security protocols},
nopages = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HCL-fsttcs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HCL-fsttcs08.pdf},
abstract = {In this paper, mostly consisting of definitions, we~revisit the
models of security protocols: we~show that the symbolic and the
computational models (as~well as others) are instances of a same generic
model. Our definitions are also parametrized by the security primitives,
the notion of attacker and, to some extent, the process calculus.}
}
@phdthesis{oreiby-these2008,
author = {Oreiby, Ghassan},
title = {Logiques temporelles pour le contr{\^o}le temporis{\'e}},
year = 2008,
month = dec,
type = {Th{\`e}se de doctorat},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-GO08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-GO08.pdf}
}
@article{GLLN-mscs08,
publisher = {Cambridge University Press},
journal = {Mathematical Structures in Computer Science},
author = {Goubault{-}Larrecq, Jean and Lasota, S{\l}awomir
and Nowak, David},
title = {Logical Relations for Monadic Types},
volume = 18,
number = 6,
pages = {1169-1217},
month = dec,
year = 2008,
note = {81~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GLLN-arxiv05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GLLN-arxiv05.pdf},
doi = {10.1017/S0960129508007172},
abstract = {Logical relations and their generalisations are a fundamental
tool in proving properties of lambda calculi, for example,
for yielding sound principles for observational equivalence.
We propose a natural notion of logical relations that is
able to deal with the monadic types of Moggi's computational
lambda calculus. The treatment is categorical, and is based
on notions of subsconing, mono factorisation systems and
monad morphisms. Our approach has a number of interesting
applications, including cases for lambda calculi with
non-determinism (where being in a logical relation means
being bisimilar), dynamic name creation and probabilistic
systems.}
}
@phdthesis{bursztein-these2008,
author = {Bursztein, Elie},
title = {Anticipation games. Th{\'e}orie des jeux appliqu{\'e}s {\`a} la
s{\'e}curit{\'e} r{\'e}seau},
year = 2008,
month = nov,
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-EB08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-EB08.pdf},
futureslides = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/
these-AS07-slides.pdf}
}
@phdthesis{sangnier-these2008,
author = {Sangnier, Arnaud},
title = {V{\'e}rification de syst{\`e}mes avec compteurs et pointeurs},
year = 2008,
month = nov,
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-AS07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-AS07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/these-AS07.ps}
}
@phdthesis{arapinis-these2008,
author = {Arapinis, Myrto},
title = {S{\'e}curit{\'e} des protocoles cryptographiques~:
d{\'e}cidabilit{\'e} et r{\'e}sultats de r{\'e}duction},
year = 2008,
month = nov,
type = {Th{\`e}se de doctorat},
school = {Universit{\'e} Paris~12, Cr{\'e}teil, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-MA07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-MA07.pdf},
futureslides = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/
these-FC07-slides.pdf}
}
@article{BB-lmcs08,
journal = {Logical Methods in Computer Science},
author = {Bollig, Benedikt},
title = {On the Expressive Power of {\(2\)}-Stack Visibly Pushdown Automata},
volume = 4,
number = {4\string:16},
month = dec,
year = 2008,
nopages = {},
doi = {10.2168/LMCS-4(4:16)2008},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BB-lmcs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BB-lmcs08.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BB-lmcs08.ps},
abstract = {Visibly pushdown automata are input-driven pushdown automata
that recognize some non-regular context-free languages while
preserving the nice closure and decidability properties of
finite automata. Visibly pushdown automata with multiple
stacks have been considered recently by La~Torre,
Madhusudan, and Parlato, who exploit the concept of
visibility further to obtain a rich automata class that can
even express properties beyond the class of context-free
languages. At the same time, their automata are closed under
boolean operations, have a decidable emptiness and inclusion
problem, and enjoy a logical characterization in terms of a
monadic second-order logic over words with an additional
nesting structure. These results require a restricted
version of visibly pushdown automata with multiple stacks
whose behavior can be split up into a fixed number of
phases. In this paper, we~consider 2-stack visibly pushdown
automata (i.e., visibly pushdown automata with two stacks)
in their unrestricted form. We show that they are
expressively equivalent to the existential fragment of
monadic second-order logic. Furthermore, it turns out that
monadic second-order quantifier alternation forms an
infinite hierarchy wrt.~words with multiple nestings.
Combining these results, we conclude that 2-stack visibly
pushdown automata are not closed under complementation.
Finally, we discuss the expressive power of B{\"u}chi
2-stack visibly pushdown automata running on infinite
(nested) words. Extending the logic by an infinity
quantifier, we can likewise establish equivalence to
existential monadic second-order logic.}
}
@incollection{DH-afsec08,
author = {Donatelli, Susanna and Haddad, Serge},
title = {V{\'e}rification quantitative de cha{\^\i}nes de {M}arkov},
booktitle = {Approches formelles des syst{\`e}mes embarqu{\'e}s communicants},
editor = {Roux, Olivier H. and Jard, Claude},
publisher = {Herm{\`e}s},
year = 2008,
month = oct,
pages = {177-198},
chapter = 6,
url = {http://www.lavoisier.fr/notice/fr335499.html},
futureisbn = {}
}
@incollection{CM-afsec08,
author = {Cassez, Franck and Markey, Nicolas},
title = {Contr{\^o}le des syst{\`e}mes temporis{\'e}s},
booktitle = {Approches formelles des syst{\`e}mes embarqu{\'e}s communicants},
editor = {Roux, Olivier H. and Jard, Claude},
publisher = {Herm{\`e}s},
year = 2008,
month = oct,
pages = {105-144},
chapter = 4,
url = {http://www.lavoisier.fr/notice/fr335499.html},
nops = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/.ps},
nopsgz = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PSGZ/.ps.gz},
futureisbn = {}
}
@misc{NM-AV2008,
author = {Markey, Nicolas},
title = {Infinite Runs In Weighted Times Games with Energy Constraints},
year = 2008,
month = aug,
noslides = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/.pdf},
howpublished = {Invited talk, Workshop {A}utomata and {V}erification
({AV}'08), Mons, Belgium}
}
@misc{PB-AV2008,
author = {Bouyer, Patricia},
title = {Probabilities in Timed Automata},
year = 2008,
month = aug,
noslides = {},
howpublished = {Invited talk, Workshop {A}utomata and {V}erification
({AV}'08), Mons, Belgium}
}
@misc{PhS-AV2008,
author = {Schnoebelen, {\relax Ph}ilippe},
title = {The complexity of lossy channel systems},
year = 2008,
month = aug,
noslides = {},
howpublished = {Invited talk, Workshop {A}utomata and {V}erification
({AV}'08), Mons, Belgium}
}
@inproceedings{CLC-ccs08,
address = {Alexandria, Virginia, USA},
month = oct,
year = 2008,
publisher = {ACM Press},
acronym = {{CCS}'08},
booktitle = {{P}roceedings of the 15th {ACM} {C}onference
on {C}omputer and {C}ommunications {S}ecurity
({CCS}'08)},
author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique},
title = {Computational Soundness of Observational Equivalence},
pages = {109-118},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CLC-ccs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CLC-ccs08.pdf},
doi = {10.1145/1455770.1455786},
abstract = {Many security properties are naturally expressed as
indistinguishability between two versions of a protocol. In
this paper, we show that computational proofs of
indistinguishability can be considerably simplified, for a
class of processes that covers most existing protocols. More
precisely, we show a soundness theorem, following the line
of research launched by Abadi and Rogaway in~2000:
computational indistinguishability in presence of an active
attacker is implied by the observational equivalence of the
corresponding symbolic processes. We prove our result for
symmetric encryption, but the same techniques can be applied
to other security primitives such as signatures and
public-key encryption. The proof requires the introduction
of new concepts, which are general and can be reused in
other settings.}
}
@mastersthesis{ciobaca-master,
author = {Ciob{\^a}c{\u{a}}, {\c{S}}tefan},
title = {Verification of anonymity properties in e-voting protocols},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2008},
month = sep,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/master-ciobaca.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/master-ciobaca.pdf}
}
@misc{dots-rapp-18m,
author = {Fran{\c{c}}ois Laroussinie and others},
title = {Projet DOTS (ANR-06-SETI-003)~: Rapport {\`a} \(18\)~mois},
year = 2008,
month = sep,
type = {Contract Report},
note = {5~pages}
}
@misc{dots-rapp-12m,
author = {Fran{\c{c}}ois Laroussinie and others},
title = {Projet DOTS (ANR-06-SETI-003)~: Rapport {\`a} \(12\)~mois},
year = 2008,
month = mar,
type = {Contract Report},
note = {6~pages}
}
@misc{dots-1.1,
author = {Cassez, Franck and Laroussinie, Fran{\c{c}}ois and Lime,
Didier and Markey, Nicolas},
title = {Quantitative Objectives in Timed Games},
howpublished = {Deliverable DOTS~1.1 (ANR-06-SETI-003)},
year = 2008,
month = sep
}
@misc{dots-3.1,
author = {Bollig, Benedikt and Bouyer, Patricia and Cassez, Franck and
Chatain, {\relax Th}omas and Gastin, Paul and Haddad, Serge
and Jard, Claude},
title = {Model for distributed timed systems},
howpublished = {Deliverable DOTS~3.1 (ANR-06-SETI-003)},
year = 2008,
month = sep
}
@inproceedings{ADK-lpar08,
address = {Doha, Qatar},
month = nov,
year = 2008,
volume = {5330},
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Cervesato, Iliano and Veith, Helmut and Voronkov, Andrei},
acronym = {{LPAR}'08},
booktitle = {{P}roceedings of the 15th {I}nternational
{C}onference on {L}ogic for {P}rogramming,
{A}rtificial {I}ntelligence, and {R}easoning
({LPAR}'08)},
author = {Arapinis, Myrto and Delaune, St{\'e}phanie and Kremer, Steve},
title = {From One Session to Many: Dynamic Tags for Security Protocols},
pages = {128-142},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ADK-lpar08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ADK-lpar08.pdf},
doi = {10.1007/978-3-540-89439-1_9},
abstract = {The design and verification of cryptographic
protocols is a notoriously difficult task, even in abstract
Dolev-Yao models. This is mainly due to several sources of
unboundedness (size of messages, number of sessions,~...).
In~this paper, we~present a transformation which maps a protocol
that is secure for a single session to a protocol that is secure
for an unbounded number of sessions. The~transformation is
surprisingly simple, computationally light and works for
arbitrary protocols that rely on usual cryptographic primitives,
such as symmetric and asymmetric encryption as well as digital
signatures. Our~result provides an effective strategy to design
secure protocols: (i)~design a protocol intended to be secure
for one session (this can be verified with existing automated
tools); (ii)~apply our transformation and obtain a protocol
which is secure for an unbounded number of sessions.
A~side-effect of this result is that we characterize a class of
protocols for which secrecy for an unbounded number of sessions
is decidable.}
}
@inproceedings{HCL-ijcar08,
address = {Sydney, Australia},
month = aug,
year = 2008,
volume = {5195},
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer-Verlag},
editor = {Armando, Alessandro and Baumgartner, Peter and
Dowek, Gilles},
acronym = {{IJCAR}'08},
booktitle = {{P}roceedings of the 4th {I}nternational {J}oint
{C}onference on {A}utomated {R}easoning
({IJCAR}'08)},
author = {Comon{-}Lundh, Hubert},
title = {Challenges in the Automated Verification of Security
Protocols},
pages = {396-409},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HCL-ijcar08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HCL-ijcar08.pdf},
doi = {10.1007/978-3-540-71070-7_34},
abstract = {The application area of security protocols raises several
problems that are relevant to automated deduction. We
describe in this note some of these challenges.}
}
@article{DG-tcs08,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Demri, St{\'e}phane and Gascon, R{\'e}gis},
title = {Verification of Qualitative {\(\mathbb{\MakeUppercase{Z}}\)}~constraints},
volume = 409,
number = 1,
month = dec,
year = 2008,
pages = {24-40},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-tcs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-tcs08.pdf},
doi = {10.1016/j.tcs.2008.07.023},
abstract = {We introduce an LTL-like logic with atomic formulae built over a
constraint language interpreting variables in~\(\mathbb{Z}\).
The~constraint language includes periodicity constraints, comparison
constraints of the form \({x = y}\) and \({x < y}\), is~closed under Boolean
operations and admits a restricted form of existential quantification.
Such constraints are used for instance in calendar formalisms or
abstractions of counter automata by using congruences modulo some power of
two. Indeed, various programming languages perform arithmetic operators
modulo some integer. We~show that the satisfiability and model-checking
problems (with respect to an appropriate class of constraint automata) for
this logic are decidable in polynomial space improving significantly known
results about its strict fragments. This is the largest set of qualitative
constraints over~\(\mathbb{Z}\) known so~far, shown to admit a decidable
LTL extension.}
}
@inproceedings{BCFH-valuetools08,
address = {Athens, Greece},
month = oct,
year = 2008,
publisher = {Institute for Computer Sciences, Social-Informatics and
Telecommunications Engineering},
editor = {Chahed, Tijani and Toumpis, Stavros and Yechiali, Uri},
acronym = {{VALUETOOLS}'08},
booktitle = {{P}roceedings of the 3rd {I}nternational {C}onference
on {P}erformance {E}valuation {M}ethodologies and {T}ools
({VALUETOOLS}'08)},
author = {Beccuti, Marco and Codetta{-}Raiteri, Daniele and
Franceschinis, Giuliana and Haddad, Serge},
title = {Non Deterministic Repairable Fault Trees for Computing
Optimal Repair Strategy},
nopages = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFH-valuetools08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFH-valuetools08.pdf},
doi = {10.4108/ICST.VALUETOOLS2008.4411},
abstract = {In~this paper, the Non deterministic Repairable Fault
Tree~(NdRFT) formalism is proposed: it allows to model failure modes of
complex systems as well as their repair processes. The originality of this
formalism with respect to other Fault Tree extensions is that it allows to
face repair strategies optimization problems: in~an NdRFT model, the
decision on whether to start or not a given repair action is non
deterministic, so that all the possibilities are left open. The formalism
is rather powerful allowing to specify which failure events are
observable, whether local repair or global repair can be applied, and the
resources needed to start a repair action. The optimal repair strategy can
then be computed by solving an optimization problem on a Markov Decision
Process~(MDP) derived from the NdRFT. A~software framework is proposed in
order to perform in automatic way the derivation of an MDP from a NdRFT
model, and to deal with the solution of the MDP.}
}
@article{DDMR-fmsd08,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {De{~}Wulf, Martin and Doyen, Laurent and Markey, Nicolas
and Raskin, Jean-Fran{\c{c}}ois},
title = {Robust Safety of Timed Automata},
year = 2008,
month = dec,
volume = 33,
number = {1-3},
pages = {45-84},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDMR-fmsd08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDMR-fmsd08.pdf},
doi = {10.1007/s10703-008-0056-7},
abstract = {Timed automata are governed by an idealized semantics that
assumes a perfectly precise behavior of the clocks. The traditional
semantics is not robust because the slightest perturbation in the timing
of actions may lead to completely different behaviors of the automaton.
Following several recent works, we consider a relaxation of this
semantics, in which guards on transitions are widened by~\(\Delta>0\) and
clocks can drift by~\(\epsilon>0\). The relaxed semantics encompasses the
imprecisions that are inevitably present in an implementation of a timed
automaton, due to the finite precision of digital clocks.\par
We solve the safety verification problem for this robust semantics: given
a timed automaton and a set of bad states, our algorithm decides if there
exist positive values for the parameters~\(\Delta\) and~\(\epsilon\) such
that the timed automaton never enters the bad states under the relaxed
semantics.}
}
@inproceedings{Bur-atva08,
address = {Seoul, Korea},
month = oct,
year = {2008},
volume = 5311,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cha, Sungdeok and Choi, Jin-Young and Kim, Moonzoo
and Lee, Insup and Viswanathan, Mahesh},
acronym = {{ATVA}'08},
booktitle = {{P}roceedings of the 6th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'08)},
author = {Bursztein, Elie},
title = {Net{Q}i: A~Model Checker for Anticipation Game},
pages = {246-251},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bur-atva08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bur-atva08.pdf},
doi = {10.1007/978-3-540-88387-6_22},
abstract = {NetQi is a freely available model-checker designed to analyze
network incidents such as intrusion. This tool is an implementation of the
anticipation game framework, a variant of timed game tailored for network
analysis. The main purpose of NetQi is to find, given a network initial
state and a set of rules, the best strategy that fulfills player
objectives by model-checking the anticipation game and comparing the
outcome of each play that fulfills strategy constraints. For instance, it
can be used to find the best patching strategy. NetQi has been
successfully used to analyze service failure due to hardware, network
intrusion, worms and multiple-site intrusion defense cooperation.}
}
@inproceedings{ACEF-rp08,
address = {Liverpool, UK},
month = dec,
year = 2008,
volume = 223,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Halava, Vesa and Potapov, Igor},
acronym = {{RP}'08},
booktitle = {{P}roceedings of the 2nd {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'08)},
author = {Andr{\'e}, {\'E}tienne and Chatain, {\relax Th}omas and
Encrenaz, Emmanuelle and Fribourg, Laurent},
title = {An Inverse Method for Parametric Timed Automata},
pages = {29-46},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACEF-rp08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACEF-rp08.pdf},
doi = {10.1016/j.entcs.2008.12.029},
abstract = {Given a timed automaton with parametric timings, our objective
is to describe a procedure for deriving constraints on the parametric
timings in order to ensure that, for~each value of parameters satisfying
these constraints, the behaviors of the timed automata are time-abstract
equivalent. We~will exploit a reference valuation of the parameters that
is supposed to capture a characteristic proper behavior of the system.
The~method has been implemented and is illustrated on various examples of
asynchronous circuits.}
}
@techreport{LSV:08:18,
author = {Goubault{-}Larrecq, Jean},
title = {A Cone-Theoretic {K}rein-{M}ilman Theorem},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = 2008,
month = jun,
type = {Research Report},
number = {LSV-08-18},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-18.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-18.pdf},
note = {8~pages},
abstract = {We prove the following analogue of the Krein-Milman
Theorem: in any locally convex \(T_{0}\) topological cone, every
convex compact saturated subset is the compact saturated convex hull
of its extreme points.}
}
@inproceedings{bbjlr-formats08,
address = {Saint-Malo, France},
month = sep,
year = 2008,
volume = 5215,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cassez, Franck and Jard, Claude},
acronym = {{FORMATS}'08},
booktitle = {{P}roceedings of the 6th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'08)},
author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and
Jurdzi{\'n}ski, Marcin and Lazi{\'c}, Ranko and
Rutkowski, Micha{\l}},
title = {Average-Price and Reachability-Price Games on Hybrid
Automata with Strong Resets},
pages = {63-77},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bbjlr-formats08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bbjlr-formats08.pdf},
doi = {10.1007/978-3-540-85778-5_6},
abstract = {We introduce and study hybrid automata with strong resets. They
generalize o-minimal hybrid automata, a class of hybrid automata which
allows modeling of complex continuous dynamics. A number of analysis
problems, such as reachability testing and controller synthesis, are
decidable for classes of o-minimal hybrid automata. We generalize existing
decidability results for controller synthesis on hybrid automata and we
establish new ones by proving that average-price and reachability-price
games on hybrid systems with strong resets are decidable, provided that
the structure on which the hybrid automaton is defined has a decidable
first-order theory. Our proof techniques include a novel characterization
of values in games on hybrid systems by optimality equations, and a
definition of a new finitary equivalence relation on the states of a
hybrid system which enables a reduction of games on hybrid systems to
games on finite graphs. }
}
@inproceedings{bflms-formats08,
address = {Saint-Malo, France},
month = sep,
year = 2008,
volume = 5215,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cassez, Franck and Jard, Claude},
acronym = {{FORMATS}'08},
booktitle = {{P}roceedings of the 6th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'08)},
author = {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim G.
and Markey, Nicolas and Srba, Ji{\v{r}}{\'\i}},
title = {Infinite Runs in Weighted Timed Automata with Energy
Constraints},
pages = {33-47},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLMS-formats08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLMS-formats08.pdf},
doi = {10.1007/978-3-540-85778-5_4},
abstract = {We~study the problems of existence and construction of
infinite schedules for finite weighted automata and one-clock weighted
timed automata, subject to boundary constraints on the accumulated
weight. More specifically, we~consider automata equipped with positive
and negative weights on transitions and locations, corresponding to the
production and consumption of some resource (\emph{e.g.}~energy). We~ask the
question whether there exists an infinite path for which the accumulated
weight for any finite prefix satisfies certain constraints (\emph{e.g.}~remains
between~\(0\) and some given upper-bound). We~also consider a game version
of the above, where certain transitions may be uncontrollable.}
}
@article{CJP-lmcs08,
journal = {Logical Methods in Computer Science},
author = {Comon{-}Lundh, Hubert and Jacquemard, Florent and Perrin, Nicolas},
title = {Visibly Tree Automata with Memory and Constraints},
year = 2008,
month = jun,
volume = 4,
number = {2\string:8},
nopages = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CJP-lmcs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CJP-lmcs08.pdf},
doi = {10.2168/LMCS-4(2:8)2008},
abstract = {Tree automata with one memory have been introduced in~2001. They
generalize both pushdown (word) automata and the tree automata with
constraints of equality between brothers of Bogaert and Tison. Though it
has a decidable emptiness problem, the main weakness of this model is its
lack of good closure properties.\par
We propose a generalization of the visibly pushdown automata of Alur
and~Madhusudan to a family of tree recognizers which carry along their
(bottom-up) computation an auxiliary unbounded memory with a tree
structure (instead of a symbol stack). In~other words, these recognizers,
called Visibly Tree Automata with Memory~(VTAM) define a subclass of tree
automata with one memory enjoying Boolean closure properties. We~show in
particular that they can be determinized and the problems like emptiness,
membership, inclusion and universality are decidable for VTAM. Moreover,
we propose several extensions of VTAM whose transitions may be constrained
by different kinds of tests between memories and also constraints
\emph{{\`a}~la} Bogaert and~Tison. We~show that some of these classes of
constrained VTAM keep the good closure and decidability properties, and we
demonstrate their expressiveness with relevant examples of tree
languages.}
}
@inproceedings{ABH-dlt08,
address = {Kyoto, Japan},
month = sep,
year = 2008,
volume = 5257,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ito, Masami and Toyama, Masafumi},
acronym = {{DLT}'08},
booktitle = {{P}roceedings of the 12th {I}nternational
{C}onference on {D}evelopments in {L}anguage {T}heory
({DLT}'08)},
author = {Atig, Mohamed Faouzi and Bollig, Benedikt and Habermehl, Peter},
title = {Emptiness of multi-pushdown automata is \(2\){ETIME}-complete},
pages = {121-133},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABH-dlt08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABH-dlt08.pdf},
doi = {10.1007/978-3-540-85780-8_9},
abstract = {We consider multi-pushdown automata, a multi-stack extension of
pushdown automata that comes with a constraint on stack operations: a pop
can only be performed on the first non-empty stack (which implies that we
assume a linear ordering on the collection of stacks). We show that the
emptiness problem for multi-pushdown automata is 2ETIME-complete wrt.~the
number of stacks. Containment in 2ETIME is shown by translating an
automaton into a grammar for which we can check if the generated language
is empty. The lower bound is established by simulating the behavior of an
alternating Turing machine working in exponential space. We also compare
multi-pushdown automata with the model of bounded-phase multi-stack
(visibly) pushdown automata.}
}
@inproceedings{CDFPS-qest08,
address = {Saint~Malo, France},
month = sep,
year = 2008,
publisher = {{IEEE} Computer Society Press},
acronym = {{QEST}'08},
booktitle = {{P}roceedings of the 5th {I}nternational
{C}onference on {Q}uantitative
{E}valuation of {S}ystems
({QEST}'08)},
author = {Chamseddine, Najla and Duflot, Marie and Fribourg,
Laurent and Picaronny, Claudine and Sproston, Jeremy},
title = {Computing Expected Absorption Times for Parametric
Determinate Probabilistic Timed Automata},
pages = {254-263},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDFPS-qest08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDFPS-qest08.pdf},
doi = {10.1109/QEST.2008.34},
abstract = {We consider a variant of probabilistic timed automata called
\emph{parametric determinate probabilistic timed automata}. Such~automata
are fully probabilistic: there~is a single distribution of outgoing
transitions from each of the automaton's nodes, and~it~is possible to
remain at a node only for a given amount of time. The~residence time
within a node may be given in terms of a parameter, and~hence we do not
assume that its concrete value is known.\par
We claim that, often in practice, the maximal expected time to reach a
given absorbing node of a probabilistic timed automaton can be captured
using a parametric determinate probabilistic timed automaton. We give a
method for computing the expected time for a parametric determinate
probabilistic timed automaton to reach an absorbing node. The~method
consists in constructing a variant of a Markov chain with costs (where the
costs correspond to durations), and~is parametric in the sense that the
expected absorption time is computed as a function of the model's
parameters. The~complexity of the analysis is independent from the maximal
constant bounding the values of the clocks, and is polynomial in the
number of edges of the original parametric determinate probabilistic timed
automaton.}
}
@inproceedings{JR-rta2008,
address = {Hagenberg, Austria},
month = jul,
year = 2008,
volume = 5117,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Voronkov, Andrei},
acronym = {{RTA}'08},
booktitle = {{P}roceedings of the 19th {I}nternational
{C}onference on {R}ewriting {T}echniques
and {A}pplications
({RTA}'08)},
author = {Jacquemard, Florent and Rusinowitch, Micha{\"e}l},
title = {Closure of {H}edge-Automata Languages by {H}edge
Rewriting},
pages = {157-171},
doi = {10.1007/978-3-540-70590-1_11},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JR-rta08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JR-rta08.pdf},
abstact = {We consider rewriting systems for unranked ordered terms,
\textit{i.e.}, trees where the number of successors of a node is not
determined by its label, and is not \textit{a priori} bounded. The
rewriting systems are defined such that variables in the rewrite rules can
be substituted by hedges (sequences of terms) instead of just terms.
Consequently, this notion of rewriting subsumes both standard term
rewriting and word rewriting.\par
We investigate some preservation properties for two classes of languages
of unranked ordered terms under this generalization of term rewriting. The
considered classes include languages of hedge automata (HA) and some
extension (called CF-HA) with context-free languages in transitions,
instead of regular languages.\par
In particular, we show that the set of unranked terms reachable from a
given HA language, using a so called inverse context-free rewrite system,
is a HA language. The proof, based on a HA completion procedure, reuses
and combines known techniques with non-trivial adaptations. Moreover, we
prove, with different techniques, that the closure of CF-HA languages with
respect to restricted context-free rewrite systems, the symmetric case of
the above rewrite systems, is a CF-HA language. As a consequence, the
problems of ground reachability and regular hedge model checking are
decidable in both cases. We give several counter examples showing that we
cannot relax the restrictions.}
}
@proceedings{DJ-time2008,
title = {{P}roceedings of the 15th {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'08)},
booktitle = {{P}roceedings of the 15th {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'08)},
editor = {Demri, St{\'e}phane and Jensen, {\relax Ch}ristian S.},
publisher = {{IEEE} Computer Society Press},
year = 2008,
month = jun,
address = {Montr{\'e}al, Canada}
}
@inproceedings{CS-concur08,
address = {Toronto, Canada},
month = aug,
year = 2008,
volume = 5201,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {van Breugel, Franck and Chechik, Marsha},
acronym = {{CONCUR}'08},
booktitle = {{P}roceedings of the 19th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'08)},
author = {Chambart, Pierre and Schnoebelen, {\relax Ph}ilippe},
title = {Mixing Lossy and Perfect Fifo Channels},
pages = {340-355},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-concur08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-concur08.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CS-concur08.ps},
doi = {10.1007/978-3-540-85361-9_28},
abstract = {We~consider asynchronous networks of finite-state systems
communicating \emph{via} a combination of reliable and lossy fifo channels.
Depending on the topology, the~reachability problem for such networks may
be decidable. We~provide a complete classification of network topologies
according to whether they lead to a decidable reachability problem.
Furthermore, this classification can be decided in polynomial-time.}
}
@inproceedings{BCHK-concur08,
address = {Toronto, Canada},
month = aug,
year = 2008,
volume = 5201,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {van Breugel, Franck and Chechik, Marsha},
acronym = {{CONCUR}'08},
booktitle = {{P}roceedings of the 19th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'08)},
author = {Baldan, Paolo and Chatain, {\relax Th}omas and Haar, Stefan and K{\"o}nig,
Barbara},
title = {Unfolding-based Diagnosis of Systems with an Evolving Topology},
pages = {203-217},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHK-concur08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHK-concur08.pdf},
doi = {10.1007/978-3-540-85361-9_19},
abstract = {We propose a framework for model-based diagnosis of systems with
mobility and variable topologies, modelled as graph transformation
systems. Generally speaking, model-based diagnosis is aimed at
constructing explanations of observed faulty behaviours on the basis of a
given model of the system. Since the number of possible explanations may
be huge we exploit the unfolding as a compact data structure to store
them, along the lines of previous work dealing with Petri net models.
Given a model of a system and an observation, the explanations can be
constructed by unfolding the model constrained by the observation, and
then removing incomplete explanations in a pruning phase. The theory is
formalised in a general categorical setting: constraining the system by
the observation corresponds to taking a product in the chosen category of
graph grammars, so that the correctness of the procedure can be proved by
using the fact that the unfolding is a right adjoint and thus it preserves
products. The theory thus should be easily applicable to a wide class of
system models, including graph grammars and Petri nets.}
}
@inproceedings{BKKL-concur08,
address = {Toronto, Canada},
month = aug,
year = 2008,
volume = 5201,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {van Breugel, Franck and Chechik, Marsha},
acronym = {{CONCUR}'08},
booktitle = {{P}roceedings of the 19th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'08)},
author = {Bollig, Benedikt and Katoen, Joost-Pieter and Kern, Carsten and
Leucker, Martin},
title = {{\itshape Smyle}: A Tool for Synthesizing Distributed Models from
Scenarios by Learning},
pages = {162-166},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-concur08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-concur08.pdf},
doi = {10.1007/978-3-540-85361-9_15}
}
@inproceedings{LV-concur08,
address = {Toronto, Canada},
month = aug,
year = 2008,
volume = 5201,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {van Breugel, Franck and Chechik, Marsha},
acronym = {{CONCUR}'08},
booktitle = {{P}roceedings of the 19th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'08)},
author = {Lozes, {\'E}tienne and Villard, Jules},
title = {A Spatial Equational Logic for the Applied {{\(\pi\)}}-Calculus},
pages = {387-401},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LV-concur08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LV-concur08.pdf},
doi = {10.1007/978-3-540-85361-9_31},
abstract = {Spatial logics have been proposed to reason locally and
modularly on algebraic models of distributed systems. In this paper we
define the spatial equational logic A\(\pi\)L whose models are processes
of the applied \(\pi\)-calculus. This extension of the \(\pi\)-calculus
allows term manipulation and records communications as active
substitutions in a frame, thus augmenting the underlying predefined
equational theory. Our logic allows one to reason locally either on frames
or on processes, thanks to static and dynamic spatial operators. We study
the logical equivalences induced by various relevant fragments
of~A\(\pi\)L, and~show in particular that the whole logic induces a
coarser equivalence than structural congruence. We give characteristic
formulae for some of these equivalences and for static equivalence. Going
further into the exploration of A\(\pi\)L's expressivity, we~also show
that it can eliminate standard term quantification.}
}
@inproceedings{ABGMN-concur08,
address = {Toronto, Canada},
month = aug,
year = 2008,
volume = 5201,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {van Breugel, Franck and Chechik, Marsha},
acronym = {{CONCUR}'08},
booktitle = {{P}roceedings of the 19th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'08)},
author = {Akshay, S. and Bollig, Benedikt and Gastin, Paul and Mukund,
Madhavan and Narayan Kumar, K.},
title = {Distributed Timed Automata with Independently Evolving
Clocks},
pages = {82-97},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABGMN-concur08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABGMN-concur08.pdf},
doi = {10.1007/978-3-540-85361-9_10},
abstract = { We propose a model of distributed timed systems where each
component is a timed automaton with a set of local clocks that evolve at a
rate independent of the clocks of the other components. A clock can be
read by any component in the system, but it can only be reset by the
automaton it belongs to.\par
There are two natural semantics for such systems. The \emph{universal}
semantics captures behaviors that hold under any choice of clock rates for
the individual components. This is a natural choice when checking that a
system always satisfies a positive specification. However, to check if a
system avoids a negative specification, it is better to use the
\emph{existential} semantics---the set of behaviors that the system can
possibly exhibit under some choice of clock rates.\par
We show that the existential semantics always describes a regular set of
behaviors. However, in the case of universal semantics, checking emptiness
turns out to be undecidable. As an alternative to the universal semantics,
we propose a \emph{reactive} semantics that allows us to check positive
specifications and yet describes a regular set of behaviors. }
}
@inproceedings{FS-mfcs08,
address = {Toru{\'n}, Poland},
month = aug,
year = 2008,
volume = {5162},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ochma{\'n}ski, Edward and Tyszkiewicz, Jerzy},
acronym = {{MFCS}'08},
booktitle = {{P}roceedings of the 33rd
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'08)},
author = {Finkel, Alain and Sangnier, Arnaud},
title = {Reversal-bounded Counter Machines Revisited},
pages = {323-334},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-mfcs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-mfcs08.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FS-mfcs08.ps},
doi = {10.1007/978-3-540-85238-4_26},
abstract = {We~extend the class of reversal-bounded counter machines by
authorizing a finite number of alternations between increasing and
decreasing mode over a given bound. We~prove that extended
reversal-bounded counter machines also have effective semi-linear
reachability sets. We~also prove that the property of being
reversal-bounded is undecidable in general even when we fix the bound,
whereas this problem becomes decidable when considering Vector Addition
System with States.}
}
@inproceedings{place-csl08,
address = {Bertinoro, Italy},
month = sep,
year = 2008,
volume = 5213,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Kaminski, Michael and Martini, Simone},
acronym = {{CSL}'08},
booktitle = {{P}roceedings of the 17th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'08)},
author = {Place, {\relax Th}omas},
title = {Characterization of Logics Over Ranked Tree Languages},
pages = {401-415},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/place-csl08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/place-csl08.pdf},
doi = {10.1007/978-3-540-87531-4_29},
abstract = {We study the expressive power of the logics
\(\textit{EF}+\textit{F}^{-1}\), \(\Delta_{2}\), and boolean combinations
of \(\Sigma_{1}\) over ranked trees. In~particular, we provide effective
characterizations of those three logics using algebraic identities.
Characterizations had already been obtained for those logics over
unranked trees, but both the algebra and the proofs were dependant on the
properties of the unranked structure and the problem remained open for
ranked trees.}
}
@inproceedings{BDL-csl08,
address = {Bertinoro, Italy},
month = sep,
year = 2008,
volume = 5213,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Kaminski, Michael and Martini, Simone},
acronym = {{CSL}'08},
booktitle = {{P}roceedings of the 17th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'08)},
author = {Brochenin, R{\'e}mi and Demri, St{\'e}phane and
Lozes, {\'E}tienne},
title = {On~the Almighty Wand},
pages = {323-338},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-csl08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-csl08.pdf},
doi = {10.1007/978-3-540-87531-4_24},
abstract = {We investigate decidability, complexity and expressive power
issues for (first-order) separation logic with one record field (herein
called~SL) and its fragments. SL~can specify properties about the memory
heap of programs with singly-linked lists. Separation logic with two
record fields is known to be undecidable by reduction of finite
satisfiability for classical predicate logic with one binary relation.
Surprisingly, we~show that second-order logic is as expressive as SL and
as a by-product we get undecidability of~SL. This is refined by showing
that SL without the separating conjunction is as expressive as~SL, whence
undecidable too. As~a consequence of this deep result, in~SL the magic
wand can simulate the separating conjunction. By~contrast, we~establish
that SL without the magic wand is decidable with non-elementary complexity
by reduction from satisfiability for the first-order theory over finite
words. Equivalence between second-order logic and separation logic extends
to the case with more than one selector.}
}
@inproceedings{bhhtv08ciaa,
address = {San Francisco, California, USA},
month = jul,
year = 2008,
volume = 5148,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Ibarra, Oscar H. and Ravikumar, Bala},
acronym = {{CIAA}'08},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onference on {I}mplementation and
{A}pplication of {A}utomata
({CIAA}'08)},
author = {Bouajjani, Ahmed and Habermehl, Peter and Hol\'{\i}k, Luk{\'a}{\v{s}} and
Touili, Tayssir and Vojnar, Tom{\'a}{\v{s}}},
title = {Antichain-based Universality and Inclusion Testing over
Nondeterministic Finite Tree Automata},
pages = {57-67},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bhhtv-ciaa08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bhhtv-ciaa08.pdf},
doi = {10.1007/978-3-540-70844-5_7},
abstract = {We propose new antichain-based algorithms for checking
universality and inclusion of nondeterministic tree automata. We have
implemented these algorithms in a prototype tool and we present
experiments which show that the algorithms provide a significant
improvement over the traditional determinisation-based approaches.
Furthermore, we use the proposed antichain-based inclusion checking
algorithm to build an abstract regular tree model checking framework based
entirely on nondeterministic tree automata. We show the significantly
improved efficiency of this framework on a series of experiments with
verifying various programs over dynamic tree-shaped data structures linked
by pointers.}
}
@inproceedings{tCS-pods08,
address = {Vancouver, Canada},
month = jun,
year = 2008,
publisher = {ACM Press},
editor = {Lenzerini, Maurizio and Lembo, Domenico},
acronym = {{PODS}'08},
booktitle = {{P}roceedings of the 27th {A}nnual
{ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium
on {P}rinciples of {D}atabase {S}ystems
({PODS}'08)},
author = {ten~Cate, Balder and Segoufin, Luc},
title = {{XP}ath, Transitive Closure Logic, and Nested Tree Walking
Automata},
pages = {251-260},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/tCS-pods08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/tCS-pods08.pdf},
doi = {10.1145/1376916.1376952},
abstract = {We consider the navigational core of XPath, extended with two
operators: the Kleene star for taking the transitive closure of path
expressions, and a subtree relativisation operator, allowing one to
restrict attention to a specific subtree while evaluating a subexpression.
We show that the expressive power of this XPath dialect equals that of
FO(MTC), first order logic extended with monadic transitive closure. We
also give a characterization in terms of nested tree-walking automata.
Using the latter we then proceed to show that the language is strictly
less expressive than MSO. This solves an open question about the relative
expressive power of FO(MTC) and MSO on trees. We~also investigate the
complexity for our XPath dialect. We~show that query evaluation be done in
polynomial time (combined complexity), but that satisfiability and query
containment (as~well as emptiness for our automaton model) are
2ExpTime-complete (it is ExpTime-complete for Core XPath).}
}
@inproceedings{ASV-pods08,
address = {Vancouver, Canada},
month = jun,
year = 2008,
publisher = {ACM Press},
editor = {Lenzerini, Maurizio and Lembo, Domenico},
acronym = {{PODS}'08},
booktitle = {{P}roceedings of the 27th {A}nnual
{ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium
on {P}rinciples of {D}atabase {S}ystems
({PODS}'08)},
author = {Abiteboul, Serge and Segoufin, Luc and Vianu, Victor},
title = {Static Analysis of Active {XML} Systems},
pages = {221-230},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ASV-pods08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ASV-pods08.pdf},
doi = {10.1145/1376916.1376948},
abstract = {Active XML is a high-level specification language tailored to
data-intensive, distributed, dynamic Web services. Active
XML is based on XML documents with embedded function calls.
The state of a document evolves depending on the result of
internal function calls (local computations) or external
ones (interactions with users or other services). Function
calls return documents that may be active, so may activate
new subtasks. The focus of the paper is on the verification
of temporal properties of runs of Active XML systems,
specified in a tree-pattern based temporal logic, Tree-LTL,
that allows expressing a rich class of semantic properties
of the application. The main results establish the boundary
of decidability and the complexity of automatic verification
of Tree-LTL properties.}
}
@inproceedings{BBBM-qest08,
address = {Saint~Malo, France},
month = sep,
year = 2008,
publisher = {{IEEE} Computer Society Press},
acronym = {{QEST}'08},
booktitle = {{P}roceedings of the 5th {I}nternational
{C}onference on {Q}uantitative
{E}valuation of {S}ystems
({QEST}'08)},
author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye,
{\relax Th}omas and Markey, Nicolas},
title = {Quantitative Model-Checking of One-Clock Timed Automata under
Probabilistic Semantics},
pages = {55-64},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBM-qest08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBM-qest08.pdf},
doi = {10.1109/QEST.2008.19},
abstract = {In [Baier \emph{et~al.}, \textit{Probabilistic and Topological
Semantics for Timed Automata}, FSTTCS'07] a probabilistic semantics for
timed automata has been defined in order to rule out unlikely (sequences
of) events. The qualitative model-checking problem for LTL properties has
been investigated, where the aim is to check whether a given LTL property
holds with probability~\(1\) in a timed automaton, and solved for the class of
single-clock timed automata.\par
In this paper, we consider the quantitative model-checking problem for
\(\omega\)-regular properties: we aim at computing the exact probability
that a given timed automaton satisfies an \(\omega\)-regular property. We
develop a framework in which we can compute a closed-form expression for
this probability; we furthermore give an approximation algorithm, and
finally prove that we can decide the threshold problem in that
framework.}
}
@article{BLM-lmcs08,
journal = {Logical Methods in Computer Science},
author = {Bouyer, Patricia and Larsen, Kim G. and Markey, Nicolas},
title = {Model Checking One-clock Priced Timed Automata},
volume = 4,
number = {2\string:9},
nopages = {},
month = jun,
year = 2008,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLM-lmcs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLM-lmcs08.pdf},
doi = {10.2168/LMCS-4(2:9)2008},
abstract = {We consider the model of priced (a.k.a.~weighted) timed automata, an
extension of timed automata with cost information on both locations and
transitions, and we study various model-checking problems for that model
based on extensions of classical temporal logics with cost constraints on
modalities. We prove that, under the assumption that the model has only one
clock, model-checking this class of models against the logic~WCTL, CTL
with cost-constrained modalities, is PSPACE-complete (while it has been
shown undecidable as soon as the model has three clocks).
We~also prove that model checking WMTL (LTL with cost-constrained
modalities) is decidable only if there is a single clock in the model and a
single stopwatch cost variable (\textit{i.e.}, whose slopes lie
in~\(\{0,1\}\)).}
}
@inproceedings{AFFM-wollic08,
address = {Edinburgh, Scotland, UK},
month = jul,
year = 2008,
volume = 5110,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hodges, Wilfrid and de Queiroz, Ruy},
acronym = {{WoLLIC}'08},
booktitle = {{P}roceedings of the 15th {W}orkshop on {L}ogic, {L}anguage,
{I}nformation and {C}omputation ({WoLLIC}'08)},
author = {Areces, Carlos and Figueira, Diego and Figueira, Santiago
and Mera, Sergio},
title = {Expressive Power and Decidability for Memory Logics},
pages = {56-68},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AFFM-wollic08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AFFM-wollic08.pdf},
doi = {10.1007/978-3-540-69937-8_7},
abstract = {Taking as inspiration the hybrid
logic~\(\mathcal{HL}(\downarrow)\), we~introduce a new family of logics
that we call memory logics. In~this article we~present in detail two
interesting members of this family defining their formal syntax and
semantics. We then introduce a proper notion of bisimulation and
investigate their expressive power (in comparison with modal and hybrid
logics). We~will prove that in terms of expressive power, the memory
logics we discuss in this paper are more expressive than orthodox modal
logic, but less expressive than~\(\mathcal{HL}(\downarrow)\). We~also
establish the undecidability of their satisfiability problems.}
}
@inproceedings{EF-lix06,
address = {Palaiseau, France},
month = apr,
year = 2008,
volume = 209,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Palamidessi, Catuscia and Valencia, Franck},
acronym = {{LIX}'06},
booktitle = {{P}roceedings of the {LIX} {C}olloquium on {E}merging
{T}rends in {C}oncurrency {T}heory
({LIX}'06)},
author = {Encrenaz, Emmanuelle and Fribourg, Laurent},
title = {Time Separation of Events: An Inverse Method},
pages = {135-148},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EF-lix06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EF-lix06.pdf},
doi = {10.1016/j.entcs.2008.04.008},
abstract = {The problem of {"}time separation{"} can be stated as follows:
Given a system made of several connected components, each
one entailing a local delay known with uncertainty, what is
the maximum time for traversing the global system? This
problem is useful, \textit{e.g.} in the domain of digital circuits,
for determining the global traversal time of a signal from
the knowledge of bounds on the component propagation delays.
The uncertainty on each component delay is given under the
form of an interval. The general problem is NP-complete. We
focus here on the inverse problem: we seek intervals for
component delays for which the global traversal time is
guaranteed to be no greater than a specified maximum. We
give a polynomial time method to solve it. As a typical
application, we show how to use the method in order to relax
some specified local delays while preserving the maximum
traversal time. This is especially useful, in the area of
digital circuits, for optimizing {"}setup{"} timings of input
signals (minimum timings required for stability).}
}
@article{LMO-lmcs08,
journal = {Logical Methods in Computer Science},
author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and Oreiby,
Ghassan},
title = {On the Expressiveness and Complexity of~{ATL}},
volume = {4},
number = {2\string:7},
month = may,
year = 2008,
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LMO-lmcs08.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LMO-lmcs08.pdf},
corrigendumpdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LMO-lmcs08-erratum.pdf},
doi = {10.2168/LMCS-4(2:7)2008},
abstract = {ATL is a temporal logic geared towards the specification and
verification of properties in multi-agents systems. It allows to reason on the
existence of strategies for coalitions of agents in order to enforce a given
property. We prove that the standard definition of~ATL (built on modalities
{"}Next{"}, {"}Always{"} and~{"}Until{"}) has to be completed in order to express the
duals of its modalities: it~is necessary to add the modality {"}Release{"}.
We~then precisely characterize the complexity of ATL model-checking when the
number of agents is not fixed. We prove that it is \(\Delta_{2}^{P}\) and
\(\Delta_{3}^{P}\)-complete, depending on the underlying multi-agent model
(ATS and CGS,~resp.). We also prove that~ATL\({}^{+}\) model-checking is
\(\Delta_{3}^{P}\)-complete over both models, even with a fixed number of
agents.}
}
@inproceedings{BJ-ijcar08,
address = {Sydney, Australia},
month = aug,
year = 2008,
volume = {5195},
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer-Verlag},
editor = {Armando, Alessandro and Baumgartner, Peter and
Dowek, Gilles},
acronym = {{IJCAR}'08},
booktitle = {{P}roceedings of the 4th {I}nternational {J}oint
{C}onference on {A}utomated {R}easoning
({IJCAR}'08)},
author = {Bouhoula, Adel and Jacquemard, Florent},
title = {Automated Induction with Constrained Tree Automata},
pages = {539-553},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BJ-ijcar08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BJ-ijcar08.pdf},
doi = {10.1007/978-3-540-71070-7_44},
abstract = {We propose a procedure for automated implicit inductive theorem
proving for equational specifications made of rewrite rules with
conditions and constraints. The constraints are interpreted over
constructor terms (representing data values), and may express syntactic
equality, disequality, ordering and also membership in a fixed tree
language. Constrained equational axioms between constructor terms are
supported and can be used in order to specify complex data structures like
sets, sorted lists, trees, powerlists...\par
Our procedure is based on tree grammars with constraints, a formalism
which can describe exactly the initial model of the given specification
(when it is sufficiently complete and terminating). They are used in the
inductive proofs first as an induction scheme for the generation of
subgoals at induction steps, second for checking validity and redundancy
criteria by reduction to an emptiness problem, and third for defining and
solving membership constraints.\par
We show that the procedure is sound and refutationally complete.
It~generalizes former test set induction techniques and yields natural
proofs for several non-trivial examples presented in the paper, these
examples are difficult (if not impossible) to specify and carry on
automatically with other induction procedures.}
}
@inproceedings{KMT-ijcar08,
address = {Sydney, Australia},
month = aug,
year = 2008,
volume = {5195},
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer-Verlag},
editor = {Armando, Alessandro and Baumgartner, Peter and
Dowek, Gilles},
acronym = {{IJCAR}'08},
booktitle = {{P}roceedings of the 4th {I}nternational {J}oint
{C}onference on {A}utomated {R}easoning
({IJCAR}'08)},
author = {Kremer, Steve and Mercier, Antoine and Treinen, Ralf},
title = {Proving Group Protocols Secure Against Eavesdroppers},
pages = {116-131},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KMT-ijcar08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KMT-ijcar08.pdf},
doi = {10.1007/978-3-540-71070-7_9},
abstract = {Security protocols are small programs
designed to ensure properties such as secrecy of messages
or authentication of parties in a hostile environment. In
this paper we investigate automated verification of a
particular type of security protocols, called \emph{group
protocols}, in the presence of an eavesdropper, i.e., a
passive attacker. The specificity of group protocols is
that the number of participants is not bounded.\par
Our approach consists in representing an infinite set of
messages exchanged during an unbounded number of sessions,
one session for each possible number of participants, as
well as the infinite set of associated secrets. We use
so-called visibly tree automata with memory and structural
constraints (introduced recently by Comon-Lundh
\textit{et~al.}) to represent over-approximations of these
two sets. We~identify restrictions on the specification of
protocols which allow us to reduce the attacker
capabilities guaranteeing that the above mentioned class of
automata is closed under the application of the remaining
attacker rules. The class of protocols respecting these
restrictions is large enough to cover several existing
protocols, such as the GDH family, GKE, and others.}
}
@inproceedings{BHHKT-wodes08,
address = {Gothenburg, Sweden},
month = may,
year = 2008,
acronym = {{WODES}'08},
booktitle = {{P}roceedings of the 9th {W}orkshop on {D}iscrete {E}vent {S}ystems
({WODES}'08)},
author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Hillah, Lom
Messan and Kordon, Fabrice and Thierry{-}Mieg, Yann},
title = {Collision Avoidance in Intelligent Transport Systems: Towards
an Application of Control Theory},
pages = {346-351},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHHKT-wodes08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHHKT-wodes08.pdf},
doi = {10.1109/WODES.2008.4605970},
abstract = {Safety is a prevalent issue in Intelligent Transport
Systems~(ITS). To~ensure such a vital requirement, methodologies must
offer support for the careful design and analysis of such systems. Indeed
these steps must cope with temporal and spatial constraints associated
with mobility rules and parallelism which induce a high complexity. Here
we handle the problem of unexpected and uncontrollable vehicles which
significantly endanger the traffic. In~this context, we~propose to apply
discrete control theory to a model of automatic motorway in order to
synthesize a controller that handles collision avoidance. This approach
includes two parts: the design of a formal model and an efficient
implementation based on hierarchical decision diagrams.}
}
@proceedings{CKR-dagstuhl07,
editor = {Chen, Liqun and Kremer, Steve and Ryan, Mark D.},
booktitle = {Formal Protocol Verification Applied},
title = {Formal Protocol Verification Applied},
year = 2008,
address = {Dagstuhl, Germany},
series = {Dagstuhl Seminar Proceedings},
volume = {07421},
url = {http://drops.dagstuhl.de/portals/index.php?semnr=07421}
}
@incollection{HM-mvrts08,
author = {Haddad, Serge and Moreaux, Patrice},
title = {Verification of Probabilistic Systems Methods and
Tools},
booktitle = {Modeling and Verification of Real-Time Systems},
editor = {Merz, Stephan and Navet, Nicolas},
year = {2008},
month = jan,
pages = {289-318},
publisher = {ISTE Ltd. -- John Wiley \& Sons, Ltd.},
url = {http://www.lavoisier.fr/notice/fr1848210130.html}
}
@inproceedings{BS-icalp08,
address = {Reykjavik, Iceland},
month = jul,
year = 2008,
volume = 5126,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Aceto, Luca and Damg{\aa}rd, Ivan and
Goldberg, Leslie~Ann and Halld{\'o}rsson, Magn{\'u}s M.
and Ing{\'o}lfsd{\'o}ttir, Anna and Walukiewicz, Igor},
acronym = {{ICALP}'08},
booktitle = {{P}roceedings of the 35th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'08)~-- {P}art~{II}},
author = {Boja{\'n}czyk, Miko{\l}aj and Segoufin, Luc},
title = {Tree languages defined in first-order logic with one quantifier alternation},
pages = {233-245},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BS-icalp08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BS-icalp08.pdf},
doi = {10.1007/978-3-540-70583-3_20},
abstract = {We study tree languages that can be defined in
\(\Delta_{2}\). These are tree languages definable by a
first-order formula whose quantifier prefix
is~\(\exists^{*}\forall^{*}\), and simultaneously by a
first-order formula whose quantifier prefix
is~\(\forall^{*}\exists^{*}\), both formulas over the
signature with the descendant relation. We~provide an
effective characterization of tree languages definable
in~\(\Delta_{2}\). This characterization is in terms of
algebraic equations. Over words, the class of word languages
definable in~\(\Delta_{2}\) forms a robust class, which was
given an effective algebraic characterization by Pin and
Weil.}
}
@inproceedings{BMOW-icalp08,
address = {Reykjavik, Iceland},
month = jul,
year = 2008,
volume = 5126,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Aceto, Luca and Damg{\aa}rd, Ivan and
Goldberg, Leslie~Ann and Halld{\'o}rsson, Magn{\'u}s M.
and Ing{\'o}lfsd{\'o}ttir, Anna and Walukiewicz, Igor},
acronym = {{ICALP}'08},
booktitle = {{P}roceedings of the 35th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'08)~-- {P}art~{II}},
author = {Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo{\"e}l
and Worrell, James},
title = {On Expressiveness and Complexity in Real-time Model Checking},
pages = {124-135},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMOW-icalp08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMOW-icalp08.pdf},
doi = {10.1007/978-3-540-70583-3_11},
abstract = {Metric Interval Temporal Logic (MITL) is a popular formalism for
expressing real-time specifications. This logic achieves decidability by
restricting the precision of timing constraints, in particular, by banning
so-called \emph{punctual} specifications. In~this paper we~introduce a
significantly more expressive logic that can express a wide variety of
punctual specifications, but whose model-checking problem has the same
complexity as that of~MITL. We~conclude that for model checking the most
commonly occurring specifications, such as invariance and bounded
response, punctuality can be accommodated at no cost.}
}
@techreport{LSV:08:10,
author = {Villard, Jules and Lozes, {\'E}tienne and Treinen, Ralf},
title = {A Spatial Equational Logic for the Applied pi-calculus},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = 2008,
month = mar,
type = {Research Report},
number = {LSV-08-10},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-10.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-10.pdf},
note = {44~pages},
abstract = {Spatial logics have been proposed to reason locally and
modularly on algebraic models of distributed systems. In~this paper
we~investigate a spatial equational logic (A\(\pi\)L) whose models are
processes of the applied \(\pi\)-calculus, an extension of the
\(\pi\)-calculus allowing term manipulation modulo a predefined
equational theory, and wherein communications are recorded as active
substitutions in a frame. Our logic allows us to reason locally either on
frames or on processes, thanks to static and dynamic spatial operators.
We study the logical equivalences induced by various relevant fragments
of~A\(\pi\)L, and show in particular that the whole logic induces a coarser
equivalence than structural congruence. We give characteristic formulae
for this new equivalence as well as for static equivalence on frames.
Going further into the exploration of A\(\pi\)L's expressivity, we also show
that it can eliminate standard term quantication, and that the
model-checking problem for the adjunct-free fragment of A\(\pi\)L can be
reduced to satisfiability of a purely first-order logic of a term
algebra.}
}
@inproceedings{JGL:badweeds,
address = {Budapest, Hungary},
month = mar,
year = 2008,
volume = 5289,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Leucker, Martin},
acronym = {{RV}'08},
booktitle = {{P}roceedings of the 8th {W}orkshop on {R}untime {V}erification ({RV}'08)},
author = {Goubault{-}Larrecq, Jean and Olivain, Julien},
title = {A Smell of Orchids},
pages = {1-20},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/go-rv08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/go-rv08.pdf},
doi = {10.1007/978-3-540-89247-2_1},
abstract = {Orchids is an intrusion detection tool based on techniques for
fast, on-line model-checking. Orchids detects complex, correlated strands
of events with very low overhead in practice, although its detec- tion
algorithm has worst-case exponential time complexity.\par
The purpose of this paper is twofold. First, we explain the salient
features of the basic model-checking algorithm in an intuitive way, as a
form of dynamically-spawned monitors. One distinctive feature of the
Orchids algorithm is that fresh monitors need to be spawned at a pos-
sibly alarming rate.\par
The second goal of this paper is therefore to explain how we tame the
complexity of the procedure, using abstract interpretation techniques to
safely kill useless monitors. This includes monitors which will provably
detect nothing, but also monitors that are subsumed by others, in the
sense that they will definitely fail the so-called shortest run criterion.
We take the opportunity to show how the Orchids algorithm maintains its
monitors sorted in such a way that the subsumption operation is effected
with no overhead, and we correct a small, but definitely annoying bug in
its core algorithm, as it was published in~2001.}
}
@article{BCHLR08-tcs,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {B{\'e}rard, B{\'e}atrice and Cassez, Franck and Haddad,
Serge and Lime, Didier and Roux, Olivier H.},
title = {When are Timed Automata Weakly Timed Bisimilar to Time
{P}etri Nets?},
year = 2008,
month = sep,
volume = 403,
number = {2-3},
pages = {202-220},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHLR-tcs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHLR-tcs08.pdf},
doi = {10.1016/j.tcs.2008.03.030},
abstract = {In this paper, we compare Timed Automata~(TA) and Time Petri
Nets~(TPN) with respect to weak timed bisimilarity. It~is already known
that the class of bounded TPNs is strictly included in the class of~TA.
It~is thus natural to try and identify the
subclass~\(\mathcal{TA}^{\textit{wtb}}\) of~TA equivalent to some TPN for
the weak timed bisimulation relation. We~give a characterization of this
subclass and we show that the membership problem and the reachability
problem for \(\mathcal{TA}^{\textit{wtb}}\) are PSPACE-complete.
Furthermore we show that for a TA in~\(\mathcal{TA}^{\textit{wtb}}\) with
integer constants, an~equivalent TPN can be built with integer bounds but
with a size exponential w.r.t.~the original model. Surprisingly, using
rational bounds yields a TPN whose size is linear.}
}
@inproceedings{JGL-csf08,
address = {Pittsburgh, Pennsylvania, USA},
month = jun,
year = 2008,
publisher = {{IEEE} Computer Society Press},
acronym = {{CSF}'08},
booktitle = {{P}roceedings of the
21st {IEEE} {C}omputer {S}ecurity {F}oundations
{S}ymposium ({CSF}'08)},
author = {Goubault{-}Larrecq, Jean},
title = {Towards Producing Formally Checkable Security Proofs, Automatically},
pages = {224-238},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-15.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-15.pdf},
doi = {10.1109/CSF.2008.21},
abstract = {First-order logic models of security for cryptographic protocols,
based on variants of the Dolev-Yao model, are now well-established
tools. Given that we have checked a given security protocol~\(\pi\)
using a given first-order prover, how hard is it to extract a
formally checkable proof of~it, as~required in, e.g., common
criteria at evaluation level~\(7\)? We~demonstrate that this is
surprisingly hard: the problem is non-recursive in general.
On~the practical side, we show how we can extract finite models~\(\mathcal{M}\)
from a set~\(\mathcal{S}\) of clauses representing~\(\pi\),
automatically, in two ways. We~then define a model-checker
testing \(\mathcal{M} \models \mathcal{S}\), and show how we can instrument it
to output a formally checkable proof, e.g., in~Coq. This was
implemented in the \texttt{h1} tool suite. Experience on a number of
protocols shows that this is practical.}
}
@inproceedings{DKR-csf08,
address = {Pittsburgh, Pennsylvania, USA},
month = jun,
year = 2008,
publisher = {{IEEE} Computer Society Press},
acronym = {{CSF}'08},
booktitle = {{P}roceedings of the
21st {IEEE} {C}omputer {S}ecurity {F}oundations
{S}ymposium ({CSF}'08)},
author = {Delaune, St{\'e}phanie and Kremer, Steve and
Ryan, Mark D.},
title = {Composition of Password-based Protocols},
pages = {239-251},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-csf08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-csf08.pdf},
doi = {10.1109/CSF.2008.6},
abstract = {We investigate the composition of protocols that share a common
secret. This situation arises when users employ the same password
on different services. More precisely we study whether resistance
against guessing attacks composes when the same password is used.
We model guessing attacks using a common definition based on static
equivalence in a cryptographic process calculus close to the applied
pi calculus. We show that resistance against guessing attacks
composes in the presence of a passive attacker. However, composition
does not preserve resistance against guessing attacks for an active
attacker. We therefore propose a simple syntactic criterion under
which we show this composition to hold. Finally, we present a
protocol transformation that ensures this syntactic criterion and
preserves resistance against guessing attacks.}
}
@inproceedings{DKS-csf08,
address = {Pittsburgh, Pennsylvania, USA},
month = jun,
year = 2008,
publisher = {{IEEE} Computer Society Press},
acronym = {{CSF}'08},
booktitle = {{P}roceedings of the
21st {IEEE} {C}omputer {S}ecurity {F}oundations
{S}ymposium ({CSF}'08)},
author = {Delaune, St{\'e}phanie and Kremer, Steve and
Steel, Graham},
title = {Formal Analysis of {PKCS}\#11},
pages = {331-344},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKS-csf08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKS-csf08.pdf},
doi = {10.1109/CSF.2008.16},
abstract = {PKCS\#11 defines an API for cryptographic devices that has
been widely adopted in industry. However, it~has been shown to be
vulnerable to a variety of attacks that could, for example, compromise
the sensitive keys stored on the device. In~this paper, we~set out a
formal model of the operation of the API, which differs from previous
security API models notably in that it accounts for non-monotonic
mutable global state. We~give decidability results for our formalism,
and describe an implementation of the resulting decision procedure
using a model checker. We~report some new attacks and prove the safety
of some configurations of the API in our model.}
}
@techreport{LSV:08:08,
author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me},
title = {Presburger Functions are Piecewise Linear},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = 2008,
month = mar,
type = {Research Report},
number = {LSV-08-08},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-08.pdf},
note = {9~pages},
abstract = {In this paper we geometrically characterize sets and functions
definable in the first order additive theory of the reals and the
integers, a decidable extension of the Presburger arithmetic combining
both integral and real variables. We introduce the notion of polinear
sets, an extension of the linear sets that characterizes these sets and we
prove that a function is definable in this logic if and only if it is
piecewise rational linear.}
}
@inproceedings{BSS-lics08,
address = {Pittsburgh, Pennsylvania, USA},
month = jun,
year = 2008,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'08},
booktitle = {{P}roceedings of the 23rd
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'08)},
author = {Boja{\'n}czyk, Miko{\l}aj and Segoufin, Luc and Straubing, Howard},
title = {Piecewise Testable Tree Languages},
pages = {442-451},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BSS-lics08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BSS-lics08.pdf},
doi = {10.1109/LICS.2008.46},
abstract = {This paper presents a decidable characterization of tree
languages that can be defined by a boolean combination of \(\Sigma_{1}\)
formulas. This is a tree extension of the Simon theorem, which says that a
string language can be defined by a boolean combination of \(\Sigma_{1}\)
formulas if and only if its syntactic monoid is \(J\)-trivial. }
}
@inproceedings{CS-lics08,
address = {Pittsburgh, Pennsylvania, USA},
month = jun,
year = 2008,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'08},
booktitle = {{P}roceedings of the 23rd
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'08)},
author = {Chambart, Pierre and Schnoebelen, {\relax Ph}ilippe},
title = {The Ordinal Recursive Complexity of Lossy Channel Systems},
pages = {205-216},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-lics08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-lics08.pdf},
doi = {10.1109/LICS.2008.47},
abstract = {We show that reachability and termination for lossy channel
systems is exactly at level \(\mathcal{F}_{\omega^{\omega}}\) in the
Fast-Growing Hierarchy of recursive functions, the first level that
dominates all multiply-recursive functions.}
}
@inproceedings{BBBBG-lics08,
address = {Pittsburgh, Pennsylvania, USA},
month = jun,
year = 2008,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'08},
booktitle = {{P}roceedings of the 23rd
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'08)},
author = {Baier, Christel and Bertrand, Nathalie and Bouyer,
Patricia and Brihaye, {\relax Th}omas and Gr{\"o}{\ss}er, Marcus},
title = {Almost-Sure Model Checking of Infinite Paths in One-Clock
Timed Automata},
pages = {217-226},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBBG-lics08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBBG-lics08.pdf},
doi = {10.1109/LICS.2008.25},
abstract = { In this paper, we~define two relaxed semantics (one based
on probabilities and the other one based on the topological notion of
largeness) for LTL over infinite runs of timed automata which rule out
unlikely sequences of events. We~prove that these two semantics match in
the framework of single-clock timed automata (and~only in that framework),
and prove that the corresponding relaxed model-checking problems are
PSPACE-Complete. Moreover, we~prove that the probabilistic non-Zenoness
can be decided for single-clock timed automata in NLOGSPACE.}
}
@inproceedings{DKS-TFIT2008,
address = {Taipei, Taiwan},
month = mar,
year = 2008,
editor = {Kuo, Tei-Wei and Cruz-Lara, Samuel},
acronym = {{TFIT}'08},
booktitle = {{P}roceedings of the 4th {T}aiwanese-{F}rench
{C}onference on {I}nformation {T}echnology ({TFIT}'08)},
author = {Delaune, St{\'e}phanie and Kremer, Steve and
Steel, Graham},
title = {Formal Analysis of {PKCS}\#11},
pages = {267-278},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKS-tfit08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKS-tfit08.pdf},
abstract = {PKCS\#11 defines an API for cryptographic devices that has been
widely adopted in industry. However, it~has been shown to be vulnerable to
a variety of attacks that could, for~example, compromise the sensitive
keys stored on the device. In~this paper, we~set out a formal model of the
operation of the API, which differs from previous security API models
notably in that it accounts for non-monotonic mutable global state. We
give decidability results for our formalism, and describe an
implementation of the resulting decision procedure using a model checker.
We report some new attacks and prove the safety of some configurations of
the API in our model.}
}
@inproceedings{poti-TFIT2008,
address = {Taipei, Taiwan},
month = mar,
year = 2008,
editor = {Kuo, Tei-Wei and Cruz-Lara, Samuel},
acronym = {{TFIT}'08},
booktitle = {{P}roceedings of the 4th {T}aiwanese-{F}rench
{C}onference on {I}nformation {T}echnology ({TFIT}'08)},
author = {Bouyer, Patricia},
title = {Model-Checking Timed Temporal Logics},
pages = {132-142},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bouyer-tfit08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bouyer-tfit08.pdf},
abstract = {In this paper, we~present several timed extensions of
temporal logics, that can be used for model-checking real-time
systems. We~give different formalisms and the corresponding
decidability\slash complexity results. We also give intuition
to explain these results.}
}
@inproceedings{DRS-ifiptm08,
address = {Trondheim, Norway},
month = jun,
year = 2008,
volume = 263,
series = {IFIP Conference Proceedings},
publisher = {Springer},
editor = {Karabulut, Yuecel and Mitchell, John and Herrmann, Peter and
Jensen, Christian Damsgaard},
acronym = {IFIPTM'08},
booktitle = {{P}roceedings of the 2nd {J}oint i{T}rust and {PST}
{C}onferences on {P}rivacy, {T}rust {M}anagement and
{S}ecurity (IFIPTM'08)},
author = {Delaune, St{\'e}phanie and Ryan, Mark D. and Smyth, Ben},
title = {Automatic verification of privacy properties in the applied pi-calculus},
pages = {263-278},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DRS-ifiptm08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DRS-ifiptm08.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DRS-ifiptm08.ps},
abstract = {We develop a formal method verification technique for
cryptographic protocols. We~focus on proving observational equivalences of
the kind \(P \sim Q\), where the processes \(P\) and~\(Q\) have the same
structure and differ only in the choice of terms. The calculus of
ProVerif, a variant of the applied pi-calculus, makes some progress in
this direction. We~expand the scope of ProVerif, to provide reasoning
about further equivalences. We~also provide an extension which allows
modelling of protocols which require global synchronisation. Finally we
develop an algorithm to enable automated reasoning.\par
We demonstrate the practicality of our work with two case studies.}
}
@inproceedings{BFL-time08,
address = {Montr{\'e}al, Canada},
month = jun,
year = 2008,
publisher = {{IEEE} Computer Society Press},
noeditor = {Demri, St{\'e}phane and Jensen, {\relax Ch}ristian S.},
acronym = {{TIME}'08},
booktitle = {{P}roceedings of the 15th {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'08)},
author = {Bouchy, Florent and Finkel, Alain and Leroux, J{\'e}r{\^o}me},
title = {Decomposition of Decidable First-Order Logics over Integers
and Reals},
pages = {147-155},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFL-time08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFL-time08.pdf},
doi = {10.1109/TIME.2008.22},
abstract = {We tackle the issue of representing infinite sets of realvalued
vectors. This paper introduces an operator for combining
integer and real sets. Using this operator, we~decompose
three well-known logics extending Presburger with reals. Our
decomposition splits the logic into two parts: one~integer,
and one decimal (\textit{i.e.},~on the interval~\([0,1[\)).
We~also give some basis for an implementation of our
representation.}
}
@inproceedings{Bur-wistp08,
address = {Sevilla, Spain},
month = may,
year = 2008,
volume = 5019,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Onieva, Jose A. and Sauveron, Damien and
Chaumette, Serge and Gollmann, Dieter and
Markantonakis, Konstantinos},
acronym = {{WISTP}'08},
booktitle = {{P}roceedings of the
2nd {I}nternational {W}orkshop
on {I}nformation {S}ecurity {T}heory and {P}ractices
({WISTP}'08)},
author = {Bursztein, Elie},
title = {Probabilistic Protocol Identification for Hard to Classify Protocol},
pages = {49-63},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bur-wistp08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bur-wistp08.pdf},
doi = {10.1007/978-3-540-79966-5_4},
note = {Best paper award},
abstract = {With the growing use of protocols obfuscation techniques,
protocol identification for Q.O.S enforcement, traffic prohibition, and
intrusion detection has became a complex task. This paper address this
issue with a probabilistic identification analysis that combines multiples
advanced identification techniques and returns an ordered list of probable
protocols. It~combines a payload analysis with a classifier based on
several discriminators, including packet entropy and size. We~show with
its implementation, that it overcomes the limitations of traditional
port-based protocol identification when dealing with hard to classify
protocol such as peer to peer protocols. We also details how it deals with
tunneled session and covert channel.}
}
@inproceedings{BGMR-time08,
address = {Montr{\'e}al, Canada},
month = jun,
year = 2008,
publisher = {{IEEE} Computer Society Press},
noeditor = {Demri, St{\'e}phane and Jensen, {\relax Ch}ristian S.},
acronym = {{TIME}'08},
booktitle = {{P}roceedings of the 15th {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'08)},
author = {Brihaye, {\relax Th}omas and Ghannem, Mohamed and Markey,
Nicolas and Rieg, Lionel},
title = {Good friends are hard to find!},
pages = {32-40},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGMR-time08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGMR-time08.pdf},
doi = {10.1109/TIME.2008.10},
abstract = {We focus on the problem of finding (the~size of) a~minimal
winning coalition in a multi-player game. More precisely, we~prove that
deciding whether there is a winning coalition of size at most~\(k\) is
NP-complete, while deciding whether \(k\) is the optimal size is
DP-complete. We~also study different variants of our original problem: the
function problem, where the aim is to effectively compute the coalition;
more succinct encoding of the game; and richer families of winning
objectives.}
}
@article{DGK-ijfcs08,
publisher = {World Scientific},
journal = {International Journal of Foundations of Computer Science},
author = {Diekert, Volker and Gastin, Paul and Kufleitner,
Manfred},
title = {A Survey on Small Fragments of First-Order Logic over
Finite Words},
volume = 19,
number = 3,
pages = {513-548},
year = 2008,
month = jun,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DGK-ijfcs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DGK-ijfcs08.pdf},
doi = {10.1142/S0129054108005802},
abstract = {We consider fragments of first-order logic over finite
words. In~particular, we~deal with
first-order logic with a restricted number of
variables and with the lower levels of the
alternation hierarchy. We~use the algebraic
approach to show decidability of
expressibility within these fragments. As~a
byproduct, we~survey several characterizations
of the respective fragments. We~give complete
proofs for all characterizations and we
provide all necessary background. Some of the
proofs seem to be new and simpler than those
which can be found elsewhere. We also give a
proof of Simon's theorem on factorization
forests restricted to aperiodic monoids
because this is simpler and sufficient for our
purpose.}
}
@techreport{LSV:08:02,
author = {Bursztein, Elie},
title = {Network Administrator and Intruder Strategies},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = 2008,
month = feb,
type = {Research Report},
number = {LSV-08-02},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-02.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-02.pdf},
note = {23~pages},
abstract = {The anticipation game framework is an
extension of attack graphs based on game theory. It
is used to anticipate and analyze intruder and
administrator interactions with the network. In this
paper we extend this framework with cost and reward
in order to analyze and find player strategies.
Additionally this extension allows to take into
account the financial aspect of network security in
the analysis. Intuitively a strategy is the best
succession of actions that the administrator or the
intruder can perform to achieve his objectives.
Player objectives range from patching the network
efficiently to compromising the most valuable
network assets. We prove that finding the optimal
strategy is decidable and only requires a linear
memory space. Finally we show that finding strategy
can be done in practice by evaluating the
performance of our analyzer called NetQi.}
}
@article{BFLP-sttt08,
publisher = {Springer},
journal = {International Journal on Software Tools
for Technology Transfer},
author = {Bardin, S{\'e}bastien and Finkel, Alain and
Leroux, J{\'e}r{\^o}me and Petrucci, Laure},
title = {{FAST}: Acceleration from theory to practice},
year = 2008,
month = oct,
volume = 10,
number = 5,
pages = {401-424},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-16.pdf},
doi = {10.1007/s10009-008-0064-3},
abstract = {Fast acceleration of symbolic transition
systems~(\textsc{Fast}) is a tool for the
analysis of systems manipulating unbounded integer variables. We~check
safety properties by
computing the reachability set of the system under study. Even if this
reachability set is not
necessarily recursive, we~use innovative techniques, namely symbolic
representation, acceleration and circuit selection, to~increase
convergence. \textsc{Fast} has proved to perform very well on case
studies. This~paper describes the tool, from the underlying theory to
the architecture choices. Finally, \textsc{Fast} capabilities are
compared with those of other tools. A~range of case studies from the
literature is investigated.}
}
@incollection{BL-litron08,
author = {Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois},
title = {Model Checking Timed Automata},
booktitle = {Modeling and Verification of Real-Time Systems},
editor = {Merz, Stephan and Navet, Nicolas},
year = {2008},
month = jan,
pages = {111-140},
publisher = {ISTE Ltd. -- John Wiley \& Sons, Ltd.},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BL-litron08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BL-litron08.pdf}
}
@article{PPSLBCH-commag08,
publisher = {{IEEE} Communications Society},
journal = {IEEE Communications Magazine},
author = {Papadimitratos, Panos and Poturalski, Marcin and Schaller,
Patrick and Lafourcade, Pascal and Basin, David and
{\v{C}}apkun, Srdjan and Hubaux, Jean-Pierre},
title = {Secure Neighborhood Discovery: A~Fundamental
Element for Mobile Ad Hoc Networking},
year = 2008,
month = feb,
volume = 46,
number = 2,
pages = {132-139},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PPSLBCH-commag08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PPSLBCH-commag08.pdf},
doi = {10.1109/MCOM.2008.4473095},
abstract = {Pervasive computing systems will likely be deployed in the near
future, with the proliferation of wireless devices and the emergence of ad
hoc networking as key enablers. Coping with mobility and the volatility of
wireless communications in such systems is critical. Neighborhood
Discovery~(ND), namely, the discovery of devices directly reachable for
communication or in physical proximity, becomes a fundamental requirement
and a building block for various applications. However, the very nature of
wireless mobile networks makes it easy to abuse ND and thereby compromise
the overlying protocols and applications. Thus, providing methods to
mitigate this vulnerability and to secure ND is crucial. In~this article,
we~focus on this problem and provide definitions of neighborhood types and
ND protocol properties, as well as a broad classification of attacks. Our
ND literature survey reveals that securing ND is indeed a difficult and
largely open problem. Moreover, given the severity of the problem, we
advocate the need to formally model neighborhood and to analyze ND
schemes.}
}
@article{BK-IC08,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Bollig, Benedikt and Kuske, Dietrich},
title = {{M}uller Message-Passing Automata and Logics},
volume = 206,
number = {9-10},
pages = {1084-1094},
year = 2008,
month = sep # {-} # oct,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BK-IC08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BK-IC08.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BK-IC08.ps},
doi = {10.1016/j.ic.2008.03.010},
abstract = {We study nonterminating message-passing automata whose behavior
is described by infinite message sequence charts. As~a first result, we~show
that Muller, B{\"u}chi, and termination-detecting Muller acceptance are
equivalent for these devices. To~describe the expressive power of these
automata, we give a logical characterization. More precisely, 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. This result is based
on Vinner's extension of the classical Ehrenfeucht-Fra{\"\i}ss{\'e} game to
cope with the infinity quantifier.}
}
@misc{netanalyser-v0.7.5,
author = {Bursztein, Elie},
title = {NetAnalyzer~v0.7.5},
year = {2008},
month = jan,
nohowpublished = {Available at .... },
note = {Written in~C and Perl (about 25000 lines)},
note-fr = {\'Ecrit en~C et en Perl (environ 25000 lignes)}
}
@incollection{DiGa08Thomas,
author = {Diekert, Volker and Gastin, Paul},
title = {First-order definable languages},
booktitle = {Logic and Automata: History and Perspectives},
editor = {Flum, J{\"o}rg and Gr{\"a}del, Erich and Wilke, Thomas},
publisher = {Amsterdam University Press},
series = {Texts in Logic and Games},
volume = 2,
year = 2008,
pages = {261-306},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-WT08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-WT08.pdf},
abstract = {We give an essentially self-contained presentation of some principal
results for first-order definable languages over finite and infinite
words. We~introduce the notion of a \emph{counter-free} B{\"u}chi
automaton; and we relate counter-freeness to \emph{aperiodicity}
and to the notion of \emph{very weak alternation}.
We also show that aperiodicity of a regular
\(\infty\)-language can be decided in polynomial
space, if the language is specified by some B{\"u}chi automaton.}
}
@inproceedings{HMY-csndsp08,
address = {Graz, Austria},
month = jul,
year = 2008,
publisher = {{IEEE} Computer Society Press},
noeditor = {},
acronym = {{CSNDSP}'08},
booktitle = {{P}roceedings of the 6th {S}ymposium on {C}ommunication {S}ystems,
{N}etworks and {D}igital {S}ignal {P}rocessing
({CSNDSP}'08)},
author = {Haddad, Serge and Mokdad, Lynda and Youcef, Samir},
title = {Response Time Analysis of Composite Web Services},
pages = {506-510},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HMY-csndsp08.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HMY-csndsp08.pdf},
abstract = {Service Oriented Computing (SOC) strives for applications with
services as the fundamental items of design, and Web services acting as
the enabling technology. Web services use open XML-based standards and are
becoming the most important technology for communication between
heterogenous business applications over Internet. In this paper, we focus
on mean response times. Thus we propose analytical formulas for mean
response times for structured BPEL constructors such as sequence, flow and
switch. We propose also a response time formula for multi-choice pattern
which is a generalization of switch constructor. Contrarily to previous
studies in the literature, we consider that the servers can be
heterogenous and the number of invoked elementary Web services can be
variable.}
}
@article{RBHJ-tsc08,
publisher = {{IEEE} Computer Society Press},
journal = {IEEE Transactions on Services Computing},
author = {Rosario, Sidney and Benveniste, Albert and Haar, Stefan and
Jard, Claude},
title = {Probabilistic {Q}o{S} and Soft Contracts for
Transaction-Based Web Services Orchestrations},
pages = {187-200},
volume = 1,
number = 4,
month = oct # {-} # dec,
year = 2008,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/RBHJ-tsc08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/RBHJ-tsc08.pdf},
doi = {10.1109/TSC.2008.17},
abstract = {Service level agreements (SLAs), or contracts, have an
important role in web services. They define the obligations
and rights between the provider of a web service and its
client, about the function and the Quality of the service
(QoS). For composite services like orchestrations, contracts
are deduced by a process called QoS contract composition,
based on contracts established between the orchestration and
the called web services. Contracts are typically stated as
hard guarantees (e.g., response time always less than 5
msec). Using hard bounds is not realistic, however, and more
statistical approaches are needed. In this paper we propose
using soft probabilistic contracts instead, which consist of
a probability distribution for the considered QoS
parameter---in this paper, we focus on timing. We show how to
compose such contracts, to yield a global probabilistic
contract for the orchestration. Our approach is implemented
by the TOrQuE tool. Experiments on TOrQuE show that overly
pessimistic contracts can be avoided and significant room
for safe overbooking exists. An essential component of SLA
management is then the continuous monitoring of the
performance of called web services, to check for violations
of the SLA. We propose a statistical technique for run-time
monitoring of soft contracts.}
}
@article{BHK-njc09,
journal = {Nordic Journal of Computing},
author = {Boichut, Yohan and H{\'e}am, Pierre-Cyrille and Kouchnarenko,
Olga},
title = {Approximation-based Tree Regular Model-Checking},
volume = {14},
number = {3},
pages = {216-241},
month = oct,
year = 2008,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHK-njc09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHK-njc09.pdf},
abstract = {This paper addresses the following general problem of tree
regular model-checking: decide whether \(\mathcal{R}^*(L)\cap L_{p} =
\varnothing\) where \(\mathcal{R}^*\) is the reflexive and transitive
closure of a successor relation induced by a term rewriting
system~\(\mathcal{R}\), and \(L\) and \(L_p\) are both regular tree
languages. We develop an automatic approximation-based technique to handle
this---undecidable in general---problem in most practical cases, extending
a recent work by Feuillade, Genet and Viet~Triem~Tong. We also make this
approach fully automatic for practical validation of security protocols.}
}
@article{LHS-lmcs08,
journal = {Logical Methods in Computer Science},
author = {Lozes, {\'E}tienne and Hirschkoff, Daniel and
Sangiorgi, Davide},
title = {Separability in the Ambient Logic},
volume = 4,
number = {3:4},
year = 2008,
month = sep,
nopages = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LHS-lmcs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LHS-lmcs08.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LHS-lmcs08.ps},
doi = {10.2168/LMCS-4(3:4)2008},
abstract = {The Ambient Logic~(AL) has been proposed for expressing
properties of process mobility in the calculus of Mobile
Ambients~(MA), and as a basis for query languages on
semistructured data. \par
We study some basic questions concerning the
discriminating power of~AL, focusing on the equivalence on
processes induced by the logic~(\(=_{L}\)). As underlying
calculi besides~MA we~consider a subcalculus in which an
image-finiteness condition holds and that we prove to be
Turing complete. Synchronous variants of these calculi are
studied as well. \par
In these calculi, we provide two operational
characterisations of~\(=_{L}\): a~coinductive one (as a form
of bisimilarity) and an inductive one (based on structual
properties of processes). After showing \(=_{L}\) to be
stricly finer than barbed congruence, we establish
axiomatisations of~\(=_{L}\) on the subcalculus of~MA (both
the asynchronous and the synchronous version), enabling us
to relate~\(=_{L}\) to structural congruence. We~also
present some (un)decidability results that are related to
the above separation properties for~AL: the~undecidability
of~\(=_{L}\) on~MA and its decidability on the
subcalculus.}
}
@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.