@inproceedings{FLS-ilc07,
address = {Cape Town, South Africa},
month = oct,
year = 2009,
volume = 5489,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer-Verlag},
editor = {Archibald, Margaret and Brattka, Vasco and
Goranko, Valentin and L{\"o}we, Benedikt},
acronym = {{ILC}'07},
booktitle = {{R}evised {S}elected {P}apers of the
{I}nternational {C}onference on {I}nfinity
in {L}ogic {\&} {C}omputation ({ILC}'07)},
author = {Finkel, Alain and Lozes, {\'E}tienne and Sangnier, Arnaud},
title = {Towards Model Checking Pointer Systems},
pages = {56-82},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FLS-ilc07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FLS-ilc07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FLS-ilc07.ps},
doi = {10.1007/978-3-642-03092-5_6},
abstract = {We aim at checking safety and temporal properties over models
representing the behavior of programs manipulating dynamic singly-linked
lists. The properties we consider not only allow to perform a classical
shape analysis, but we also want to check quantitative aspect on the
manipulated memory heap. We first explain how a translation of programs
into counter systems can be used to check safety problems and temporal
properties. We then study the decidability of these two problems
considering some restricted classes of programs, namely flat programs
without destructive update. We obtain the following results: (1)~the
model-checking problem is decidable if the considered program works over
acyclic lists; (2)~the safety problem is decidable for programs without
alias test. We finally explain the limit of our decidability results,
showing that relaxing one of the hypothesis leads to undecidability
results.}
}
@article{CEFX-fmsd08,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Chevallier, R{\'e}my and Encrenaz{-}Tiph{\`e}ne, Emmanuelle and
Fribourg, Laurent and Xu, Weiwen},
title = {Timed Verification of the Generic Architecture of a Memory
Circuit Using Parametric Timed Automata},
volume = 34,
number = 1,
pages = {59-81},
year = 2009,
month = feb,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-fmsd08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-fmsd08.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CEFX-fmsd08.ps},
doi = {10.1007/s10703-008-0061-x},
abstract = {Using a variant of Clariso-Cortadella's parametric
method for verifying asynchronous circuits, we analyse some crucial timing
behaviors of the architecture of SPSMALL memory, a~commercial product of
STMicroelectronics. Using the model of parametric timed automata and model
checker HYTECH, we~formally derive a set of linear constraints that ensure
the correctness of the response times of the memory. We are also able to
infer the constraints characterizing the optimal setup timings of input
signals. We have checked, for two different implementations of this
architecture, that the values given by our model match remarkably with the
values obtained by the designer through electrical simulation. }
}
@inproceedings{EF-infinity07,
optaddress = {Lisbon, Portugal},
month = jul,
year = 2009,
volume = 239,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
realeditor = {Madhusudan, P. and Kahlon, Vineet},
editor = {Habermehl, Peter and Vojnar, Tom{\'a}{\v{s}}},
acronym = {{INFINITY}'06,'07,'08},
booktitle = {{J}oint {P}roceedings of the 8th, 9th and 10th {I}nternational
{W}orkshops on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'06,'07,'08)},
author = {Encrenaz, Emmanuelle and Finkel, Alain},
title = {Automatic verification of counter systems with ranking functions},
pages = {85-103},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EF-infinity07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EF-infinity07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/EF-infinity07.ps},
doi = {10.1016/j.entcs.2009.05.032},
abstract = {The verification of final termination for counter systems is
undecidable. For non flattable counter systems, the verification of this
type of property is generally based on the exhibition of a ranking
function. Proving the existence of a ranking function for general counter
systems is also undecidable. We~provide a framework in which the
verification whether a given function is a ranking function is decidable.
This framework is applicable to convex counter systems which admit a
Presburger or a LPDS ranking function. This extends the results of
[A.~Bradley, Z.~Manna, and B.~Sipma. \textit{Termination analysis of
integer linear loops}. In~CONCUR'05, LNCS~3653, p.~488-502. Springer].
From this framework, we derive a model-checking algorithm to verify
whether a final termination property is satisfied or not. This approach
has been successfully applied to the verification of a parametric version
of the ZCSP protocol.}
}
@inproceedings{Bouyer-M4M5,
address = {Cachan, France},
month = mar,
year = 2009,
volume = 231,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Areces, Carlos and Demri, St{\'e}phane},
acronym = {{M4M-5}},
booktitle = {{P}roceedings of the 4th
{W}orkshop on {M}ethods for {M}odalities
({M4M-5})},
author = {Bouyer, Patricia},
title = {Model-Checking Timed Temporal Logics},
pages = {323-341},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-M4M5.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-M4M5.pdf},
doi = {10.1016/j.entcs.2009.02.044},
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/complexity results. We also give intuition to
explain these results.}
}
@proceedings{M4M5-AD,
editor = {Areces, Carlos and Demri, St{\'e}phane},
title = {{P}roceedings of the 5th {I}nternational {W}orkshop on
{M}ethods for {M}odalities ({M4M-5})},
booktitle = {{P}roceedings of the 5th {I}nternational {W}orkshop on
{M}ethods for {M}odalities ({M4M-5})},
publisher = {Elsevier Science Publishers},
series = {Electronic Notes in Theoretical Computer Science},
volume = 231,
year = 2009,
month = mar,
address = {Cachan, France},
url = {http://www.sciencedirect.com/science/journal/15710661/231},
doi = {10.1016/j.entcs.2009.02.025}
}
@article{CD-fmsd08,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
title = {Safely Composing Security Protocols},
volume = 34,
number = 1,
pages = {1-36},
month = feb,
year = 2009,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CD-fmsd08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CD-fmsd08.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CD-fmsd08.ps},
doi = {10.1007/s10703-008-0059-4},
abstract = {Security protocols are small programs that are executed in
hostile environments. Many results and tools have been developed to
formally analyze the security of a protocol in the presence of an active
attacker that may block, intercept and send new messages. However even
when a protocol has been proved secure, there is absolutely no guarantee
if the protocol is executed in an environment where other protocols are
executed, possibly sharing some common keys like public keys or long-term
symmetric keys.\par
In this paper, we show that security of protocols can be easily composed.
More precisely, we show that whenever a protocol is secure, it remains
secure even in an environment where arbitrary protocols satisfying a
reasonable (syntactic) condition are executed. This result holds for a
large class of security properties that encompasses secrecy and various
formulations of authentication.}
}
@inproceedings{GGJ-wrs08,
address = {Castle of Hagenberg, Austria},
month = apr,
year = 2009,
volume = 237,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Middeldorp, Aart},
acronym = {{WRS}'08},
booktitle = {{P}roceedings of the 8th {I}nternational {W}orkshop on
{R}eduction {S}trategies in {R}ewriting and {P}rogramming ({WRS}'08)},
author = {Gasc{\'o}n, Adri{\`a} and Godoy, Guillem and Jacquemard,
Florent},
title = {Closure of Tree Automata Languages under Innermost Rewriting},
pages = {23-38},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GGJ-wrs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GGJ-wrs08.pdf},
doi = {10.1016/j.entcs.2009.03.033},
abstract = {Preservation of regularity by a term rewriting system~(TRS)
states that the set of reachable terms from a tree automata~(TA) language
(a.k.a.~regular term set) is also a TA language. It~is an important and
useful property, and there have been many works on identifying classes of
TRS ensuring~it; unfortunately, regularity is not preserved for
restricted classes of TRS like shallow~TRS. Nevertheless, this property
has not been studied for important strategies of rewriting like the
innermost strategy which corresponds to the call by value computation of
programming languages.\par
We prove that the set of innermost-reachable terms from a TA language by
a shallow TRS is not necessarily regular, but it can be recognized by a
TA with equality and disequality constraints between brothers. As~a
consequence we conclude decidability of regularity of the reachable set
of terms from a TA language by innermost rewriting and shallow TRS. This
result is in contrast with plain (not necessarily innermost) rewriting
for which we prove undecidability. We also show that, like for plain
rewriting, innermost rewriting with linear and right-shallow TRS
preserves regularity.}
}
@inproceedings{EB-fast08,
address = {Malaga, Spain},
month = apr,
year = 2009,
volume = 5491,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Degano, Pierpaolo and Guttman, Joshua and
Martinelli, Fabio},
acronym = {{FAST}'08},
booktitle = {{R}evised {S}elected {P}apers of the 5th {I}nternational {W}orkshop on
{F}ormal {A}spects in {S}ecurity and {T}rust ({FAST}'08)},
author = {Bursztein, Elie},
title = {Extending Anticipation Games with Location, Penalty and
Timeline},
pages = {272-286},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/eb-fast08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/eb-fast08.pdf},
doi = {10.1007/978-3-642-01465-9_18},
abstract = {Over the last few years, attack graphs have became a well
recognized tool to analyze and model complex network attack. The most
advanced evolution of attack graphs, called anticipation games, is based
on game theory. However even if anticipation games allow to model time,
collateral effects and player interactions with the network, there is
still key aspects of the network security that cannot be modeled in this
framework. Theses aspects are network cooperation to fight unknown attack,
the cost of attack based on its duration and the introduction of new
attack over the time. In this paper we address these needs, by introducing
a three-fold extension to anticipation games. We prove that this extension
does not change the complexity of the framework. We illustrate the
usefulness of this extension by presenting how it can be used to find a
defense strategy against 0 days that use an honey net. Finally, we have
implemented this extension into a prototype, to show that it can be used
to analyze large networks security.}
}
@article{DKR-jcs08,
publisher = {{IOS} Press},
journal = {Journal of Computer Security},
author = {Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D.},
title = {Verifying Privacy-type Properties of Electronic Voting
Protocols},
volume = 17,
number = 4,
month = jul,
year = 2009,
pages = {435-487},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-jcs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-jcs08.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DKR-jcs08.ps},
doi = {10.3233/JCS-2009-0340},
abstract = {Electronic voting promises the possibility of a convenient,
efficient and secure facility for recording and tallying votes in an
election. Recently highlighted inadequacies of implemented systems have
demonstrated the importance of formally verifying the underlying voting
protocols. We study three privacy-type properties of electronic voting
protocols: in increasing order of strength, they are vote-privacy,
receipt-freeness, and coercion-resistance.\par
We use the applied pi calculus, a formalism well adapted to modelling such
protocols, which has the advantages of being based on well-understood
concepts. The privacy-type properties are expressed using observational
equivalence and we show in accordance with intuition that
coercion-resistance implies receipt-freeness, which implies vote-privacy.\par
We illustrate our definitions on three electronic voting protocols from
the literature. Ideally, these three properties should hold even if the
election officials are corrupt. However, protocols that were designed to
satisfy receipt-freeness or coercion-resistance may not do so in the
presence of corrupt officials. Our model and definitions allow us to
specify and easily change which authorities are supposed to be
trustworthy.}
}
@inproceedings{BFS-infinity08,
optaddress = {Toronto, Canada},
month = jul,
year = 2009,
volume = 239,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Habermehl, Peter and Vojnar, Tom{\'a}{\v{s}}},
acronym = {{INFINITY}'06,'07,'08},
booktitle = {{J}oint {P}roceedings of the 8th, 9th and 10th {I}nternational
{W}orkshops on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'06,'07,'08)},
author = {Bouchy, Florent and Finkel, Alain and Sangnier, Arnaud},
title = {Reachability in Timed Counter Systems},
pages = {167-178},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFS-infinity08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFS-infinity08.pdf},
doi = {10.1016/j.entcs.2009.05.038},
abstract = {We introduce Timed Counter Systems, a~new class of systems
mixing clocks and counters. Such systems have an infinite state space,
hence their reachability problems are undecidable. By~abstracting clock
values with a Region Graph, we~show the Counter Reachability Problem to be
decidable for three subclasses: Timed~VASS, Bounded Timed Counter Systems,
and Reversal-Bounded Timed Counter Systems.}
}
@proceedings{HV-infinity2008,
title = {{J}oint {P}roceedings of the 8th, 9th and 10th {I}nternational
{W}orkshops on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'06,'07,'08)},
booktitle = {{J}oint {P}roceedings of the 8th, 9th and 10th {I}nternational
{W}orkshops on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'06,'07,'08)},
optacronym = {{INFINITY}'06,'07,'08},
editor = {Habermehl, Peter and Vojnar, Tom{\'a}{\v{s}}},
publisher = {Elsevier Science Publishers},
doi = {10.1016/j.entcs.2009.05.026},
series = {Electronic Notes in Theoretical Computer Science},
volume = 239,
year = 2009,
month = jul,
optaddress = {Toronto, Canada}
}
@incollection{DG-hwa08,
year = 2009,
series = {EATCS Monographs in Theoretical Computer Science},
publisher = {Springer},
editor = {Kuich, Werner and Vogler, Heiko and Droste, Manfred},
booktitle = {Handbook of Weighted Automata},
author = {Droste, Manfred and Gastin, Paul},
title = {Weighted automata and weighted logics},
pages = {175-211},
chapter = 5,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-hwa08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-hwa08.pdf}
}
@incollection{DG-pct08,
futureaddress = {},
month = jan,
year = 2009,
series = {IARCS-Universities},
publisher = {Universities Press},
booktitle = {Perspectives in Concurrency Theory},
editor = {Lodaya, Kamal and Mukund, Madhavan and
Ramanujam, R.},
author = {Diekert, Volker and Gastin, Paul},
title = {Local safety and local liveness for distributed systems},
pages = {86-106},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-pct08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-pct08.pdf},
abstract = {We introduce local safety and local liveness for distributed
systems whose executions are modeled by Mazurkiewicz traces. We
characterize local safety by local closure and local liveness by local
density. Restricting to first-order definable properties, we prove a
decomposition theorem in the spirit of the separation theorem for linear
temporal logic. We then characterize local safety and local liveness by
means of canonical local temporal logic formulae.}
}
@article{DL-tocl08,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko},
title = {{LTL} with the freeze quantifier and register automata},
volume = 10,
number = 3,
nopages = {},
month = apr,
year = 2009,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DL-tocl08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DL-tocl08.pdf},
doi = {10.1145/1507244.1507246},
abstract = {A data word is a sequence of pairs of a letter from a finite
alphabet and an element from an infinite set, where the latter can only be
compared for equality. To reason about data words, linear temporal logic
is extended by the freeze quantifier, which stores the element at the
current word position into a register, for equality comparisons deeper in
the formula. By translations from the logic to alternating automata with
registers and then to faulty counter automata whose counters may
erroneously increase at any time, and from faulty and error-free counter
automata to the logic, we obtain a complete complexity table for logical
fragments defined by varying the set of temporal operators and the number
of registers. In~particular, the~logic with future-time operators and
\(1\)~register is decidable but not primitive recursive over finite data
words. Adding past-time operators or \(1\)~more register, or switching to
infinite data words, cause undecidability.}
}
@article{AP-ieeedeb09,
publisher = {{IEEE} Computer Society Press},
journal = {IEEE Data Engineering Bulletin},
author = {Abiteboul, Serge and Polyzotis, Neoklis},
title = {Searching Shared Content in Communities with the Data Ring},
volume = 32,
number = 2,
pages = {44-51},
year = 2009,
month = jun,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AP-ieeedeb09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AP-ieeedeb09.pdf},
doi = {},
abstract = {Information ubiquity has created a large crowd of users (most
notably scientists), who could employ DBMS technology to share and search
their data more effectively. Still, this user base prefers to keep its
data in files that can be easily managed by applications such as
spreadsheets, rather than deal with the complexity and rigidity of modern
database systems.\par
In this article, we describe a vision for enabling non-experts, such as
scientists, to build content sharing communities in a true database
fashion: declaratively. The proposed infrastructure, called the data ring,
enables users to share and search their data with minimal effort; the user
points to the data that should be shared, and the data ring becomes
responsible for automatically indexing the data (to make it accessible),
replicating it (for availability), and reorganizing its physical storage
(for better query performance). We outline the salient features of our
proposal, and outline recent technical advancements in realizing data
rings.}
}
@article{ASV-ieeedeb09,
publisher = {{IEEE} Computer Society Press},
journal = {IEEE Data Engineering Bulletin},
author = {Abiteboul, Serge and Segoufin, Luc and Vianu, Victor},
title = {Modeling and Verifying Active {XML} Artifacts},
volume = 32,
number = 3,
pages = {10-15},
year = 2009,
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ASV-ieeedeb09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ASV-ieeedeb09.pdf},
doi = {}
}
@article{AKSS-jvldb09,
publisher = {ACM Press},
journal = {The VLDB Journal},
author = {Abiteboul, Serge and Kimelfeld, Benny and Sagiv, Yehoshua and
Senellart, Pierre},
title = {On the expressiveness of probabilistic {XML} models},
volume = 18,
number = 5,
pages = {1041-1064},
year = 2009,
month = oct,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AKSS-jvldb09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AKSS-jvldb09.pdf},
doi = {10.1007/s00778-009-0146-1},
abstract = {Various known models of probabilistic XML can be
represented as instantiations of the abstract notion of
\emph{p-documents}. In addition to ordinary nodes, p-documents have
\emph{distributional} nodes that specify the possible worlds and their
probabilistic distribution. Particular families of p-documents are
determined by the types of distributional nodes that can be used as well
as by the structural constraints on the placement of those nodes in a
p-document. Some of the resulting families provide natural extensions and
combinations of previously studied probabilistic XML models. The focus of
the paper is on the expressive power of families of p-documents. In
particular, two main issues are studied. The first is the ability to
(efficiently) \emph{translate} a given p-document of one family into
another family. The second is \emph{closure under updates}, namely, the
ability to (efficiently) represent the result of updating the instances of
a p-document of a given family as another p-document of that family. For
both issues, we distinguish two variants corresponding to
\emph{value-based} and \emph{object-based} semantics of p-documents.}
}
@inproceedings{ABM-edbt09,
address = {Saint Petersburg, Russia},
month = mar,
year = 2009,
novolume = {},
series = {ACM International Conference Proceeding Series},
publisher = {Springer},
editor = {Kersten, Martin L. and Novikov, Boris and Teubner, Jens and
Polutin, Vladimir and Manegold, Stefan},
acronym = {{EDBT}'09},
booktitle = {{A}dvances in {D}atabase {T}echnology~---
{P}roceedings of the 12th {I}nternational {C}onference on
{E}xtending {D}atabase {T}echnology ({EDBT}'09)},
author = {Abiteboul, Serge and Bourhis, Pierre and Marinoiu, Bogdan},
title = {Efficient maintenance techniques for views over active
documents},
pages = {1076-1087},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABM-edbt09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABM-edbt09.pdf},
doi = {10.1145/1516360.1516483},
abstract = {Many Web applications are based on dynamic interactions between
Web components exchanging flows of information. Such a situation arises
for instance in mashup systems or when monitoring distributed autonomous
systems. Our work is in this challenging context that has generated
recently a lot of attention; see Web~2.0. We introduce the axlog formal
model for capturing such interactions and show how this model can be
supported efficiently. The central component is the axlog widget defined
by one tree-pattern query or more, over an active document (in the Active
XML style) that includes some input streams of updates. A widget generates
a stream of updates for each query, the updates that are needed to
maintain the view corresponding to the query. We exploit an array of known
technologies: datalog optimization techniques such as Differential or
MagicSet, constraint query languages, and efficient XML filtering
(YFilter). The novel optimization technique we propose is based on
fundamental new notions: a relevance (different than that of MagicSet),
satisfiability and provenance for active documents. We briefly discuss an
implementation of an axlog engine, an application that we used to test the
approach, and results of experiments.}
}
@inproceedings{AGMP-icde2009,
address = {Shanghai, China},
month = mar # {-} # apr,
year = 2009,
publisher = {{IEEE} Computer Society Press},
editor = {Ioannidis, Yannis E. and Lee, Dik Lun and Ng, Raymond T.},
acronym = {{ICDE}'09},
booktitle = {{P}roceedings of the 25th {I}nternational {C}onference on
{D}ata {E}ngineering ({ICDE}'09)},
author = {Abiteboul, Serge and Greenshpan, Ohad and Milo, Tova and
Polyzotis, Neoklis},
title = {Match{U}p: Autocompletion for Mashups},
pages = {1479-1482},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGMP-icde2009.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGMP-icde2009.pdf},
doi = {10.1109/ICDE.2009.47},
abstract = {A~\emph{mashup} is a Web application that integrates data,
computation and GUI provided by several systems into a unique tool. The
concept originated from the understanding that the number of applications
available on the Web and the need for combining them to meet user
requirements, are growing very rapidly. This demo presents \emph{MatchUp},
a system that supports rapid, on-demand, intuitive development of
\emph{mashups}, based on a novel \emph{autocompletion} mechanism. The key
observation guiding the development of \emph{MatchUp} is that mashups
developed by different users typically share common characteristics; they
use similar classes of mashup components and glue them together in a
similar manner. \emph{MatchUp} exploits these similarities to predict,
given a user's partial mashup specification, what are the most likely
potential \emph{completions} (missing components and connection between
them) for the specification. Using a novel ranking algorithm, users are
then offered top-k completions from which they choose and refine according
to their needs.}
}
@article{CDMP-apal09,
publisher = {Elsevier Science Publishers},
journal = {Annals of Pure and Applied Logics},
author = {Chevalier, Fabrice and D'Souza, Deepak and Matteplackel, Raj Mohan
and Prabhakar, Pavithra},
title = {Automata and logics over finitely varying functions},
year = {2009},
month = dec,
volume = {161},
number = {3},
pages = {324-336},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDMP-apal09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDMP-apal09.pdf},
doi = {10.1016/j.apal.2009.07.007},
abstract = {We extend some of the classical connections between automata and
logic due to B{\"u}chi~(1960) and McNaughton and Papert~(1971) to
languages of finitely varying functions or {"}signals{"}. In particular,
we introduce a natural class of automata for generating finitely varying
functions called ST-NFAs, and show that it coincides in terms of language
definability with a natural monadic second-order logic interpreted over
finitely varying functions (Rabinovich, 2002). We also identify a
{"}counter-free{"} subclass of ST-NFAs which characterise the first-order
definable languages of finitely varying functions. Our proofs mainly
factor through the classical results for word languages. These results
have applications in automata characterisations for continuously
interpreted real-time logics like Metric Temporal Logic (MTL) (Chevalier
\emph{et~al.}, 2006,~2007).}
}
@phdthesis{mercier-phd2009,
author = {Mercier, Antoine},
title = {Contributions {\`a} l'analyse automatique des protocoles
cryptographiques en pr{\'e}sence de propri{\'e}t{\'e}s
alg{\'e}briques : protocoles de groupe, {\'e}quivalence
statique},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2009,
month = dec,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AM-these09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AM-these09.pdf}
}
@phdthesis{bursuc-phd2009,
author = {Bursuc, Sergiu},
title = {Contraintes de d{\'e}ductibilit{\'e} dans une alg{\`e}bre
quotient: r{\'e}duction de mod{\`e}les et applications {\`a}
la s{\'e}curit{\'e}},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2009,
month = dec,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SB-these09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SB-these09.pdf}
}
@incollection{CM-CES09,
author = {Cassez, Franck and Markey, Nicolas},
title = {Control of Timed Systems},
booktitle = {Communicating Embedded Systems~-- Software and Design},
editor = {Jard, Claude and Roux, Olivier H.},
publisher = {Wiley-ISTE},
year = 2009,
month = oct,
pages = {83-120},
chapter = 3,
url = {http://www.iste.co.uk/index.php?f=x&ACTION=View&id=288},
nops = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/.ps},
nopsgz = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PSGZ/.ps.gz},
isbn = {9781848211438}
}
@incollection{DH-CES09,
author = {Donatelli, Susanna and Haddad, Serge},
title = {Quantitative Verification of {M}arkov Chains},
booktitle = {Communicating Embedded Systems~-- Software and Design},
editor = {Jard, Claude and Roux, Olivier H.},
publisher = {Wiley-ISTE},
year = 2009,
month = oct,
pages = {139-163},
chapter = 5,
url = {http://www.iste.co.uk/index.php?f=x&ACTION=View&id=288},
nops = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/.ps},
nopsgz = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PSGZ/.ps.gz},
isbn = {9781848211438}
}
@inproceedings{JGL-asian09,
address = {Seoul, Korea},
month = dec,
year = 2009,
volume = 5913,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Datta, Anupam},
acronym = {{ASIAN}'09},
booktitle = {{P}roceedings of the 13th {A}sian
{C}omputing {S}cience {C}onference
({ASIAN}'09)},
author = {Goubault{-}Larrecq, Jean},
title = {{\textquotedbl}{L}ogic Wins!{\textquotedbl}},
pages = {1-16},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-asian09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-asian09.pdf},
doi = {10.1007/978-3-642-10622-4_1},
abstract = {Clever algorithm design is sometimes superseded by simple
encodings into logic. We apply this motto to a few case studies in the
formal verification of security properties. In particular, we examine
confidentiality objectives in hardware circuit descriptions written in
VHDL.}
}
@phdthesis{chamseddine-phd2009,
author = {Chamseddine, Najla},
title = {Analyse quantitative parametr{\'e}e d'automates temporis{\'e}s probabilistes},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2009,
month = oct,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/NC-these09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/NC-these09.pdf}
}
@phdthesis{bouchy-phd2009,
author = {Bouchy, Florent},
title = {Logiques et mod{\`e}les pour la v{\'e}rification de syst{\`e}mes infinis},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2009,
month = nov,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FB-these09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FB-these09.pdf}
}
@phdthesis{sznajder-phd2009,
author = {Sznajder, Nathalie},
title = {Synth{\`e}se de syst{\`e}mes distribu{\'e}s ouverts},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2009,
month = nov,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/NS-these09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/NS-these09.pdf}
}
@inproceedings{SRKK-wissec09,
address = {Louvain-la-Neuve, Belgium},
month = nov,
year = 2009,
editor = {Pereira, Olivier and Quisquater, Jean-Jacques and
Standaert, Fran\c{c}ois-Xavier},
acronym = {{WISSEC}'09},
booktitle = {{P}roceedings of the 4th {B}enelux {W}orkshop on
{I}nformation and {S}ystem {S}ecurity ({WISSEC}'09)},
author = {Smyth, Ben and Ryan, Mark D. and Kremer, Steve and
Kourjieh, Mounira},
title = {Election verifiability in electronic voting protocols
(Preliminary version)},
nopages = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SRKK-wissec09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SRKK-wissec09.pdf},
abstract = {We~present a symbolic definition of election verifiability for
electronic voting protocols. Our definition is given in terms of
reachability assertions in the applied pi calculus and is amenable to
automated reasoning using the tool ProVerif. The~definition distinguishes
three aspects of verifiability, which we call individual, universal, and
eligibility verifiability. It also allows us to determine precisely what
aspects of the system are required to be trusted. We demonstrate our
formalism by analysing the protocols due to Fujioka, Okamoto \&~Ohta and
Juels, Catalano \&~Jakobsson; the~latter of which has been implemented by
Clarkson, Chong \&~Myers. }
}
@inproceedings{CCD-secco09,
address = {Bologna, Italy},
month = oct,
year = 2009,
editor = {Boreale, Michele and Kremer, Steve},
acronym = {{SecCo}'09},
booktitle = {{P}reliminary {P}roceedings of the 7th {I}nternational
{W}orkshop on {S}ecurity {I}ssues in
{C}oordination {M}odels, {L}anguages and
{S}ystems ({SecCo}'09)},
author = {Cheval, Vincent and Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie},
title = {A~decision procedure for proving observational equivalence},
nmnote = {did not appear in postproceedings EPTCS7},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CCD-secco09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CCD-secco09.pdf}
}
@proceedings{BK-secco2009,
title = {{P}roceedings of the 7th {I}nternational {W}orkshop on
{S}ecurity {I}ssues in {C}oncurrency ({S}ec{C}o'09)},
booktitle = {{P}roceedings of the 7th {I}nternational {W}orkshop on
{S}ecurity {I}ssues in {C}oncurrency ({S}ec{C}o'09)},
acronym = {{S}ec{C}o'09},
editor = {Boreale, Michele and Kremer, Steve},
doi = {10.4204/EPTCS.7},
url = {http://eptcs.web.cse.unsw.edu.au/content.cgi?SECCO2009},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = 7,
year = 2009,
month = aug,
address = {Bologna, Italy}
}
@mastersthesis{dimino-m1,
author = {Dimino, J{\'e}r{\'e}mie},
title = {Les syst{\`e}mes {\`a} canaux non-fiables vus comme des
transducteurs},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de stage de {M1}},
year = {2009},
month = oct,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/dimino-m1.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/dimino-m1.pdf}
}
@mastersthesis{cheval-master,
author = {Cheval, Vincent},
title = {Algorithme de d{\'e}cision de l'{\'e}quivalence symbolique de
syst{\`e}mes de contraintes},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2009},
month = sep,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/master-cheval.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/master-cheval.pdf}
}
@mastersthesis{brenguier-master,
author = {Brenguier, Romain},
title = {Calcul des {\'e}quilibres de Nash dans les jeux temporis{\'e}s},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2009},
month = sep,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/master-brenguier.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/master-brenguier.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/master-brenguier.ps}
}
@techreport{LSV:09:20,
author = {Andr{\'e}, {\'E}tienne},
title = {Everything You Always Wanted to Know About {IMITATOR} (But~Were Afraid to~Ask)},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2009},
month = jul,
type = {Research Report},
number = {LSV-09-20},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-20.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-20.pdf},
note = {11~pages},
abstract = {We present here the user manual of IMITATOR, a tool for
synthesizing constraints on timing bounds (seen as parameters) in the
framework of timed automata. Unlike classical synthesis methods, the tool
IMITATOR takes advantage of a given reference valuation of the parameters
for which the system is known to behave properly. The goal of IMITATOR is
to generate a constraint such that, under any valuation satisfying this
constraint, the system is guaranteed to behave, in terms of alternating
sequences of locations and actions, as under the reference valuation.\par
We give here the installation requirements and the launching commands of
IMITATOR, as well as the source code of a toy example.}
}
@inproceedings{DJLL-fsttcs09,
address = {Kanpur, India},
month = dec,
year = 2009,
volume = 4,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Kannan, Ravi and Narayan Kumar, K.},
acronym = {{FSTTCS}'09},
booktitle = {{P}roceedings of the 29th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'09)},
author = {Demri, St{\'e}phane and Jurdzi{\'n}ski, Marcin and Lachish,
Oded and Lazi{\'c}, Ranko},
title = {The covering and boundedness problems for branching vector addition systems},
pages = {181-192},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/djll-fsttcs09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/djll-fsttcs09.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2009.2317},
abstract = {The covering and boundedness problems for branching vector
addition systems are shown complete for doubly-exponential time.}
}
@inproceedings{DKP-fsttcs09,
address = {Kanpur, India},
month = dec,
year = 2009,
volume = 4,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Kannan, Ravi and Narayan Kumar, K.},
acronym = {{FSTTCS}'09},
booktitle = {{P}roceedings of the 29th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'09)},
author = {Delaune, St{\'e}phanie and Kremer, Steve and Pereira,
Olivier},
title = {Simulation based security in the applied pi calculus},
pages = {169-180},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DKP-fsttcs09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DKP-fsttcs09.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2009.2316},
abstract = {We present a symbolic framework for refinement and composition
of security protocols. The framework uses the notion of ideal
functionalities. These are abstract systems which are secure by
construction and which can be combined into larger systems. They can be
separately refined in order to obtain concrete protocols implementing
them. Our work builds on ideas from computational models such as the
universally composable security and reactive simulatability frameworks.
The underlying language we use is the applied pi calculus which is a
general language for specifying security protocols. In our framework we
can express the different standard flavours of simulation-based security
which happen to all coincide. We illustrate our framework on an
authentication functionality which can be realized using the
Needham-Schroeder-Lowe protocol. For this we need to define an ideal
functionality for asymmetric encryption and its realization. We also show
a joint state result for this functionality which allows composition (even
though the same key material is reused) using a tagging mechanism.}
}
@article{BCHMMR-ijwsr09,
publisher = {{IGI} Publishing},
journal = {International Journal of Web Services Research},
author = {Boutrous{-}Saab, C{\'e}line and Coulibaly, Demba and Haddad, Serge
and Melliti, Tarek and Moreaux, Patrice and Rampacek, Sylvain},
title = {An Integrated Framework for Web Services Orchestration},
volume = 6,
number = 4,
pages = {1-29},
year = 2009,
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHMMR-ijwsr09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHMMR-ijwsr09.pdf},
abstract = {Currently, Web services give place to active research and this
is due both to industrial and theoretical factors. On one hand, Web
services are essential as the design model of applications dedicated to
the electronic business. On the other hand, this model aims to become one
of the major formalisms for the design of distributed and cooperative
applications in an open environment (the Internet). In this article, the
authors will focus on two features of Web services. The first one concerns
the interaction problem: given the interaction protocol of a Web service
described in BPEL, how to generate the appropriate client? Their approach
is based on a formal semantics for BPEL via process algebra and yields an
algorithm which decides whether such a client exists and synthesizes the
description of this client as a (timed) automaton. The second one concerns
the design process of a service. They propose a method which proceeds by
two successive refinements: first the service is described via UML, then
refined in a BPEL model and finally enlarged with JAVA code using JCSWL, a
new language that we introduce here. Their solutions are integrated in a
service development framework that will be presented in a synthetic way.}
}
@inproceedings{VLC-aplas09,
address = {Seoul, Korea},
month = dec,
year = 2009,
volume = {5904},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hu, Zhenjiang},
acronym = {{APLAS}'09},
booktitle = {{P}roceedings of the 7th {A}sian {S}ymposium
on {P}rogramming {L}anguages and {S}ystems
({APLAS}'09)},
author = {Villard, Jules and Lozes, {\'E}tienne and Calcagno, Cristiano},
title = {Proving Copyless Message Passing},
pages = {194-209},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/VLC-aplas09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/VLC-aplas09.pdf},
doi = {10.1007/978-3-642-10672-9_15},
abstract = {Handling concurrency using a shared memory and locks is tedious
and error-prone. One solution is to use message passing instead. We study
here a particular, contract-based flavor that makes the ownership transfer
of messages explicit. In this case, ownership of the heap region
representing the content of a message is lost upon sending, which can lead
to efficient implementations. In this paper, we define a proof system for
a concurrent imperative programming language implementing this idea and
inspired by the Singularity OS. The proof system, for which we prove
soundness, is an extension of separation logic, which has already been
used successfully to study various ownership-oriented paradigms.}
}
@inproceedings{AFS-avocs09,
address = {Swansea, UK},
month = sep,
year = {2009},
volume = 23,
series = {Electronic Communications of the EASST},
publisher = {European Association of Software Science and Technology},
editor = {Roggenbach, Markus},
acronym = {{AVoCS}'09},
booktitle = {{P}roceedings of the 9th {I}nternational
{W}orkshop on {A}utomated {V}erification
of {C}ritical {S}ystems
({AVoCS}'09)},
author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent and Sproston,
Jeremy},
title = {An Extension of the Inverse Method to Probabilistic Timed Automata},
nopages = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AFS-avocs09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AFS-avocs09.pdf},
abstract = {Probabilistic timed automata can be used to model systems in
which probabilistic and timing behavior coexist. Verification of
probabilistic timed automata models is generally performed with regard to
a single reference valuation of the timing parameters. Given such a
parameter valuation, we present a method for obtaining automatically a
constraint on timing parameters for which the reachability probabilities
(1)~remain invariant and (2)~are~equal to the reachability probabilities
for the reference valuation. The method relies on parametric analysis of a
non-probabilistic version of the probabilistic timed automata model using
the {"}inverse method{"}. Our approach is useful for avoiding repeated
executions of probabilistic model checking analyses for the same model
with different parameter valuations. We provide examples of the
application of our technique to models of randomized protocols.}
}
@incollection{HI-petrinet-diaz,
year = 2009,
publisher = {Wiley-ISTE},
editor = {Diaz, Michel},
booktitle = {Petri Nets: Fundamental Models, Verification and Applications},
author = {Haddad, Serge and Ili{\'e}, Jean-Michel},
title = {Symmetry and Temporal Logic},
pages = {435-460},
url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html}
}
@incollection{HV-petrinet-diaz-b,
year = 2009,
publisher = {Wiley-ISTE},
editor = {Diaz, Michel},
booktitle = {Petri Nets: Fundamental Models, Verification and Applications},
author = {Haddad, Serge and Vernadat, Fran{\c{c}}ois},
title = {Verification of Specific Properties},
pages = {349-414},
url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html}
}
@incollection{HM-petrinet-diaz-c,
year = 2009,
publisher = {Wiley-ISTE},
editor = {Diaz, Michel},
booktitle = {Petri Nets: Fundamental Models, Verification and Applications},
author = {Haddad, Serge and Moreaux, Patrice},
title = {Tensor Methods and Stochastic {P}etri Nets},
pages = {321-346},
url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html}
}
@incollection{HM-petrinet-diaz-b,
year = 2009,
publisher = {Wiley-ISTE},
editor = {Diaz, Michel},
booktitle = {Petri Nets: Fundamental Models, Verification and Applications},
author = {Haddad, Serge and Moreaux, Patrice},
title = {Stochastic Well-formed {P}etri Nets},
pages = {303-320},
url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html}
}
@incollection{HM-petrinet-diaz-a,
year = 2009,
publisher = {Wiley-ISTE},
editor = {Diaz, Michel},
booktitle = {Petri Nets: Fundamental Models, Verification and Applications},
author = {Haddad, Serge and Moreaux, Patrice},
title = {Stochastic {P}etri Nets},
pages = {269-302},
url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html}
}
@incollection{H-petrinet-diaz,
year = 2009,
publisher = {Wiley-ISTE},
editor = {Diaz, Michel},
booktitle = {Petri Nets: Fundamental Models, Verification and Applications},
author = {Haddad, Serge},
title = {Decidability and Complexity of {P}etri Net Problems},
pages = {87-122},
url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html}
}
@incollection{HV-petrinet-diaz-a,
year = 2009,
publisher = {Wiley-ISTE},
editor = {Diaz, Michel},
booktitle = {Petri Nets: Fundamental Models, Verification and Applications},
author = {Haddad, Serge and Vernadat, Fran{\c{c}}ois},
title = {Analysis Methods for {P}etri Nets},
pages = {41-86},
url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html}
}
@article{BBC-apal09,
publisher = {Elsevier Science Publishers},
journal = {Annals of Pure and Applied Logics},
author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and
Chevalier, Fabrice},
title = {Weighted O-Minimal Hybrid Systems},
year = {2009},
month = dec,
volume = {161},
number = {3},
pages = {268-288},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-apal09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-apal09.pdf},
doi = {10.1016/j.apal.2009.07.014},
abstract = {We consider weighted o-minimal hybrid systems, which extend
classical o-minimal hybrid systems with cost functions. These cost
functions are 'observer variables' which increase while the system evolves
but do not constrain the behaviour of the system. In this paper, we prove
two main results: (i)~optimal o-minimal hybrid games are decidable;
(ii)~the~model-checking of~WCTL, an~extension of CTL which can constrain
the cost variables, is decidable over that model. This has to be compared
with the same problems in the framework of timed automata where both
problems are undecidable in general, while they are decidable for the
restricted class of one-clock timed automata.}
}
@inproceedings{FLS-nordsec09,
address = {Oslo, Norway},
month = oct,
year = 2009,
volume = 5838,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {J{\o}sang, Audun and Maseng, Torleiv and Knapskog, Svein Johan},
acronym = {{NordSec}'09},
booktitle = {{P}roceedings of the 14th {N}ordic {W}orkshop on {S}ecure {IT}
{S}ystems ({NordSec}'09)},
author = {Focardi, Riccardo and Luccio, Flaminia L. and
Steel, Graham},
title = {Blunting Differential Attacks on {PIN} Processing {API}s},
pages = {88-103},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FLS-nordsec09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FLS-nordsec09.pdf},
doi = {10.1007/978-3-642-04766-4_7},
abstract = {We~propose a countermeasure for a class of known attacks on the
PIN processing API used in the ATM (cash machine) network. This API
controls access to the tamper-resistant Hardware Security Modules where
PIN encryption, decryption and verification takes place. The~attacks are
differential attacks, whereby an attacker gains information about the
plaintext values of encrypted customer PINs by making changes to the
non-confidential inputs to a command. Our~proposed fix adds an integrity
check to the parameters passed to the command. It~is novel in that it
involves very little change to the existing ATM network infrastructure.}
}
@inproceedings{KMT-asian09,
address = {Seoul, Korea},
month = dec,
year = 2009,
volume = 5913,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Datta, Anupam},
acronym = {{ASIAN}'09},
booktitle = {{P}roceedings of the 13th {A}sian
{C}omputing {S}cience {C}onference
({ASIAN}'09)},
author = {Kremer, Steve and Mercier, Antoine and Treinen, Ralf},
title = {Reducing Equational Theories for the Decision of Static
Equivalence},
pages = {94-108},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KMT-asian09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KMT-asian09.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/KMT-asian09.ps},
doi = {10.1007/978-3-642-10622-4_8},
abstract = {Static equivalence is a well established notion of
indistinguishability of sequences of terms which is useful in the symbolic
analysis of cryptographic protocols. Static equivalence modulo equational
theories allows a more accurate representation of cryptographic primitives
by modelling properties of operators by equational axioms. We develop a
method that allows in some cases to simplify the task of deciding static
equivalence in a multi-sorted setting, by removing a symbol from the term
signature and reducing the problem to several simpler equational theories.
We illustrate our technique at hand of bilinear pairings.}
}
@inproceedings{AF-ijcai09,
address = {Pasadena, California, USA},
month = jul,
year = 2009,
publisher = {AAAI Press},
editor = {Boutilier, Craig},
acronym = {{IJCAI}'09},
booktitle = {{P}roceedings of the 21st {I}nternational {J}oint
{C}onference on {A}rtificial {I}ntelligence
({IJCAI}'09)},
author = {Areces, Carlos and Figueira, Diego},
title = {Which Semantics for Neighbourhood Semantics?},
pages = {671-676},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AF-ijcai09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AF-ijcai09.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/AF-ijcai09.ps},
abstract = {In this article we discuss two alternative proposals for
neighbourhood semantics (which we call strict and loose neighbourhood
semantics, NSS~and~NSL respectively) that have been previously introduced
in the literature. Our~main tools are suitable notions of bisimulation.
While an elegant notion of bisimulation exists for NSL, the required
bisimulation for NSS is rather involved. We~propose a simple extension of
NSS with a universal modality that we call NSS(E), which comes together
with a natural notion of bisimulation. We~also investigate the complexity
of the satisfiability problem for NSL and NSS(E).}
}
@techreport{LSV:09:16,
author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Sassolas, Mathieu},
title = {Verification on Interrupt Timed Automata},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2009},
month = jul,
type = {Research Report},
number = {LSV-09-16},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-16.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-16.pdf},
note = {16~pages},
abstract = {The class of Interrupt Timed Automata (ITA) has been introduced to
model multi-task systems with interruptions in a single processor
environment. This is a subclass of hybrid automata in which real
valued variables consist of a restricted type of stopwatches
(variables with rate \(0\) or~\(1\)) organized along levels. While
reachability is undecidable with usual stopwatches, it was proved
that this problem is decidable in ITA and that untimed languages of
ITA are effectively regular. Here we investigate the problem of
model checking timed extensions of CTL over ITA and show in
contrast that this problem is undecidable. On~the other hand, we
prove that model checking is decidable for two relevant fragments of this
timed logic: (1)~the~first one where formula contain only model
clocks and (2)~the~second one where formulas have a single external
clock.}
}
@techreport{LSV:09:15,
author = {H{\'e}am, Pierre-Cyrille and Nicaud, Cyril},
title = {Seed: an Easy-to-Use Random Generator of Recursive Data Structures for Testing},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2009},
month = jul,
type = {Research Report},
number = {LSV-09-15},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-15.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-15.pdf},
note = {16~pages},
abstract = {Random testing represents a simple and tractable way for software
assessment. This paper presents the Seed tool dedicated to the
uniform random generation of recursive data structures as labelled
trees or logical formulas. We show how Seed can be used in several
testing contexts, from model based testing to performance
testing. Generated data structures are defined by grammar-like rules,
given in an XML format, multiplying Seed possible applications.
Seed is based on combinatorial techniques, and can generate uniformly
at random \(k\)~structures of size~\(n\) with a
time complexity in \(O(n^{2}+ kn\cdot \log(n))\). Finally, Seed is available as a free
java application and a great effort has been made to make it
easy-to-use.}
}
@techreport{LSV:09:13,
author = {Andr{\'e}, {\'E}tienne and Encrenaz, Emmanuelle and Fribourg, Laurent},
title = {Synthesizing Parametric Constraints on Various Case Studies Using {IMITATOR}},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2009},
month = jun,
type = {Research Report},
number = {LSV-09-13},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-13.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-13.pdf},
note = {18~pages},
abstract = {We present here applications of IMITATOR, a tool for
synthesizing constraints on timing bounds (seen as parameters) in the
framework of timed automata. Unlike classical synthesis methods, we take
advantage of a given reference valuation of the parameters for which the
system is known to behave properly. Our aim is to generate a constraint
such that, under any valuation satisfying this constraint, the system is
guaranteed to behave, in terms of alternating sequences of locations and
actions, as under the reference valuation. This is useful for safely
relaxing some values of the reference valuation, and optimizing timing
bounds of the system. We have successfully applied our tool to various
examples of asynchronous circuits and protocols, which are detailed in
this report.}
}
@inproceedings{BFSP-infinity09,
address = {Bologna, Italy},
month = nov,
year = 2009,
volume = 10,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Farzan, Azadeh and Legay, Axel},
acronym = {{INFINITY}'09},
booktitle = {{P}roceedings of the 11th {I}nternational
{W}orkshops on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'09)},
author = {Bouchy, Florent and Finkel, Alain and San{ }Pietro, Pierluigi},
title = {Dense-choice Counter Machines Revisited},
pages = {3-22},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFSP-infinity09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFSP-infinity09.pdf},
doi = {10.4204/EPTCS.10.1},
abstract = {This paper clarifies the picture about Dense-choice Counter
Machines, which have been less studied than (discrete) Counter Machines.
We revisit the definition of {"}Dense Counter Machines{"} so that it now
extends (discrete) Counter Machines, and we provide new undecidability and
decidability results. Using the first-order additive mixed theory of reals
and integers, we give a logical characterization of the sets of
configurations reachable by reversal-bounded Dense-choice Counter
Machines.}
}
@inproceedings{AF-infinity09,
address = {Bologna, Italy},
month = nov,
year = 2009,
volume = 10,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Farzan, Azadeh and Legay, Axel},
acronym = {{INFINITY}'09},
booktitle = {{P}roceedings of the 11th {I}nternational
{W}orkshops on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'09)},
author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent},
title = {An Inverse Method for Policy-Iteration Based Algorithms},
pages = {44-61},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AF-infinity09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AF-infinity09.pdf},
doi = {10.4204/EPTCS.10.4},
abstract = {We present an extension of two policy-iteration based algorithms
on weighted graphs (viz.,~Markov Decision Problems and Max-Plus Algebras).
This extension allows us to solve the following inverse problem:
considering the weights of the graph to be unknown constants or
parameters, we suppose that a reference instantiation of those weights is
given, and we aim at computing a constraint on the parameters under which
an optimal policy for the reference instantiation is still optimal. The
original algorithm is thus guaranteed to behave well around the reference
instantiation, which provides us with some criteria of robustness. We
present an application of both methods to simple examples. A prototype
implementation has been done.}
}
@inproceedings{BCLD-asian09,
address = {Seoul, Korea},
month = dec,
year = 2009,
volume = 5913,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Datta, Anupam},
acronym = {{ASIAN}'09},
booktitle = {{P}roceedings of the 13th {A}sian
{C}omputing {S}cience {C}onference
({ASIAN}'09)},
author = {Bursuc, Sergiu and Delaune, St{\'e}phanie and Comon{-}Lundh,
Hubert},
title = {Deducibility constraints},
pages = {24-38},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCD-asian09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCD-asian09.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCD-asian09.ps},
doi = {10.1007/978-3-642-10622-4_3},
abstract = {In their work on tractable deduction systems, D.~McAllester and
later D.~Basin and H.~Ganzinger have identified a property of inference
systems (the~locality property) that ensures the tractability of the
\textit{Entscheidungsproblem}.\par
On~the other hand, deducibility constraints are sequences of deduction
problems in which some parts (formulas) are unknown. The~problem is to
decide their satisfiability and to represent the set of all possible
solutions. Such constraints have also been used for deciding some security
properties of cryptographic protocols.\par
In this paper we show that local inference systems (actually a slight
modification of such systems) yield not only a tractable deduction
problem, but also decidable deducibility constraints. Our algorithm not
only allows to decide the existence of a solution, but also gives a
representation of all solutions.}
}
@incollection{ACL-fps09,
noaddress = {},
month = may,
year = 2009,
volume = 5458,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
noacronym = {},
booktitle = {{F}ormal to {P}ractical {S}ecurity},
editor = {Cortier, V{\'e}ronique and Kirchner, Claude and
Okada, Mitsuhiro and Sakurada, Hideki},
author = {Affeldt, Reynald and Comon{-}Lundh, Hubert},
title = {Verification of Security Protocols with a Bounded Number of
Sessions Based on Resolution for Rigid Variables},
pages = {1-20},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACL-fps09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACL-fps09.pdf},
doi = {10.1007/978-3-642-02002-5_1},
abstract = {First-order logic resolution is a standard way to automate the
verification of security protocols. However, it sometimes fails to produce
security proofs for secure protocols because of the detection of false
attacks. For the verification of a bounded number of sessions, false
attacks can be avoided by introducing rigid variables. Unfortunately, this
yields complicated resolution procedures. We show here that there is a
simple translation of the security problem for a bounded number of
sessions into first-order logic, that does not introduce false attacks.
This is shown by translating clauses involving rigid variables into
classical first-order clauses, while preserving satisfiability. We
illustrate this approach by giving a complete and terminating strategy for
a first-order logic fragment resulting from the above translation, that
yields a decision procedure for a bounded number of sessions.}
}
@inproceedings{HMY-msr09,
address = {Nantes, France},
month = nov,
year = 2009,
number = {7-9},
volume = {43},
series = {Journal Europ{\'e}en des Syst{\`e}mes Automatis{\'e}s},
publisher = {Herm{\`e}s},
editor = {Lime, Didier and Roux, Olivier H.},
acronym = {{MSR}'09},
booktitle = {{A}ctes du 7{\`e}me {C}olloque sur la
{M}od{\'e}lisation des {S}yst{\`e}mes
{R}{\'e}actifs
({MSR}'09)},
author = {Haddad, Serge and Mokdad, Lynda and Youcef, Samir},
title = {Bornes du temps de r{\'e}ponse des services Web composites},
pages = {969-983},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HMY-msr09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HMY-msr09.pdf},
abstract = {The quality of service (QoS) of Web services is a key
factor of their success. This requires to design new methods in order to
study~it. Here we propose families of upper bounding models for the
response time of composite Web services for two kinds of composition: the
statical and random {"}fork and merge{"}. In~the first~case, the~complexity of
bounding models belongs to~\(O(n\cdot \sqrt{n})\) where \(n\)~is the
number of called services whereas the complexity of the exact model
belongs to~\(O(n^2)\). In~the second~case, the~complexity of bounding
models still belongs to~\(O(n\cdot \sqrt{n})\) whereas the complexity of
the exact model belongs to~\(O(n^3)\). Furthermore, having a family of
bounding models allows to choose the bounding model depending on the
parameters of the exact model. The numerical results show the interest of
our approach w.r.t. complexity and accuracy of the bound.}
}
@inproceedings{ACDFR-msr09,
address = {Nantes, France},
month = nov,
year = 2009,
number = {7-9},
volume = {43},
series = {Journal Europ{\'e}en des Syst{\`e}mes Automatis{\'e}s},
publisher = {Herm{\`e}s},
editor = {Lime, Didier and Roux, Olivier H.},
acronym = {{MSR}'09},
booktitle = {{A}ctes du 7{\`e}me {C}olloque sur la
{M}od{\'e}lisation des {S}yst{\`e}mes
{R}{\'e}actifs
({MSR}'09)},
author = {Andr{\'e}, {\'E}tienne and Chatain, {\relax Th}omas and
De{ }Smet, Olivier and Fribourg, Laurent and Ruel, Silvain},
title = {Synth{\`e}se de contraintes temporis{\'e}es pour
une architecture d'automatisation en r{\'e}seau},
pages = {1049-1064},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACDFR-msr09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACDFR-msr09.pdf},
abstract = {We deal with the problem of synthesis of timing constraints for
concurrent systems. Such systems are modeled by networks of timed automata
where some constants, represented as parameters, can be tuned. A suitable
value of these parameters is assumed to be known from a preliminarily
simulation process. We present a method which infers a zone of suitable
points around this reference functioning point. This zone is defined by a
system of linear inequalities over the parameters. This method is applied
to the case study of a networked automation system.}
}
@inproceedings{ABC-cav09,
address = {Grenoble, France},
month = jun # {-} # jul,
year = 2009,
volume = 5643,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Bouajjani, Ahmad and Maler, Oded},
acronym = {{CAV}'09},
booktitle = {{P}roceedings of the 21st
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'09)},
author = {Abadi, Mart{\'\i}n and Blanchet, Bruno and Comon{-}Lundh,
Hubert},
title = {Models and Proofs of Protocol Security: A~Progress Report},
pages = {35-49},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABC-cav09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABC-cav09.pdf},
doi = {10.1007/978-3-642-02658-4_5},
abstract = {This paper discusses progress in the verification of security
protocols. Focusing on a small, classic example, it stresses
the use of program-like representations of protocols, and
their automatic analysis in symbolic and computational
models.}
}
@inproceedings{CDL-adhs09,
address = {Zaragoza, Spain},
month = sep,
year = 2009,
editor = {Giua, Alessandro and Silva, Manuel and Zaytoon, Janan},
acronym = {{ADHS}'09},
booktitle = {{P}roceedings of the 3rd {IFAC} {C}onference on {A}nalysis and
{D}esign of {H}ybrid {S}ystems ({ADHS}'09)},
author = {Chatain, {\relax Th}omas and David, Alexandre and Larsen, Kim
G.},
title = {Playing Games with Timed Games},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDL-adhs09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDL-adhs09.pdf},
abstract = {In this paper we focus on property-preserving preorders between
timed game automata and their application to control of partially
observable systems. Following the example of timed simulation between
timed automata, we define timed alternating simulation as a preorder
between timed game automata, which preserves controllability. We define a
method to reduce the timed alternating simulation problem to a safety
game. We show how timed alternating simulation can be used to control
efficiently a partially observable system. This method is illustrated by a
generic case study.}
}
@inproceedings{BHK-rp09,
address = {Palaiseau, France},
month = sep,
year = 2009,
volume = 5797,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Bournez, Olivier and Potapov, Igor},
acronym = {{RP}'09},
booktitle = {{P}roceedings of the 3rd {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'09)},
author = {Boichut, Yohan and H{\'e}am,
Pierre-Cyrille and Kouchnarenko, Olga},
title = {How to Tackle Integer Weighted Automata Positivity},
pages = {79-92},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHK-rp09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHK-rp09.pdf},
doi = {10.1007/978-3-642-04420-5_9},
abstract = {This paper is dedicated to candidate abstractions to capture
relevant aspects of the integer weighted automata. The
expected effect of applying these abstractions is studied to
build the deterministic reachability graphs allowing us to
semi-decide the positivity problem on these automata.
Moreover, the papers reports on the implementations and
experimental results, and discusses other encodings.}
}
@article{BCHK-ijfcs09,
publisher = {World Scientific},
journal = {International Journal of Foundations of Computer Science},
author = {Boichut, Yohan and Courbis, Rom{\'e}o and H{\'e}am,
Pierre-Cyrille and Kouchnarenko, Olga},
title = {Handling Non-left Linear Rules when Completing Tree Automata},
volume = 20,
number = 5,
pages = {837-849},
year = 2009,
month = oct,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHK-ijfcs09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHK-ijfcs09.pdf},
doi = {10.1142/S0129054109006917},
abstract = {This paper addresses the following general problem of tree
regular model-checking: decide whether \(\mathcal{R}^*(\mathcal{L}) \cap
\mathcal{L}_p = \emptyset\) where \(\mathcal{R}^*\) is the reflexive and
transitive closure of a successor relation induced by a term rewriting
system~\(\mathcal{R}\), and \(\mathcal{L}\) and~\(\mathcal{L}_p\) are both
regular tree languages. We~develop an automatic approximation-based
technique to handle this---undecidable in general---problem in the case
when term rewriting system rules are non left-linear.}
}
@article{BDL-apal09,
publisher = {Elsevier Science Publishers},
journal = {Annals of Pure and Applied Logics},
author = {Brochenin, R{\'e}mi and Demri, St{\'e}phane and Lozes,
{\'E}tienne},
title = {Reasoning about sequences of memory states},
volume = {161},
number = {3},
pages = {305-323},
year = 2009,
month = dec,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-apal09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-apal09.pdf},
doi = {10.1016/j.apal.2009.07.004},
abstract = {Motivated by the verification of programs with pointer
variables, we introduce a temporal logic LTL\textsuperscript{mem} whose
underlying assertion language is the quantifier-free fragment of
separation logic and the temporal logic on the top of it is the standard
linear-time temporal logic LTL. We analyze the complexity of various
model-checking and satisfiability problems for LTL\textsuperscript{mem},
considering various fragments of separation logic (including pointer
arithmetic), various classes of models (with or without constant heap),
and the influence of fixing the initial memory state. We provide a
complete picture based on these criteria. Our main decidability result is
pspace-completeness of the satisfiability problems on the record fragment
and on a classical fragment allowing pointer arithmetic.
\(\Sigma_1^0\)-completeness or \(\Sigma_1^1\)-completeness results are
established for various problems by reducing standard problems for Minsky
machines, and underline the tightness of our decidability results.}
}
@inproceedings{BCDL-formats09,
address = {Budapest, Hungary},
month = sep,
year = 2009,
volume = 5813,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ouaknine, Jo{\"e}l and Vaandrager, Frits},
acronym = {{FORMATS}'09},
booktitle = {{P}roceedings of the 7th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'09)},
author = {Bulychev, Peter and Chatain, {\relax Th}omas and David,
Alexandre and Larsen, Kim G.},
title = {Checking simulation relation between timed game automata},
pages = {73-87},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCDL-formats09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCDL-formats09.pdf},
doi = {10.1007/978-3-642-04368-0_8},
abstract = {In this paper we focus on property-preserving preorders between
timed game automata and their application to control of
partially observable systems. We define timed weak
alternating simulation as a preorder between timed game
automata, which preserves controllability. We define the
rules of building a symbolic turn-based two-player game such
that the existence of a winning strategy is equivalent to
the simulation being satisfied. We also propose an
on-the-fly algorithm for solving this game. This simulation
checking method can be applied to the case of
non-alternating or strong simulations as well. We illustrate
our algorithm by a case study and report on results.}
}
@inproceedings{HP-qest09,
address = {Budapest, Hungary},
month = sep,
year = 2009,
publisher = {{IEEE} Computer Society Press},
acronym = {{QEST}'09},
booktitle = {{P}roceedings of the 6th {I}nternational
{C}onference on {Q}uantitative
{E}valuation of {S}ystems
({QEST}'09)},
author = {Haddad, Serge and Pekergin, Nihal},
title = {Using Stochastic Comparison for Efficient
Model Checking of Uncertain {M}arkov Chains},
pages = {177-186},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HP-qest09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HP-qest09.pdf},
doi = {10.1109/QEST.2009.42},
abstract = {We consider model checking of Discrete Time Markov Chains~(DTMC)
with transition probabilities which are not exactly known but lie in a
given interval. Model checking a Probabilistic Computation Tree
Logic~(PCTL) formula for interval-valued DTMCs~(IMC) has been shown to be
NP hard and co-NP hard. Since the state space of a realistic DTMC is
generally huge, these lower bounds prevent the application of exact
algorithms for such models. Therefore we propose to apply the stochastic
comparison method to check an extended version of PCTL for IMCs. More
precisely, we first design linear time algorithms to quantitatively
analyze IMCs. Then we develop an efficient, semi-decidable PCTL model
checking procedure for IMCs. Furthermore, our procedure returns more
refined answers than traditional ones: YES, NO, DON'T~KNOW. Thus we may
provide useful partial information for modelers in the {"}DON'T~KNOW{"}
case.}
}
@inproceedings{CFLS-esorics09,
address = {Saint~Malo, France},
month = sep,
year = 2009,
volume = 5789,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Backes, Michael and Ning, Peng},
acronym = {{ESORICS}'09},
booktitle = {{P}roceedings of the 14th {E}uropean {S}ymposium on
{R}esearch in {C}omputer {S}ecurity ({ESORICS}'09)},
author = {Centenaro, Matteo and Focardi, Riccardo and
Luccio, Flaminia L. and Steel, Graham},
title = {Type-based Analysis of {PIN} Processing {API}s},
pages = {53-68},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CFLS-esorics09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CFLS-esorics09.pdf},
doi = {10.1007/978-3-642-04444-1_4},
abstract = {We examine some known attacks on the PIN verification framework,
based on weaknesses of the security API for the tamper-resistant Hardware
Security Modules used in the network. We specify this API in an imperative
language with cryptographic primitives, and show how its flaws are
captured by a notion of robustness that extends the one of Myers,
Sabelfeld and Zdancewic to our cryptographic setting. We~propose an
improved API, give an extended type system for assuring integrity and for
preserving confidentiality via randomized and non-randomized encryptions,
and show our new API to be type-checkable.}
}
@inproceedings{CS-esorics09,
address = {Saint~Malo, France},
month = sep,
year = 2009,
volume = 5789,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Backes, Michael and Ning, Peng},
acronym = {{ESORICS}'09},
booktitle = {{P}roceedings of the 14th {E}uropean {S}ymposium on
{R}esearch in {C}omputer {S}ecurity ({ESORICS}'09)},
author = {Cortier, V{\'e}ronique and Steel, Graham},
title = {A~generic security {API} for symmetric key management on
cryptographic devices},
pages = {605-620},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-esorics09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-esorics09.pdf},
doi = {10.1007/978-3-642-04444-1_37},
abstract = {Security APIs are used to define the boundary between trusted
and untrusted code. The security properties of existing APIs are not
always clear. In~this paper, we~give a new generic API for managing
symmetric keys on a trusted cryptographic device. We state and prove
security properties for our API. In~particular, our API offers a high
level of security even when the host machine is controlled by an attacker.
Our API is generic in the sense that it can implement a wide variety of
(symmetric~key) protocols. As a proof of concept, we give an algorithm for
automatically instantiating the API commands for a given key management
protocol. We demonstrate the algorithm on a set of key establishment
protocols from the Clark-Jacob suite.}
}
@article{CAM-jcss09,
publisher = {Elsevier Science Publishers},
journal = {Journal of Computer and System Sciences},
author = {Cautis, Bogdan and Abiteboul, Serge and Milo, Tova},
title = {Reasoning about {XML} update constraints},
month = sep,
year = 2009,
volume = 75,
number = 6,
pages = {336-358},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CAM-jcss09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CAM-jcss09.pdf},
doi = {10.1016/j.jcss.2009.02.001},
abstract = {We introduce in this paper a class of constraints for describing
how an XML document can evolve, namely \emph{XML update
constraints}. For these constraints, we~study the implication
problem, giving algorithms and complexity results for
constraints of varying expressive power. Besides classical
constraint implication, we also consider an instance-based
approach in which we take into account data. More precisely,
we study implication with respect to a current tree
instance, resulting from a series of unknown updates. The
main motivation of our work is reasoning about data
integrity under update restrictions in contexts where owners
may lose control over their data, such as in publishing or
exchange.}
}
@inproceedings{FS-mfcs09,
address = {Novy Smokovec, Slovakia},
month = aug,
year = 2009,
volume = 5734,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Kr{\'a}lovi{\v c}, Rastislav and Niwi{\'n}ski, Damian},
acronym = {{MFCS}'09},
booktitle = {{P}roceedings of the 34th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'09)},
author = {Figueira, Diego and Segoufin, Luc},
title = {Future-looking logics on data words and trees},
pages = {331-343},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-mfcs09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-mfcs09.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FS-mfcs09.ps},
doi = {10.1007/978-3-642-03816-7_29},
abstract = {In a data word or a data tree each position carries a label
from a finite alphabet and a data value from an infinite domain. These
models have been considered in the realm of semistructured data, timed
automata and extended temporal logics.\par
Over data words we consider the logic 1-reg-LTL(\(\textbf{F}\)), that
extends LTL(\(\textbf{F}\)) with one register for storing data values for
later comparisons. We show that satisfiability over data words of
1-reg-LTL(\(\textbf{F}\)) is already not primitive recursive. We also show
that the extension of 1-reg-LTL(\(\textbf{F}\)) with either the reverse
modality \(\textbf{F}^{-1}\) or with one extra register is undecidable.
All those lower bounds were already known for
1-reg-LTL(\(\textbf{X}\),\(\textbf{F}\)) and our results essentially show
that the \(\textbf{X}\) modality was not necessary.\par
Moreover we show that over data trees similar lower bounds hold for
certain fragments of XPATH.}
}
@article{DG-jlc09,
publisher = {Oxford University Press},
journal = {Journal of Logic and Computation},
author = {Demri, St{\'e}phane and Gascon, R{\'e}gis},
title = {The Effects of Bounding Syntactic Resources on {P}resburger
{LTL}},
pages = {1541-1575},
volume = {19},
number = {6},
month = dec,
year = 2009,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DG-jlc09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DG-jlc09.pdf},
doi = {10.1093/logcom/exp037},
abstract = {LTL over Presburger constraints is the extension of LTL where
the atomic formulae are quantifier-free Presburger formulae having as free
variables the counters at different states of the model. This logic is
known to admit undecidable satisfiability and model-checking problems.
We~study decidability and complexity issues for fragments of LTL with
Presburger constraints obtained by restricting the syntactic resources of
the formulae (the number of variables, the maximal distance between two
states for which counters can be compared and, to a smaller extent, the
set of Presburger constraints) while preserving the strength of the
logical operators. We~provide a complete picture refining known results
from the literature. We~show that model-checking and satisfiability
problems for the fragments of LTL with difference constraints restricted
to two variables and distance one and to one variable and distance two are
highly undecidable, enlarging significantly the class of known undecidable
fragments. On the positive side, we prove that the fragment restricted to
one variable and to distance one augmented with propositional variables is
\textsc{pspace}-complete. Since the atomic formulae can state quantitative
properties on the counters, this extends some results about model-checking
pushdown systems and one-counter automata. In~order to establish the
pspace upper bound, we show that the nonemptiness problem for B{\"u}chi
one-counter automata taking values in~\(\mathbb{Z}\) and allowing zero
tests and sign tests, is~only \textsc{nlogspace}-complete. Finally,
we~establish that model-checking one-counter automata with complete
quantifier-free Presburger LTL restricted to one variable is also
\textsc{pspace}-complete whereas the satisfiability problem is
undecidable.}
}
@inproceedings{KAS-arspawits09,
address = {York, UK},
month = aug,
year = 2009,
volume = 5511,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Degano, Pierpaolo and Vigan{\`o}, Luca},
acronym = {{ARSPA-WITS}'09},
booktitle = {{R}evised {S}elected {P}apers of the {J}oint {W}orkshop
on {A}utomated {R}easoning for {S}ecurity {P}rotocol {A}nalysis and
{I}ssues in the {T}heory of {S}ecurity ({ARSPA-WITS}'09)},
author = {Keighren, Gavin and Aspinall, David and Steel, Graham},
title = {Towards a Type System for Security {API}s},
pages = {173-192},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KAS-arspawits09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KAS-arspawits09.pdf},
doi = {10.1007/978-3-642-03459-6_12},
abstract = {Security API analysis typically only considers a subset of an
API's functions, with results bounded by the number of function calls.
Furthermore, attacks involving partial leakage of sensitive information
are usually not covered. Type-based static analysis has the potential to
alleviate these shortcomings. To that end, we present a type system for
secure information flow based upon the one of Volpano, Smith and Irvine,
extended with types for cryptographic keys and ciphertext similar to those
in Sumii and Pierce. In~contrast to some other type systems, the
encryption and decryption of keys does not require special treatment. We
show that a well-typed sequence of commands is non-interferent, based upon
a definition of indistinguishability where, in certain circumstances, the
adversary can distinguish between ciphertexts that correspond to encrypted
public data.}
}
@inproceedings{FS-arspawits09,
address = {York, UK},
month = aug,
year = 2009,
volume = 5511,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Degano, Pierpaolo and Vigan{\`o}, Luca},
acronym = {{ARSPA-WITS}'09},
booktitle = {{R}evised {S}elected {P}apers of the {J}oint {W}orkshop
on {A}utomated {R}easoning for {S}ecurity {P}rotocol {A}nalysis and
{I}ssues in the {T}heory of {S}ecurity ({ARSPA-WITS}'09)},
author = {Fr{\"o}schle, Sibylle and Steel, Graham},
title = {Analysing {PKCS}\#11 Key Management {API}s with Unbounded
Fresh Data},
pages = {92-106},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-arspawits09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-arspawits09.pdf},
doi = {10.1007/978-3-642-03459-6_7},
abstract = {We extend Delaune, Kremer and Steel's framework for analysis of
PKCS#11-based APIs from bounded to unbounded fresh data. We achieve this
by: formally defining the notion of an \emph{attribute policy}; showing
that a well-designed API should have a certain class of policy we call
\emph{complete}; showing that APIs with complete policies may be safely
abstracted to APIs where the attributes are fixed; and proving that these
\emph{static} APIs can be analysed in a small bounded model such that
security properties will hold for the unbounded case. We automate analysis
in our framework using the SAT-based security protocol model checker
SATMC. We show that a symmetric key management subset of the Eracom
PKCS#11 API, used in their ProtectServer product, preserves the secrecy of
sensitive keys for unbounded numbers of fresh keys and \emph{handles},
i.e.~pointers to keys. We also show that this API is not robust: if~an
encryption key is lost to the intruder, SATMC finds an attack whereby all
the keys may be compromised.}
}
@inproceedings{CDK-secret09,
address = {Port Jefferson, New~York, USA},
month = jul,
year = 2009,
editor = {Comon{-}Lundh, Hubert and Meadows, Catherine},
acronym = {{SecReT}'09},
booktitle = {{P}reliminary {P}roceedings of the 4th
{I}nternational {W}orkshop on {S}ecurity and {R}ewriting {T}echniques
({SecReT}'09)},
author = {Ciob{\^a}c{\u{a}}, {\c{S}}tefan and Delaune, St{\'e}phanie and
Kremer, Steve},
title = {Computing knowledge in security protocols under convergent
equational theories},
pages = {47-58},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDK-secret09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDK-secret09.pdf},
abstract = {We propose a procedure for the intruder deduction problem and
for the static equivalence problem, in the case where cryptographic
primitives are modeled by a convergent equational theory. Our~procedure
terminates on a wide range of equational theories. In~particular,
we~obtain a new decidability result for a theory of trapdoor commitment
that we encountered in the study of e-voting protocols. We~also provide a
prototype implementation.}
}
@inproceedings{ACD-secret09,
address = {Port Jefferson, New~York, USA},
month = jul,
year = 2009,
editor = {Comon{-}Lundh, Hubert and Meadows, Catherine},
acronym = {{SecReT}'09},
booktitle = {{P}reliminary {P}roceedings of the 4th
{I}nternational {W}orkshop on {S}ecurity and {R}ewriting {T}echniques
({SecReT}'09)},
author = {Arnaud, Mathilde and Cortier, V{\'e}ronique and
Delaune, St{\'e}phanie},
title = {Modeling and Verifying Ad Hoc Routing Protocol},
pages = {33-46},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACD-secret09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACD-secret09.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ACD-secret09.ps},
abstract = {Mobile ad hoc networks consist of mobile wireless devices which
autonomously organize their infrastructure. In~such a network, a~central
issue, ensured by routing protocols, is to find a route from one device to
another. Those protocols use cryptographic mechanisms in order to prevent
a malicious node from compromising the discovered route.\par
We present a calculus for modeling and reasoning about security protocols,
including in particular secured routing protocols. Our calculus extends
standard symbolic models to take into account the characteristics of
routing protocols and to model wireless communication in a more accurate
way. Then, by using constraint solving techniques, we propose a decision
procedure for analyzing routing protocols for a bounded number of sessions
and for a fixed network topology. We~demonstrate the usage and usefulness
of our approach by analyzing the protocol SRP applied to~DSR.}
}
@inproceedings{KMT-secret09,
address = {Port Jefferson, New~York, USA},
month = jul,
year = 2009,
editor = {Comon{-}Lundh, Hubert and Meadows, Catherine},
acronym = {{SecReT}'09},
booktitle = {{P}reliminary {P}roceedings of the 4th
{I}nternational {W}orkshop on {S}ecurity and {R}ewriting {T}echniques
({SecReT}'09)},
author = {Kremer, Steve and Mercier, Antoine and Treinen, Ralf},
title = {Reducing Equational Theories for the Decision of Static
Equivalence (Preliminary Version)},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KMT-secret09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KMT-secret09.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/KMT-secret09.ps},
abstract = {Static equivalence is a well established notion of
indistinguishability of sequences of terms which is useful in the symbolic
analysis of cryptographic protocols. Static equivalence modulo equational
theories allows a more accurate representation of cryptographic primitives
by modelling properties of operators by equational axioms. We develop a
method that allows in some cases to simplify the task of deciding static
equivalence in a multi-sorted setting, by removing a symbol from the term
signature and reducing the problem to several simpler equational theories.
We illustrate our technique at hand of bilinear pairings.}
}
@article{ACEF-ijfcs09,
publisher = {World Scientific},
journal = {International Journal of Foundations of Computer Science},
author = {Andr{\'e}, {\'E}tienne and Chatain, {\relax Th}omas and
Encrenaz, Emmanuelle and Fribourg, Laurent},
title = {An Inverse Method for Parametric Timed Automata},
volume = 20,
number = 5,
pages = {819-836},
month = oct,
year = 2009,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACEF-ijfcs09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACEF-ijfcs09.pdf},
doi = {10.1142/S0129054109006905},
abstract = {We consider in this paper systems modeled by timed automata. The
timing bounds involved in the action guards and location invariants of our
timed automata are not constants, but parameters. Those parametric timed
automata allow the modelling of various kinds of timed systems,
\textit{e.g.} communication protocols or asynchronous circuits. We will
also assume that we are given an initial tuple~\(\pi_0\) of values for the
parameters, which corresponds to values for which the system is known to
behave properly. Our goal is to compute a constraint~\(K_0\) on the
parameters, satisfied by~\(\pi_0\), guaranteeing that, under any parameter
valuation satisfying~\(K_0\), the system behaves in the same manner: for any
two parameter valuations satisfying~\(K_0\), the behaviors of the timed
automata are (time-abstract) equivalent, \textit{i.e.}, the traces of execution
viewed as alternating sequences of actions and locations are identical. We
present an algorithm \texttt{InverseMethod} that terminates in the case of acyclic
models, and discuss how to extend it in the cyclic case. We also explain
how to combine our method with classical synthesis methods which are based
on the avoidance of a given set of bad states. A prototype implementation
has been done, and various experiments are described.}
}
@techreport{LSV:09:09,
author = {Goubault{-}Larrecq, Jean},
title = {On a Generalization of a Result by {V}alk and {J}antzen},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2009},
month = may,
type = {Research Report},
number = {LSV-09-09},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-09.pdf},
note = {18~pages},
abstract = {We~show that, under mild assumptions on the effective, well
quasi-ordered set~\(X\), one~can compute a finite basis of an
upward-closed subset~\(U\) of~\(X\) if and only if one can decide whether
\(U \cap \downarrow z\) is empty for every \(z \in \widehat{X}\). Here
\(\widehat{X}\) is the completion of \(X\) as defined in Finkel and
Goubault-Larrecq, {\em Forward Analysis for WSTS, Part~{I:} Completions},
STACS'09, pages 433-444, 2009. This generalizes a useful result proved by
Valk and Jantzen in~1985, which is the case \(X = \\mathbb{N}^k\).}
}
@inproceedings{RBH-formats09,
address = {Budapest, Hungary},
month = sep,
year = 2009,
volume = 5813,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ouaknine, Jo{\"e}l and Vaandrager, Frits},
acronym = {{FORMATS}'09},
booktitle = {{P}roceedings of the 7th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'09)},
author = {Bouillard, Anne and Haar, Stefan and Rosario, Sidney},
title = {Critical paths in the Partial Order Unfolding of a
Stochastic {P}etri Net},
pages = {43-57},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-formats09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-formats09.pdf},
doi = {10.1007/978-3-642-04368-0_6},
abstract = {In concurrent real-time processes, the speed of individual
components has a double impact: on the one hand, the overall
latency of a compound process is affected by the latency of
its components. But, if the composition has race conditions,
the very outcome of the process will also depend on the
latency of component processes. Using stochastic Petri nets,
we investigate the probability of a transition occurrence
being critical for the entire process, i.e. such that a
small increase or decrease of the duration of the occurrence
entails an increase or decrease of the total duration of the
process. The first stage of the analysis focuses on
occurrence nets, as obtained by partial order unfoldings, to
determine criticality of events; we then lift to workflow
nets to investigate criticality of transitions inside a
workflow.}
}
@inproceedings{LA-ictac09,
address = {Kuala Lumpur, Malaysia},
month = aug,
year = 2009,
volume = 5684,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Leucker, Martin and Morgan, Carroll},
acronym = {{ICTAC}'09},
booktitle = {{P}roceedings of the 6th {I}nternational {C}olloquium on
{T}heoretical {A}spects of {C}omputing ({ICTAC}'09)},
author = {Longuet, Delphine and Aiguier, Marc},
title = {Integration Testing from Structured First-Order
Specifications via Deduction Modulo},
pages = {261-276},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LA-ictac09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LA-ictac09.pdf},
doi = {10.1007/978-3-642-03466-4_17},
abstract = {Testing from first-order specifications has mainly been studied
for flat specifications, that are specifications of a single software
module. However, the specifications of large software systems are
generally built out of small specifications of individual modules, by
enriching their union. The aim of integration testing is to test the
composition of modules assuming that they have previously been verified,
i.e. assuming their correctness. One of the main method for the selection
of test cases from first-order specifications, called axiom unfolding, is
based on a proof search for the different instances of the property to be
tested, thus allowing the coverage of this property. The idea here is to
use deduction modulo as a proof system for structured first-order
specifications in the context of integration testing, so as to take
advantage of the knowledge of the correctness of the individual modules.}
}
@inproceedings{andre-ictac09,
address = {Kuala Lumpur, Malaysia},
month = aug,
year = 2009,
volume = 5684,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Leucker, Martin and Morgan, Carroll},
acronym = {{ICTAC}'09},
booktitle = {{P}roceedings of the 6th {I}nternational {C}olloquium on
{T}heoretical {A}spects of {C}omputing ({ICTAC}'09)},
author = {Andr{\'e}, {\'E}tienne},
title = {{IMITATOR}: A~Tool for Synthesizing Constraints on Timing
Bounds of Timed Automata},
pages = {336-342},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/andre-ictac09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/andre-ictac09.pdf},
doi = {10.1007/978-3-642-03466-4_22},
abstract = {We present here Imitator, a tool for synthesizing constraints on
timing bounds (seen as parameters) in the framework of timed automata.
Unlike classical synthesis methods, we take advantage of a given reference
valuation of the parameters for which the system is known to behave
properly. Our aim is to generate a constraint such that, under any
valuation satisfying this constraint, the system is guaranteed to behave,
in terms of alternating sequences of locations and actions, as under the
reference valuation. This is useful for safely relaxing some values of the
reference valuation, and optimizing timing bounds of the system. We have
successfully applied our tool to various examples of asynchronous circuits
and protocols.}
}
@inproceedings{BRBH-atpn09,
address = {Paris, France},
month = jun,
year = 2009,
volume = 5606,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Franceschinis, Giuliana and Wolf, Karsten},
acronym = {{PETRI~NETS}'09},
booktitle = {{P}roceedings of the 30th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'09)},
author = {Bouillard, Anne and Rosario, Sidney and
Benveniste, Albert and Haar, Stefan},
title = {Monotonicity in Service Orchestrations},
pages = {263-282},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BRBH-atpn09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BRBH-atpn09.pdf},
doi = {10.1007/978-3-642-02424-5_16},
abstract = {Web Service orchestrations are compositions of different Web
Services to form a new service. The services called during the orchestration
guarantee a given performance to the orchestrater, usually in the form of
contracts.\par
These contracts can be used by the orchestrater to deduce the contract it
can offer to its own clients, by performing contract composition. An
implicit assumption in contract based QoS management is: {"}the better the
component services perform, the better the orchestration's performance
will~be{"}. Thus, contract based QoS management for Web services
orchestrations implicitly assumes monotony.\par
In some orchestrations, however, monotony can be violated, i.e., the
performance of the orchestration improves when the performance of a
component service degrades. This is highly undesirable since it can render
the process of contract composition inconsistent.\par
In this paper we define monotony for orchestrations modelled by Colored
Occurrence Nets (CO-nets) and we characterize the classes of monotonic
orchestrations. We show that few orchestrations are indeed monotonic,
mostly since latency can be traded for quality of data. We also propose a
sound refinement of monotony, called \emph{conditional monotony}, which
forbids this kind of cheating and show that conditional monotony is widely
satisfied by orchestrations. This finding leads to reconsidering the way
SLAs should be formulated.}
}
@inproceedings{BDMR-concur09,
address = {Bologna, Italy},
month = sep,
year = 2009,
volume = 5710,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Bravetti, Mario and Zavattaro, Gianluigi},
acronym = {{CONCUR}'09},
booktitle = {{P}roceedings of the 20th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'09)},
author = {Bouyer, Patricia and Duflot, Marie and Markey, Nicolas and
Renault, Gabriel},
title = {Measuring Permissivity in Finite Games},
pages = {196-210},
doi = {10.1007/978-3-642-04081-8_14},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDMR-concur09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDMR-concur09.pdf},
abstract = {In this paper, we extend the classical notion of strategies in
turn-based finite games by allowing several moves to be selected.
We~define and study a quantitative measure for permissivity of such
strategies by assigning penalties when blocking transitions. We~prove that
for reachability objectives, most permissive strategies exist, can be
chosen memoryless, and can be computed in polynomial time, while it is in
\(\textsf{NP}\cap\textsf{coNP}\) for discounted and mean penalties.}
}
@incollection{EFH-tsmaai09,
author = {El~Fallah Seghrouchni, Amal and Haddad, Serge},
title = {Interop{\'e}rabilit{\'e} des syst{\`e}mes multi-agents
{\`a} l'aide des services web},
booktitle = {Technologies des syst{\`e}mes multi-agents et
applications industrielles},
editor = {El~Fallah Seghrouchni, Amal and Briot, Jean-Pierre},
publisher = {Herm{\`e}s},
year = 2009,
month = apr,
pages = {77-99},
chapter = 3,
url = {http://www.lavoisier.fr/notice/fr2746217850.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 = {}
}
@inproceedings{HKPPT-acc09,
address = {Saint Louis, Missouri, USA},
month = jun,
year = 2009,
acronym = {{ACC}'09},
booktitle = {{P}roceedings of the 28th {A}merican {C}ontrol
{C}onference ({ACC}'09)},
author = {Haddad, Serge and Kordon, Fabrice and Petrucci, Laure and
Pradat{-}Peyre, Jean-Fran{\c{c}}ois and Tr{\`e}ves, Nicolas},
title = {Efficient State-Based Analysis by Introducing Bags in
{P}etri Nets Color Domains},
pages = {5018-5025},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HKPPT-acc09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HKPPT-acc09.pdf},
doi = {10.1109/ACC.2009.5160020},
abstract = {The use of high-level nets, such as coloured Petri nets, is very
convenient for modelling complex controllable systems in order to have a
compact, readable and structured specification. However, when coming to
the analysis phase, using too elaboratc types becomes a burden.\par
A good trade-off between expressivene and analy is capabilities is then to
have only imple types, which is achieved with symmetric nels. These latter
nels enjoy the possibility of generating a symbolic reachability gralph,
which is much smallcr than the whole state space and still allows for
exhaustive analysis.\par
In this paper, we extend the symmetric net model with bags on arcs. Hence,
variables can be bags of tokens,leading to more flexible models. We show
that symmetric nets with bags also allow for applying the symbolic
reachability graph technique with application to deadlock detection and
more generally for safety properties.}
}
@misc{dots-2.2,
author = {Chatain, {\relax Th}omas and Gastin, Paul and Muscholl, Anca
and Sznajder, Nathalie and Walukiewicz, Igor and
Zeitoun, Marc},
title = {Distributed control for restricted specifications},
howpublished = {Deliverable DOTS~2.2 (ANR-06-SETI-003)},
year = 2009,
month = mar
}
@misc{dots-1.2a,
author = {Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois and
Lime, Didier and Markey, Nicolas},
title = {Synthesis of timed controllers},
howpublished = {Deliverable DOTS~1.2a (ANR-06-SETI-003)},
year = 2009,
month = mar
}
@article{DHS-tose09,
publisher = {{IEEE} Computer Society Press},
journal = {IEEE Transactions on Software Engineering},
author = {Donatelli, Susanna and Haddad, Serge and Sproston, Jeremy},
title = {Model Checking Timed and Stochastic Properties with {CSL\textsuperscript{TA}}},
volume = 35,
number = 2,
month = mar # {-} # apr,
year = 2009,
pages = {224-240},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DHS-tose09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DHS-tose09.pdf},
doi = {10.1109/TSE.2008.108},
abstract = {Markov chains are a well-known stochastic process that provide
a balance between being able to adequately model the system's behavior and
being able to afford the cost of the model solution. Systems can be
modelled directly as Markov chains, or with a higher-level formalism for
which Markov chains represent the underlying semantics. Markov chains are
widely used to study the performance of computer and telecommunication
systems. The definition of stochastic temporal logics like Continuous
Stochastic Logic~(CSL) and its variant~asCSL, and of their model-checking
algorithms, allows a unified approach to the verification of systems,
allowing the mix of performance evaluation and probabilistic verification.
\par
In this paper we present the stochastic logic CSL\textsuperscript{TA} ,
which is more expressive than CSL and~asCSL, and in which properties can
be specified using automata (more precisely, timed automata with a single
clock). The extension with respect to expressiveness allows the
specification of properties referring to the probability of a finite
sequence of timed events. A~typical example is the responsiveness property
{"}with probability at least~0.75, a~message sent at time~0 by a
system~\(A\) will be received before time~5 by system~\(B\) and the
acknowledgment will be back at~\(A\) before time~7{"}, a property that
cannot be expressed in either CSL or~asCSL. Furthermore, the choice of
using automata rather than the classical temporal operators Next and Until
should help in enlarging the accessibility of model checking to a larger
public. We~also present a model-checking algorithm
for~CSL\textsuperscript{TA}.}
}
@inproceedings{AFGM-tableaux09,
address = {Oslo, Norway},
month = jul,
year = 2009,
volume = 5607,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Giese, Martin and Waaler, Arild},
acronym = {{TABLEAUX}'09},
booktitle = {{P}roceedings of the 18th {I}nternational
{W}orkshop on {T}heorem {P}roving with
{A}nalytic {T}ableaux and {R}elated {M}ethods
({TABLEAUX}'09)},
author = {Areces, Carlos and Figueira, Diego and Gor{\'\i}n, Daniel
and Mera, Sergio},
title = {Tableaux and Model Checking for Memory Logics},
pages = {47-61},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AFGM-tableaux09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AFGM-tableaux09.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/AFGM-tableaux09.ps},
doi = {10.1007/978-3-642-02716-1_5},
abstract = {Memory logics are modal logics whose semantics is specified in
terms of relational models enriched with additional data structure to
represent memory. The logical language is then extended with a collection
of operations to access and modify the data structure. In~this paper we
study their satisfiability and the model checking problems.\par
We first give sound and complete tableaux calculi for the memory logic
\(ML(k,r,e)\) (the basic modal language extended with the operator \(r\) used
to memorize a state, the operator \(e\) used to wipe out the memory, and the
operator \(k\) used to check if the current point of evaluation is
memorized) and some of its sublanguages. As the satisfiability problem of
\(ML(k,r,e)\) is undecidable, the tableau calculus we present is non
terminating. Hence, we furthermore study a variation that ensures
termination, at the expense of completeness, and we use model checking to
ensure soundness. Secondly, we show that the model checking problem is
PSpace-complete.}
}
@inproceedings{DHL-mbt09,
address = {York, UK},
month = oct,
year = 2009,
number = {2},
volume = {253},
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
acronym = {{MBT}'09},
booktitle = {{P}roceedings of the 5th Workshop on Model-Based Testing
({MBT}'09)},
author = {Dadeau, Fr{\'e}d{\'e}ric and H{\'e}am, Pierre-Cyrille and
Levrey, Jocelyn},
title = {On the Use of Uniform Random Generation of Automata for Testing},
pages = {37-51},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DHL-mbt09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DHL-mbt09.pdf},
doi = {10.1016/j.entcs.2009.09.050 },
abstract = {Developing efficient and automatic testing techniques is one of
the major challenges facing software validation community. In this paper,
we show how a uniform random generation process of finite automata,
developed in a recent work by Bassino and Nicaud, is relevant for many
faces of automatic testing. The main contribution is to show how to
combine two major testing approaches: model-based testing and random
testing. This leads to a new testing technique successfully experimented
on a realistic case study. We also illustrate how the power of random
testing, applied on a Chinese Postman Problem implementation, points out
an error in a well-known algorithm. Finally, we provide some statistics on
model-based testing algorithms.}
}
@inproceedings{CDK-cade09,
address = {Montreal, Canada},
month = aug,
year = 2009,
volume = {5663},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Schmidt, Renate},
acronym = {{CADE}'09},
booktitle = {{P}roceedings of the 22nd {I}nternational
{C}onference on {A}utomated {D}eduction
({CADE}'09)},
author = {Ciob{\^a}c{\u{a}}, {\c{S}}tefan and Delaune, St{\'e}phanie and
Kremer, Steve},
title = {Computing knowledge in security protocols under convergent
equational theories},
pages = {355-370},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDK-cade09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDK-cade09.pdf},
doi = {10.1007/978-3-642-02959-2_27},
abstract = {In the symbolic analysis of security protocols, two classical
notions of knowledge, deducibility and indistinguishability, yield
corresponding decision problems. We~propose a procedure for both problems
under arbitrary convergent equational theories. Our~procedure terminates
on a wide range of equational theories. In~particular, we~obtain a new
decidability result for a theory we encountered when studying electronic
voting protocols. We~also provide a prototype implementation.}
}
@inproceedings{CHK-ciaa09,
address = {Sydney, Australia},
month = jul,
year = 2009,
volume = 5642,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Maneth, Sebastian},
acronym = {{CIAA}'09},
booktitle = {{P}roceedings of the 14th {I}nternational
{C}onference on {I}mplementation and
{A}pplication of {A}utomata
({CIAA}'09)},
author = {Courbis, Rom{\'e}o and H{\'e}am, Pierre-Cyrille and
Kouchnarenko, Olga},
title = {{TAGED} Approximations for Veriying Temporal Patterns},
pages = {135-144},
doi = {10.1007/978-3-642-02979-0_17},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CHK-ciaa09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CHK-ciaa09.pdf},
abstract = {This paper investigates the use of tree automata with global
equalities and disequalities (TAGED for short) in reachability analysis
over term rewriting systems (TRSs). The reachability problem being in
general undecidable on non terminating TRSs, we provide TAGED-based
construction, and then design approximation-based semi-decision procedures
to model-check useful temporal patterns on infinite state rewriting
graphs. To show that the above TAGED-based construction can be effectively
carried out, complexity analysis for rewriting TAGED-definable languages
is given.}
}
@inproceedings{HNS-ciaa09,
address = {Sydney, Australia},
month = jul,
year = 2009,
volume = 5642,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Maneth, Sebastian},
acronym = {{CIAA}'09},
booktitle = {{P}roceedings of the 14th {I}nternational
{C}onference on {I}mplementation and
{A}pplication of {A}utomata
({CIAA}'09)},
author = {H{\'e}am, Pierre-Cyrille and Nicaud, Cyril and Schmitz, Sylvain},
title = {Random Generation of Deterministic Tree (Walking) Automata},
pages = {115-124},
doi = {10.1007/978-3-642-02979-0_15},
url = {http://hal.inria.fr/inria-00408316},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HNS-ciaa09.pdf},
abstract = {Uniform random generators deliver a simple empirical means to
estimate the average complexity of an algorithm. We present a general
rejection algorithm that generates sequential letter-to-letter transducers
up to isomorphism. We tailor this general scheme to randomly generate
deterministic tree walking automata and deterministic top-down tree
automata. We apply our implementation of the generator to the estimation
of the average complexity of a deterministic tree walking automata to
nondeterministic top-down tree automata construction we also implemented.}
}
@inproceedings{BG-dlt09,
address = {Stuttgart, Germany},
month = jun # {-} # jul,
year = 2009,
volume = {5583},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Diekert, Volker and Nowotka, Dirk},
acronym = {{DLT}'09},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onference on {D}evelopments in {L}anguage {T}heory
({DLT}'09)},
author = {Bollig, Benedikt and Gastin, Paul},
title = {Weighted versus Probabilistic Logics},
pages = {18-38},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BG-dlt09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BG-dlt09.pdf},
doi = {10.1007/978-3-642-02737-6_2},
abstract = {While a mature theory around logics such as MSO, LTL, and CTL
has been developed in the pure boolean setting of finite automata,
weighted automata lack such a natural connection with (temporal) logic and
related verification algorithms. In this paper, we will identify weighted
versions of MSO and CTL that generalize the classical logics and even
other quantitative extensions such as probabilistic CTL. We establish
expressiveness results on our logics giving translations from weighted and
probabilistic CTL into weighted MSO.}
}
@inproceedings{AGM-pods09,
address = {Providence, Rhode Island, USA},
month = jun # {-} # jul,
year = 2009,
publisher = {ACM Press},
editor = {Su, Jianwen},
acronym = {{PODS}'09},
booktitle = {{P}roceedings of the 28th {A}nnual
{ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium
on {P}rinciples of {D}atabase {S}ystems
({PODS}'09)},
author = {Abiteboul, Serge and Gottlob, Georg and Manna, Marco},
title = {Distributed {XML} Design},
pages = {247-258},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AGM-pods09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AGM-pods09.pdf},
doi = {10.1145/1559795.1559833},
abstract = {A \emph{distributed XML document} is an XML document that spans
several machines or Web repositories. We assume that a distribution design
of the document tree is given, providing an XML tree some of whose leaves
are {"}docking points{"}, to which XML subtrees can be attached. These
subtrees may be provided and controlled by peers at remote locations, or
may correspond to the result of function calls, e.g., Web services. If a
global type~\(t\), e.g. a DTD, is specified for a distributed
document~\(T\), it~would be most desirable to be able to break this type
into a collection of local types, called a local typing, such that the
document satisfies~\(t\) if and only if each peer (or~function) satisfies
its local type. In this paper we lay out the fundamentals of a theory of
local typing and provide formal definitions of three main variants of
locality: local typing, maximal local typing, and perfect typing, the
latter being the most desirable. We study the following relevant decision
problems: (i)~given a typing for a design, determine whether it is local,
maximal local, or perfect; (ii)~given a design, establish whether a
(maximal) local, or perfect typing does exist. For some of these problems
we provide tight complexity bounds (polynomial space), while for the
others we show exponential upper bounds. A~main contribution is a
polynomial-space algorithm for computing a perfect typing in this context,
if it exists.}
}
@inproceedings{ABM-pods09,
address = {Providence, Rhode Island, USA},
month = jun # {-} # jul,
year = 2009,
publisher = {ACM Press},
editor = {Su, Jianwen},
acronym = {{PODS}'09},
booktitle = {{P}roceedings of the 28th {A}nnual
{ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium
on {P}rinciples of {D}atabase {S}ystems
({PODS}'09)},
author = {Abiteboul, Serge and Bourhis, Pierre and Marinoiu, Bogdan},
title = {Satisfiability and relevance for queries over active documents},
pages = {87-96},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABM-pods09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABM-pods09.pdf},
doi = {10.1145/1559795.1559810},
abstract = {Many Web applications are based on dynamic interactions between
Web components exchanging flows of information. Such a situation arises
for instance in mashup systems or when monitoring distributed autonomous
systems. This is a challenging problem that has generated recently a lot
of attention; see~Web~2.0. For capturing interactions between Web
components, we use active documents interacting with the rest of the world
via streams of updates. Their input streams specify updates to the
document (in the spirit of RSS feeds), whereas their output streams are
defined by queries on the document. In most of the paper, the focus is on
input streams where the updates are only insertions, although we do
consider also deletions. \par
We introduce and study two fundamental concepts in this setting, namely,
satisfiability and relevance. Some fact is \emph{satisfiable} for an
active document and a query if it has a chance to be in the result of the
query in some future state. Given an active document and a query, a call
in the document is \emph{relevant} if the data brought by this call has a
chance to impact the answer to the query. We analyze the complexity of
computing satisfiability in our core model (insertions only) and for
extensions (e.g., with deletions). We also analyze the complexity of
computing relevance in the core model.}
}
@inproceedings{BLPS-pods09,
address = {Providence, Rhode Island, USA},
month = jun # {-} # jul,
year = 2009,
publisher = {ACM Press},
editor = {Su, Jianwen},
acronym = {{PODS}'09},
booktitle = {{P}roceedings of the 28th {A}nnual
{ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium
on {P}rinciples of {D}atabase {S}ystems
({PODS}'09)},
author = {Barcel{\'o}, Pablo and Libkin, Leonid and Poggi, Antonella and
Sirangelo, Cristina},
title = {{XML} with Incomplete Information: Models, Properties, and
Query Answering},
pages = {237-246},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLPS-pods09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLPS-pods09.pdf},
doi = {10.1145/1559795.1559832},
abstract = {We study models of incomplete information for XML, their
computational properties, and query answering. While our approach is
motivated by the study of relational incompleteness, incomplete
information in XML documents may appear not only as null values but also
as missing structural information. Our goal is to provide a classification
of incomplete descriptions of XML documents, and separate features---or
groups of features---that lead to hard computational problems from those
that admit efficient algorithms. Our classification of incomplete
information is based on the combination of null values with partial
structural descriptions of documents. The key computational problems we
consider are consistency of partial descriptions, representability of
complete documents by incomplete ones, and query answering. We show how
factors such as schema information, the presence of node ids, and missing
structural information affect the complexity of these main computational
problems, and find robust classes of incomplete XML descriptions that
permit tractable query evaluation.}
}
@inproceedings{fig-pods09,
address = {Providence, Rhode Island, USA},
month = jun # {-} # jul,
year = 2009,
publisher = {ACM Press},
editor = {Su, Jianwen},
acronym = {{PODS}'09},
booktitle = {{P}roceedings of the 28th {A}nnual
{ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium
on {P}rinciples of {D}atabase {S}ystems
({PODS}'09)},
author = {Figueira, Diego},
title = {Satisfiability of Downward {XP}ath with Data Equality Tests},
pages = {197-206},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/fig-pods09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/fig-pods09.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/fig-pods09.ps},
doi = {10.1145/1559795.1559827},
abstract = {In this work we investigate the satisfiability problem for the
logic \(\textup{XPath}(\downarrow,\downarrow^{*},=)\), that includes all
downward axes as well as equality and inequality tests. We address this
problem in the absence of DTDs and the sibling axis. We prove that this
fragment is decidable, and we nail down its complexity, showing the
problem to be ExpTime-complete. The result also holds when path
expressions allow closure under the Kleene star operator. To obtain these
results, we introduce a new automaton model over data trees that captures
\(\textup{XPath}(\downarrow,\downarrow^*,=)\) and has an ExpTime emptiness
problem. Furthermore, we give the exact complexity of several
downward-looking fragments. }
}
@inproceedings{PS-icalp09,
address = {Rhodes, Greece},
month = jul,
year = 2009,
volume = 5556,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Albers, Susanne and Marchetti-Spaccamela, Alberto and
Matias, Yossi and Thomas, Wolfgang},
acronym = {{ICALP}'09},
booktitle = {{P}roceedings of the 36th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'09)},
author = {Place, {\relax Th}omas and Segoufin, Luc},
title = {A decidable characterization of Locally Testable Tree Languages},
pages = {285-296},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PS-icalp09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PS-icalp09.pdf},
doi = {10.1007/978-3-642-02930-1_24},
abstract = {A regular tree language~\(L\) is locally testable if the
membership of a tree into~\(L\) depends only on the presence or
absence of some neighborhoods in the tree. In~this paper we
show that it is decidable whether a regular tree language is
locally testable.}
}
@inproceedings{FGL-icalp09,
address = {Rhodes, Greece},
month = jul,
year = 2009,
volume = 5556,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Albers, Susanne and Marchetti-Spaccamela, Alberto and
Matias, Yossi and Thomas, Wolfgang},
acronym = {{ICALP}'09},
booktitle = {{P}roceedings of the 36th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'09)},
author = {Finkel, Alain and Goubault{-}Larrecq, Jean},
title = {Forward Analysis for {WSTS}, Part~{II}: Complete {WSTS}},
pages = {188-199},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGL-icalp09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGL-icalp09.pdf},
doi = {10.1007/978-3-642-02930-1_16},
abstract = {We~describe a simple, conceptual forward analysis procedure for
\(\infty\)-complete WSTS~\(\mathcal{S}\). This computes the \emph{clover}
of a state~\(s_0\) , \textit{i.e.}, a~finite description of the closure of
the cover of~\(s_0\) . When \(S\) is the completion of a
WSTS~\(\mathcal{X}\), the clover in~\(\mathcal{S}\) is a finite
description of the cover in~\(\mathcal{X}\). We~show that this applies
exactly when \(\mathcal{X}\) is an \(\omega^2\)-WSTS, a~new robust class
of WSTS. We~show that our procedure terminates in more cases than the
generalized Karp-Miller procedure on extensions of Petri nets. We
characterize the WSTS where our procedure terminates as those that are
\emph{clover-flattable}. Finally, we~apply this to well-structured counter
systems.}
}
@inproceedings{BBBB-icalp09,
address = {Rhodes, Greece},
month = jul,
year = 2009,
volume = 5556,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Albers, Susanne and Marchetti-Spaccamela, Alberto and
Matias, Yossi and Thomas, Wolfgang},
acronym = {{ICALP}'09},
booktitle = {{P}roceedings of the 36th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'09)},
author = {Baier, Christel and Bertrand, Nathalie and Bouyer,
Patricia and Brihaye, {\relax Th}omas},
title = {When are Timed Automata Determinizable?},
pages = {43-54},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBB-icalp09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBB-icalp09.pdf},
doi = {10.1007/978-3-642-02930-1_4},
abstract = {In this paper, we propose an abstract procedure which, given a
timed automaton, produces a language-equivalent deterministic infinite
timed tree. We~prove that under a certain boundedness condition, the
infinite timed tree can be reduced into a classical deterministic timed
automaton. The boundedness condition is satisfied by several subclasses of
timed automata, some of them were known to be determinizable (event-clock
timed automata, automata with integer resets), but some others were not.
We prove for instance that strongly non-Zeno timed automata can be
determinized. As a corollary of those constructions, we get for those
classes the decidability of the universality and of the inclusion
problems, and compute their complexities (the inclusion problem is for
instance EXPSPACE-complete for strongly non-Zeno timed automata).}
}
@inproceedings{BF-icalp09,
address = {Rhodes, Greece},
month = jul,
year = 2009,
volume = 5556,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Albers, Susanne and Marchetti-Spaccamela, Alberto and
Matias, Yossi and Thomas, Wolfgang},
acronym = {{ICALP}'09},
booktitle = {{P}roceedings of the 36th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'09)},
author = {Bouyer, Patricia and Forejt, Vojt{\v e}ch},
title = {Reachability in Stochastic Timed Games},
pages = {103-114},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BF-icalp09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BF-icalp09.pdf},
doi = {10.1007/978-3-642-02930-1_9},
abstract = {We define stochastic timed games, which extend two-player timed
games with probabilities (following a recent approach by Baier
\textit{et~al.}), and which extend in a natural way continuous-time Markov
decision processes. We~focus on the reachability problem for these games,
and ask whether one of the players has a strategy to ensure that the
probability of reaching a fixed set of states is equal~to (or~below,
resp.~above) a~certain number~\(r\), whatever the second player does.
We~show that the problem is undecidable in general, but that it becomes
decidable if we restrict to single-clock 1\(\frac{1}{2}\)-player games and
ask whether the player can ensure that the probability of reaching the set
is~\(=1\) (or~\(>0\),~\(=0\)).}
}
@inproceedings{CD-csf09,
address = {Port Jefferson, New York, USA},
month = jul,
year = 2009,
publisher = {{IEEE} Computer Society Press},
acronym = {{CSF}'09},
booktitle = {{P}roceedings of the
22nd {IEEE} {C}omputer {S}ecurity {F}oundations
{S}ymposium ({CSF}'09)},
author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
title = {A~method for proving observational equivalence},
pages = {266-276},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CD-csf09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CD-csf09.pdf},
doi = {10.1109/CSF.2009.9},
abstract = {Formal methods have proved their usefulness for analyzing the
security of protocols. Most existing results focus on trace properties
like secrecy or authentication. There are however several security
properties, which cannot be defined (or cannot be naturally defined) as
trace properties and require the notion of \emph{observational
equivalence}. Typical examples are anonymity, privacy related properties
or statements closer to security properties used in cryptography.\par
In this paper, we consider the applied pi calculus and we show that for
\emph{determinate} processes, observational equivalence actually coincides
with trace equivalence, a notion simpler to reason with. We~exhibit a
large class of determinate processes, called \emph{simple processes}, that
capture most existing protocols and cryptographic primitives. Then, for
simple processes without replication, we~reduce the decidability of trace
equivalence to deciding an equivalence relation introduced by M.~Baudet.
Altogether, this yields the first decidability result of observational
equivalence for a general class of equational theories.}
}
@inproceedings{CDK-forte09,
address = {Lisbon, Portugal},
month = jun,
year = 2009,
volume = {5522},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Lee, David and Lopes, Ant{\'o}nia and Poetzsch-Heffter, Arnd},
acronym = {{FMOODS/FORTE}'09},
booktitle = {{P}roceedings of {IFIP} {I}nternational {C}onference on {F}ormal
{T}echniques for {D}istributed {S}ystems ({FMOODS/FORTE}'09)},
author = {Chadha, Rohit and Delaune, St{\'e}phanie and
Kremer, Steve},
title = {Epistemic Logic for the Applied Pi Calculus},
pages = {182-197},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/cdk-forte09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/cdk-forte09.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/cdk-forte09.ps},
doi = {10.1007/978-3-642-02138-1_12},
abstract = {We propose an epistemic logic for the applied pi calculus, which
is a variant of the pi calculus with extensions for modeling cryptographic
protocols. In such a calculus, the security guarantees are usually stated
as equivalences. While process calculi provide a natural means to describe
the protocols themselves, epistemic logics are often better suited for
expressing certain security properties such as secrecy and anonymity.\par
We intend to bridge the gap between these two approaches: using the set of
traces generated by a process as models, we define a logic which has
constructs for reasoning about both intruder's epistemic knowledge and the
set of messages in possession of the intruder. As an example we consider
two formalizations of privacy in electronic voting and study the
relationship between them.}
}
@inproceedings{BHKL-ijcai2009,
address = {Pasadena, California, USA},
month = jul,
year = 2009,
publisher = {AAAI Press},
editor = {Boutilier, Craig},
acronym = {{IJCAI}'09},
booktitle = {{P}roceedings of the 21st {I}nternational {J}oint
{C}onference on {A}rtificial {I}ntelligence
({IJCAI}'09)},
author = {Bollig, Benedikt and Habermehl, Peter and Kern, Carsten and
Leucker, Martin},
title = {Angluin-Style Learning of~{NFA}},
pages = {1004-1009},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHKL-ijcai09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHKL-ijcai09.pdf},
abstract = {We introduce NL\(^{*}\), a learning algorithm for inferring
non-deterministic finite-state automata using membership and equivalence
queries. More specifically, residual finite-state automata (RFSA) are
learned similarly as in Angluin's popular L\(^{*}\) algorithm, which,
however, learns deterministic finite-state automata~(DFA). Like in a~DFA,
the~states of an RFSA represent residual languages. Unlike a~DFA, an~RFSA
restricts to prime residual languages, which cannot be described as the
union of other residual languages. In~doing~so, RFSA can be exponentially
more succinct than~DFA. They are, therefore, the preferable choice for
many learning applications. The implementation of our algorithms is
applied to a collection of examples and confirms the expected advantage of
NL\(^{*}\) over L\(^{*}\).}
}
@inproceedings{BCDDH-tacas09,
address = {York, UK},
month = mar,
year = 2009,
volume = {5505},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Kowalewski, Stefan and Philippou, Anna},
acronym = {{TACAS}'09},
booktitle = {{P}roceedings of the 15th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'09)},
author = {Berwanger, Dietmar and Chatterjee, Krishnendu and
De{~}Wulf, Martin and Doyen, Laurent and
Henzinger, {\relax Th}omas~A.},
title = {Alpaga: A~Tool for Solving Parity Games with Imperfect
Information},
pages = {58-61},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCDDH-tacas09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCDDH-tacas09.pdf},
doi = {10.1007/978-3-642-00768-2_7},
abstract = {Alpaga is a solver for two-player parity games with imperfect
information. Given the description of a game, it~determines
whether the first player can ensure to win and, if~so,
it~constructs a winning strategy. The~tool provides a
symbolic implementation of a recent algorithm based on
antichains.}
}
@inproceedings{BCL-rta09,
address = {Bras{\'\i}lia, Brazil},
month = jun # {-} # jul,
year = 2009,
volume = 5595,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Treinen, Ralf},
acronym = {{RTA}'09},
booktitle = {{P}roceedings of the 20th {I}nternational
{C}onference on {R}ewriting {T}echniques
and {A}pplications
({RTA}'09)},
author = {Bursuc, Sergiu and Comon{-}Lundh, Hubert},
title = {Protocol security and algebraic properties: decision results
for a bounded number of sessions},
pages = {133-147},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCL-rta09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCL-rta09.pdf},
doi = {10.1007/978-3-642-02348-4_10},
abstract = {We consider the problem of deciding the security of
cryptographic protocols for a bounded number of sessions, taking into
account some algebraic properties of the security primitives, for instance
Abelian group properties. We propose a general method for deriving
decision algorithms, splitting the task into 4 properties of the rewriting
system describing the intruder capabilities: locality, conservativity,
finite variant property and decidability of one-step deducibility
constraints. We illustrate this method on a non trivial example, combining
several Abelian Group properties, exponentiation and a homomorphism,
showing a decidability result for this combination. }
}
@inproceedings{GJ-rta09,
address = {Bras{\'\i}lia, Brazil},
month = jun # {-} # jul,
year = 2009,
volume = 5595,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Treinen, Ralf},
acronym = {{RTA}'09},
booktitle = {{P}roceedings of the 20th {I}nternational
{C}onference on {R}ewriting {T}echniques
and {A}pplications
({RTA}'09)},
author = {Godoy, Guillem and Jacquemard, Florent},
title = {Unique Normalization for Shallow {TRS}},
pages = {63-77},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-21.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-21.pdf},
doi = {10.1007/978-3-642-02348-4_5},
abstract = {Computation with a term rewrite system (TRS) consists in
the application of its rules from a given starting
term until a normal form is reached, which is
considered the result of the computation.
The unique normalization (UN) property for a TRS~\(R\)
states that
any starting term can reach at most one normal form
when \(R\) is used, i.e. that the computation with R is
unique. \par
We study the decidability of this property
for classes of TRS defined by syntactic restrictions
such as linearity (variables can occur only once in
each side of the rules), flatness (sides of the
rules have depth at most one) and shallowness
(variables occur at depth at most one in the rules).\par
We prove that UN is decidable in polynomial time for
shallow and linear TRS, using tree automata
techniques. This result is very near to the limits
of decidability, since this property is known
undecidable even for very restricted classes like
right-ground TRS, flat TRS and also right-flat and
linear TRS. We also show that that UN is even
undecidable for flat and right-linear TRS. The
latter result is in contrast with the fact that many
other natural properties like reachability,
termination, confluence, weak normalization... are
decidable for this class of TRS.}
}
@inproceedings{BCD-rta09,
address = {Bras{\'\i}lia, Brazil},
month = jun # {-} # jul,
year = 2009,
volume = 5595,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Treinen, Ralf},
acronym = {{RTA}'09},
booktitle = {{P}roceedings of the 20th {I}nternational
{C}onference on {R}ewriting {T}echniques
and {A}pplications
({RTA}'09)},
author = {Baudet, Mathieu and Cortier, V{\'e}ronique and Delaune,
St{\'e}phanie},
title = {{YAPA}: A~generic tool for computing intruder knowledge},
pages = {148-163},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCD-rta09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCD-rta09.pdf},
doi = {10.1007/978-3-642-02348-4_11},
abstract = {Reasoning about the knowledge of an attacker is a necessary step
in many formal analyses of security protocols. In the framework of the
applied pi calculus, as in similar languages based on equational logics,
knowledge is typically expressed by two relations: deducibility and static
equivalence. Several decision procedures have been proposed for these
relations under a variety of equational theories. However, each theory has
its particular algorithm, and none has been implemented so~far.\par
We provide a generic procedure for deducibility and static equivalence
that takes as input any convergent rewrite system. We show that our
algorithm covers all the existing decision procedures for convergent
theories. We also provide an efficient implementation, and compare it
briefly with the more general tool ProVerif.}
}
@article{BHR-fi09,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {Bouyer, Patricia and Haddad, Serge and Reynier, Pierre-Alain},
title = {Undecidability Results for Timed Automata with Silent
Transitions},
year = 2009,
volume = 92,
number = {1-2},
pages = {1-25},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-12.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-12.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2007-12.ps},
abstract = {In this work, we study decision problems related to timed
automata with silent transitions (TA-epsilon) which strictly extend the
expressiveness of timed automata~(TA). First, we answer negatively a
central question raised by the introduction of silent transitions: can we
decide whether the language recognized by a TA-epsilon can be recognized
by some TA? Then we establish in the framework of TA-epsilon some old open
conjectures that O.~Finkel has recently solved for~TA. Its proofs follow a
generic scheme which relies on the fact that only a finite number of
configurations can be reached by a TA while reading a timed word. This
property does not hold for TA-epsilon, the proofs in the framework of
TA-epsilon thus require more elaborated arguments. We~establish
undecidability of complementability, minimization of the number of clocks,
and closure under shuffle. We~also show these results in the framework of
infinite timed languages.}
}
@techreport{LSV:09:02,
author = {Bursuc, Sergiu and Comon{-}Lundh, Hubert},
title = {Protocols, insecurity decision and combination of equational theories},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2009},
month = feb,
type = {Research Report},
number = {LSV-09-02},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-02.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-02.pdf},
note = {43~pages},
abstract = {We consider the problem of finding attacks for a bounded number
of sessions of security protocols. We~contribute to this field, showing
how to decompose the problem into pieces for a class of equational
theories, which includes the hierarchical combinations, as well as
non-hierarchical ones. We apply this result to an electronic purse case
study: we~show the decidability in co-NP of the insecurity problem for a
complex equational theory mixing three Abelian groups, exponentiation and
homomorphism properties.\par
The main technical contributions rely on equational logic, term rewriting
and combination of theories.}
}
@article{BS-tocl08,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Benedikt, Michael and Segoufin, Luc},
title = {Regular tree languages definable in {FO} and in {FO}\(_{\textit{mod}}\)},
volume = 11,
number = 1,
nopages = {},
month = oct,
year = 2009,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-tocl09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-tocl09.pdf},
doi = {10.1145/1614431.1614435},
abstract = {We~consider regular languages of labeled trees. We~give an
effective characterization of the regular languages over such trees that
are definable in first-order logic in the language of labeled graphs.
These languages are the analog on trees of the {"}locally threshold
testable{"} languages on strings. We~show that this characterization yields
a decision procedure for determining whether a regular tree language is
first-order definable: the~procedure is polynomial time in the minimal
automaton presenting the regular language. We~also provide an algorithm
for deciding whether a regular language is definable in first-order logic
supplemented with modular quantifiers.}
}
@misc{Quasimodo-3.1,
author = {Bouyer, Patricia and Katoen, Joost-Pieter and
Langerak, Rom and Laroussinie, Fran{\c{c}}ois and
Markey, Nicolas and Raskin, Jean-Fran{\c{c}}ois},
title = {Transfer of correctness from models to implementation},
howpublished = {Deliverable QUASIMODO~3.1 (ICT-FP7-STREP-214755)},
year = 2009,
month = jan
}
@inproceedings{JKV-lata09,
address = {Tarragona, Spain},
month = apr,
year = 2009,
volume = 5457,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Dediu, Adrian Horia and Mihai Ionescu, Armand and Mart{\'\i}n-Vide, Carlos},
acronym = {{LATA}'09},
booktitle = {{P}roceedings of the 3rd {I}nternational {C}onference on {L}anguage
and {A}utomata {T}heory and {A}pplications ({LATA}'09)},
author = {Jacquemard, Florent and Klay, Francis and Vacher, Camille},
title = {Rigid Tree Automata},
pages = {446-457},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JKV-lata09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JKV-lata09.pdf},
doi = {10.1007/978-3-642-00982-2_38},
abstract = {We introduce the class of Rigid Tree Automata (RTA), an
extension of standard bottom-up automata on ranked trees with
distinguished states called rigid. Rigid states define a restriction on
the computation of RTA on trees: RTA can test for equality in subtrees
reaching the same rigid state. RTA are able to perform local and global
tests of equality between subtrees, non-linear tree pattern matching, and
restricted disequality tests as well. Properties like determinism, pumping
lemma, boolean closure, and several decision problems are studied in
detail. In particular, the emptiness problem is shown decidable in linear
time for RTA whereas membership of a given tree to the language of a given
RTA is NP-complete. Our main result is the decidability of whether a given
tree belongs to the rewrite closure of a RTA language under a restricted
family of term rewriting systems, whereas this closure is not a RTA
language. This result, one of the first on rewrite closure of languages of
tree automata with constraints, is enabling the extension of model
checking procedures based on finite tree automata techniques. Finally, a
comparison of RTA with several classes of tree automata with local and
global equality tests, and with dag automata is also provided.}
}
@phdthesis{bouyer-hab2009,
author = {Bouyer, Patricia},
title = {From Qualitative to Quantitative Analysis of Timed Systems},
school = {Universit{\'e} Paris~7, Paris, France},
type = {M{\'e}moire d'habilitation},
year = 2009,
month = jan,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PB-hdr09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PB-hdr09.pdf}
}
@incollection{GMN-pct08,
futureaddress = {},
month = jan,
year = 2009,
series = {IARCS-Universities},
publisher = {Universities Press},
booktitle = {Perspectives in Concurrency Theory},
editor = {Lodaya, Kamal and Mukund, Madhavan and
Ramanujam, R.},
author = {Gastin, Paul and Mukund, Madhavan and Narayan Kumar, K.},
title = {Reachability and boundedness in time-constrained {MSC} graphs},
pages = {157-183},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GMN-pct08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GMN-pct08.pdf},
abstract = {Channel boundedness is a necessary condition for a
message-passing system to exhibit regular, finite-state behaviour at the
global level. For Message Sequence Graphs~(MSGs), the most basic form of
High-level Message Sequence Charts~(HMSCs), channel boundedness can be
characterized in terms of structural conditions on the underlying graph.
We consider MSGs enriched with timing constraints between events. These
constraints restrict the global behaviour and can impose channel
boundedness even when it is not guaranteed by the graph structure of the
MSG. We~show that we can use MSGs with timing constraints to simulate
computations of a two-counter machine. As~a consequence, even the more
fundamental problem of reachability, which is trivial for untimed MSGs,
becomes undecidable when we add timing constraints. Different forms of
channel boundedness also then turn out to be undecidable, using reductions
from the reachability problem.}
}
@incollection{BP-pct08,
futureaddress = {},
month = jan,
year = 2009,
series = {IARCS-Universities},
publisher = {Universities Press},
booktitle = {Perspectives in Concurrency Theory},
editor = {Lodaya, Kamal and Mukund, Madhavan and
Ramanujam, R.},
author = {Bouyer, Patricia and Petit, Antoine},
title = {On extensions of timed automata},
pages = {35-63},
abstract = {Since their definition in the early nineties, timed automata have
been one of the most used and widely studied models for
representing and analyzing real-time systems. In their seminal
paper, Alur and Dill proved the probably most important property
of timed automata: checking emptiness of the language accepted by
a timed automaton, or equivalently checking a reachability
property in a timed automaton, is decidable. This result relies on
the construction of the so-called region automaton, which
abstracts behaviours of a timed automaton into behaviours of a
finite automaton. Since then, symbolic algorithms have been
developed to solve that problem, several model-checkers have been
implemented, and numerous case studies have been verified.\par
Lots of works have naturally aimed at proposing extensions of
timed automata with new features, while preserving the
above-mentioned fundamental decidability result. The motivation
for these extensions is basically twofold. First it can increase the
expressiveness of timed automata, allowing to model larger classes
of systems. Then it can improve the conciseness (and hence the
readability) of models by constructing more compact
representations for a given system.\par
In this paper, we discuss and compare some of the most important
extensions of timed automata that have been considered in the
literature.}
}
@inproceedings{BBL-Fossacs09,
address = {York, UK},
month = mar,
year = 2009,
volume = 5504,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {de Alfaro, Luca},
acronym = {{FoSSaCS}'09},
booktitle = {{P}roceedings of the 12th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'09)},
author = {Bansal, Kshitij and Brochenin, R{\'e}mi and
Lozes, {\'E}tienne},
title = {Beyond Shapes: Lists with Ordered Data},
pages = {425-439},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBL-fossacs09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBL-fossacs09.pdf},
doi = {10.1007/978-3-642-00596-1_30},
abstract = {Standard analysis on recursive data structures restrict their
attention to shape properties (for instance, a program that manipulates a
list returns a list), excluding properties that deal with the actual
content of these structures. For instance, these analysis would not
establish that the result of merging two ordered lists is an ordered list.
Separation logic, one of the prominent framework for these kind of
analysis, proposed a heap model that could represent data, but, to our
knowledge, no predicate dealing with data has ever been integrated to the
logic while preserving decidability. We~establish decidability for
(first-order) separation logic with a predicate that allows to compare two
successive data in a list. We~then consider the extension where two data
in arbitrary positions may be compared, and establish the undecidability
in general. We~define a guarded fragment that turns out to be both
decidable and sufficiently expressive to prove the preservation of the
loop invariant of a standard program merging ordered lists. We~finally
consider the extension with the magic-wand and prove that, by constrast
with the data-free case, even a very restricted use of the magic wand
already introduces undecidability.}
}
@article{GSZ-fmsd09,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Gastin, Paul and Sznajder, Nathalie and Zeitoun, Marc},
title = {Distributed synthesis for well-connected
architectures},
volume = 34,
number = 3,
pages = {215-237},
month = jun,
year = 2009,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GSZ-fmsd09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GSZ-fmsd09.pdf},
doi = {10.1007/s10703-008-0064-7},
abstract = {We study the synthesis problem for external linear or branching
specifications and distributed, synchronous architectures with arbitrary
delays on processes. External means that the specification only relates
input and output variables. We introduce the subclass of uniformly
well-connected (UWC) architectures for which there exists a routing
allowing each output process to get the values of all inputs it is
connected to, as soon as possible. We prove that the distributed synthesis
problem is decidable on UWC architectures if and only if the output
variables are totally ordered by their knowledge of input variables. We
also show that if we extend this class by letting the routing depend on
the output process, then the previous decidability result fails. Finally,
we provide a natural restriction on specifications under which the whole
class of UWC architectures is decidable.}
}
@proceedings{KP-secco2008,
title = {{P}roceedings of the 6th {I}nternational {W}orkshop on
{S}ecurity {I}ssues in {C}oncurrency ({S}ec{C}o'08)},
booktitle = {{P}roceedings of the 6th {I}nternational {W}orkshop on
{S}ecurity {I}ssues in {C}oncurrency ({S}ec{C}o'08)},
editor = {Kremer, Steve and Panangaden, Prakash},
publisher = {Elsevier Science Publishers},
doi = {10.1016/j.entcs.2009.07.077},
url = {http://www.sciencedirect.com/science/journal/15710661/242/3},
series = {Electronic Notes in Theoretical Computer Science},
volume = 242,
number = 3,
year = 2009,
month = aug,
address = {Toronto, Canada}
}
@article{BCK-IC09,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Baudet, Mathieu and Cortier, V{\'e}ronique and Kremer, Steve},
title = {Computationally Sound Implementations of Equational Theories
against Passive Adversaries},
year = {2009},
month = apr,
volume = 207,
number = 4,
pages = {496-520},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCK-ic09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCK-ic09.pdf},
doi = {10.1016/j.ic.2008.12.005},
abstract = {In~this paper we study the link between formal and cryptographic
models for security protocols in the presence of passive adversaries.
In~contrast to other works, we~do not consider a fixed set of primitives
but aim at results for arbitrary equational theories. We~define a
framework for comparing a cryptographic implementation and its
idealization with respect to various security notions. In~particular, we
concentrate on the computational soundness of static equivalence, a
standard tool in cryptographic pi calculi. We~present a soundness
criterion, which for many theories is not only sufficient but also
necessary. Finally, to~illustrate our framework, we~establish the
soundness of static equivalence for the exclusive OR and a theory of
ciphers and lists.}
}
@inproceedings{BH-Fossacs09,
address = {York, UK},
month = mar,
year = 2009,
volume = 5504,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {de Alfaro, Luca},
acronym = {{FoSSaCS}'09},
booktitle = {{P}roceedings of the 12th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'09)},
author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge},
title = {Interrupt Timed Automata},
pages = {197-211},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BH-fossacs09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BH-fossacs09.pdf},
doi = {10.1007/978-3-642-00596-1_15},
abstract = {In this work, we introduce the class of Interrupt Timed Automata
(ITA), which are well suited to the description of multi-task systems with
interruptions in a single processor environment. This model is a subclass
of hybrid automata. While reachability is undecidable for hybrid automata
we show that in ITA the reachability problem is in 2EXPSPACE and in PSPACE
when the number of clocks is fixed, with a procedure based on a
generalized class graph. Furthermore we consider a subclass ITA\(_{-}\)
which still describes usual interrupt systems and for which the
reachability problem is in NEXPTIME and in NP when the number of clocks is
fixed (without any class graph). There exist languages accepted by an
ITA\(_{-}\) but neither by timed automata nor by controlled real-time
automata (CRTA), another extension of timed automata. However we
conjecture that CRTA is not contained in ITA. So, we combine ITA with CRTA
in a model which encompasses both classes and show that the reachability
problem is still decidable.}
}
@inproceedings{BGH-Fossacs09,
address = {York, UK},
month = mar,
year = 2009,
volume = 5504,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {de Alfaro, Luca},
acronym = {{FoSSaCS}'09},
booktitle = {{P}roceedings of the 12th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'09)},
author = {Bollig, Benedikt and Grindei, Manuela-Lidia and
Habermehl, Peter},
title = {Realizability of Concurrent Recursive Programs},
pages = {410-424},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGH-fossacs09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGH-fossacs09.pdf},
doi = {10.1007/978-3-642-00596-1_29},
abstract = {We define and study an automata model of concurrent recursive
programs. An~automaton consists of a finite number of pushdown systems
running in parallel and communicating via shared actions. Actually, we
combine multi-stack visibly pushdown automata and Zielonka's asynchronous
automata towards a model with an undecidable emptiness problem. However, a
reasonable restriction allows us to lift Zielonka's Theorem to this
recursive setting and permits a logical characterization in terms of a
suitable monadic second-order logic. Building on results from Mazurkiewicz
trace theory and work by La~Torre, Madhusudan, and Parlato, we thus develop
a framework for the specification, synthesis, and verification of concurrent
recursive processes.}
}
@inproceedings{FGL-stacs2009,
address = {Freiburg, Germany},
month = feb,
year = 2009,
volume = 3,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Albers, Susanne and Marion, Jean-Yves},
acronym = {{STACS}'09},
booktitle = {{P}roceedings of the 26th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'09)},
author = {Finkel, Alain and Goubault{-}Larrecq, Jean},
title = {Forward Analysis for~{WSTS}, Part~{I}: Completions},
pages = {433-444},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGL-stacs2009.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGL-stacs2009.pdf},
abstract = {Well-structured transition systems provide the right foundation
to compute a finite basis of the set of predecessors of the upward closure
of a state. The~dual problem, to compute a finite representation of the
set of successors of the downward closure of a state, is~harder: Until
now, the theoretical framework for manipulating downward-closed sets was
missing. We~answer this problem, using insights from domain theory (dcpos
and ideal completions), from topology (sobrifications), and shed new light
on the notion of adequate domains of limits.}
}
@inproceedings{CGS-sofsem09,
address = {\v{S}pindler\r{u}v Ml\'{y}n, Czech Republic},
month = jan,
year = 2009,
volume = 5404,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Nielsen, Mogens and Ku{\v c}era, Anton{\'\i}n and Bro
Miltersen, Peter and Palamidessi, Catuscia and T{\r{u}}ma,
Petr and Valencia, Franck},
acronym = {{SOFSEM}'09},
booktitle = {{P}roceedings of the 35th International Conference on
Current Trends in Theory and Practice of
Computer Science ({SOFSEM}'09)},
author = {Chatain, {\relax Th}omas and Gastin, Paul and Sznajder, Nathalie},
title = {Natural Specifications Yield Decidability for Distributed
Synthesis of Asynchronous Systems},
pages = {141-152},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CGS-sofsem09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CGS-sofsem09.pdf},
doi = {10.1007/978-3-540-95891-8_16},
abstract = {We study the synthesis problem in an asynchronous distributed
setting: a finite set of processes interact locally with an uncontrollable
environment and communicate with each other by sending signals---actions
that are immediately received by the target process. The synthesis problem
is to come up with a local strategy for each process such that the
resulting behaviours of the system meet a given specification. We consider
external specifications over partial orders. External means that
specifications only relate input and output actions from and to the
environment and not signals exchanged by processes. We also ask for some
closure properties of the specification. We present this new setting for
studying the distributed synthesis problem, and give decidability results:
the non-distributed case, and the subclass of networks where communication
happens through a strongly connected graph. We believe that this framework
for distributed synthesis yields decidability results for many more
architectures.}
}
@inproceedings{BDLM-lfcs09,
address = {Deerfield Beach, Florida, USA},
month = jan,
year = 2009,
volume = 5407,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Artemov, Sergei N. and Nerode, Anil},
notefortitle = {6th edition of the conference},
acronym = {{LFCS}'09},
booktitle = {{P}roceedings of the {S}ymposium on {L}ogical {F}oundations of
{C}omputer {S}cience ({LFCS}'09)},
author = {Brihaye, {\relax Th}omas and Da{~}Costa, Arnaud and
Laroussinie, Fran{\c{c}}ois and
Markey, Nicolas},
title = {{ATL}~with Strategy Contexts and Bounded Memory},
pages = {92-106},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDLM-lfcs09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDLM-lfcs09.pdf},
doi = {10.1007/978-3-540-92687-0_7},
abstract = {We extend the alternating-time temporal logics ATL
and ATL\textsuperscript{*} with \emph{strategy contexts} and
\emph{memory constraints}: the first extension make strategy
quantifiers to not {"}forget{"} the strategies being executed by
the other players. The second extension allows strategy
quantifiers to restrict to memoryless or bounded-memory
strategies.\par
We first consider expressiveness issues. We show that our logics
can express important properties such as equilibria, and we
formally compare them with other similar formalisms (ATL,
ATL\textsuperscript{*}, Game Logic, Strategy Logic,~...).
We~then address the problem of model-checking for our logics,
providing a PSPACE algoritm for the sublogics involving only
memoryless strategies and an EXPSPACE algorithm for the
bounded-memory case.}
}
@inproceedings{steel-escar09,
address = {D{\"u}sseldorf, Germany},
month = nov,
year = 2009,
editor = {Paar, Christof and Wollinger, Thomas},
acronym = {{ESCAR}'09},
booktitle = {{P}roceedings of the 7th
{C}onference on {E}mbedded {S}ecurity in {C}ars
({ESCAR}'09)},
author = {Steel, Graham},
title = {Towards a Formal Analysis of the {S}e{V}e{C}o{M}~{API}},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/steel-escar09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/steel-escar09.pdf}
}
@inproceedings{steel-fcc09,
address = {Port Jefferson, New York, USA},
month = jul,
year = 2009,
editor = {K{\"u}sters, Ralf},
acronym = {{FCC}'09},
booktitle = {{P}roceedings of the 5th {W}orkshop on {F}ormal and
{C}omputational {C}ryptography ({FCC}'09)},
author = {Steel, Graham},
title = {Computational Soundness for {API}s},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/steel-fcc09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/steel-fcc09.pdf}
}
@inproceedings{LS-DL09,
address = {Oxford, UK},
month = jul,
year = 2009,
volume = 477,
series = {CEUR Workshop Proceedings},
publisher = {RWTH Aachen, Germany},
editor = {Cuenca Grau, Bernardo and Horrocks, Ian and Motik, Boris and Sattler, Ulrike },
acronym = {{DL}'09},
booktitle = {{P}roceedings of the 22nd {I}nternational
{W}orkshop {D}escription {L}ogic ({DL}'09)},
author = {Libkin, Leonid and Sirangelo, Cristina},
title = {Open and closed world assumptions in data exchange},
pages = {1-6},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-DL09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-DL09.pdf}
}
@inproceedings{BFCH-dsn09,
address = {Estoril, Portugal},
month = jun # {-} # jul,
year = 2009,
publisher = {{IEEE} Computer Society Press},
noeditor = {},
acronym = {{DSN}'09},
booktitle = {{P}roceedings of the 39th {A}nnual {IEEE}{\slash}{IFIP}
{I}nternational {C}onference on {D}ependable {S}ystems and
{N}etworks ({DSN}'09)},
author = {Beccuti, Marco and Franceschinis, Giuliana and
Codetta{-}Raiteri, Daniele and Haddad, Serge},
title = {Parametric {NdRFT} for the derivation of optimal repair
strategies},
pages = {399-408},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFCH-dsn09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFCH-dsn09.pdf},
doi = {10.1109/DSN.2009.5270312},
abstract = {Non deterministic Repairable Fault Trees~(NdRFT) are a recently
proposed modeling formalism for the study of optimal repair strategies:
they are based on the widely adopted Fault Tree formalism, but in addition
to the failure modes, NdRFTs allow to define possible repair actions. In a
previous pa per the formalism has been introduced together with an
analysis method and a tool allowing to automatically derive the best
repair strategy to be applied in each state. The analysis technique is
based on the generation and solution of a Markov Decision Process. In this
paper we present an extension, ParNdRFT, that allows to exploit the
presence of redundancy to reduce the complexity of the model and of the
analysis. It is based on the translation of the ParNdRFT in to a Markov
Decision Well-Formed Net, i.e. a model specified by means of an High Level
Petri Net formalism. The translated model can be efficiently solved thanks
to existing algorithms that generate a reduced state space automatically
exploiting the model symmetries.}
}
@article{ASV-tods09,
publisher = {ACM Press},
journal = {ACM Transactions on Database Systems},
author = {Abiteboul, Serge and Segoufin, Luc and Vianu, Victor},
title = {Static Analysis of {A}ctive {XML} Systems},
volume = 34,
number = 4,
month = dec,
year = 2009,
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ASV-tods09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ASV-tods09.pdf},
doi = {10.1145/1620585.1620590},
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, and so may
activate new subtasks. The focus of this article is on the verification of
temporal properties of runs of Active XML systems, specified in a
tree-pattern-based temporal logic, Tree-LTL, which 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.}
}
@article{BMSS-jacm09,
publisher = {ACM Press},
journal = {Journal of the~{ACM}},
author = {Boja{\'n}czyk, Miko{\l}aj and Muscholl, Anca and
Schwentick, {\relax Th}omas and Segoufin, Luc},
title = {Two-variable logic on data trees and applications to {XML}
reasoning},
volume = 56,
number = 3,
month = may,
year = 2009,
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMSS-jacm09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMSS-jacm09.pdf},
doi = {10.1145/1516512.1516515},
abstract = {Motivated by reasoning tasks for XML languages, the
satisfiability problem of logics on \emph{data trees} is investigated. The
nodes of a data tree have a \emph{label} from a finite set and a
\emph{data value} from a possibly infinite set. It is shown that
satisfiability for two-variable first-order logic is decidable if the tree
structure can be accessed only through the \emph{child} and the \emph{next
sibling} predicates and the access to data values is restricted to
equality tests. From this main result, decidability of satisfiability and
containment for a data-aware fragment of XPath and of the implication
problem for unary key and inclusion constraints is concluded.}
}
@article{BS-jsl09,
publisher = {Association for Symbolic Logic},
journal = {Journal of Symbolic Logic},
author = {Benedikt, Michael and Segoufin, Luc},
title = {Towards a Characterization of Order-Invariant Queries over
Tame Structures},
volume = 74,
number = 1,
pages = {168-186},
month = mar,
year = 2009,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-jsl09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-jsl09.pdf},
doi = {10.2178/jsl/1231082307},
abstract = {This work deals with the expressive power of logics on finite
graphs with access to an additional {"}arbitrary{"} linear order. The
queries that can be expressed this way are the \emph{order-invariant
queries} for the logic. For the standard logics used in computer science,
such as first-order logic, it is known that access to an arbitrary linear
order increases the expressiveness of the logic. However, when we look at
the separating examples, we find that they have satisfying models whose
Gaifman Graph is complex---unbounded in valence and in treewidth. We thus
explore the expressiveness of order-invariant queries over well-behaved
graphs. We prove that first-order order-invariant queries over strings and
trees have no additional expressiveness over first-order logic in the
original signature. We also prove new upper bounds on order-invariant
queries over bounded treewidth and bounded valence graphs. Our results
make use of a new technique of independent interest: the application of
algebraic characterizations of definability to show collapse results.}
}
@incollection{DBBetal-CES09,
author = {David, Alexandre and Behrmann, Gerd and Bulychev, Peter and
Byg, Joakin and Chatain, {\relax Th}omas and Larsen, Kim G.
and
Pettersson, Paul and Rasmussen, Jacob Illum and
Srba, Ji{\v{r}}{\'\i} and
Yi, Wang and Joergensen, Kenneth Y. and Lime, Didier and
Magnin, Morgan and Roux, Olivier H. and Traonouez, Louis-Marie},
title = {Tools for Model-Checking Timed Systems},
booktitle = {Communicating Embedded Systems~-- Software and Design},
editor = {Jard, Claude and Roux, Olivier H.},
publisher = {Wiley-ISTE},
year = 2009,
month = oct,
pages = {165-225},
chapter = 6,
url = {http://www.iste.co.uk/index.php?f=x&ACTION=View&id=288},
nops = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/.ps},
nopsgz = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PSGZ/.ps.gz},
isbn = {9781848211438}
}
@misc{avote-D21,
nocontributor = {Ciob{\^a}c{\u{a}}, {\c{S}}tefan and Delaune,
St{\'e}phanie and Kremer, Steve},
author = {Ciob{\^a}c{\u{a}}, {\c{S}}tefan and Cortier, V{\'e}ronique},
title = {Algorithmes pour l'{\'e}quivalence statique},
year = 2009,
month = sep,
type = {Contract Report},
howpublished = {Deliverable AVOTE~2.1 (ANR-07-SESU-002)},
note = {17~pages},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/avote-d21.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/avote-d21.pdf}
}
@inproceedings{BBJ-iscc09,
address = {Sousse, Tunisia},
month = jul,
year = 2009,
publisher = {{IEEE} Computer Society Press},
noeditor = {},
acronym = {{ISCC}'09},
booktitle = {{P}roceedings of the 14th {IEEE} {S}ymposium on {C}omputers and
{C}ommunications ({ISCC}'09)},
author = {Ben Youssef, Nihel and Bouhoula, Adel and Jacquemard,
Florent},
title = {Automatic Verification of Conformance of Firewall
Configurations to Security Policies},
pages = {526 - 531},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBJ-iscc09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBJ-iscc09.pdf},
doi = {10.1109/ISCC.2009.5202309},
abstract = {The configuration of firewalls is highly error prone and
automated solution are needed in order to analyze its
correctness. We propose a formal and automatic method for
checking whether a firewall reacts correctly with respect to
a security policy given in an high level declarative
language. When errors are detected, some feedback is
returned to the user in order to correct the firewall
configuration. Furthermore, the procedure verifies that no
conflicts exist within the security policy. We show that our
method is both correct and complete. Finally, it has been
implemented in a prototype of verifier based on a
satisfiability solver modulo theories (SMT). Experiment
conducted on relevant case studies demonstrate the
efficiency and scalability of the approach.}
}
@misc{averiles09-f2.2,
author = {LIAFA and CRIL and EDF and LSV and Verimag},
title = {Projet {RNTL} {A}veriles~-- Fourniture F2.2~: Algorithmes de
v{\'e}rification~-- Rapport final},
year = 2009,
month = nov,
type = {Contract Report},
note = {25~pages},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/averiles-f22.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/averiles-f22.pdf}
}
@inproceedings{haar-cdcccc09,
address = {Shanghai, China},
month = dec,
year = 2009,
publisher = {{IEEE} Control System Society},
acronym = {{CDC/CCC}'09},
booktitle = {{P}roceedings of the Joint 48th {IEEE} {C}onference on {D}ecision
and {C}ontrol ({CDC}'09) and 28th {C}hinese {C}ontrol {C}onference ({CCC}'09)},
author = {Haar, Stefan},
title = {Qualitative Diagnosability of Labeled {P}etri Nets Revisited},
pages = {1248-1253},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-cdc09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-cdc09.pdf},
doi = {10.1109/CDC.2009.5400917},
abstract = {In recent years, classical discrete event fault diagnosis
techniques have been extended to Petri Net system models under partial
order semantics. In~a recent paper, we showed how to take further
advantage of the partial order representation of concurrent processes, by
decomposing the unfolding into 'facets', formed by subnets whose events
either all occur eventually, or none of them occurs. A~notion of
\emph{q(ualitative)}-diagnosability was proposed based on this
decomposition. The present paper corrects the definition of
q-diagnosability and develops its properties. Sufficient and necessary
criteria, on the transition labeling, for q-diagnosability are shown; for
their verification, and diagnosis itself, compact data structures are
sufficient.}
}
@misc{Quasimodo-3.5,
author = {Laroussinie, Fran{\c{c}}ois and Vaandrager, Frits and
Neuh{\"a}u{\ss}er, Martin},
title = {Extended timed automata for scheduling},
howpublished = {Deliverable QUASIMODO~3.5 (ICT-FP7-STREP-214755)},
year = 2009,
month = jul
}
@misc{Quasimodo-2.2,
author = {Markey, Nicolas and Berendsen, Jasper
and David, Alexandre and Han, Tingting and
Hermanns, Holger and Larsen, Kim G. and Neuh{\"a}u{\ss}er, Martin},
title = {Symbolic data structures and analysis of models
with multiple quantitative aspects},
howpublished = {Deliverable QUASIMODO~2.2 (ICT-FP7-STREP-214755)},
year = 2009,
month = jul
}
@inproceedings{ABGM-time09,
address = {Brixen-Bressanone, Italy},
month = jul,
year = 2009,
publisher = {{IEEE} Computer Society Press},
noeditor = {Lutz, Carsten and Raskin, Jean-Fran{\c{c}}ois},
acronym = {{TIME}'09},
booktitle = {{P}roceedings of the 16th {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'09)},
title = {The {AXML} Artifact Model},
author = {Abiteboul, Serge and Bourhis, Pierre and Galland, Alban and
Marinoiu, Bogdan},
pages = {11-17},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGM-time09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGM-time09.pdf},
abstract = {Towards a data-centric workflow approach, we introduce an
\emph{artifact model} to capture data and workflow management activities
in distributed settings. The model is built on Active XML, \textit{i.e.},
XML trees including Web service calls. We argue that the model captures
the essential features of business artifacts as described informally in
[Nigam and Caswell~(2003)] or discussed in [Hull~(2008)]. To illustrate,
we briefly consider the \emph{monitoring} of distributed systems and the
\emph{verification} of temporal properties for them.}
}
@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.