@inproceedings{BFLM-hscc10,
address = {Stockholm, Sweden},
month = apr,
year = 2010,
publisher = {ACM Press},
editor = {Johansson, Karl Henrik and Yi, Wang},
acronym = {{HSCC}'10},
booktitle = {{P}roceedings of the 13th {I}nternational {C}onference
on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
({HSCC}'10)},
author = {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim G.
and Markey, Nicolas},
title = {Timed Automata with Observers under Energy Constraints},
pages = {61-70},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLM-hscc10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLM-hscc10.pdf},
doi = {10.1145/1755952.1755963},
abstract = {In this paper, we study one-clock priced timed automata in which
prices can grow linearly (\(\frac{dp}{dt}=k\)) or exponentially
(\(\frac{dp}{dt}=kp\)), with discontinuous updates on edges. We propose
EXPTIME algorithms to decide the existence of controllers that ensure
existence of infinite runs or reachability of some goal location with
non-negative observer value all along the run. These algorithms consist in
computing the optimal delays that should be elapsed in each location along
a run, so that the final observer value is maximized (and never goes below
zero).}
}
@inproceedings{VLC-tacas10,
address = {Paphos, Cyprus},
month = mar,
year = 2010,
volume = {6015},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Esparza, Javier and Majumdar, Rupak},
acronym = {{TACAS}'10},
booktitle = {{P}roceedings of the 16th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'10)},
author = {Villard, Jules and Lozes, {\'E}tienne and Calcagno, Cristiano},
title = {Tracking Heaps that Hop with Heap-Hop},
pages = {275-279},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/VLC-tacas10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/VLC-tacas10.pdf},
doi = {10.1007/978-3-642-12002-2_23},
abstract = {Heap-Hop is a program prover for concurrent heap-manipulating
programs that use Hoare monitors and message-passing synchronization.
Programs are annotated with pre and post-conditions and loop invariants,
written in a fragment of separation logic. Communications are governed by
a form of session types called contracts. Heap-Hop can prove safety and
race-freedom and, thanks to contracts, absence of memory leaks and
deadlock-freedom. It has been used in several case studies, including
concurrent programs for copyless list transfer, service provider
protocols, and load-balancing parallel tree disposal.}
}
@inproceedings{DS-fossacs10,
address = {Paphos, Cyprus},
month = mar,
year = 2010,
volume = {6014},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ong, C.-H. Luke},
acronym = {{FoSSaCS}'10},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'10)},
author = {Demri, St{\'e}phane and Sangnier, Arnaud},
title = {When Model-Checking
Freeze {LTL} over Counter Machines Becomes Decidable},
pages = {176-190},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DS-fossacs10.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DS-fossacs10.pdf},
doi = {10.1007/978-3-642-12032-9_13},
abstract = {We study the decidability status of model-checking freeze LTL
over various subclasses of counter machines for which the reachability
problem is known to be decidable (reversal-bounded counter machines,
vector additions systems with states, flat counter machines, one-counter
machines). In freeze LTL, a register can store a counter value and at some
future position an equality test can be done between a register and a
counter value. Herein, we complete an earlier work started on one-counter
machines by considering other subclasses of counter machines, and
especially the class of reversal-bounded counter machines. This gives us
the opportuniy to provide a systematic classification that distinguishes
determinism vs. nondeterminism and we consider subclasses of formulae by
restricting the set of atomic formulae or\slash and the polarity of the
occurrences of the freeze operators, leading to the flat fragment.}
}
@inproceedings{tCF-fossacs10,
address = {Paphos, Cyprus},
month = mar,
year = 2010,
volume = {6014},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ong, C.-H. Luke},
acronym = {{FoSSaCS}'10},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'10)},
author = {ten~Cate, Balder and Fontaine, Ga{\"e}lle},
title = {An Easy Completeness Proof for the Modal \(\mu\)-Calculus on Finite Trees},
pages = {161-175},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/tCF-fossacs10.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/tCF-fossacs10.pdf},
doi = { 10.1007/978-3-642-12032-9_12},
abstract = {We give a complete axiomatization for the modal \(\mu\)-calculus on
finite trees. While the completeness of our axiomatization already follows
from a more powerful result by Igor Walukiewicz, our proof is easier and
uses very different tools, inspired from model theory. We show that our
approach generalizes to certain axiomatic extensions, and to the extension
of the \(\mu\)-calculus with graded modalities. We hope that the method might
be helpful for other completeness proofs as well.}
}
@inproceedings{CS-fossacs10,
address = {Paphos, Cyprus},
month = mar,
year = 2010,
volume = {6014},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ong, C.-H. Luke},
acronym = {{FoSSaCS}'10},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'10)},
author = {Chambart, Pierre and Schnoebelen, {\relax Ph}ilippe},
title = {Toward a compositional theory of leftist grammars and
transformations},
pages = {237-251},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-fossacs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-fossacs10.pdf},
doi = {10.1007/978-3-642-12032-9_17},
abstract = {Leftist grammars [Motwani \textit{et~al.}, STOC~2000] are
special semi-Thue systems where symbols can only insert or erase to their
left. We~develop a theory of leftist grammars seen as word transformers as
a tool toward rigorous analyses of their computational power. Our~main
contributions in this first paper are (1)~constructions proving that
leftist transformations are closed under compositions and transitive
closures, and (2)~a~proof that bounded reachability is NP-complete even
for leftist grammars with acyclic rules.}
}
@article{schmitz-scp10,
publisher = {Elsevier Science Publishers},
journal = {Science of Computer Programming},
author = {Sylvain Schmitz},
title = {An Experimental Ambiguity Detection Tool},
volume = 75,
number = {1-2},
pages = {71-84},
month = jan,
year = 2010,
doi = {10.1016/j.scico.2009.07.002},
url = {http://hal.archives-ouvertes.fr/hal-00436398},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/schmitz-scp10.pdf},
abstract = {Although programs convey an unambiguous meaning, the grammars
used in practice to describe their syntax are often ambiguous, and
completed with disambiguation rules. Whether these rules achieve the
removal of all the ambiguities while preserving the original intended
language can be difficult to ensure. We present an experimental ambiguity
detection tool for GNU Bison, and illustrate how it can assist a
grammatical development for a subset of Standard~ML.}
}
@inproceedings{CLPV-vmcai10,
address = {Madrid, Spain},
month = jan,
year = 2010,
volume = 5944,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Barthe, Gilles and Hermenegildo, Manuel},
acronym = {{VMCAI}'10},
booktitle = {{P}roceedings of the 11th {I}nternational {C}onference on
{V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation
({VMCAI}'10)},
author = {Chadha, Rohit and Legay, Axel and Prabhakar, Pavithra
and Viswanathan, Mahesh},
title = {Complexity bounds for the verification of real-time software},
pages = {95-111},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CLPV-vmcai10.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CLPV-vmcai10.pdf},
doi = {10.1007/978-3-642-11319-2_10},
abstract = {We present uniform approaches to establish complexity bounds for
decision problems such as reachability and simulation, that arise
naturally in the verification of timed software systems. We model timed
software systems as timed automata augmented with a data store (like a
pushdown stack) and show that there is at least an exponential blowup in
complexity of verification when compared with untimed systems. Our proof
techniques also establish complexity results for boolean programs, which
are automata with stores that have additional boolean variables.}
}
@article{JGL-mscs09,
publisher = {Cambridge University Press},
journal = {Mathematical Structures in Computer Science},
author = {Goubault{-}Larrecq, Jean},
title = {{D}e~{G}root Duality and Models of Choice: Angels, Demons, and Nature},
volume = {20},
number = 2,
pages = {169-237},
month = apr,
year = 2010,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-mscs09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-mscs09.pdf},
doi = {10.1017/S0960129509990363},
abstract = {We introduce convex-concave duality for various models of
non-deterministic choice, probabilistic choice, and the two of them
together. This complements the well-known duality of stably compact spaces
in a pleasing way: convex-concave duality swaps angelic and demonic
choice, and leaves probabilistic choice invariant.}
}
@article{bbc09-lmcs,
journal = {Logical Methods in Computer Science},
author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and Chevalier, Fabrice},
title = {O-Minimal Hybrid Reachability Games},
year = 2010,
month = jan,
volume = 6,
number = {1:1},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBC-lmcs09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBC-lmcs09.pdf},
doi = {10.2168/LMCS-6(1:1)2010},
abstract = {In this paper, we consider reachability games over general
hybrid systems, and distinguish between two possible observation
frameworks for those games: either the precise dynamics of the system is
seen by the players (this is the perfect observation framework), or only
the starting point and the delays are known by the players (this is the
partial observation framework). In the first more classical framework, we
show that time-abstract bisimulation is not adequate for solving this
problem, although it is sufficient in the case of timed automata. That is
why we consider an other equivalence, namely the suffix equivalence based on
the encoding of tra jectories through words. We show that this suffix
equivalence is in general a correct abstraction for games. We apply this
result to o-minimal hybrid systems, and get decidability and computability
results in this framework. For the second framework which assumes a
partial observation of the dynamics of the system, we propose another
abstraction, called the superword encoding, which is suitable to solve the
games under that assumption. In that framework, we also provide
decidability and computability results.}
}
@article{BCM-icomp2009,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Bouyer, Patricia and Chevalier, Fabrice and Markey, Nicolas},
title = {On the Expressiveness of {TPTL} and~{MTL}},
volume = {208},
number = 2,
pages = {97-116},
month = feb,
year = 2010,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCM-icomp09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCM-icomp09.pdf},
doi = {10.1016/j.ic.2009.10.004},
abstract = {TPTL and MTL are two classical timed extensions of~LTL. In~this
paper, we prove the 20-year-old conjecture that TPTL is strictly more
expressive than~MTL. But we show that, surprisingly, the TPTL~formula
proposed by Alur and Henzinger for witnessing this conjecture \emph{can}
be expressed in~MTL. More generally, we show that TPTL formulae using only
modality~F can be translated into~MTL.}
}
@inproceedings{FS-sofsem10,
address = {\v{S}pindler\r{u}v Ml\'{y}n, Czech Republic},
month = jan,
year = 2010,
volume = 5901,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Peleg, David and Muscholl, Anca},
acronym = {{SOFSEM}'10},
booktitle = {{P}roceedings of the 36th International Conference on
Current Trends in Theory and Practice of
Computer Science ({SOFSEM}'10)},
author = {Finkel, Alain and Sangnier, Arnaud},
title = {Mixing coverability and reachability to analyze {VASS}
with one zero-test},
pages = {394-406},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-sofsem10.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-sofsem10.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FS-sofsem10.ps},
doi = {10.1007/978-3-642-11266-9_33},
abstract = {We study Vector Addition Systems with States (VASS) extended in
such a way that one of the manipulated integer variables can be tested to
zero. For this class of system, it has been proved that the reachability
problem is decidable. We prove here that boundedness, termination and
reversal-boundedness are decidable for VASS with one zero-test. To decide
reversal-boundedness, we provide an original method which mixes both the
construction of the coverability graph for VASS and the computation of the
reachability set of reversal-bounded counter machines. The same
construction can be slightly adapted to decide boundedness and hence
termination.}
}
@article{BKKL-tse09,
publisher = {{IEEE} Computer Society Press},
journal = {IEEE Transactions on Software Engineering},
author = {Bollig, Benedikt and Katoen, Joost-Pieter and Kern, Carsten
and Leucker, Martin},
title = {Learning Communicating Automata from~{MSCs}},
volume = {36},
number = {3},
pages = {390-408},
month = may # {-} # jun,
year = 2010,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-tse09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-tse09.pdf},
doi = {10.1109/TSE.2009.89},
abstract = {This paper is concerned with bridging the gap between
requirements and distributed systems. Requirements are defined as basic
message sequence charts (MSCs) specifying positive and negative scenarios.
Communicating finite-state machines (CFMs), \textit{i.e.}, finite automata
that communicate via FIFO buffers, act as system realizations. The key
contribution is a generalization of Angluin's learning algorithm for
synthesizing CFMs from MSCs. This approach is exact---the resulting CFM
precisely accepts the set of positive scenarions and rejects all negative
ones---and yields fully asynchronous implementations. The paper
investigates for which classes of MSC languages CFMs can be learned,
presents an optimization technique for learning partial orders, and
provides substantial empirical evidence indicating the practical
feasibility of the approach.}
}
@article{BKKL-cai09,
publisher = {Slovak Academy of Sciences},
journal = {Computing and Informatics},
author = {Bollig, Benedikt and Katoen, Joost-Pieter and Kern, Carsten
and Leucker, Martin},
title = {{SMA}---The Smyle Modeling Approach},
volume = {29},
number = {1},
pages = {45-72},
year = 2010,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-cai09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-cai09.pdf},
abstract = {This paper introduces the model-based software development
lifecycle model \emph{SMA}---the Smyle \emph{Modeling Approach}---which is
centered around \emph{Smyle}. \emph{Smyle} is a dedicated learning
procedure to support engineers to interactively obtain design models from
requirements, characterized as either being desired (positive) or unwanted
(negative) system behavior. Within \emph{SMA}, the learning approach is
complemented by so-called \emph{scenario patterns} where the engineer can
specify \emph{clearly} desired or unwanted behavior. This way, user
interaction is reduced to the interesting scenarios limiting the design
effort considerably. In~\emph{SMA}, the learning phase is further
complemented by an effective analysis phase that allows for detecting
design flaws at an early design stage. Using learning techniques allows us
to gradually develop and refine requirements, naturally supporting
evolving requirements, and allows for a rather inexpensive redesign in
case anomalous system behavior is detected during analysis, testing, or
maintenance. This paper describes the approach and reports on first
practical experiences.}
}
@inproceedings{ZBH-lads09,
address = {Turin, Italy},
year = 2010,
volume = 6039,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Dastani, Mehdi and El~Fallah Seghrouchni, Amal and Leite, Jo{\~a}o
and Torroni, Paolo},
acronym = {{LADS}'09},
booktitle = {{R}evised {S}elected {P}apers of the 2nd {W}orkshop on {LA}nguages, methodologies and
{D}evelopment tools for multi-agent system{S} ({LADS}'09)},
author = {Zargayouna, Mahdi and Balbo, Flavien and Haddad, Serge},
title = {Agents Secure Interaction in Data Driven Languages},
pages = {72-91},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ZBH-lads09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ZBH-lads09.pdf},
doi = {10.1007/978-3-642-13338-1_5},
abstract = {This paper discusses the security issues in data driven
coordination languages. These languages rely on a data space shared by the
agents and used to coordinate their activities. We extend these languages
with a main distinguishing feature, which is the possibility to define
fine-grained security conditions, associated with every datum in the
shared space. Two main ideas makes it possible: the consideration of an
abstraction of agents' states in the form of data at language level and
the introduction of a richer interaction mechanism than state-of-the-art
templates. This novel security mechanism allows both agents and system
designers to prohibit undesirable interactions.}
}
@article{DKS-jcs09,
publisher = {{IOS} Press},
journal = {Journal of Computer Security},
author = {Delaune, St{\'e}phanie and Kremer, Steve and Steel, Graham},
title = {Formal Analysis of {PKCS\#11} and Proprietary Extensions},
volume = 18,
number = 6,
pages = {1211-1245},
year = 2010,
month = nov,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKS-jcs09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKS-jcs09.pdf},
doi = {10.3233/JCS-2009-0394},
abstract = {PKCS\#11 denes an API for cryptographic devices that has been
widely adopted in industry. However, it has been shown to be vulnerable to
a variety of attacks that could, for example, compromise the sensitive
keys stored on the device. In this paper, we set out a formal model of the
operation of the API, which diers from previous security API models
notably in that it accounts for non-monotonic mutable global state. We
give decidability results for our formalism, and describe an
implementation of the resulting decision procedure using the model checker
NuSMV. We report some new attacks and prove the safety of some
congurations of the API in our model. We also analyse proprietary
extensions proposed by nCipher (Thales) and Eracom (Safenet), designed to
address the shortcomings of PKCS\#11.}
}
@article{goubault-jcs09,
publisher = {{IOS} Press},
journal = {Journal of Computer Security},
author = {Goubault{-}Larrecq, Jean},
title = {Finite Models for Formal Security Proofs},
volume = 18,
number = 6,
pages = {1247-1299},
year = 2010,
month = nov,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-jcs09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-jcs09.pdf},
doi = {10.3233/JCS-2009-0395},
abstract = {First-order logic models of security for cryptographic
protocols, based on variants of the Dolev-Yao model, are now
well-established tools. Given that we have checked a given security
protocol using a given first-order prover, how hard is it to extract a
formally checkable proof of it, as required in, \textit{e.g.}, common
criteria at the highest evaluation level~(EAL7)? We~demonstrate that this
is surprisingly hard in the general case: the problem is non-recursive.
Nonetheless, we show that we can instead extract finite
models~\(\mathcal{M}\) from a set~\(S\) of clauses representing~\(\pi\),
automatically, and give two ways of doing~so. We~then define a
model-checker testing \(\mathcal{M} \models S\), and show how we can
instrument it to output a formally checkable proof, \textit{e.g.}, in~Coq.
Experience on a number of protocols shows that this is practical, and that
even complex (secure) protocols modulo equational theories have small
finite models, making our approach suitable.}
}
@article{LAL-jar09,
publisher = {Springer},
journal = {Journal of Automated Reasoning},
author = {Longuet, Delphine and Aiguier, Marc and Le{~}Gall, Pascale},
title = {Proof-guided test selection from first-order specifications
with equality},
year = {2010},
month = dec,
volume = 45,
number = 4,
pages = {437-473},
nmnote = {special issue on Tests and Proofs},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LAL-jar09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LAL-jar09.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LAL-jar09.ps},
doi = {10.1007/s10817-009-9128-7},
abstract = {This paper deals with test case selection from axiomatic
specifications whose axioms are quantifier-free first-order formulas with
equality. We first prove the existence of an ideal exhaustive test set to
start the selection from. We then propose an extension of the test
selection method called axiom unfolding, originally defined for algebraic
specifications, to quantifier-free first-order specifications with
equality. This method basically consists of a case analysis of the
property under test (the test purpose) according to the specification
axioms. It is based on a proof search for the different instances of the
test purpose. Since the calculus is sound and complete, this allows us to
provide a full coverage of this property. The generalisation we propose
allows to deal with any kind of predicate (not only equality) and with any
form of axiom and test purpose (not only equations or Horn clauses).
Moreover, it improves our previous works with efficiently dealing with the
equality predicate, thanks to the paramodulation rule.}
}
@article{CCZ-tocl08,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique and
Z{\u{a}}linescu, Eugen},
title = {Deciding security properties for cryptographic
protocols. Application to key cycles},
volume = 11,
number = 2,
nopages = {},
month = jan,
year = 2010,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CCZ-tocl09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CCZ-tocl09.pdf},
doi = {10.1145/1656242.1656244},
abstract = {There is a large amount of work dedicated to the formal
verification of security protocols. In~this paper, we~revisit and extend
the NP-complete decision procedure for a bounded number of sessions. We
use a, now standard, deducibility constraint formalism for modeling
security protocols. Our~first contribution is to give a simple set of
constraint simplification rules, that allows to reduce any deducibility
constraint to a set of solved forms, representing all solutions (within
the bound on sessions).\par
As a consequence, we prove that deciding the existence of key cycles is
NP-complete for a bounded number of sessions. The problem of key-cycles
has been put forward by recent works relating computational and symbolic
models. The so-called soundness of the symbolic model requires indeed that
no key cycle (\textit{e.g.},~enc\((k, k)\)) ever occurs in the
execution of the protocol. Otherwise, stronger security assumptions (such
as KDM-security) are required.\par
We show that our decision procedure can also be applied to prove again the
decidability of authentication-like properties and the decidability of a
significant fragment of protocols with timestamps.}
}
@article{KM-jcs09,
publisher = {{IOS} Press},
journal = {Journal of Computer Security},
author = {Kremer, Steve and Mazar{\'e}, Laurent},
title = {Computationally Sound Analysis of Protocols using
Bilinear Pairings},
year = 2010,
month = nov,
volume = 18,
number = 6,
pages = {999-1033},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KM-jcs09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KM-jcs09.pdf},
doi = {10.3233/JCS-2009-0388},
abstract = {In this paper, we introduce a symbolic model to analyse
protocols that use a bilinear pairing between two cyclic groups. This
model consists in an extension of the Abadi-Rogaway logic and we prove
that the logic is still computationally sound: symbolic
indistinguishability implies computational indistinguishability provided
that the Bilinear Decisional Diffie-Hellman assumption holds and that the
encryption scheme is \textsf{IND-CPA} secure. We~illustrate our results on
classical protocols using bilinear pairing like Joux tripartite
Diffie-Hellman protocol or the TAK-2 and TAK-3 protocols. We also
investigate the security of a newly designed variant of the
Burmester-Desmedt protocol using bilinear pairings. More precisely, we
show for each of these protocols that the generated key is
indistinguishable from a random element.}
}
@article{DKR-jcs09,
publisher = {{IOS} Press},
journal = {Journal of Computer Security},
author = {Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D.},
title = {Symbolic bisimulation for the applied pi~calculus},
year = 2010,
month = mar,
volume = 18,
number = 2,
pages = {317-377},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-jcs09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-jcs09.pdf},
doi = {10.3233/JCS-2010-0363},
abstract = {We propose a symbolic semantics for the finite applied
pi~calculus. The~applied pi calculus is a variant of the pi~calculus with
extensions for modelling cryptographic protocols. By~treating inputs
symbolically, our semantics avoids potentially infinite branching of
execution trees due to inputs from the environment. Correctness is
maintained by associating with each process a set of constraints on terms.
We~define a symbolic labelled bisimulation relation, which is shown to be
sound but not complete with respect to standard bisimulation. We explore
the lack of completeness and demonstrate that the symbolic bisimulation
relation is sufficient for many practical examples. This~work is an
important step towards automation of observational equivalence for the
finite applied pi calculus, \textit{e.g.}~for verification of anonymity or
strong secrecy properties.}
}
@techreport{rr-lsv-10-23,
author = {Bonnet, R{\'e}mi and Finkel, Alain and Haddad, Serge and
Rosa{-}Velardo, Fernando},
title = {Comparing Petri Data Nets and Timed Petri Nets},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2010},
month = dec,
type = {Research Report},
number = {LSV-10-23},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-23.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-23.pdf},
note = {16~pages},
abstract = {Well-Structured Transitions Systems (WSTS) constitute a generic
class of infinite-state systems for which several properties like
coverability remain decidable. The family of coverability languages that
they generate is an appropriate criterium for measuring their
expressiveness. Here we establish that Petri Data nets (PDNs) and Timed
Petri nets (TdPNs), two powerful classes of WSTS are equivalent w.r.t this
criterium.}
}
@phdthesis{vacher-phd2010,
author = {Vacher, Camille},
title = {Automates {\`a} contraintes globales pour la v{\'e}rification de
propri{\'e}t{\'e}s de s{\'e}curit{\'e}},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2010,
month = dec,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/vacher-phd.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/vacher-phd.pdf}
}
@phdthesis{place-phd2010,
author = {Place, {\relax Th}omas},
title = {Decidable Characterizations for Tree Logics},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2010,
month = dec,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/place-phd.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/place-phd.pdf}
}
@phdthesis{figueira-phd2010,
author = {Figueira, Diego},
title = {On decidable automata on data words and data trees
in relation to satisfiability of {LTL} and {XP}ath},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2010,
month = dec,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/figueira-phd.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/figueira-phd.pdf}
}
@phdthesis{andre-phd2010,
author = {Andr{\'e}, {\'E}tienne},
title = {An Inverse Method for the Synthesis of Timing Parameters in
Concurrent Systems},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2010,
month = dec,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/andre-phd.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/andre-phd.pdf},
abstract = {This thesis proposes a novel approach for the synthesis of
delays for timed systems. When verifying a real-time system, e.g., a
hardware device or a communication protocol, it is important to check that
not only the functional but also the timed behavior is correct. This
correctness depends on the values of the delays of internal operations and
of the environment.\par
Formal verification methods guarantee the correctness of a timed system
for a given set of delays, but do not give information for other values of
the delays. Checking the correctness of for various values of those delays
can be difficult and time consuming. It is thus interesting to consider
that these delays are parameters. The problem then consists in
synthesizing {"}good values{"} for those parameters, i.e., values for which
the system is guaranteed to behave well.\par
We are here interested in the synthesis of parameters in the framework of
timed automata, a model for verifying real-time systems. Our approach
relies on the following inverse method: given a reference valuation of the
parameters, we synthesize a constraint on the parameters, guaranteeing the
same time-abstract linear behavior as for the reference valuation. This
gives a criterion of robustness to the system. By iterating this inverse
method on various points of a bounded parameter domain, we are then able
to partition the parametric space into good and bad zones, with respect to
a given property one wants to verify. This gives a behavioral cartography
of the system.\par
This method extended to probabilistic systems allows to preserve minimum
and maximum probabilities of reachability properties. We also present
variants of the inverse method for directed weighted graphs and Markov
Decision Processes. Several prototypes have been implemented; in
particular, IMITATOR II implements the inverse method and the cartography
for timed automata. It allowed us to synthesize parameter values for
several case studies such as an abstract model of a memory circuit sold by
the chipset manufacturer ST-Microelectronics, and various communication
protocols. }
}
@techreport{rr-lsv-10-22,
author = {Soulat, Romain},
title = {On Properties of the Inverse Method:
Commutation of Instanciation
and Full Covering of the Behavioral Cartography},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2010},
month = dec,
type = {Research Report},
number = {LSV-10-22},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-22.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-22.pdf},
note = {14~pages},
abstract = {When one performs an Inverse Method on a Parametric Timed Automata over an
instance \(\pi_0\), one can instantiate some parameters at the very beginning
of the analysis or at the end, with a restriction of the constraint \(K_0\)
obtained in order to get a constraint over a subset of the parameters. In
this report, we show that the results of either methods are the same. We
present a theoretical proof and then an illustration of this property on
the flip-flop example and the Root Contention protocol. We also present
some results about the coverage of behavioral cartography and an
illustration of the full covering on the SPSMALL memory.}
}
@techreport{rr-lsv-10-21,
author = {Andr{\'e}, {\'E}tienne},
title = {Synthesizing Parametric Constraints on Various Case Studies
Using {IMITATOR}~{II}},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2010},
month = dec,
type = {Research Report},
number = {LSV-10-21},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-21.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-21.pdf},
note = {66~pages},
abstract = {We present here various case studies analyzed using IMITATOR II,
a tool implementing the {"}inverse method{"} in the framework of
parametric timed automata: given a reference valuation of the parameters,
it synthesizes a constraint such that the system behaves the same as under
the reference valuation in terms of traces, i.e., alternating sequences of
locations and actions.\par
This is useful for safely relaxing some values of the reference valuation,
and optimizing timing bounds of the system.\par
Besides the inverse method, IMITATOR~II also implements the {"}behavioral
cartography algorithm{"}, allowing to solve the following good parameters
problem: find a set of valuations within a given rectangle for which the
system behaves well.\par
We present here a range of case studies, communication protocols, hardware
circuits and industrial case studies for which constraints guaranteeing a
good behavior were synthesized using IMITATOR~II.}
}
@techreport{rr-lsv-10-20,
author = {Andr{\'e}, {\'E}tienne},
title = {{IMITATOR}~{II} User Manual},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2010},
month = nov,
type = {Research Report},
number = {LSV-10-20},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-20.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-20.pdf},
note = {31~pages},
abstract = {We present here the user manual of IMITATOR~II, a~tool
implementing the {"}inverse method{"} in the framework of parametric timed
automata: given a reference valuation of the parameters, its generates a
constraint such that the system behaves the same as under the reference
valuation in terms of traces, i.e., alternating sequences of locations and
actions. This is useful for safely relaxing some values of the reference
valuation, and optimizing timing bounds of the system.\par
Besides the inverse method, IMITATOR II also implements the {"}behavioral
cartography algorithm{"}, allowing to solve the following good parameters
problem: find a set of valuations within a given rectangle for which the
system behaves well.\par
We give here the installation requirements and the launching commands of
IMITATOR~II, as~well as the source code of a toy example.}
}
@mastersthesis{rodriguez-master,
author = {Rodr{\'\i}guez, C{\'e}sar},
title = {Implementation of a complete prefix unfolder for contextual nets},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2010},
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/cr-m2.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/cr-m2.pdf}
}
@inproceedings{hmy-bpsc10,
address = {Leipzig, Germany},
month = sep # {-} # oct,
year = 2010,
volume = {177},
series = {Lecture Notes in Informatics},
publisher = {Gesellschaft f{\"u}r Informatik},
editor = {Abramowicz, Witold and Alt, Rainer and F{\"a}hnrich, Klaus-Peter
and Franczyk, Bogdan and Maciaszek, Leszek A.},
acronym = {{ISSS}{\slash}{BPSC}'10},
booktitle = {{P}roceedings of the 2nd {I}nternational {S}ymposium on {S}ervices
{S}cience and 3rd {I}nternational {C}onference on {B}usiness
{P}rocess and {S}ervices {C}omputing
({ISSS}{\slash}{BPSC}'10)},
author = {Haddad, Serge and Mokdad, Lynda and Youcef, Samir},
title = {Selection of the Best composite Web Service Based on Quality
of Service},
pages = {255-266},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/hmy-bpsc10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/hmy-bpsc10.pdf},
abstract = {The paper proposes a general framework to composite Web services
selection based on multicriteria evaluation. The proposed framework
extends the Web services architecture by adding, in the registry, a new
Multicriteria Evaluation Component~(MEC) devoted to multicriteria
evaluation. This additional component takes as input a set of composite
Web services and a set of evaluation criteria and generates a set of
recommended composite Web services. In~addition to the description of the
conceptual architecture of the formwork, the paper also proposes solutions
to construct and evaluate composite web services. In order to show the
feasibility of the proposed architecture, we~have developed a prototype
based on the open source jUDDI registry.}
}
@mastersthesis{scerri-master,
author = {Scerri, Guillaume},
title = {Mod{\'e}lisation des cl{\'e}s de l'intrus},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2010},
month = sep,
nmnote = {Hubert prefere ne pas diffuser le rapport, et prepare une version 'conf'}
}
@mastersthesis{bonnet-master,
author = {Bonnet, R{\'e}mi},
title = {Well-structured {P}etri-nets extensions with data},
school = {{M}aster Computer Science, EPFL,
Lausanne, Switzerland},
type = {Rapport de {M}aster},
year = {2010},
month = mar,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/bonnet-m2.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bonnet-m2.pdf}
}
@article{LMT-tcs10,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Lanotte, Ruggero and Maggiolo{-}Schettini, Andrea and Troina, Angelo},
title = {Weak bisimulation for Probabilistic Timed Automata?},
volume = 411,
number = 50,
year = 2010,
month = nov,
pages = {4291-4322},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LMT-tcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LMT-tcs10.pdf},
doi = {10.1016/j.tcs.2010.09.003},
abstract = {We are interested in describing timed systems that exhibit
probabilistic behaviour. To this purpose, we consider a
model of Probabilistic Timed Automata and introduce a
concept of weak bisimulation for these automata, together
with an algorithm to decide it. The weak bisimulation
relation is shown to be preserved when either time, or
probability is abstracted away. As an application, we use
weak bisimulation for Probabilistic Timed Automata to model
and analyze a timing attack on the dining cryptographers protocol.}
}
@techreport{rr-lsv-10-17,
author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Sassolas,
Mathieu and Zeitoun, Marc},
title = {Distributed Synthesis with Incomparable Information},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2010},
month = oct,
type = {Research Report},
number = {LSV-10-17},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-17.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-17.pdf},
note = {20~pages},
abstract = {Given (1)~an architecture defined by processes and communication
channels between them or with the environment, and (2)~a~specification on
the messages transmitted over the channels, distributed synthesis aims at
deciding existence of local programs, one for each process, that together
meet the specification, whatever the environment does. Recent work shows
that this problem can be solved when a \emph{linear preorder} sorts the
agents w.r.t. the information received from the environment.\par
In this paper we show a new decidability result in the case where this
preorder is broken by the addition of noisy agents embedded in a pipeline
architecture. This case cannot be captured by the classical framework.
Besides, this architecture makes it possible to model particular security
threats, known as covert channels, where two users (the sender and the
receiver) manage to communicate via a noisy protocol, and despite
incomparable views over the environment.}
}
@article{CDH-lmcs10,
journal = {Logical Methods in Computer Science},
author = {Chatterjee, Krishnendu and Doyen, Laurent and Henzinger,
{\relax Th}omas A.},
title = {Expressiveness and Closure Properties for Quantitative
Languages},
volume = 6,
number = {3:10},
nopages = {},
month = sep,
year = 2010,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDH-lmcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDH-lmcs10.pdf},
ps = {CDH-lmcs10.ps},
doi = {10.2168/LMCS-6(3:10)2010},
abstract = {Weighted automata are nondeterministic automata with numerical
weights on transitions. They can define quantitative languages~\(L\) that
assign to each word~\(w\) a real number~\(L(w)\). In the case of infinite
words, the value of a run is naturally computed as the maximum, limsup,
liminf, limit-average, or discounted-sum of the transition weights. The
value of a word \(w\) is the supremum of the values of the runs over
\(w\). We study expressiveness and closure questions about these
quantitative languages.\par
We first show that the set of words with value greater than a threshold
can be non-\(omega\)-regular for deterministic limit-average and
discounted-sum automata, while this set is always \(omega\)-regular when
the threshold is isolated (i.e., some neighborhood around the threshold
contains no word). In the latter case, we prove that the \(omega\)-regular
language is robust against small perturbations of the transition
weights.\par
We next consider automata with transition weights~\(0\) or \(1\) and show
thatthey are as expressive as general weighted automata in the
limit-average case, but not in the discounted-sum case.\par
Third, for quantitative languages \(L_1\) and~\(L_2\), we consider the
operations\(max(L_1,L_2)\), \(min(L_1,L_2)\), and \(1-L_1\), which
generalize the booleanoperations on languages, as well as the sum \(L_1 +
L_2\). We establish the closure properties of all classes of quantitative
languages with respect to these four operations.}
}
@inproceedings{CD-lpar10,
address = {Yogyakarta, Indonesia},
month = oct,
year = 2010,
volume = {6397},
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Fernm{\"u}ller, Chrisaitn G. and Voronkov, Andrei},
acronym = {{LPAR}'10},
booktitle = {{P}roceedings of the 17th {I}nternational
{C}onference on {L}ogic for {P}rogramming,
{A}rtificial {I}ntelligence, and {R}easoning
({LPAR}'10)},
author = {Chatterjee, Krishnendu and Doyen, Laurent},
title = {The Complexity of Partial-Observation Parity Games},
pages = {1-14},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-lpar10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-lpar10.pdf},
ps = {CD-lpar10.ps},
doi = {10.1007/978-3-642-16242-8_1},
abstract = {We consider two-player zero-sum games on graphs. On the basis of
the information available to the players these games can be classified as
follows: (a)~partial-observation (both players have partial view of the
game); (b)~one-sided partial-observation (one player has
partial-observation and the other player has complete-observation); and
(c)~complete-observation (both players have complete view of the game). We
survey the complexity results for the problem of deciding the winner in
various classes of partial-observation games with \(\omega\)-regular
winning conditions specified as parity objectives. We present a reduction
from the class of parity objectives that depend on sequence of states of
the game to the sub-class of parity objectives that only depend on the
sequence of observations. We also establish that partial-observation
acyclic games are PSPACE-complete.}
}
@inproceedings{haar-wodes10,
address = {Berlin, Germany},
month = aug # {-} # sep,
year = 2010,
publisher = {IFAC},
editor = {Raisch, J{\"o}rg and Giua, Alessandro and Lafortune,
St{\'e}phane and Moor, Thomas},
acronym = {{WODES}'10},
booktitle = {{P}roceedings of the 10th {W}orkshop on {D}iscrete {E}vent {S}ystems
({WODES}'10)},
author = {Haar, Stefan},
title = {What Topology Tells us about Diagnosability in Partial Order Semantics},
pages = {221-226},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SH-wodes10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SH-wodes10.pdf},
abstract = {From a partial observation of the behaviour of a labeled
Discrete Event System, fault Diagnosis strives to determine whether or not
a given {"}invisible{"} fault event has occurred. The diagnosability problem
can be stated as follows: does the labeling allow for an outside observer
to determine the occurrence of the fault, no later than a bounded number
of events after that unobservable occurrence? In concurrent systems,
partial order semantics adds to the difficulty of the problem, but also
provides a richer and more complex picture of observation and diagnosis.
In particular, it is crucial to clarify the intuitive notion of {"}time
after fault occurrence{"}. To this end, we will use a unifying metric
framework for event structures, providing a general topological
description of diagnosability in both sequential and nonsequential
semantics for Petri nets.}
}
@inproceedings{AJRG-comnet10,
address = {Tozeur, Tunisia},
month = nov,
year = 2010,
publisher = {{IEEE} Computer Society Press},
noeditor = {},
acronym = {{C}om{N}et'10},
booktitle = {{P}roceedings of the 2nd {I}nternational {C}onference on
{C}ommunications and {N}etworking ({C}om{N}et'10)},
author = {Abassi, Ryma and Jacquemard, Florent and Rusinowitch,
Micha{\"e}l and Guemara{ }El{~}Fatmi, Sihem},
title = {{XML} Access Control: from {XACML} to Annotated Schemas},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AJRG-comnet10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AJRG-comnet10.pdf},
doi = {10.1109/COMNET.2010.5699810},
abstract = {XML became the \textit{de facto} standard for the data
representation and exchange on the internet. Regarding XML documents
access control policy definition, OASIS ratified the XACML standard. It is
a declarative language allowing the specification of authorizations as
rules. Furthermore, it is common to formally represent XML documents as
labeled trees and to handle secure requests through `user views'. A user
view is the part of the document accessible to a given user according to
the existing policy. Moreover, control access polices can be depicted as
annotated rules where annotations define for each document node whether it
is accessible. Hence, an annotated schema is a formal representation of
`user views'.\par
Our main contribution in this paper is then three folds. First, we compare
XACML policies and annotated schemas. Second, we identify a significant
fragment of XACML since this latter is very expressive and consequently
complex. Third, we define adequate translation algorithms from XACML
policies to annotated schemas.}
}
@inproceedings{JR-ppdp10,
address = {Hagenberg, Austria},
month = jul,
year = 2010,
publisher = {ACM Press},
editor = {Kutsia, Temur and Schreiner, Wolfgang and Fern{\'a}ndez, Maribel},
acronym = {{PPDP}'10},
booktitle = {{P}roceedings of the 12th {I}nternational {ACM} {SIGPLAN}
{C}onference on {P}rinciples and {P}ractice of {D}eclarative
{P}rogramming ({PPDP}'10)},
author = {Jacquemard, Florent and Rusinowitch, Micha{\"e}l},
title = {Rewrite-based verification of {XML} updates},
pages = {119-130},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/JR-ppdp10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JR-ppdp10.pdf},
doi = {10.1145/1836089.1836105},
abstract = {We propose a model for XML update primitives of the W3C XQuery
Update Facility as parameterized rewriting rules of the form: {"}insert an
unranked tree from a regular tree language~\(L\) as the first child of a
node labeled by~\(a\){"}. For these rules, we give type inference
algorithms, considering types defined by several classes of unranked tree
automata. These type inference algorithms are directly applicable to XML
static typechecking, which is the problem of verifying whether, a given
document transformation always converts source documents of a given input
type into documents of a given output type. We show that typechecking for
arbitrary sequences of XML update primitives can be done in polynomial
time when the unranked tree automaton defining the output type is
deterministic and complete, and that it is EXPTIME-complete otherwise.\par
We then apply the results to the verification of access control policies
for XML updates. We propose in particular a polynomial time algorithm for
the problem of local consistency of a policy, that is, for deciding the
non-existence of a sequence of authorized update operations starting from
a given document that simulates a forbidden update operation.}
}
@article{NSV-tods10,
publisher = {ACM Press},
journal = {ACM Transactions on Database Systems},
author = {Nash, Alan and Segoufin, Luc and Vianu, Victor},
title = {Views and queries: Determinacy and rewriting},
volume = 35,
number = 3,
month = jul,
year = 2010,
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/NSV-tods10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/NSV-tods10.pdf},
doi = {10.1145/1806907.1806913},
abstract = {We investigate the question of whether a query~\(Q\) can be
answered using a set~\(\textbf{V}\) of views. We first define the problem
in information-theoretic terms: we say that \(\textbf{V}\)
determines~\(Q\) if \(\textbf{V}\)~provides enough information to uniquely
determine the answer to~\(Q\). Next, we look at the problem of
rewriting~\(Q\) in terms of~\(\textbf{V}\) using a specific language.
Given a view language~\(\textbf{V}\) and query language~\(\mathcal{Q}\),
we say that a rewriting language is complete for
\(\mathcal{V}\)-to-\(\mathcal{Q}\) rewritings if every \(Q\in\mathcal{Q}\)
can be rewritten in terms of \(\textbf{V}\in\mathcal{V}\) using a query
in~\(\mathcal{R}\), whenever \(\textbf{V}\) determines~\(Q\). While query
rewriting using views has been extensively investigated for some specific
languages, the connection to the information-theoretic notion of
determinacy, and the question of completeness of a rewriting language,
have received little attention. In this paper we investigate
systematically the notion of determinacy and its connection to rewriting.
The results concern decidability of determinacy for various view and query
languages, as well as the power required of complete rewriting languages.
We consider languages ranging from first-order to conjunctive queries.}
}
@inproceedings{KBBB-fmcad10,
address = {Lugano, Switzerland},
month = oct,
year = 2010,
publisher = {{IEEE} Computer Society Press},
editor = {Bloem, Roderick and Sharygina, Natasha},
acronym = {{FMCAD}'10},
booktitle = {{P}roceedings of the 10th {I}nternational {C}onference on
{F}ormal {M}ethods in {C}omputer {A}ided {D}esign ({FMCAD}'10)},
author = {K{\"u}hne, Ulrich and Beyer, Sven and Bormann, J{\"o}rg
and Barstow, John},
title = {Automated Formal Verification of Processors Based on
Architectural Models},
pages = {129-136},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KBBB-fmcad10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KBBB-fmcad10.pdf},
abstract = {To keep up with the growing complexity of digital systems, high
level models are used in the design process. In today's processor design,
a comprehensive tool chain can be built automatically from architectural
or transaction level models, but disregarding formal verification. We
present an approach to automatically generate a complete property suite
from an architecture description, that can be used to formally verify a
register transfer level (RTL) implementation of a processor. The property
suite is complete by construction, i.e. an exhaustive verification of all
the functionality of the processor is ensured by the method. It allows for
the efficient verification of single pipeline processors, including
several advanced processor features like multicycle instructions. At the
same time, the structured approach reduces the effort for verification
significantly compared to a manual complete formal verification. The
presented techniques have been implemented in the tool FISACo, which is
demonstrated on an industrial processor.}
}
@article{AHLNW-mscs10,
publisher = {Cambridge University Press},
journal = {Mathematical Structures in Computer Science},
author = {Antonik, Adam and Huth, Michael and Larsen, Kim~G. and Nyman,
Ulrik and W{\k{a}}sowski, Andrzej},
title = {Modal and mixed specifications: key decision
problems and their complexities},
volume = 10,
number = 1,
month = feb,
year = 2010,
pages = {75-103},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AHLNW-mscs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AHLNW-mscs10.pdf},
doi = {10.1017/S0960129509990260},
abstract = {Modal and mixed transition systems are specification formalisms
that allow the mixing of over- and under-approximation. We discuss three
fundamental decision problems for such specifications:
\begin{itemize}
\item whether a set of specifications has a common implementation;
\item whether an individual specification has an implementation; and
\item whether all implementations of an individual specification are implementations of
another one.
\end{itemize}
For each of these decision problems we investigate the worst-case
computational complexity for the modal and mixed cases. We show that the
first decision problem is EXPTIME-complete for both modal and mixed
specifications. We prove that the second decision problem is
EXPTIME-complete for mixed specifications (it is known to be trivial for
modal ones). The third decision problem is also shown to be
EXPTIME-complete for mixed specifications.}
}
@inproceedings{BGGLP-scan10,
address = {Lyon, France},
month = sep,
year = 2010,
noeditor = {},
acronym = {SCAN'10},
booktitle = {{P}roceedings of the 14th {GAMM}-{IMACS} {I}nternational
{S}ymposium on {S}cientific {C}omputing, {C}omputer
{A}rithmetic and {V}alidated {N}umerics ({SCAN}'10)},
author = {Bouissou, Olivier and Goubault, {\'E}ric and
Goubault{-}Larrecq, Jean and Putot, Sylvie},
title = {A Generalization of {P}-boxes to Affine Arithmetic, and Applications to
Static Analysis of Programs},
nopages = {}
}
@article{DR-lmcs10,
journal = {Logical Methods in Computer Science},
author = {Demri, St{\'e}phane and Rabinovich, Alexander},
title = {The Complexity of Linear-time Temporal Logic over the Class
of Ordinals},
volume = 6,
number = 4,
nopages = {},
month = dec,
year = 2010,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DR-lmcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DR-lmcs10.pdf},
doi = {10.2168/LMCS-6(4:9)2010},
abstract = {We consider the temporal logic with since and until modalities.
This temporal logic is expressively equivalent over the class of ordinals
to first-order logic by Kamp's theorem. We show that it has a
PSPACE-complete satisfiability problem over the class of ordinals. Among
the consequences of our proof, we show that given the code of some
countable ordinal~\(\alpha\) and a formula, we can decide in PSPACE
whether the formula has a model over~\(\alpha\). In order to show these
results, we introduce a class of simple ordinal automata, as expressive as
B{\"u}chi ordinal automata. The PSPACE upper bound for the satisfiability
problem of the temporal logic is obtained through a reduction to the
nonemptiness problem for the simple ordinal automata.}
}
@inproceedings{SD-jelia10,
address = {Helsinki, Finland},
month = sep,
year = 2010,
volume = 6431,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Niemel{\"a}, Ilkka and Janhunen, Tomi},
acronym = {{JELIA}'10},
booktitle = {{P}roceedings of the 12th {E}uropean {C}onference on {L}ogics in
{A}rtificial {I}ntelligence ({JELIA}'10)},
author = {Demri, St{\'e}phane},
title = {Counter Systems for Data Logics},
pages = {10},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SD-jelia10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SD-jelia10.pdf},
doi = {10.1007/978-3-642-15675-5_3},
abstract = {Data logics are logical formalisms that are used to specify
properties on structures equipped with data (data words, data trees, runs
from counter systems, timed words, etc.). In this survey talk, we shall
see how satisfiability problems for such data logics are related to
reachability problems for counter systems (including counter automata with
errors, vector addition systems with states, etc.). This is the
opportunity to provide an overview about the relationships between data
logics and verification problems for counter systems.}
}
@inproceedings{CSV-fsttcs10,
address = {Chennai, India},
month = dec,
year = 2010,
volume = 8,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Lodaya, Kamal and Mahajan, Meena},
acronym = {{FSTTCS}'10},
booktitle = {{P}roceedings of the 30th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'10)},
author = {Chadha, Rohit and Sistla, A. Prasad and Viswanathan, Mahesh},
title = {Model Checking Concurrent Programs with Nondeterminism and Randomization},
pages = {364-375},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CSV-fsttcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CSV-fsttcs10.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2010.364},
abstract = {For concurrent probabilistic programs having process-level
nondeterminism, it is often necessary to restrict the class of schedulers
that resolve nondeterminism to obtain sound and precise model checking
algorithms. In this paper, we introduce two classes of schedulers called
\emph{view consistent} and \emph{locally Markovian} schedulers and
consider the model checking problem of concurrent, probabilistic programs
under these alternate semantics. Specifically, given a B{\"u}chi
automaton~\(\textsf{Spec}\), a~threshold~\(x\in[0,1]\), and a concurrent
program~\(\mathbb{P}\), the model checking problem asks if the measure of
computations of~\(\mathbb{P}\) that satisfy~\(\textsf{Spec}\) is at
least~\(x\), under all view consistent (or locally Markovian) schedulers.
We give precise complexity results for the model checking problem (for
different classes of B{\"u}chi automata specifications) and contrast it
with the complexity under the standard semantics that considers all
schedulers. }
}
@inproceedings{AGMN-fsttcs10,
address = {Chennai, India},
month = dec,
year = 2010,
volume = 8,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Lodaya, Kamal and Mahajan, Meena},
acronym = {{FSTTCS}'10},
booktitle = {{P}roceedings of the 30th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'10)},
author = {Akshay, S. and Gastin, Paul and Mukund, Madhavan and Narayan Kumar, K.},
title = {Model checking time-constrained scenario-based specifications},
pages = {204-215},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGMN-fsttcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGMN-fsttcs10.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2010.204},
abstract = {We consider the problem of model checking message-passing
systems with real-time requirements. As behavioural specifications, we use
message sequence charts (MSCs) annotated with timing constraints. Our
system model is a network of communicating finite state machines with
local clocks, whose global behaviour can be regarded as a timed automaton.
Our goal is to verify that all timed behaviours exhibited by the system
conform to the timing constraints imposed by the specification. In
general, this corresponds to checking inclusion for timed languages, which
is an undecidable problem even for timed regular languages. However, we
show that we can translate regular collections of time-constrained MSCs
into a special class of event-clock automata that can be determinized and
complemented, thus permitting an algorithmic solution to the model
checking problem.}
}
@inproceedings{CDHR-fsttcs10,
address = {Chennai, India},
month = dec,
year = 2010,
volume = 8,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Lodaya, Kamal and Mahajan, Meena},
acronym = {{FSTTCS}'10},
booktitle = {{P}roceedings of the 30th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'10)},
author = {Chatterjee, Krishnendu and
Doyen, Laurent and Henzinger, {\relax Th}omas A. and Raskin, Jean-Fran{\c{c}}ois},
title = {Generalized Mean-payoff and Energy Games},
pages = {505-516},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDHR-fsttcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDHR-fsttcs10.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2010.505}
}
@inproceedings{BFLZ-fsttcs10,
address = {Chennai, India},
month = dec,
year = 2010,
volume = 8,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Lodaya, Kamal and Mahajan, Meena},
acronym = {{FSTTCS}'10},
booktitle = {{P}roceedings of the 30th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'10)},
author = {Bonnet, R{\'e}mi and Finkel, Alain and Leroux, J{\'e}r{\^o}me
and Zeitoun, Marc},
title = {Place-Boundedness for Vector Addition Systems with one zero-test},
pages = {192-203},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLZ-fsttcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLZ-fsttcs10.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2010.192},
abstract = {Reachability and boundedness problems have been shown decidable
for Vector Addition Systems with one zero-test. Surprisingly,
place-boundedness remained open. We provide here a variation of the
Karp-Miller algorithm to compute a basis of the downward closure of the
reachability set which allows to decide place-boundedness. This forward
algorithm is able to pass the zero-tests thanks to a finer cover, hybrid
between the reachability and cover sets, reclaiming accuracy on one
component. We show that this filtered cover is still recursive, but that
equality of two such filtered covers, even for usual Vector Addition
Systems (with no zero-test), is undecidable.}
}
@inproceedings{HBMOW-fsttcs10,
address = {Chennai, India},
month = dec,
year = 2010,
volume = 8,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Lodaya, Kamal and Mahajan, Meena},
acronym = {{FSTTCS}'10},
booktitle = {{P}roceedings of the 30th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'10)},
author = {Hunter, Paul and Bouyer, Patricia and Markey, Nicolas and
Ouaknine, Jo{\"e}l and Worrell, James},
title = {Computing rational radical sums in uniform \(\textsf{TC}^{0}\)},
pages = {308-316},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HBMOW-fsttcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HBMOW-fsttcs10.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2010.308},
abstract = {A~fundamental problem in numerical computation and computational
geometry is to determine the sign of arithmetic expressions in radicals.
Here we consider the simpler problem of deciding whether \(\sum_{i=1}^m
C_i \cdot A_i^{X_i}\) is zero for given rational numbers~\(A_i\),
\(C_i\),~\(X_i\). It~has been known for almost twenty years that this can
be decided in polynomial time. In this paper we improve this result by
showing membership in uniform \(\textsf{TC}^0\). This requires several
significant departures from Bl{\"o}mer's polynomial-time algorithm as the
latter crucially relies on primitives, such as gcd computation and binary
search, that are not known to be in~\(\textsf{TC}^0\).}
}
@inproceedings{DLM-fsttcs10,
address = {Chennai, India},
month = dec,
year = 2010,
volume = 8,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Lodaya, Kamal and Mahajan, Meena},
acronym = {{FSTTCS}'10},
booktitle = {{P}roceedings of the 30th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'10)},
author = {Da{~}Costa, Arnaud and Laroussinie, Fran{\c{c}}ois and Markey, Nicolas},
title = {{ATL} with strategy contexts: Expressiveness and Model Checking},
pages = {120-132},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DLM-fsttcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DLM-fsttcs10.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2010.120},
abstract = {We study the alternating-time temporal logics \(\textsf{ATL}\)
and~\(\textsf{ATL}^{*}\) extended with strategy contexts: these make
agents commit to their strategies during the evaluation of formulas,
contrary to plain \(\textsf{ATL}\) and~\(\textsf{ATL}^{*}\) where strategy
quantifiers reset previously selected strategies.\par
We illustrate the important expressive power of strategy contexts by
proving that they make the extended logics, namely
\(\textsf{ATL}_{\textsf{sc}}\) and~\(\textsf{ATL}_{\textsf{sc}}^{*}\), equally
expressive: any~formula in~\(\textsf{ATL}_{\textsf{sc}}^{*}\) can be
translated into an equivalent, linear-size \(\textsf{ATL}_{\textsf{sc}}\)
formula. Despite the high expressiveness of these logics, we prove that
they remain decidable by designing a tree-automata-based algorithm for
model-checking \(\textsf{ATL}_{\textsf{sc}}\) on the full class of
\(n\)-player concurrent game structures.}
}
@proceedings{MW-time2010,
author = {Markey, Nicolas and Wijsen, Jef},
editor = {Markey, Nicolas and Wijsen, Jef},
title = {{P}roceedings of the 17th {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'10)},
booktitle = {{P}roceedings of the 17th {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'10)},
year = 2010,
month = sep,
publisher = {{IEEE} Computer Society Press},
address = {Paris, France},
url = {http://ieeexplore.ieee.org/xpl/tocresult.jsp?reload=true&isnumber=5601852},
doi = {10.1109/TIME.2010.4}
}
@proceedings{GL-concur10,
author = {Gastin, Paul and Laroussinie, Fran{\c{c}}ois},
editor = {Gastin, Paul and Laroussinie, Fran{\c{c}}ois},
title = {{P}roceedings of the 21st
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'10)},
booktitle = {{P}roceedings of the 21st
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'10)},
year = 2010,
month = aug # {-} # sep,
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6269},
url = {http://www.springerlink.com/content/978-3-642-15374-7},
doi = {10.1007/978-3-642-15375-4}
}
@inproceedings{FHL-express2010,
address = {Paris, France},
month = aug,
year = 2010,
volume = 41,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Fr{\"o}schle, Sibylle and Valencia, Franck},
acronym = {{EXPRESS}'10},
booktitle = {{P}roceedings of the 17th {I}nternational
{W}orkshop on {E}xpressiveness in
{C}oncurrency
({EXPRESS}'10)},
author = {Figueira, Diego and Hofman, Piotr and Lasota, S{\l}awomir},
title = {Relating timed and register automata},
pages = {61-75},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FHL-express10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FHL-express10.pdf},
doi = {10.4204/EPTCS.41.5},
abstract = {Timed automata and register automata are well-known models of
computation over timed and data words respectively. The former has clocks
that allow to test the lapse of time between two events, whilst the latter
includes registers that can store data values for later comparison.
Although these two models behave in appearance differently, several
decision problems have the same (un)decidability and complexity results
for both models. As a prominent example, emptiness is decidable for
alternating automata with one clock or register, both with non-primitive
recursive complexity. This is not by chance.\par
This work confirms that there is indeed a tight relationship between the
two models. We show that a run of a timed automaton can be simulated by a
register automaton, and conversely that a run of a register automaton can
be simulated by a timed automaton. Our results allow to transfer
complexity and decidability results back and forth between these two kinds
of models. We justify the usefulness of these reductions by obtaining new
results on register automata.}
}
@inproceedings{DKRS-fast10,
address = {Pisa, Italy},
month = sep,
year = 2010,
volume = 6561,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Degano, Pierpaolo and Etalle, Sandro and Guttman, Joshua},
acronym = {{FAST}'10},
booktitle = {{R}evised {S}elected {P}apers of the 7th {I}nternational {W}orkshop on
{F}ormal {A}spects in {S}ecurity and {T}rust ({FAST}'10)},
author = {Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D. and
Steel, Graham},
title = {A~Formal Analysis of Authentication in the {TPM}},
pages = {111-125},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DKRS-fast10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DKRS-fast10.pdf},
ps = {DKRS-fast10.ps},
doi = {10.1007/978-3-642-19751-2_8},
abstract = {The Trusted Platform Module~(TPM) is a hardware chip designed to
enable computers to achieve a greater level of security than is possible
in software alone. To this end, the TPM provides a way to store
cryptographic keys and other sensitive data in its shielded memory.
Through its API, one can use those keys to achieve some security goals.
The TPM is a complex security component, whose specification consists of
more than \(700\)~pages.\par
We model a collection of four TPM commands, and we identify and formalise
their security properties. Using the tool ProVerif, we rediscover some
known attacks and some new variations on them. We propose modifications to
the API and verify our properties for the modified API.}
}
@inproceedings{DKRS-secco10,
address = {Paris, France},
month = aug,
year = 2010,
editor = {Cortier, V{\'e}ronique and Chatzikokolakis, Kostas},
acronym = {{SecCo}'10},
booktitle = {{P}reliminary {P}roceedings of the 8th {I}nternational
{W}orkshop on {S}ecurity {I}ssues in
{C}oordination {M}odels, {L}anguages and
{S}ystems ({SecCo}'10)},
author = {Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D. and
Steel, Graham},
title = {A~Formal Analysis of Authentication in the~{TPM} (short paper)},
nopages = {},
nmnote = {did not appear in postproc. EPTCS 51},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DKRS-secco10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DKRS-secco10.pdf},
ps = {DKRS-secco10.ps}
}
@article{bwa-jcs10,
publisher = {{IOS} Press},
journal = {Journal of Computer Security},
author = {Baudet, Mathieu and Warinschi,
Bogdan and Abadi, Mart{\'\i}n},
title = {Guessing Attacks and the Computational Soundness of Static
Equivalence},
volume = 18,
number = 5,
pages = {909-968},
month = sep,
year = 2010,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/bwa-jcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bwa-jcs10.pdf},
doi = {10.3233/JCS-2009-0386},
abstract = {The indistinguishability of two pieces of data (or two lists of
pieces of data) can be represented formally in terms of a relation called
static equivalence. Static equivalence depends on an underlying equational
theory. The choice of an inappropriate equational theory can lead to
overly pessimistic or overly optimistic notions of indistinguishability,
and in turn to security criteria that require protection against
impossible attacks or---worse yet---that ignore feasible ones. In this
paper, we define and justify an equational theory for standard,
fundamental cryptographic operations. This equational theory yields a
notion of static equivalence that implies computational
indistinguishability. Static equivalence remains liberal enough for use in
applications. In particular, we develop and analyze a principled formal
account of guessing attacks in terms of static equivalence.}
}
@inproceedings{bgl-setop10,
address = {Athens, Greece},
month = sep,
year = 2010,
volume = 6514,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cavalli, Ana and Leneutre, Jean},
acronym = {{DPM}{{\slash}}{SETOP}'10},
booktitle = {{R}evised {S}elected {P}apers of the 5th {I}nternational {W}orkshop
on {D}ata {P}rivacy {M}anagement and {A}utonomous
{S}pontaneous {S}ecurity ({DPM}'10) and 3rd {I}nternational
{W}orkshop on {A}utonomous
and {S}pontaneous {S}ecurity ({SETOP}'10)},
author = {Benzina, Hedi and Goubault{-}Larrecq, Jean},
title = {Some Ideas on Virtualized Systems Security, and Monitors},
pages = {244-258},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/bgl-setop10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bgl-setop10.pdf},
doi = {10.1007/978-3-642-19348-4_18},
abstract = {Virtualized systems such as Xen, VirtualBox, VMWare or QEmu have
been proposed to increase the level of security achievable on personal
computers. On the other hand, such virtualized systems are now targets for
attacks. We propose an intrusion detection architecture for virtualized
systems, and discuss some of the security issues that arise. We argue that
a weak spot of such systems is domain zero administration, which is left
entirely under the administrator's responsibility, and is in particular
vulnerable to trojans. To~avert some of the risks, we~propose to install a
role-based access control model with possible role delegation, and to
describe all undesired activity ows through simple temporal formulas. We
show how the latter are compiled into Orchids rules, via a fragment of
linear temporal logic, through a generalization of the so-called history
variable mechanism.}
}
@article{LV-dc10,
publisher = {Springer},
journal = {Distributed Computing},
author = {Lozes, {\'E}tienne and Villard, Jules},
title = {A~spatial equational logic for the applied \(\pi\)-calculus},
pages = {61-83},
volume = 23,
number = 1,
year = 2010,
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LV-discomp10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LV-discomp10.pdf},
doi = {10.1007/s00446-010-0112-6},
abstract = {Spatial logics have been proposed to reason locally and
modularly on algebraic models of distributed systems. In this paper we
define the spatial equational logic \(\textsf{A}\pi\textsf{L}\) whose
models are processes of the applied \(\pi\)-calculus. This extension of
the \(\pi\)-calculus allows term manipulation and records communications
as aliases in a frame, thus augmenting the predefined underlying
equational theory. Our logic allows one to reason locally either on frames
or on processes, thanks to static and dynamic spatial operators. We study
the logical equivalences induced by various relevant fragments of
\(\textsf{A}\pi\textsf{L}\), and show in particular that the whole logic
induces a coarser equivalence than structural congruence. We give
characteristic formulae for some of these equivalences and for static
equivalence. Going further into the exploration of
\(\textsf{A}\pi\textsf{L}\)'s expressivity, we also show that it can
eliminate standard term quantification.}
}
@inproceedings{andre-infinity2010,
address = {Singapore},
month = sep,
year = 2010,
volume = 39,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Chen, Yu-Fang and Rezine, Ahmed},
acronym = {{INFINITY}'10},
booktitle = {{P}roceedings of the 12th {I}nternational
{W}orkshops on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'10)},
author = {Andr{\'e}, {\'E}tienne},
title = {{IMITATOR~II}: A~Tool for Solving the Good Parameters Problem in Timed
Automata},
pages = {91-99},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/andre-infinity10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/andre-infinity10.pdf},
doi = {10.4204/EPTCS.39.7},
abstract = {We present here IMITATOR~II, a~new version of IMITATOR, a~tool
implementing the {"}inverse method{"} for parametric timed automata: given
a reference valuation of the parameters, it~synthesizes a constraint such
that, for any valuation satisfying this constraint, the system behaves the
same as under the reference valuation in terms of traces, \textit{i.e.},
alternating sequences of locations and actions.\par
IMITATOR~II also implements the {"}behavioral cartography algorithm{"},
allowing us to solve the following good parameters problem: find a set of
valuations within a given bounded parametric domain for which the system
behaves well.\par
We present new features and optimizations of the tool, and give results of
applications to various examples of asynchronous circuits and
communication protocols.}
}
@inproceedings{demri-infinity2010,
address = {Singapore},
month = sep,
year = 2010,
volume = 39,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Chen, Yu-Fang and Rezine, Ahmed},
acronym = {{INFINITY}'10},
booktitle = {{P}roceedings of the 12th {I}nternational
{W}orkshops on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'10)},
author = {Demri, St{\'e}phane},
title = {On Selective Unboundedness of~{VASS}},
pages = {1-15},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/demri-infinity10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/demri-infinity10.pdf},
doi = {10.4204/EPTCS.39.1},
abstract = {Numerous properties of vector addition systems with states
amount to checking the (un)boundedness of some selective feature
(\textit{e.g.}, number of reversals, run length). Some of these features
can be checked in exponential space by using Rackoff's proof or its
variants, combined with Savitch's theorem. However, the question is still
open for many others, e.g., reversal-boundedness. In the paper, we
introduce the class of generalized unboundedness properties that can be
verified in exponential space by extending Rackoff's technique, sometimes
in an unorthodox way. We obtain new optimal upper bounds, for example for
place-boundedness problem, reversal-boundedness detection (several
variants exist), strong promptness detection problem and regularity
detection. Our analysis is sufficiently refined so as we also obtain a
polynomial-space bound when the dimension is fixed.}
}
@phdthesis{carre-phd2010,
author = {Carr{\'e}, Jean-Loup},
title = {Analyse statique de programmes multi-thread pour l'embarqu{\'e}},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2010,
month = jul,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/carre-these10.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/carre-these10.pdf}
}
@phdthesis{akshay-phd2010,
author = {Akshay, S.},
title = {Sp{\'e}cification et v{\'e}rification pour des syst{\`e}mes
distribu{\'e}s et temporis{\'e}s},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2010,
month = jul,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/akshay-phd.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/akshay-phd.pdf}
}
@inproceedings{BDF-nsmc10,
address = {Williamsburg, Virginia, USA},
month = sep,
year = 2010,
editor = {Benzi, Michele and Dayar, Tugrul},
acronym = {{NSMC}'10},
booktitle = {{P}roceedings of the 6th {I}nternational {M}eeting on the
{N}umerical {S}olution of {M}arkov {C}hain ({NSMC}'10)},
author = {Bu\v{s}i\'{c}, Ana and Djafri, Hilal and Fourneau, Jean-Michel},
title = {Stochastic Bounds for Censored {M}arkov Chains},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDF-nsmc10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDF-nsmc10.pdf},
abstract = {Censored Markov chains~(CMC) allow to represent the conditional
behavior of a system within a subset of observed states. They provide a
theoretical framework to study the truncation of a discrete-time Markov
chain when the generation of the state-space is too hard or when the
number of states is too large. But the stochastic matrix of a CMC may be
difficult to obtain. Dayar \textit{et~al.}~(2006) have proposed an
algorithm, called DPY, that computes a stochastic bounding matrix for a
CMC with a smaller complexity with only a partial knowledge of the chain.
We prove that this algorithm is optimal for the information they take into
account. We also show how some additional knowledge on the chain can
improve stochastic bounds for~CMC.}
}
@inproceedings{BCFS-ccs10,
address = {Chicago, Illinois, USA},
month = oct,
year = 2010,
publisher = {ACM Press},
acronym = {{CCS}'10},
booktitle = {{P}roceedings of the 17th {ACM} {C}onference
on {C}omputer and {C}ommunications {S}ecurity
({CCS}'10)},
author = {Bortolozzo, Matteo and Centenaro, Matteo and Focardi,
Riccardo and Steel, Graham},
title = {Attacking and Fixing {PKCS}\#11 Security Tokens},
pages = {260-269},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCFS-ccs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCFS-ccs10.pdf},
doi = {10.1145/1866307.1866337},
abstract = {We show how to extract sensitive cryptographic keys from a
variety of commercially available tamper resistant cryptographic security
tokens, exploiting vulnerabilities in their RSA PKCS\#11 based APIs. The
attacks are performed by Tookan, an automated tool we have developed,
which reverse-engineers the particular token in use to deduce its
functionality, constructs a model of its API for a model checker, and then
executes any attack trace found by the model checker directly on the
token. We describe the operation of Tookan and give results of testing the
tool on 17 commercially available tokens: 9~were vulnerable to attack,
while the other 8 had severely restricted functionality. One of the
attacks found by the model checker has not previously appeared in the
literature. We show how Tookan may be used to verify patches to insecure
devices, and give a secure configuration that we have implemented in a
patch to a software token simulator. This is the first such configuration
to appear in the literature that does not require any new cryptographic
mechanisms to be added to the standard. We comment on lessons for future
key management APIs.}
}
@article{BJLMO-jwcn10,
publisher = {Hindawi Publishing Corp.},
journal = {EURASIP Journal on Wireless Communications and Networking},
author = {Brihaye, {\relax Th}omas and Jungers, Marc and Lasaulce,
Samson and Markey, Nicolas and Oreiby, Ghassan},
title = {Using Model Checking for Analyzing Distributed Power Control
Problems},
year = 2010,
volume = {2010},
number = {861472},
nopages = {},
month = jun,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BJLMO-jwcn10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BJLMO-jwcn10.pdf},
doi = {10.1155/2010/861472},
abstract = {Model checking~(MC) is a formal verification technique which has
been known and still knows a resounding success in the computer science
community. Realizing that the distributed power control~(PC) problem can be
modeled by a timed game between a given transmitter and its environment,
the authors wanted to know whether this approach can be applied to
distributed~PC. It~turns out that it can be applied successfully and allows
one to analyze realistic scenarios including the case of discrete transmit
powers and games with incomplete information. The proposed methodology is
as follows. We state some objectives a transmitter-receiver pair would like
to reach. The network is modeled by a game where transmitters are
considered as timed automata interacting with each other. The objectives
are then translated into timed alternating-time temporal logic formulae and
MC is exploited to know whether the desired properties are verified and
determine a winning strategy.}
}
@article{CKW-jar2010,
publisher = {Springer},
journal = {Journal of Automated Reasoning},
author = {Cortier, V{\'e}ronique and Kremer, Steve and Warinschi, Bogdan},
title = {A~Survey of Symbolic Methods in Computational Analysis of
Cryptographic Systems},
year = 2010,
month = apr,
pages = {225-259},
number = {3-4},
volume = {46},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CKW-jar10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CKW-jar10.pdf},
doi = {10.1007/s10817-010-9187-9},
abstract = {Since the 1980s, two approaches have been developed for
analyzing security protocols. One of the approaches relies on a
computational model that considers issues of complexity and probability.
This approach captures a strong notion of security, guaranteed against all
probabilistic polynomial-time attacks. The other approach relies on a
symbolic model of protocol executions in which cryptographic primitives
are treated as black boxes. Since the seminal work of Dolev and Yao, it
has been realized that this latter approach enables significantly simpler
and often automated proofs. However, the guarantees that it offers with
respect to the more detailed computational models have been quite
unclear.\par
For more than twenty years the two approaches have coexisted but evolved
mostly independently. Recently, significant research efforts attempt to
develop paradigms for cryptographic systems analysis that combines the
best of both worlds. There are two broad directions that have been
followed. Computational soundness aims to establish sufficient conditions
under which results obtained using symbolic models imply security under
computational models. The direct approach aims to apply the principles and
the techniques developed in the context of symbolic models directly to
computational ones.\par
In this paper we survey existing results along both of these directions.
Our goal is to provide a rather complete summary that could act as a quick
reference for researchers who want to contribute to the field, want to
make use of existing results, or just want to get a better picture of what
results already exist.}
}
@inproceedings{KRS-esorics10,
address = {Athens, Greece},
month = sep,
year = 2010,
volume = {6345},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gritzalis, Dimitris and Preneel, Bart},
acronym = {{ESORICS}'10},
booktitle = {{P}roceedings of the 15th {E}uropean {S}ymposium on
{R}esearch in {C}omputer {S}ecurity ({ESORICS}'10)},
author = {Kremer, Steve and Ryan, Mark D. and Smyth, Ben},
title = {Election verifiability in electronic voting protocols},
pages = {389-404},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KRS-esorics10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KRS-esorics10.pdf},
doi = {10.1007/978-3-642-15497-3_24},
abstract = {We present a formal, symbolic definition of election
verifiability for electronic voting protocols in the context of the
applied pi calculus. Our definition is given in terms of boolean tests
which can be performed on the data produced by an election. The definition
distinguishes three aspects of verifiability: individual, universal and
eligibility verifiability. It also allows us to determine precisely which
aspects of the system's hardware and software must be trusted for the
purpose of election verifiability. In contrast with earlier work our
definition is compatible with a large class of electronic voting schemes,
including those based on blind signatures, homomorphic encryption and
mixnets. We demonstrate the applicability of our formalism by analysing
three protocols: FOO, Helios~2.0, and Civitas (the latter two have been
deployed).}
}
@inproceedings{DDS-esorics10,
address = {Athens, Greece},
month = sep,
year = 2010,
volume = {6345},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gritzalis, Dimitris and Preneel, Bart},
acronym = {{ESORICS}'10},
booktitle = {{P}roceedings of the 15th {E}uropean {S}ymposium on
{R}esearch in {C}omputer {S}ecurity ({ESORICS}'10)},
author = {Dahl, Morten and Delaune, St{\'e}phanie and Steel, Graham},
title = {Formal Analysis of Privacy for Vehicular Mix-Zones},
pages = {55-70},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-esorics10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-esorics10.pdf},
ps = {DDS-esorics10.ps},
doi = {10.1007/978-3-642-15497-3_4},
abstract = {Safety critical applications for recently proposed vehicle to
vehicle ad-hoc networks~(VANETs) rely on a beacon signal, which poses a
threat to privacy since it could allow a vehicle to be tracked. Mix-zones,
where vehicles encrypt their transmissions and then change their
identifiers, have been proposed as a solution to this problem. \par
In this work, we~describe a formal analysis of mix-zones. We~model a
mix-zone and propose a formal definition of privacy for such a zone.
We~give a set of necessary conditions for any mix-zone protocol to preserve
privacy. We~analyse, using the tool ProVerif, a~particular proposal for key
distribution in mix-zones, the CMIX protocol. We~report attacks on privacy
and we propose a fix.}
}
@inproceedings{phs-rp10,
address = {Brno, Czech Republic},
month = aug,
year = 2010,
volume = 6227,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ku{\v c}era, Anton{\'\i}n and Potapov, Igor},
acronym = {{RP}'10},
booktitle = {{P}roceedings of the 4th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'10)},
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Lossy Counter Machines Decidability Cheat Sheet},
pages = {51-75},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/phs-rp10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/phs-rp10.pdf},
doi = {10.1007/978-3-642-15349-5_4},
abstract = {Lossy counter machines (LCM's) are a variant of Minsky counter
machines based on weak (or~unreliable) counters in the sense that they can
decrease nondeterministically and without notification. This model,
introduced by R.~Mayr [TCS~297:337-354 (2003)], is not yet very
well known, even though it has already proven useful for establishing
hardness results.\par
In this paper we survey the basic theory of LCM's and their verification
problems, with a focus on the decidability/undecidability divide. }
}
@inproceedings{AF-rp10,
address = {Brno, Czech Republic},
month = aug,
year = 2010,
volume = 6227,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ku{\v c}era, Anton{\'\i}n and Potapov, Igor},
acronym = {{RP}'10},
booktitle = {{P}roceedings of the 4th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'10)},
author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent},
title = {Behavioral Cartography of Timed Automata},
pages = {76-90},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AF-rp10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AF-rp10.pdf},
doi = {10.1007/978-3-642-15349-5_5},
abstract = {We aim at finding a set of timing parameters for which a given
timed automaton has a {"}good{"} behavior. We~present here a novel
approach based on the decomposition of the parametric space into
behavioral tiles, \textit{i.e.}, sets of parameter valuations for which
the behavior of the system is uniform. This gives us a behavioral
cartography according to the values of the parameters.\par
It is then straightforward to partition the space into a {"}good{"} and a
{"}bad{"} subspace, according to the behavior of the tiles. We extend this
method to probabilistic systems, allowing to decompose the parametric
space into tiles for which the minimal (resp. maximal) probability of
reaching a given location is uniform. An~implementation has been made, and
experiments successfully conducted.}
}
@inproceedings{CJ-notere10,
address = {Tozeur, Tunisia},
month = may # {-} # jun,
year = 2010,
publisher = {{IEEE} Computer Society Press},
noeditor = {},
acronym = {{NOTERE}'10},
booktitle = {{A}ctes de la 10{\`e}me {C}onf{\'e}rence {I}nternationale sur les
{NO}uvelles {TE}chnologies de la {R\'E}partition ({NOTERE}'10)},
author = {Chatain, {\relax Th}omas and Jard, Claude},
title = {S{\'e}mantique concurrente symbolique des r{\'e}seaux
de {P}etri saufs et d{\'e}pliages finis des r{\'e}seaux
temporels},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CJ-notere10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CJ-notere10.pdf},
abstract = {On consid\`ere des r\'eseaux de Petri color\'es, \`a contraintes
lin\'eaires et pouvant poss\'eder des arcs de lecture. Sur cette classe,
on d\'efinit une s\'emantique concurrente en termes de processus d'ordre
partiel permettant de garder explicite l'ind\'ependance entre des tirs de
transitions. L'ensemble des processus peut \^etre repr\'esent\'e en
utilisant la notion de d\'epliage symbolique. Nous montrons alors comment
les r\'eseaux de Petri temporels peuvent \^etre cod\'es dans ce mod\`ele
\`a l'aide d'une transformation syntaxique pr\'eservant la concurrence.
Cette transformation permet de d\'efinir la notion de d\'epliage de
r\'eseaux de Petri temporels et d'en donner une repr\'esentation par
pr\'efixe fini.}
}
@inproceedings{DHLN-acsd10,
address = {Braga, Portugal},
month = jun,
year = 2010,
publisher = {{IEEE} Computer Society Press},
editor = {Gomes, Lu{\'\i}s and Khomenko, Victor},
acronym = {{ACSD}'10},
booktitle = {{P}roceedings of the 10th {I}nternational
{C}onference on {A}pplication of {C}oncurrency
to {S}ystem {D}esign
({ACSD}'10)},
author = {Doyen, Laurent and Henzinger, {\relax Th}omas A. and Legay, Axel and
Nickovic, Dejan},
title = {Robustness of Sequential Circuits},
pages = {77-84},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DHLN-acsd10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DHLN-acsd10.pdf},
doi = {10.1109/ACSD.2010.26},
abstract = {Digital components play a central role in the design of complex
embedded systems. These components are interconnected with other, possibly
analog, devices and the physical environment. This environment cannot be
entirely captured and can provide inaccurate input data to the component.
It~is thus important for digital components to have a robust behavior,
\textit{i.e.},~the presence of a small change in the input sequences
should not result in a drastic change in the output sequences.\par
In this paper, we study a notion of robustness for sequential circuits.
However, since sequential circuits may have parts that are naturally
discontinuous (\textit{e.g.},~digital controllers with switching
behavior), we~need a flexible framework that accommodates this fact and
leaves discontinuous parts of the circuit out from the robustness
analysis. As a consequence, we~consider sequential circuits that have
their input variables partitioned into two disjoint sets: control and
disturbance variables. Our contributions are (1)~a~definition of
robustness for sequential circuits as a form of continuity with respect to
disturbance variables, (2)~the~characterization of the exact class of
sequential circuits that are robust according to our definition,
(3)~an~algorithm to decide whether a sequential circuit is robust
or~not.}
}
@inproceedings{DDGRT-csl10,
address = {Brno, Czech Republic},
month = aug,
year = 2010,
volume = {6247},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Dawar, Anuj and Veith, Helmut},
acronym = {{CSL}'10},
booktitle = {{P}roceedings of the 19th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'10)},
author = {Degorre, Aldric and Doyen, Laurent and Gentilini, Raffaella
and Raskin, Jean-Fran{\c{c}}ois and Toru{\'n}czyk, Szymon},
title = {Energy and Mean-Payoff Games with Imperfect Information},
pages = {260-274},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDGRT-csl10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDGRT-csl10.pdf},
doi = {10.1007/978-3-642-15205-4_22},
abstract = {We consider two-player games with imperfect information and
quantitative objective. The game is played on a weighted graph with a
state space partitioned into classes of indistinguishable states, giving
players partial knowledge of the state. In an energy game, the weights
represent resource consumption and the objective of the game is to
maintain the sum of weights always nonnegative. In a mean-payoff game, the
objective is to optimize the limit-average usage of the resource. We show
that the problem of determining if an energy game with imperfect
information with fixed initial credit has a winning strategy is decidable,
while the question of the existence of some initial credit such that the
game has a winning strategy is undecidable. This undecidability result
carries over to mean-payoff games with imperfect information. On the
positive side, using a simple restriction on the game graph (namely, that
the weights are visible), we show that these problems become
EXPTIME-complete.}
}
@inproceedings{PhS-mfcs10,
address = {Brno, Czech Republic},
month = aug,
year = 2010,
volume = 6281,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hlin{\v e}n{\'y}, Petr and Ku{\v c}era, Anton{\'\i}n},
acronym = {{MFCS}'10},
booktitle = {{P}roceedings of the 35th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'10)},
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Revisiting {A}ckermann-Hardness for Lossy Counter Machines
and Reset {P}etri Nets},
pages = {616-628},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/phs-mfcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/phs-mfcs10.pdf},
doi = {10.1007/978-3-642-15155-2_54},
abstract = {We prove that coverability and termination are not
primitive-recursive for lossy counter machines and for Reset Petri nets.}
}
@inproceedings{CDGH-mfcs10,
address = {Brno, Czech Republic},
month = aug,
year = 2010,
volume = 6281,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hlin{\v e}n{\'y}, Petr and Ku{\v c}era, Anton{\'\i}n},
acronym = {{MFCS}'10},
booktitle = {{P}roceedings of the 35th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'10)},
author = {Chatterjee, Krishnendu and Doyen, Laurent and
Gimbert, Hugo and Henzinger, {\relax Th}omas A.},
title = {Randomness for Free},
pages = {246-257},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDGH-mfcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDGH-mfcs10.pdf},
doi = {10.1007/978-3-642-15155-2_23},
abstract = {We consider two-player zero-sum games on graphs. These games can
be classified on the basis of the information of the players and on the
mode of interaction between them. On the basis of information the
classification is as follows: (a)~partial-observation (both players have
partial view of the game); (b)~one-sided complete-observation (one player
has complete observation); and (c)~complete-observation (both players have
complete view of the game). On~the basis of mode of interaction we have
the following classification: (a)~concurrent (players interact
simultaneously); and (b)~turn-based (players interact in turn). The~two
sources of randomness in these games are randomness in transition function
and randomness in strategies. In general, randomized strategies are more
powerful than deterministic strategies, and randomness in transitions
gives more general classes of games. We~present a complete
characterization for the classes of games where randomness is not
helpful~in: (a)~the~transition function (probabilistic transition can be
simulated by deterministic transition); and (b)~strategies (pure
strategies are as powerful as randomized strategies). As~consequence of
our characterization we obtain new undecidability results for these games.}
}
@inproceedings{FP-mfcs10,
address = {Brno, Czech Republic},
month = aug,
year = 2010,
volume = 6281,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hlin{\v e}n{\'y}, Petr and Ku{\v c}era, Anton{\'\i}n},
acronym = {{MFCS}'10},
booktitle = {{P}roceedings of the 35th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'10)},
author = {Fontaine, Ga{\"e}lle and Place, {\relax Th}omas},
title = {Classes of trees definable in the {{\(\mu\)}}-calculus},
pages = {381-392},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FP-mfcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FP-mfcs10.pdf},
doi = {10.1007/978-3-642-15155-2_34},
abstract = {We are interested in frame definability of classes of trees,
using formulas of the \(\mu\)-calculus. In this set up, the proposition
letters (or in other words, the free variables) in the \(\mu\)-formulas
correspond to second order variables over which universally quantify. Our
main result is a semantic characterization of the \textbf{MSO} definable
classes of trees that are definable by a \(\mu\)-formula. We~also show
that it is decidable whether a given \textbf{MSO} formula corresponds to a
\(\mu\)-formula, in the sense that they define the same class of trees.}
}
@inproceedings{CDH-mfcs10,
address = {Brno, Czech Republic},
month = aug,
year = 2010,
volume = 6281,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hlin{\v e}n{\'y}, Petr and Ku{\v c}era, Anton{\'\i}n},
acronym = {{MFCS}'10},
booktitle = {{P}roceedings of the 35th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'10)},
author = {Chatterjee, Krishnendu and Doyen, Laurent and Henzinger,
{\relax Th}omas A.},
title = {Qualitative Analysis of Partially-observable {M}arkov Decision
Processes},
pages = {258-269},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDH-mfcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDH-mfcs10.pdf},
doi = {10.1007/978-3-642-15155-2_24},
abstract = {We study observation-based strategies for partially-observable
Markov decision processes (POMDPs) with parity objectives.
An~observation-based strategy relies on partial information about the
history of a play, namely, on the past sequence of observations.
We~consider qualitative analysis problems: given a POMDP with a parity
objective, decide whether there exists an observation-based strategy to
achieve the objective with probability~\(1\) (almost-sure winning), or
with positive probability (positive winning). Our main results are
twofold. First, we present a complete picture of the computational
complexity of the qualitative analysis problem for POMDPs with parity
objectives and its subclasses: safety, reachability, B{\"u}chi, and coB{\"u}chi
objectives. We~establish several upper and lower bounds that were not
known in the literature. Second, we give optimal bounds (matching upper
and lower bounds) for the memory required by pure and randomized
observation-based strategies for each class of objectives.}
}
@inproceedings{OU-mfcs10,
address = {Brno, Czech Republic},
month = aug,
year = 2010,
volume = 6281,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hlin{\v e}n{\'y}, Petr and Ku{\v c}era, Anton{\'\i}n},
acronym = {{MFCS}'10},
booktitle = {{P}roceedings of the 35th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'10)},
author = {Olschewski, J{\"o}rg and Ummels, Michael},
title = {The Complexity of Finding Reset Words in
Finite Automata},
pages = {568-579},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/OU-mfcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/OU-mfcs10.pdf},
doi = {10.1007/978-3-642-15155-2_50},
abstract = {We study several problems related to finding reset words in
deterministic finite automata. In~particular, we~establish that the
problem of deciding whether a shortest reset word has length~\(k\) is
complete for the complexity class~\(DP\). This result answers a question
posed by Volkov. For the search problems of finding a shortest reset word
and the length of a shortest reset word, we establish membership in the
complexity classes FP\textsuperscript{NP} and FP\textsuperscript{NP[log]},
respectively. Moreover, we show that both these problems are hard for
FP\textsuperscript{NP[log]}. Finally, we~observe that computing a reset
word of a given length is FNP-complete.}
}
@inproceedings{EHH-apnoc10,
address = {Braga, Portugal},
month = jun,
year = 2010,
editor = {Sidorova, Natalia and Serebrenik, Alexander},
acronym = {{APNOC}'10},
booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on
{A}bstractions for {P}etri {N}ets and {O}ther {M}odels of
{C}oncurrency ({APNOC}'10)},
author = {El{~}Hog{-}Benzina, Dorsaf and Haddad, Serge and Hennicker, Rolf},
title = {Process Refinement and Asynchronous Composition with Modalities},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/EHH-apnoc10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/EHH-apnoc10.pdf},
abstract = {We propose a framework for the specification of infinite state
systems based on Petri nets with distinguished may- and must-transitions
(called modalities) which specify the allowed and the required behavior of
refinements and hence of implementations. Formally, refinements are
defined by relating the modal language specifications generated by two
modal Petri nets according to the refinement relation for modal language
specifications. We show that this refinement relation is decidable if the
underlying modal Petri nets are weakly deterministic. We also show that
the membership problem for the class of weakly deterministic modal Petri
nets is decidable. As an important application of our approach we consider
I/O-Petri nets which are obtained by asynchronous composition and thus
exhibit inherently an infinite behavior.}
}
@inproceedings{CDEHR-concur10,
address = {Paris, France},
month = aug # {-} # sep,
year = 2010,
volume = {6269},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gastin, Paul and Laroussinie, Fran{\c{c}}ois},
acronym = {{CONCUR}'10},
booktitle = {{P}roceedings of the 21st
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'10)},
author = {Chatterjee, Krishnendu and Doyen, Laurent and Edelsbrunner,
Herbert and Henzinger, {\relax Th}omas A. and Rannou, Philippe},
title = {Mean-Payoff Automaton Expressions},
pages = {269-283},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDEHR-concur10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDEHR-concur10.pdf},
doi = {10.1007/978-3-642-15375-4_19},
abstract = {Quantitative languages are an extension of boolean languages
that assign to each word a real number. Mean-payoff automata are finite
automata with numerical weights on transitions that assign to each
infinite path the long-run average of the transition weights. When the
mode of branching of the automaton is deterministic, nondeterministic, or
alternating, the corresponding class of quantitative languages is not
robust as it is not closed under the pointwise operations of max, min,
sum, and numerical complement. Nondeterministic and alternating
mean-payoff automata are not decidable either, as the quantitative
generalization of the problems of universality and language inclusion is
undecidable. We introduce a new class of quantitative languages, defined
by mean-payoff automaton expressions, which is robust and decidable: it is
closed under the four pointwise operations, and we show that all decision
problems are decidable for this class. Mean-payoff automaton expressions
subsume deterministic mean-payoff automata, and we show that they have
expressive power incomparable to nondeterministic and alternating
mean-payoff automata. We also present for the first time an algorithm to
compute distance between two quantitative languages, and in our case the
quantitative languages are given as mean-payoff automaton expressions.}
}
@inproceedings{BBM-concur10,
address = {Paris, France},
month = aug # {-} # sep,
year = 2010,
volume = {6269},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gastin, Paul and Laroussinie, Fran{\c{c}}ois},
acronym = {{CONCUR}'10},
booktitle = {{P}roceedings of the 21st
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'10)},
author = {Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas},
title = {{N}ash Equilibria for Reachability Objectives in Multi-player Timed Games},
pages = {192-206},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBM-concur10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBM-concur10.pdf},
doi = {10.1007/978-3-642-15375-4_14},
abstract = {We propose a procedure for computing Nash equilibria in
multi-player timed games with reachability objectives. Our procedure is
based on the construction of a finite concurrent game, and on a generic
characterization of Nash equilibria in (possibly infinite) concurrent
games. Along the way, we~use our characterization to compute Nash
equilibria in finite concurrent games.}
}
@inproceedings{BBM-formats10,
address = {Vienna, Austria},
month = sep,
year = 2010,
volume = {6246},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Chatterjee, Krishnendu and Henziner, Thomas A.},
acronym = {{FORMATS}'10},
booktitle = {{P}roceedings of the 8th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'10)},
author = {Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas},
title = {Computing Equilibria in Two-Player Timed Games {\textit{via}}~Turn-Based
Finite Games},
pages = {62-76},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBM-formats10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBM-formats10.pdf},
doi = {10.1007/978-3-642-15297-9_7},
abstract = {We study two-player timed games where the objectives of the two
players are not opposite. We focus on the standard notion of Nash
equilibrium and propose a series of transformations that builds two finite
turn-based games out of a timed game, with a precise correspondence
between Nash equilibria in the original and in final games. This provides
us with an algorithm to compute Nash equilibria in two-player timed games
for large classes of properties.}
}
@inproceedings{BCH-time10,
address = {Paris, France},
month = sep,
year = 2010,
publisher = {{IEEE} Computer Society Press},
editor = {Markey, Nicolas and Wijsen, Jef},
acronym = {{TIME}'10},
booktitle = {{P}roceedings of the 17th {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'10)},
author = {Balaguer, Sandie and Chatain, {\relax Th}omas and Haar, Stefan},
title = {A~Concurrency-Preserving Translation from Time {P}etri Nets to Networks of Timed
Automata},
pages = {77-84},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-time10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-time10.pdf},
doi = {10.1109/TIME.2010.12},
abstract = {Real-time distributed systems may be modeled in different
formalisms such as time Petri nets~(TPN) and networks of timed
automata~(NTA). This paper focuses on translating a \(1\)-bounded TPN into
an NTA and considers an equivalence which takes the distribution of
actions into account. This translation is extensible to bounded~TPNs.
We~first use \(S\)-invariants to decompose the net into components that
give the structure of the automata, then we add clocks to provide the
timing information. Although we have to use an extended syntax in the
timed automata, this is a novel approach since the other transformations
and comparisons of these models did not consider the preservation of
concurrency.}
}
@inproceedings{BHS-time10,
address = {Paris, France},
month = sep,
year = 2010,
publisher = {{IEEE} Computer Society Press},
editor = {Markey, Nicolas and Wijsen, Jef},
acronym = {{TIME}'10},
booktitle = {{P}roceedings of the 17th {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'10)},
author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Sassolas, Mathieu},
title = {Real Time Properties for Interrupt Timed Automata},
pages = {69-76},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHS-time10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHS-time10.pdf},
doi = {10.1109/TIME.2010.11},
abstract = {Interrupt Timed Automata (ITA) have been introduced to model
multi-task systems with interruptions. They form a~subclass of stopwatch
automata, where the real valued variables (with rate \(0\) or~\(1\)) are
organized along priority levels. While reachability is undecidable with
usual stopwatches, the problem was proved decidable for~ITA. In~this work,
after giving answers to some questions left open about expressiveness,
closure, and complexity for~ITA, our~main purpose is to investigate the
verification of real time properties over~ITA. While we prove that model
checking a variant of the timed logic TCTL is undecidable, we nevertheless
give model checking procedures for two relevant fragments of this logic:
one where formulas contain only model clocks and another one where
formulas have a single external clock.}
}
@inproceedings{HMY-iscc10,
address = {Riccione, Italy},
month = jun,
year = 2010,
publisher = {{IEEE} Computer Society Press},
noeditor = {},
acronym = {{ISCC}'10},
booktitle = {{P}roceedings of the 15th {IEEE} {S}ymposium on {C}omputers and
{C}ommunications ({ISCC}'10)},
author = {Haddad, Serge and Mokdad, Lynda and Youcef, Samir},
title = {Response time of {BPEL4WS} constructors},
pages = {695-700},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HMY-iscc10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HMY-iscc10.pdf},
doi = {10.1109/ISCC.2010.5546538},
abstract = {Response time is an important factor for every software system
and it becomes more salient when it is associated with introducing novel
technologies, such as Web services. Most performance evaluation of Web
services are focused toward composite Web services and their response
time. One important limitation of existing work is in the fact that only
constant or service exponential time distribution are considered. However,
experimental results have shown that the Web services response times is
typically heavy-tailed, in particulary, if there are heterogeneous. So,
heavy-tailed response times should be considered in the dimensioning Web
services. In this study, we propose analytical formulas for mean response
times for structured BPEL constructors such as \emph{sequence},
\emph{flow} and \emph{switch} constructors,~etc. The difference with
previous studies in the literature, is that we consider heterogenous
servers, the number of invoked elementary Web services can be variable and
the elementary Web services response times are heavy-tailed.}
}
@inproceedings{DDS-fcsprivmod10,
address = {Edinburgh, Scotland, UK},
month = jul,
year = 2010,
editor = {Cortier, V{\'e}ronique and Ryan, Mark D. and
Shmatikov, Vitaly},
acronym = {{FCS-PrivMod}'10},
booktitle = {{P}roceedings of the {W}orkshop on {F}oundations of {S}ecurity
and {P}rivacy ({FCS-PrivMod}'10)},
author = {Dahl, Morten and Delaune, St{\'e}phanie and Steel, Graham},
title = {Formal Analysis of Privacy for Vehicular Mix-Zones},
pages = {55-70},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-10.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-10.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2010-10.ps},
doi = {10.1007/978-3-642-15497-3_4},
abstract = {Safety critical applications for recently proposed vehicle to
vehicle ad-hoc networks (VANETs) rely on a beacon signal, which poses a
threat to privacy since it could allow a vehicle to be tracked. Mix-zones,
where vehicles encrypt their transmissions and then change their
identifiers, have been proposed as a solution to this problem.\par
In this work, we describe a formal analysis of mix-zones. We model a
mix-zone and propose a formal definition of privacy for such a zone. We
give a set of necessary conditions for any mix-zone protocol to preserve
privacy. We analyse, using the tool ProVerif, a particular proposal for
key distribution in mix-zones, the CMIX protocol. We report attacks on
privacy and we propose a fix.}
}
@article{BKM-lmcs10,
journal = {Logical Methods in Computer Science},
author = {Bollig, Benedikt and Kuske, Dietrich and Meinecke, Ingmar},
title = {Propositional Dynamic Logic for Message-Passing Systems},
year = 2010,
month = sep,
volume = 6,
number = {3:16},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BKM-lmcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BKM-lmcs10.pdf},
doi = {10.2168/LMCS-6(3:16)2010},
abstract = {We examine a bidirectional propositional dynamic logic~(PDL) for
finite and infinite message sequence charts~(MSCs) extending
\(\textsf{LTL}\) and \(\textsf{TLC}^{-}\). By~this kind of multi-modal
logic we can express properties both in the entire future and in the past
of an event. Path expressions strengthen the classical until operator of
temporal logic. For every formula defining an MSC language, we construct a
communicating finite-state machine~(CFM) accepting the same language. The
CFM obtained has size exponential in the size of the formula. This
synthesis problem is solved in full generality, \textit{i.e.}, also for
MSCs with unbounded channels. The model checking problem for CFMs and
HMSCs turns out to be in PSPACE for existentially bounded MSCs. Finally,
we show that, for PDL with intersection, the semantics of a formula cannot
be captured by a CFM anymore.}
}
@inproceedings{CS-dlt2010,
address = {London, Ontario, Canada},
month = aug,
year = 2010,
volume = {6224},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gao, Yuan and Lu, Hanlin and Seki, Shinnosuke and Yu, Sheng},
acronym = {{DLT}'10},
booktitle = {{P}roceedings of the 14th {I}nternational
{C}onference on {D}evelopments in {L}anguage {T}heory
({DLT}'10)},
author = {Chambart, Pierre and Schnoebelen, {\relax Ph}ilippe},
title = {Computing blocker sets for the Regular {P}ost Embedding
Problem},
pages = {136-147},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-dlt10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-dlt10.pdf},
doi = {10.1007/978-3-642-14455-4_14},
abstract = {Blocker and coblocker sets are regular languages involved in the
algorithmic solution of the Regular Post Embedding Problem.
We investigate the computability of these languages and
related decision problems.}
}
@inproceedings{Schmitz-acl10,
address = {Uppsala, Sweden},
month = jul,
year = 2010,
publisher = {Association for Computational Linguistics},
acronym = {{ACL}'10},
booktitle = {{P}roceedings of the 48th {A}nnual {M}eeting of the
{A}ssociation for {C}omputational {L}inguistics ({ACL}'10)},
author = {Schmitz, Sylvain},
title = {On the Computational Complexity of Dominance Links
in Grammatical Formalisms},
pages = {514-524},
url = {http://hal.archives-ouvertes.fr/hal-00482396},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Schmitz-acl10.pdf},
abstract = {Dominance links were introduced in grammars to model long
distance scrambling phenomena, motivating the definition of multiset-valued
linear indexed grammars (MLIGs) by Rambow~(1994b), and inspiring quite a
few recent formalisms. It~turns out that MLIGs have since been
rediscovered and reused in a variety of contexts, and that the complexity
of their emptiness problem has become the key to several open questions in
computer science. We survey complexity results and open issues on MLIGs
and related formalisms, and provide new complexity bounds for some
linguistically motivated restrictions.}
}
@article{HNS-tcs10,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {H{\'e}am, Pierre-Cyrille and Nicaud, Cyril and
Schmitz, Sylvain},
title = {Parametric Random Generation of Deterministic Tree
Automata},
year = 2010,
volume = 411,
number = {38-39},
pages = {3469-3480},
month = aug,
url = {http://hal.inria.fr/inria-00511450},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HNS-tcs10.pdf},
doi = {10.1016/j.tcs.2010.05.036},
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~also propose an original parametric random
generation algorithm to produce sequential letter-to-letter transducers
with a fixed number of transitions. 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.}
}
@incollection{DKR-lncs6000,
noaddress = {},
month = may,
year = 2010,
volume = 6000,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
noacronym = {},
booktitle = {{T}owards {T}rustworthy {E}lections -- {N}ew {D}irections in
{E}lectronic {V}oting},
editor = {Chaum, David and Jakobsson, Markus and Rivest, Ronald L. and
Ryan, Peter Y. A. and Benaloh, Josh and Kuty{\l}owski, Miros{\l}aw
and Adida, Ben},
author = {Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D.},
title = {Verifying Privacy-Type Properties of Electronic Voting
Protocols: A~Taster},
pages = {289-309},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DKR-lncs6000.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DKR-lncs6000.pdf},
doi = {10.1007/978-3-642-12980-3_18},
abstract = {While electronic elections promise the possibility of
convenient, efficient and secure facilities for recording and tallying
votes, recent studies have highlighted inadequacies in implemented
systems. These inadequacies provide additional motivation for applying
formal methods to the validation of electronic voting protocols.\par
In this paper we report on some of our recent efforts in using the applied
pi calculus to model and analyse properties of electronic elections. We
particularly focus on anonymity properties, namely vote-privacy and
receipt-freeness. These properties are expressed using observational
equivalence and we show in accordance with intuition that receipt-freeness
implies vote-privacy.\par
We illustrate our definitions on two electronic voting protocols from the
literature. Ideally, these properties should hold even if the election
officials are corrupt. However, protocols that were designed to satisfy
privacy or receipt-freeness 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{CCD-ijcar10,
address = {Edinburgh, Scotland, UK},
month = jul,
year = 2010,
volume = {6173},
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer-Verlag},
editor = {Giesl, J{\"u}rgen and Haehnle, Reiner},
acronym = {{IJCAR}'10},
booktitle = {{P}roceedings of the 5th {I}nternational {J}oint
{C}onference on {A}utomated {R}easoning
({IJCAR}'10)},
author = {Cheval, Vincent and Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie},
title = {Automating security analysis: symbolic equivalence of
constraint systems},
pages = {412-426},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-ijcar10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-ijcar10.pdf},
doi = {10.1007/978-3-642-14203-1_35},
abstract = {We consider security properties of cryptographic protocols, that
are either trace properties (such as confidentiality or authenticity) or
equivalence properties (such as anonymity or strong secrecy).\par
Infinite sets of possible traces are symbolically represented using
\emph{deducibility constraints}. We give a new algorithm that decides the
trace equivalence for the traces that are represented using such
constraints, in the case of signatures, symmetric and asymmetric
encryptions. Our algorithm is implemented and performs well on typical
benchmarks. This is the first implemented algorithm, deciding symbolic
trace equivalence.}
}
@inproceedings{BH-monterey2008,
address = {Budapest, Hungary},
month = apr,
year = 2010,
volume = 6028,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Choppy, {\relax Ch}ristine and Sokolsky, Oleg},
acronym = {{MONTEREY}'08},
booktitle = {{R}evised {S}elected {P}apers of the 15th {M}onterey
{W}orkshop on {F}oundations
of {C}omputer {S}oftware ({MONTEREY}'08)},
author = {Ben{ }Hmida, Mehdi and Haddad, Serge},
title = {Client Synthesis for Aspect Oriented Web Services},
pages = {24-42},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BH-monterey08.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BH-monterey08.pdf},
doi = {10.1007/978-3-642-12566-9_2},
abstract = {Client synthesis for complex Web services is a critical and
still open topic as it will enable more flexibility in the
deployment of such services. In previous works, our team has
developed a theoretical framework based on process algebra
that has led to algorithms and tools for the client
interaction. Here, we show how to generalise our approach
for aspect oriented Web services.}
}
@inproceedings{JGL-icalp10,
address = {Bordeaux, France},
month = jul,
year = 2010,
volume = 6199,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abramsky, Samson and Meyer{ }auf{ }der{ }Heide, Friedhelm
and Spirakis, Paul},
acronym = {{ICALP}'10},
booktitle = {{P}roceedings of the 37th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'10)~-- {P}art~{II}},
author = {Goubault{-}Larrecq, Jean},
title = {Noetherian Spaces in Verification},
pages = {2-21},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-icalp10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-icalp10.pdf},
doi = {10.1007/978-3-642-14162-1_2},
abstract = {Noetherian spaces are a topological concept that generalizes
well quasiorderings. We explore applications to infinite-state
verification problems, and show how this stimulated the search for
infinite procedures \`a la Karp-Miller.}
}
@inproceedings{CS-icalp10,
address = {Bordeaux, France},
month = jul,
year = 2010,
volume = 6199,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abramsky, Samson and Meyer{ }auf{ }der{ }Heide, Friedhelm
and Spirakis, Paul},
acronym = {{ICALP}'10},
booktitle = {{P}roceedings of the 37th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'10)~-- {P}art~{II}},
author = {Chambart, Pierre and Schnoebelen, {\relax Ph}ilippe},
title = {Pumping and Counting on the Regular {P}ost Embedding Problem},
pages = {64-75},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-icalp10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-icalp10.pdf},
doi = {10.1007/978-3-642-14162-1_6},
abstract = {The Regular Post Embedding Problem is a variant of Post's
Correspondence Problem where one compares strings with the subword
relation and imposes additional regular constraints on admissible
solutions. It is known that this problem is decidable, albeit with very
high complexity.\par
We consider and solve variant problems where the set of solutions is
compared to regular constraint sets and where one counts the number of
solutions. Our positive results rely on two non-trivial pumping lemmas for
Post-embedding languages and their complements.}
}
@inproceedings{CD-icalp10,
address = {Bordeaux, France},
month = jul,
year = 2010,
volume = 6199,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abramsky, Samson and Meyer{ }auf{ }der{ }Heide, Friedhelm
and Spirakis, Paul},
acronym = {{ICALP}'10},
booktitle = {{P}roceedings of the 37th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'10)~-- {P}art~{II}},
author = {Chatterjee, Krishnendu and Doyen, Laurent},
title = {Energy Parity Games},
pages = {599-610},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-icalp10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-icalp10.pdf},
doi = {10.1007/978-3-642-14162-1_50},
abstract = {Energy parity games are infinite two-player turn-based games
played on weighted graphs. The objective of the game combines a
(qualitative) parity condition with the (quantitative) requirement that
the sum of the weights (\textit{i.e.}, the level of energy in the game)
must remain positive. Beside their own interest in the design and
synthesis of resource-constrained omega-regular specifications, energy
parity games provide one of the simplest model of games with combined
qualitative and quantitative objective. Our main results are as follows:
(a)~exponential memory is sufficient and may be necessary for winning
strategies in energy parity games; (b)~the~problem of deciding the winner
in energy parity games can be solved in NP\(\cap\)coNP; and (c)~we~give an
algorithm to solve energy parity by reduction to energy games. We~also
show that the problem of deciding the winner in energy parity games is
polynomially equivalent to the problem of deciding the winner in
mean-payoff parity games, which can thus be solved in NP\(\cap\)coNP. As~a
consequence we also obtain a conceptually simple algorithm to solve
mean-payoff parity games.}
}
@inproceedings{BGMZ-icalp10,
address = {Bordeaux, France},
month = jul,
year = 2010,
volume = 6199,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abramsky, Samson and Meyer{ }auf{ }der{ }Heide, Friedhelm
and Spirakis, Paul},
acronym = {{ICALP}'10},
booktitle = {{P}roceedings of the 37th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'10)~-- {P}art~{II}},
author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin
and Zeitoun, Marc},
title = {Pebble weighted automata and transitive closure logics},
pages = {587-598},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-icalp10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-icalp10.pdf},
doi = {10.1007/978-3-642-14162-1_49},
abstract = {We introduce new classes of weighted automata on words. Equipped
with pebbles and a two-way mechanism, they go beyond the class of
recognizable formal power series, but capture a weighted version of
first-order logic with bounded transitive closure. In contrast to previous
work, this logic allows for unrestricted use of universal quantification.
Our main result states that pebble weighted automata, nested weighted
automata, and this weighted logic are expressively equivalent. We also
give new logical characterizations of the recognizable series.}
}
@inproceedings{CC-csf10,
address = {Edinburgh, Scotland, UK},
month = jul,
year = 2010,
publisher = {{IEEE} Computer Society Press},
acronym = {{CSF}'10},
booktitle = {{P}roceedings of the
23rd {IEEE} {C}omputer {S}ecurity {F}oundations
{S}ymposium ({CSF}'10)},
author = {Ciob{\^a}c{\u{a}}, {\c{S}}tefan and Cortier, V{\'e}ronique},
title = {Protocol composition for arbitrary primitives},
pages = {322-336},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-09.pdf},
doi = {10.1109/CSF.2010.29},
abstract = {We study the composition of security protocols when protocols
share secrets such as keys. We show (in a Dolev-Yao model)
that if two protocols use disjoint cryptographic primitives,
their composition is secure if the individual protocols are
secure, even if they share data. Our result holds for any
cryptographic primitives that can be modeled using
equational theories, such as encryption, signature, MAC,
exclusive-or, and Diffie-Hellman. Our main result transforms
any attack trace of the combined protocol into an attack
trace of one of the individual protocols. This allows
various ways of combining protocols such as sequentially or
in parallel, possibly with inner replications. As an
application, we show that a protocol using preestablished
keys may use any (secure) key-exchange protocol without
jeopardizing its security, provided that they do not use the
same primitives. This allows us, for example, to securely
compose a Diffie-Hellman key exchange protocol with any
other protocol using the exchanged key, provided that the
second protocol does not use the Diffie-Hellman primitives.
We also explore tagging, which is a way of forcing the
disjointness of two protocols that share cryptographic
primitives We explain why composing protocols which use
tagged cryptographic primitives like encryption and hash
functions is secure by reducing this problem to the previous
one.}
}
@inproceedings{ACD-csf10,
address = {Edinburgh, Scotland, UK},
month = jul,
year = 2010,
publisher = {{IEEE} Computer Society Press},
acronym = {{CSF}'10},
booktitle = {{P}roceedings of the
23rd {IEEE} {C}omputer {S}ecurity {F}oundations
{S}ymposium ({CSF}'10)},
author = {Arnaud, Mathilde and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
title = {Modeling and Verifying Ad Hoc Routing Protocols},
pages = {59-74},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACD-csf10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACD-csf10.pdf},
doi = {10.1109/CSF.2010.12},
abstract = {Mobile ad hoc networks consist of mobile wireless devices which
autonomously organize their infrastructure. In such networks, 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
malicious nodes from compromising the discovered route.\par
Our contribution is twofold. We first propose 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. Our second main
contribution is a decision procedure for analyzing routing protocols for
any network topology. By using constraint solving techniques, we show that
it is possible to automatically discover (in NPTIME) whether there exists
a network topology that would allow malicious nodes to mount an attack
against the protocol, for a bounded number of sessions. We also provide a
decision procedure for detecting attacks in case the network topology is
given a priori. We demonstrate the usage and usefulness of our approach by
analyzing the protocol \textsf{SRP} applied to~\textsf{DSR}.}
}
@inproceedings{BKKLNP-cav10,
address = {Edinburgh, Scotland, UK},
month = jul,
year = 2010,
volume = {6174},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cook, Byron and Jackson, Paul and Touili, Tayssir},
acronym = {{CAV}'10},
booktitle = {{P}roceedings of the 22nd
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'10)},
author = {Bollig, Benedikt and Katoen, Joost-Pieter and Kern, Carsten
and Leucker, Martin and Neider, Daniel and Piegdon, David R.},
title = {libalf: the Automata Learning Framework},
pages = {360-364},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BKKLNP-cav10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BKKLNP-cav10.pdf},
doi = {10.1007/978-3-642-14295-6_32},
abstract = {This paper presents \texttt{libalf}, a comprehensive,
open-source library for learning formal languages. \texttt{libalf} covers
various well-known learning techniques for finite automata (e.g.
Angluin's~\(\textsf{L}^*\), \textsf{Biermann}, \textsf{RPNI},~etc.) as
well as novel learning algorithms (such as for NFA and visibly one-counter
automata). \texttt{libalf}~is flexible and allows facilely interchanging
learning algorithms and combining domain-specific features in a
plug-and-play fashion. Its modular design and C++ implementation make it a
suitable platform for adding and engineering further learning algorithms
for new target models (\textit{e.g.}, B{\"u}chi automata).}
}
@article{RHS-ijfcs09,
publisher = {World Scientific},
journal = {International Journal of Foundations of Computer Science},
author = {Recalde, Laura and Haddad, Serge and Silva, Manuel},
title = {Continuous {P}etri Nets: Expressive Power and Decidability Issues},
volume = 21,
number = 2,
pages = {235-256},
year = 2010,
month = apr,
doi = {10.1142/S0129054110007222},
abstract = {State explosion is a fundamental problem in the analysis and
synthesis of discrete event systems. Continuous Petri nets can be seen as
a relaxation of the corresponding discrete model. The expected gains are
twofold: improvements in complexity and in decidability. In the case of
autonomous nets we prove that liveness or deadlock-freeness remain
decidable and can be checked more efficiently than in Petri nets. Then we
introduce time in the model which now behaves as a dynamical system driven
by differential equations and we study it w.r.t. expressiveness and
decidability issues. On the one hand, we prove that this model is
equivalent to timed differential Petri nets which are a slight extension
of systems driven by linear differential equations~(LDE). On~the other
hand, (contrary to the systems driven by~LDEs) we show that continuous
timed Petri nets are able to simulate Turing machines and thus that basic
properties become undecidable.}
}
@inproceedings{SS-lics10,
address = {Edinburgh, Scotland, UK},
month = jul,
year = 2010,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'10},
booktitle = {{P}roceedings of the 25th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'10)},
author = {Schweikardt, Nicole and Segoufin, Luc},
title = {Addition-invariant {FO} and regularity},
pages = {273-282},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SS-lics10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SS-lics10.pdf},
doi = {10.1109/LICS.2010.16},
abstract = {We consider formulas which, in addition to the symbols in the
vocabulary, may use two designated symbols~\(\prec\) and~\(+\) that must
be interpreted as a linear order and its associated addition. Such a
formula is called addition-invariant if, for each fixed interpretation of
the initial vocabulary, its result is independent of the particular
interpretation of~\(\prec\) and~\(+\).\par
This paper studies the expressive power of addition-invariant first-order
logic, \(+\)-inv-FO, on the class of finite strings. Our first main result
gives a characterization of the regular languages definable in
\(+\)-inv-FO: we show that these are exactly the languages definable in FO
with extra predicates, denoted by {"}lm{"} for short, for testing the
length of the string modulo some fixed number. Our second main result
shows that every language definable in \(+\)-inv-FO, that is bounded or
commutative or deterministic context-free, is regular. As an immediate
consequence of these two main results, we obtain that \(+\)-inv-FO is
equivalent to FO(lm) on the class of finite colored sets.\par
Our proof methods involve Ehrenfeucht-Fra{\"\i}ss{\'e} games, tools from
algebraic automata theory, and reasoning about semi-linear sets.}
}
@inproceedings{PS-lics10,
address = {Edinburgh, Scotland, UK},
month = jul,
year = 2010,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'10},
booktitle = {{P}roceedings of the 25th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'10)},
author = {Place, {\relax Th}omas and Segoufin, Luc},
title = {Deciding definability in \(\textrm{FO}_{2}(<)\) on trees},
pages = {253-262},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/PS-lics10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PS-lics10.pdf},
doi = {10.1109/LICS.2010.17},
abstract = { We prove that it is decidable whether a regular unranked tree
language is definable in~\(\textsf{FO}_{2}(<_{h}, <_{v})\).
By~\(\textsf{FO}_{2}(<_{h}, <_{v})\) we refer to the two variable fragment
of first order logic built from the descendant and following sibling
predicates. In terms of expressive power it corresponds to a fragment of
the navigational core of XPath that contains modalities for going up to
some ancestor, down to some descendant, left to some preceding sibling,
and right to some following sibling.\par
We also investigate definability in some other fragments of XPath.}
}
@inproceedings{JGL-lics10,
address = {Edinburgh, Scotland, UK},
month = jul,
year = 2010,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'10},
booktitle = {{P}roceedings of the 25th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'10)},
author = {Goubault{-}Larrecq, Jean},
title = {{{\(\omega\)}}{\textbf{\MakeUppercase{QRB}}}-Domains and the
Probabilistic Powerdomain},
pages = {352-361},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-lics10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-lics10.pdf},
doi = {10.1109/LICS.2010.50},
abstract = {Is there any cartesian-closed category of continuous domains
that would be closed under Jones and Plotkin's probabilistic powerdomain
construction? This is a major open problem in the area of denotational
semantics of probabilistic higher-order languages. We relax the question,
and look for quasi-continuous dcpos instead. We introduce a natural class
of such quasi-continuous dcpos, the \(\omega\textbf{QRB}\)-domains. We
show that they form a category \(\omega\textbf{QRB}\) with pleasing
properties: \(\omega\textbf{QRB}\) is closed under the probabilistic
powerdomain functor, has all finite products, all bilimits, and is stable
under retracts, and even under so-called quasiretracts. But...
\(\omega\textbf{QRB}\) is not cartesian closed.}
}
@inproceedings{BCGJV-lics10,
address = {Edinburgh, Scotland, UK},
month = jul,
year = 2010,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'10},
booktitle = {{P}roceedings of the 25th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'10)},
author = {Bargu{\~n}{\'o}, Luis and Creus, Carles and Godoy, Guillem
and Jacquemard, Florent and Vacher, Camille},
title = {The Emptiness Problem for Tree Automata with Global Constraints},
pages = {263-272},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGJV-lics10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGJV-lics10.pdf},
doi = {10.1109/LICS.2010.28},
abstract = {We define tree automata with global constraints~(TAGC),
generalizing the class of tree automata with global equality and
disequality constraints~(TAGED). TAGC~can test for equality and
disequality between subterms whose positions are defined by the states
reached during a computation. In~particular, TAGC~can check that all the
subterms reaching a given state are distinct. This constraint is related
to monadic key constraints for XML documents, meaning that every two
distinct positions of a given type have different values.\par
We prove decidability of the emptiness problem for~TAGC. This solves, in
particular, the open question of decidability of emptiness for TAGED. We
further extend our result by allowing global arithmetic constraints for
counting the number of occurrences of some state or the number of
different subterms reaching some state during a computation. We also allow
local equality and disequality tests between sibling positions and the
extension to unranked ordered trees. As a consequence of our results for
TAGC, we prove the decidability of a fragment of the monadic second order
logic on trees extended with predicates for equality and disequality
between subtrees, and cardinality.}
}
@inproceedings{CF-pn10,
address = {Braga, Portugal},
month = jun,
year = 2010,
volume = 6128,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Lilius, Johan and Penczek, Wojciech},
acronym = {{PETRI~NETS}'10},
booktitle = {{P}roceedings of the 31st
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'10)},
author = {Chatain, {\relax Th}omas and Fabre, {\'E}ric},
title = {Factorization Properties of Symbolic Unfoldings of Colored
{P}etri Nets},
pages = {165-184},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CF-pn10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CF-pn10.pdf},
doi = {10.1007/978-3-642-13675-7_11},
abstract = {The unfolding technique is an efficient tool to explore the runs
of a Petri net in a true concurrency semantics, \textit{i.e.}, without
constructing all the interleavings of concurrent actions. But even small
real systems are never modeled directly as ordinary Petri nets: they use
many high-level features that were designed as extensions of Petri nets.
We focus here on two such features: colors and compositionality. We show
that the symbolic unfolding of a product of colored Petri nets can be
expressed as the product of the symbolic unfoldings of these nets. This is
a necessary result in view of distributed computations based on symbolic
unfoldings, as they have been developed already for standard unfoldings,
to design modular verification techniques, or modular diagnosis
procedures, for example. The factorization property of symbolic unfoldings
is valid for several classes of colored or high-level nets. We derive it
here for a class of (high-level) open nets, for which the composition is
performed by connecting places rather than transitions.}
}
@article{DL-jal10,
publisher = {Elsevier Science Publishers},
journal = {Journal of Applied Logic},
author = {Demri, St{\'e}phane and Lugiez, Denis},
title = {Complexity of Modal Logics with {P}resburger Constraints},
year = {2010},
volume = {8},
number = {3},
pages = {233-252},
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DL-jal10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DL-jal10.pdf},
doi = {10.1016/j.jal.2010.03.001},
abstract = {We introduce the extended modal logic EML with regularity
constraints and full Presburger constraints on the number of children that
generalize graded modalities, also known as number restrictions in
description logics. We show that EML satisfiability is only
\textsc{pspace}-complete by designing a Ladner-like algorithm. This
extends a well-known and non-trivial \textsc{pspace} upper bound for
graded modal logic. Furthermore, we provide a detailed comparison with
logics that contain Presburger constraints and that are dedicated to query
XML documents. As an application, we provide a logarithmic space reduction
from a variant of Sheaves logic SL into EML that allows us to establish
that its satisfiability problem is also \textsc{pspace}-complete,
significantly improving the best known upper bound.}
}
@article{LS-jal10,
publisher = {Elsevier Science Publishers},
journal = {Journal of Applied Logic},
author = {Libkin, Leonid and Sirangelo, Cristina},
title = {Reasoning about {XML} with temporal logics and automata},
year = {2010},
volume = {8},
number = {2},
pages = {210-232},
month = jun,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-jal10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-jal10.pdf},
doi = {10.1016/j.jal.2009.09.005},
abstract = {We show that problems arising in static analysis of XML
specifications and transformations can be dealt with using techniques
similar to those developed for static analysis of programs. Many
properties of interest in the XML context are related to navigation, and
can be formulated in temporal logics for trees. We choose a logic that
admits a simple single-exponential translation into unranked tree
automata, in the spirit of the classical LTL-to-B{\"u}chi automata
translation. Automata arising from this translation have a number of
additional properties; in particular, they are convenient for reasoning
about unary node-selecting queries, which are important in the XML
context. We give two applications of such reasoning: one deals with a
classical XML problem of reasoning about navigation in the presence of
schemas, and the other relates to verifying security properties of XML
views.}
}
@article{DLS-tcs10,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko and
Sangnier, Arnaud},
title = {Model checking memoryful linear-time logics over
one-counter automata},
year = {2010},
volume = {411},
number = {22-24},
pages = {2298-2316},
month = may,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DLS-tcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DLS-tcs10.pdf},
doi = {10.1016/j.tcs.2010.02.021},
abstract = {We study complexity of the model-checking problems for LTL with
registers (also known as freeze LTL and written
LTL\(^{\downarrow}\)) and for first-order logic with data
equality tests (written \(\textrm{FO}(\sim, <, +1)\)) over
one-counter automata. We consider several classes of
one-counter automata (mainly deterministic vs.
nondeterministic) and several logical fragments (restriction
on the number of registers or variables and on the use of
propositional variables for control states). The logics have
the ability to store a counter value and to test it later
against the current counter value. We show that model
checking LTL\(^{\downarrow}\) and \(\textrm{FO}(\sim , <,
+1)\) over deterministic one-counter automata is
PSpace-complete with infinite and finite accepting runs. By
constrast, we prove that model checking LTL\(^{\downarrow}\)
in which the until operator~\(\mathbf{U}\) is restricted to
the eventually~\(\mathbf{F}\) over nondeterministic
one-counter automata is \(\Sigma_1^1\)-complete [resp.
\(\Sigma_1^0\)-complete] in the infinitary [resp. finitary]
case even if only one register is used and with no
propositional variable. As a corollary of our proof, this
also holds for \(\textrm{FO}(\sim, <, +1)\) restricted to
two variables (written \(\textrm{FO}_2 (\sim, <, +1)\)).
This makes a difference with the facts that several
verification problems for one-counter automata are known to
be decidable with relatively low complexity, and that
finitary satisfiability for LTL\(^{\downarrow}\) and
\(\textrm{FO}_2 (\sim, <, +1)\) are decidable. Our results
pave the way for model-checking memoryful (linear-time)
logics over other classes of operational models, such as
reversal-bounded counter machines.}
}
@article{AF-ijmest10,
publisher = {Taylor \& Francis},
journal = {International Journal of Mathematical Education
in Science and Technology},
author = {Arnoux, Pierre and Finkel, Alain},
title = {Using mental imagery processes for teaching and research in
mathematics and computer science},
volume = 41,
number = 2,
month = jan,
year = 2010,
pages = {229-242},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AF-ijmest10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AF-ijmest10.pdf},
doi = {10.1080/00207390903372429},
abstract = {The role of mental representations in mathematics and computer
science (for teaching or research) is often downplayed or even completely
ignored. Using an ongoing work on the subject, we argue for a more
systematic study and use of mental representations, to get an intuition of
mathematical concepts, and also to understand and build proofs. We give
two detailed examples.}
}
@article{GK-icomp10,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Gastin, Paul and Kuske, Dietrich},
title = {Uniform satisfiability problem for local temporal logics over
{M}azurkiewicz traces},
volume = 208,
number = 7,
month = jul,
year = 2010,
pages = {797-816},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GK-icomp10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GK-icomp10.pdf},
doi = {10.1016/j.ic.2009.12.003},
abstract = {We continue our study of the complexity of MSO-definable local
temporal logics over concurrent systems that can be described by
Mazurkiewicz traces. In previous papers, we showed that the satisfiability
problem for any such logic is in PSPACE (provided the dependence alphabet
is fixed) and remains in PSPACE for all classical local temporal logics
even if the dependence alphabet is part of the input. In~this paper, we
consider the uniform satisfiability problem for arbitrary MSO-definable
local temporal logics. For this problem, we prove multi-exponential lower
and upper bounds that depend on the number of alternations of set
quantifiers present in the chosen MSO-modalities.}
}
@article{Haar-tac10,
publisher = {{IEEE} Computer Society Press},
journal = {IEEE Transactions on Automatic Control},
author = {Haar, Stefan},
title = {Types of Asynchronous Diagnosability and
the {\emph{Reveals}}-Relation in Occurrence Nets},
volume = 55,
number = 10,
month = oct,
year = 2010,
pages = {2310-2320},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-tac10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-tac10.pdf},
doi = {10.1109/TAC.2010.2063490},
abstract = {We consider asynchronous diagnosis in (safe) Petri net models of
distributed systems, using the partial order semantics of occurrence net
unfoldings. Both the observability and diagnosability properties will
appear in two different forms, depending on the semantics chosen:
\emph{strong} observability and diagnosability are the classical notions
from the state machine model and correspond to interleaving semantics in
Petri nets. By contrast, the \emph{weak} form is linked to characteristics
of nonsequential processes, and requires an asynchronous \emph{progress}
assumption on those processes. We give algebraic characterizations for
both types, and give verification methods. The study of weak
diagnosability leads us to the analysis of a relation in occurrence nets,
first presented in~[S.~Haar~(2007): \textit{Unfold and Cover: Qualitative
Diagnosability for Petri Nets.}]: given the occurrence of some event~\(a\)
that \emph{reveals}~\(b\), the occurrence of~\(b\) is inevitable. Then
\(b\) may already have occurred, be concurrent to, or even in the future
of~\(a\). We show that the \emph{reveals}-relation can be effectively
computed recursively---for each pair, a suitable finite prefix of bounded
depth is sufficient---and show its use in asynchronous diagnosis. Based on
this relation, a~decomposition of the Petri net unfolding into
\emph{facets} is defined, yielding an abstraction technique that preserves
and reflects maximal partially ordered runs.}
}
@inproceedings{SRKK-arspawits10,
address = {Paphos, Cyprus},
month = oct,
year = 2010,
volume = 6186,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Armando, Alessandro and Lowe, Gavin},
acronym = {{ARSPA-WITS}'10},
booktitle = {{P}roceedings 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}'10)},
author = {Smyth, Ben and Ryan, Mark D. and Kremer, Steve and
Kourjieh, Mounira},
title = {Towards automatic analysis of election verifiability properties},
pages = {146-163},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SRKK-arspawits10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SRKK-arspawits10.pdf},
doi = {10.1007/978-3-642-16074-5_11},
abstract = {We present a symbolic definition that captures some
cases 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 software tool
ProVerif. The definition distinguishes three aspects of verifiability,
which we call individual, universal, and eligibility verifiability. We
demonstrate the applicability of our formalism by analysing the protocols
due to Fujioka, Okamoto~\& Ohta and a variant of the one by Juels,
Catalano~\& Jakobsson (implemented as Civitas by Clarkson, Chong~\& Myers).}
}
@inproceedings{BH-csr10,
address = {Kazan, Russia},
month = jun,
year = 2010,
volume = 6072,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Mayr, Ernst W.},
acronym = {{CSR}'10},
booktitle = {{P}roceedings of the 5th {I}nternational {C}omputer {S}cience
{S}ymposium in {R}ussia ({CSR}'10)},
author = {Bollig, Benedikt and H{\'e}lou{\"e}t, Lo{\"\i}c},
title = {Realizability of Dynamic {MSC} Languages},
pages = {48-59},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BH-csr10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BH-csr10.pdf},
doi = {10.1007/978-3-642-13182-0_5},
abstract = {We introduce dynamic communicating automata~(DCA), an~extension
of communicating finite-state machines that allows for dynamic creation of
processes. Their behavior can be described as sets of message sequence
charts~(MSCs). We~consider the realizability problem for DCA: given a
dynamic MSC grammar (a~high-level MSC specification), is there a DCA
defining the same set of MSCs? We~show that this problem is decidable in
doubly exponential time, and identify a class of realizable grammars that
can be implemented by \emph{finite} DCA.}
}
@article{CS-jacm10,
publisher = {ACM Press},
journal = {Journal of the~{ACM}},
author = {ten~Cate, Balder and Segoufin, Luc},
title = {Transitive Closure Logic, Nested Tree Walking Automata, and {XP}ath},
volume = 57,
number = 3,
month = mar,
year = 2010,
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-jacm10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-jacm10.pdf},
doi = {10.1145/1706591.1706598},
abstract = {We study \textsf{FO(MTC)}, first-order logic with monadic
transitive closure, a logical formalism in between \textsf{FO} and
\textsf{MSO} on trees. We characterize the expressive power of
\textsf{FO(MTC)} in terms of nested tree-walking automata. Using the
latter we show that \textsf{FO(MTC)} is strictly less expressive than
\textsf{MSO}, solving an open problem. We also present a temporal logic on
trees that is expressivel complete for \textsf{FO(MTC)}, in the form of an
extension of the XML document navigation language XPath with two
operators: the Kleene star for taking the transitive closure of path
expressions, and a subtree relativisation operator, allowing one to
restrict attention to a specific subtree while evaluating a subexpression.
We show that the expressive power of this XPath dialect equals that of
\textsf{FO(MTC)} for Boolean, unary and binary queries. We also
investigate the complexity of the automata model as well as the XPath
dialect. We show that query evaluation be done in polynomial time
(combined complexity), but that emptiness (or, satisfiability) is
2ExpTime-complete.}
}
@article{BCHK-icomp10,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Baldan, Paolo and Chatain, {\relax Th}omas and Haar, Stefan and
K{\"o}nig, Barbara},
title = {Unfolding-based Diagnosis of Systems with an Evolving Topology},
volume = 208,
number = 10,
pages = {1169-1192},
year = 2010,
month = oct,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHK-icomp10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHK-icomp10.pdf},
doi = {10.1016/j.ic.2009.11.009},
abstract = {We propose a framework for model-based diagnosis of systems with
mobility and variable topologies, modelled as graph transformation
systems. Generally speaking, model-based diagnosis is aimed at
constructing explanations of observed faulty behaviours on the basis of a
given model of the system. Since the number of possible explanations may
be huge, we exploit the unfolding as a compact data structure to store
them, along the lines of previous work dealing with Petri net models.
Given a model of a system and an observation, the explanations can be
constructed by unfolding the model constrained by the observation, and
then removing incomplete explanations in a pruning phase. The theory is
formalised in a general categorical setting: constraining the system by
the observation corresponds to taking a product in the chosen category of
graph grammars, so that the correctness of the procedure can be proved by
using the fact that the unfolding is a right adjoint and thus it preserves
products. The theory should hence be easily applicable to a wide class of
system models, including graph grammars and Petri nets.}
}
@incollection{Berwanger09,
year = 2010,
volume = 6006,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Bonnano, Giacomo and L{\"o}we, Benedikt and van der
Hoek, Wiebe},
booktitle = {Logic and the Foundations of Game and Decision Theory (LOFT8)},
author = {Berwanger, Dietmar},
title = {Infinite Coordination Games},
pages = {1-19},
futurechapter = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/Ber-loft8.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Ber-loft8.pdf},
doi = {10.1007/978-3-642-15164-4_1},
abstract = {We investigate the prescriptive power of sequential iterated
admissibility in coordination games of the Gale-Stewart style, \textit{i.e.},
perfect-information games of infinite duration with only two payoffs. We
show that, on this kind of games, the procedure of eliminating weakly
dominated strategies is independent of the elimination order and that,
under maximal simultaneous elimination, the procedure converges after at
most omega many stages.}
}
@article{BK-jlli10,
publisher = {Kluwer Academic Publishers},
journal = {Journal of Logic, Language and Information},
author = {Berwanger, Dietmar and Kaiser, {\L}ukasz},
title = {Information Tracking in Games on Graphs},
volume = 19,
number = 4,
pages = {395-412},
year = 2010,
month = oct,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BK-jlli10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BK-jlli10.pdf},
doi = {10.1007/s10849-009-9115-8},
abstract = {When seeking to coordinate in a game with imperfect information,
it is often relevant for a player to know what other players know. Keeping
track of the information acquired in a play of infinite duration may,
however, lead to infinite hierarchies of higher-order knowledge. We
present a construction that makes explicit which higher-order knowledge is
relevant in a game and allows us to describe a class of games that admit
coordinated winning strategies with finite memory.}
}
@proceedings{Seg-icdt10,
author = {Segoufin, Luc},
editor = {Segoufin, Luc},
title = {Proceedings of the 13th {I}nternational {C}onference on
{D}atabase {T}heory ({ICDT}'10)},
booktitle = {Proceedings of the 13th {I}nternational {C}onference on
{D}atabase {T}heory ({ICDT}'10)},
year = 2010,
month = mar,
url = {http://portal.acm.org/citation.cfm?id=1804669&coll=ACM&dl=ACM}
}
@inproceedings{ACKNS-icdt10,
address = {Lausanne, Switzerland},
month = mar,
year = 2010,
publisher = {ACM Press},
editor = {Segoufin, Luc},
acronym = {{ICDT}'10},
booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on
{D}atabase {T}heory ({ICDT}'10)},
author = {Abiteboul, Serge and Chan, T.-H. Hubert and Kharlamov, Evgeny
and Nutt, Werner and Senellart, Pierre},
title = {Aggregate queries for discrete and continuous probabilistic~{XML}},
pages = {50-61},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACKNS-icdt10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACKNS-icdt10.pdf},
doi = {10.1145/1804669.1804679},
abstract = {Sources of data uncertainty and imprecision are numerous. A way
to handle this uncertainty is to associate probabilistic
annotations to data. Many such probabilistic database models
have been proposed, both in the relational and in the
semi-structured setting. The latter is particularly well
adapted to the management of uncertain data coming from a
variety of automatic processes. An important problem, in the
context of probabilistic XML databases, is that of answering
aggregate queries (count, sum, avg, etc.), which has
received limited attention so far. In a model unifying the
various (discrete) semi-structured probabilistic models
studied up to now, we present algorithms to compute the
distribution of the aggregation values (exploiting some
regularity properties of the aggregate functions) and
probabilistic moments (especially, expectation and variance)
of this distribution. We also prove the intractability of
some of these problems and investigate approximation
techniques. We finally extend the discrete model to a
continuous one, in order to take into account continuous
data values, such as measurements from sensor networks, and
present algorithms to compute distribution functions and
moments for various classes of continuous distributions of
data values.}
}
@inproceedings{Fig-icdt10,
address = {Lausanne, Switzerland},
month = mar,
year = 2010,
publisher = {ACM Press},
editor = {Segoufin, Luc},
acronym = {{ICDT}'10},
booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on
{D}atabase {T}heory ({ICDT}'10)},
author = {Figueira, Diego},
title = {Forward-{XP}ath and extended register automata on data-trees},
pages = {230-240},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/fig-icdt10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/fig-icdt10.pdf},
ps = {fig-icdt10.ps},
doi = {10.1145/1804669.1804699},
abstract = {We consider a fragment of XPath named {"}forward-XPath{"}, which
contains all descendant and rightwards sibling axes as well as data
equality and inequality tests. The satisfiability problem for
forward-XPath in the presence of DTDs and even of primary key constraints
is shown here to be decidable.\par
To show decidability we introduce a model of alternating automata on data
trees that can move downwards and rightwards in the tree, have one
register for storing data and compare them for equality, and have the
ability to (1)~nondeterministically guess a data value and store it, and
(2)~quantify universally over the set of data values seen so far during
the run. This model extends the work of Jurdzi{\'n}ski and Lazi{\'c}.
Decidability of the finitary non-emptiness problem for this model is
obtained by a direct reduction to a well-structured transition system,
contrary to previous approaches.}
}
@article{CDH-tocl10,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Chatterjee, Krishnendu and Doyen, Laurent and Henzinger,
{\relax Th}omas A.},
title = {Quantitative Languages},
volume = 11,
number = 4,
nopages = {},
year = 2010,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDH-tocl10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDH-tocl10.pdf},
ps = {CDH-tocl10.ps},
abstract = {Quantitative generalizations of classical languages, which
assign to each word a real number in- stead of a boolean value, have
applications in modeling resource-constrained computation. We use weighted
automata (finite automata with transition weights) to define several
natural classes of quantitative languages over finite and infinite words;
in particular, the real value of an infinite run is computed as the
maximum, limsup, liminf, limit average, or discounted sum of the
transition weights. We define the classical decision problems of automata
theory (emptiness, universality, language inclusion, and language
equivalence) in the quantitative setting and study their compu- tational
complexity. As the decidability of the language-inclusion problem remains
open for some classes of weighted automata, we introduce a notion of
quantitative simulation that is decidable and implies language inclusion.
We also give a complete characterization of the expressive power of the
various classes of weighted automata. In particular, we show that most
classes of weighted automata cannot be determinized.}
}
@inproceedings{DR-tacas10,
address = {Paphos, Cyprus},
month = mar,
year = 2010,
volume = {6015},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Esparza, Javier and Majumdar, Rupak},
acronym = {{TACAS}'10},
booktitle = {{P}roceedings of the 16th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'10)},
author = {Doyen, Laurent and Raskin, Jean-Fran{\c{c}}ois},
title = {Antichains Algorithms for Finite Automata},
pages = {2-22},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DR-tacas10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DR-tacas10.pdf},
ps = {DR-tacas10.ps},
doi = {10.1007/978-3-642-12002-2_2},
abstract = {We present a general theory that exploits simulation relations
on transition systems to obtain antichain algorithms for solving the
reachability and repeated reachability problems. Antichains are more
succinct than the sets of states manipulated by the traditional fixpoint
algorithms. The theory justifies the correctness of the antichain
algorithms, and applications such as the universality problem for finite
automata illustrate efficiency improvements. Finally, we show that new and
provably better antichain algorithms can be obtained for the emptiness
problem of alternating automata over finite and infinite words.}
}
@article{BCDDH-icomp10,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Berwanger, Dietmar and Chatterjee, Krishnendu and Doyen, Laurent
and De{~}Wulf, Martin and Henzinger, {\relax Th}omas A.},
title = {Strategy Construction for Parity Games with Imperfect
Information},
volume = 208,
number = 10,
pages = {1206-1220},
year = 2010,
month = oct,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCDDH-icomp10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCDDH-icomp10.pdf},
ps = {BCDDH-icomp10.ps},
doi = {10.1016/j.ic.2009.09.006},
abstract = {We consider two-player parity games with imperfect information
in which strategies rely on observations that provide imperfect
information about the history of a play. To solve such games,
\textit{i.e.}, to determine the winning regions of players and
corresponding winning strategies, one can use the subset construction to
build an equivalent perfect-information game. Recently, an algorithm that
avoids the inefficient subset construction has been proposed. The
algorithm performs a fixed-point computation in a lattice of antichains,
thus maintaining a succinct representation of state sets. However, this
representation does not allow to recover winning strategies.\par
In this paper, we build on the antichain approach to develop an algorithm
for constructing the winning strategies in parity games of imperfect
information. One major obstacle in adapting the classical procedure is
that the complementation of attractor sets would break the invariant of
downward-closedness on which the antichain representation relies. We
overcome this difficulty by decomposing problem instances recursively into
games with a combination of reachability, safety, and simpler parity
conditions. We also report on an experimental implementation of our
algorithm; to our knowledge, this is the first implementation of a
procedure for solving imperfect-information parity games on graphs.}
}
@misc{Quasimodo-3.4,
author = {Markey, Nicolas and Li, Shuhao and
Raskin, Jean-Fran{\c{c}}ois and Stoelinga, Mari{\"e}lle},
title = {Synthesizing controllers with bounded resources},
howpublished = {Deliverable QUASIMODO~3.4 (ICT-FP7-STREP-214755)},
year = 2010,
month = jan
}
@article{LS-ipl10,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Libkin, Leonid and Sirangelo, Cristina},
title = {Disjoint pattern matching and implication in strings},
volume = 110,
number = 4,
pages = {143-147},
year = 2010,
month = jan,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-ipl10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-ipl10.pdf},
doi = {10.1016/j.ipl.2009.11.009},
abstract = {We deal with the problem of deciding whether a given set of
string patterns implies the presence of a fixed pattern. While checking
whether a set of patterns occurs in a string is solvable in polynomial
time, this implication problem is well known to be intractable. Here we
consider a version of the problem when patterns in the set are required to
be disjoint. We show that for such a version of the problem the situation
is reversed: checking whether a set of patterns occurs in a string is
NP-complete, but the implication problem is solvable in polynomial time.}
}
@mastersthesis{sankur-master,
author = {Sankur, Ocan},
title = {Model-checking robuste des automates temporis{\'e}s
\textit{via} les machines {\`a} canaux},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2010},
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/sankur-m2.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/sankur-m2.pdf}
}
@mastersthesis{soulat-master,
author = {Soulat, Romain},
title = {Am{\'e}liorations algorithmiques d'un moteur
de model-checking et {\'e}tudes de cas},
school = {{M}aster 2 {R}echerche {I}nformatique {P}aris {S}ud~11},
type = {Rapport de {M}aster},
year = {2010},
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/soulat-m2.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/soulat-m2.pdf}
}
@mastersthesis{boiret-master,
author = {Boiret, Adrien},
title = {Grammaires context-free pour les arbres sans rang},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2010},
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/boiret-m2.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/boiret-m2.pdf}
}
@mastersthesis{dimino-master,
author = {Dimino, J{\'e}r{\'e}mie},
title = {Sur les arbres de rang non born{\'e} avec donn{\'e}es},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2010},
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/dimino-m2.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/dimino-m2.pdf}
}
@mastersthesis{monmege-master,
author = {Monmege, Benjamin},
title = {Propri{\'e}t{\'e}s quantitatives des mots et des arbres~--
Applications aux langages~{XML}},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2010},
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/monmege-m2.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/monmege-m2.pdf}
}
@inproceedings{ABMG-vldb10,
address = {Singapore},
month = sep,
year = 2010,
volume = 3,
series = {Proceedings of the {VLDB} Endowment},
publisher = {ACM Press},
editor = {Chen, Yi and Tay, Y.C.},
acronym = {{VLDB}'10},
booktitle = {{P}roceedings of the 36th {I}nternational
{C}onference on {V}ery {L}arge {D}ata {B}ases
({VLDB}'10)},
author = {Abiteboul, Serge and Bourhis, Pierre and Marinoiu, Bogdan and
Galland, Alban},
title = {{AXART}~-- {E}nabling Collaborative Work with {AXML} Artifacts},
pages = {1553-1556},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABMG-vldb10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABMG-vldb10.pdf},
abstract = {The workflow models have been essentially operation-centric for
many years, ignoring almost completely the data aspects. Recently, a new
paradigm of data-centric workflows, called \emph{business artifacts}, has
been introduced by Nigam and Caswell. We follow this approach and propose
a model where artifacts are XML documents that evolve in time due to
interactions with their environment, i.e. human users or Web services.
This paper proposes the AXART system as a distributed platform for
collaborative work that harnesses the power of our model. We will
illustrate AXART with an example taken from the movie industry. Indeed,
applying for a role in a film is a typical collaborative process that
involves various participants, inside and outside the film company. The
demonstration scenario considers both standard workflow process and
dynamic workflow modifications, based on two extension mechanisms:
workflow specialization and workflow exception. The workflows, modeled
using artifacts, are supported by the AXART system by combining techniques
specific to active documents, like view maintenance, with security
techniques to manage access rights.}
}
@inproceedings{GAMS-wsdm10,
address = {New~York, New~York, USA},
month = feb,
year = 2010,
publisher = {ACM Press},
editor = {Davison, Brian D. and Suel, Torsten and Craswell, Nick and Liu, Bing},
acronym = {{WSDM}'10},
booktitle = {{P}roceedings of the 3rd {I}nternational {C}onference on {W}eb {S}earch and
{W}eb {D}ata {M}ining ({WSDM}'10)},
author = {Galland, Alban and Abiteboul, Serge and Marian, Am{\'e}lie
and Senellart, Pierre},
title = {Corroborating information from disagreeing views},
pages = {131-140},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GAMS-wsdm10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GAMS-wsdm10.pdf},
doi = {10.1145/1718487.1718504},
abstract = {We consider a set of views stating possibly conflicting facts.
Negative facts in the views may come, e.g., from functional dependencies
in the underlying database schema. We want to predict the truth values of
the facts. Beyond simple methods such as voting (typically rather
accurate), we explore techniques based on {"}corroboration{"}, i.e., taking
into account trust in the views. We introduce three fixpoint algorithms
corresponding to different levels of complexity of an underlying
probabilistic model. They all estimate both truth values of facts and
trust in the views. We present experimental studies on synthetic and
real-world data. This analysis illustrates how and in which context these
methods improve corroboration results over baseline methods. We believe
that corroboration can serve in a wide range of applications such as
source selection in the semantic Web, data quality assessment or semantic
annotation cleaning in social networks. This work sets the bases for a
wide range of techniques for solving these more complex problems.}
}
@inproceedings{BHB-sbmf10,
address = {},
month = nov,
year = 2010,
volume = 6527,
series = {Lecture Notes in Computer Science},
editor = {Davies, Jim and Silva, Leila and da~Silva Sim{\~a}o, Adenilso},
publisher = {Springer},
acronym = {{SBMF}'10},
booktitle = {{R}evised {S}elected {P}apers of the 13th {B}razilian {S}ymposium on {F}ormal
{M}ethods ({SBMF}'10)},
author = {Bauer, Sebastian S. and Hennicker, Rolf and Bidoit, Michel},
title = {A~Modal Interface Theory with Data Constraints},
pages = {80-95},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHB-sbmf10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHB-sbmf10.pdf},
doi = {10.1007/978-3-642-19829-8_6},
abstract = {For the design of component-based software, the behavioral
specification of component interfaces is crucial. We propose an extension
of the theory of modal I{\slash}O-transition systems by Larsen
\textit{et~al.} to cope with both control flow and data states of reactive
components at the same time. In our framework, transitions model incoming
or outgoing operation calls which are constrained by pre- and
postconditions expressing the mutual assumptions and guarantees of the
receiver and the sender of a message. We define a new interface theory by
adapting synchronous composition, modal refinement and modal compatibility
to the case of modal I{\slash}O-transition systems with data constraints.
We show that in this formalism modal compatibility is preserved by
refinement and modal refinement is preserved by composition which are
basic requirements for any interface theory.}
}
@inproceedings{bbcks-icgt10,
address = {Enschede, The Netherlands},
month = sep # {-} # oct,
year = 2010,
volume = 6372,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ehrig, Hartmut and Rensink, Arend
and Rozenberg, Grzegorz and Sch{\"u}rr, Andy},
acronym = {{ICGT}'10},
booktitle = {{P}roceedings of the 5th {I}nternational {C}onference on {G}raph
{T}ransformations ({ICGT}'10)},
author = {Baldan, Paolo and Bruni, Alessandro and Corradini, Andrea
and K{\"o}nig, Barbara and Schwoon, Stefan},
title = {On the Computation of {M}c{M}illan's Prefix for Contextual Nets
and Graph Grammars},
pages = {91-106},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/bbcks-icgt10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bbcks-icgt10.pdf},
doi = {10.1007/978-3-642-15928-2_7},
abstract = {In recent years, a research thread focused on the use of the
unfolding semantics for verification purposes. This started with a paper
by McMillan, which devises an algorithm for constructing a finite complete
prefix of the unfolding of a safe Petri net, providing a compact
representation of the reachability graph. The extension to contextual nets
and graph transformation systems is far from being trivial because events
can have multiple causal histories. Recently, we proposed an abstract
algorithm that generalizes McMillan's construction to bounded contextual
nets without resorting to an encoding into plain P\slash T nets. Here, we
provide a more explicit construction that renders the algorithm effective.
To allow for an inductive definition of concurrency, missing in the
original proposal and essential for an efficient unfolding procedure, the
key intuition is to associate histories not only with events, but also
with places. Additionally, we outline how the proposed algorithm can be
extended to graph transformation systems, for which previous algorithms
based on the encoding of read arcs would not be applicable.}
}
@article{BS-lmcs10,
journal = {Logical Methods in Computer Science},
author = {Boja{\'n}czyk, Miko{\l}aj and Segoufin, Luc},
title = {Tree Languages Defined in First-Order Logic with One Quantifier Alternation},
volume = 6,
number = {4:1},
nopages = {},
month = oct,
year = 2010,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-lmcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-lmcs10.pdf},
doi = {10.2168/LMCS-6(4:1)2010},
abstract = {We study tree languages that can be defined in~\(\Delta_{2}\).
These are tree languages definable by a first-order formula whose
quantifier prefix is \(\exists^{*}\forall^{*}\), and simultaneously by a first-order
formula whose quantifier prefix is \(\forall^{*}\exists^{*}\). For the quantifier free part we
consider two signatures, either the descendant relation alone or together
with the lexicographical order relation on nodes. We provide an effective
characterization of tree and forest languages definable in~\(\Delta_{2}\).
This characterization is in terms of algebraic equations. Over words, the
class of word languages definable in~\(\Delta_{2}\) forms a robust class,
which was given an effective algebraic characterization by Pin and Weil.}
}
@article{BLPS-jacm10,
publisher = {ACM Press},
journal = {Journal of the~{ACM}},
author = {Barcel{\'o}, Pablo and Libkin, Leonid and
Poggi, Antonella and Sirangelo, Cristina},
title = {{XML} with incomplete information},
volume = {58},
number = {1},
year = {2010},
month = dec,
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLPS-jacm10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLPS-jacm10.pdf},
doi = {10.1145/1870103.1870107}
}
@article{LBDLNP-fmsd2010,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Li, Shuhao and Balaguer, Sandie and David, Alexandre and Larsen,
Kim G. and Nielsen, Brian and Pusinskas, Saulius},
title = {Scenario-based verification of real-time systems using {\textsc{Uppaal}}},
year = {2010},
month = nov,
volume = {37},
number = {2-3},
pages = {200-264},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LBDLNP-fmsd2010.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LBDLNP-fmsd2010.pdf},
doi = {10.1007/s10703-010-0103-z},
abstract = {This article proposes two approaches to tool-supported automatic
verification of dense real-time systems against scenario-based
requirements, where a system is modeled as a network of timed automata
(TAs) or as a set of driving live sequence charts (LSCs), and a
requirement is specified as a separate monitored LSC chart. We make timed
extensions to a kernel subset of the LSC language and define a trace-based
semantics. By translating a monitored LSC chart to a behavior-equivalent
observer TA and then non-intrusively composing this observer with the
original TA-modeled real-time system, the problems of scenario-based
verification reduce to computation tree logic (CTL) real-time model
checking problems. When the real-time system is modeled as a set of
driving LSC charts, we translate these driving charts and the monitored
chart into a behavior-equivalent network of TAs by using a
{"}one-TA-per-instance line{"} approach, and then reduce the problems of
scenario-based verification also to CTL real-time model checking problems.
We show how we exploit the expressivity of the TA formalism and the CTL
query language of the real-time model checker Uppaal to accomplish these
tasks. The proposed two approaches are implemented in the Uppaal tool and
built as a tool chain, respectively. We carry out a number of experiments
with both verification approaches, and the results indicate that these
methods are viable, computationally feasible, and the tools are effective.}
}
@article{DFGD-jancl10,
publisher = {Taylor \& Francis},
journal = {Journal of Applied Non-Classical Logics},
author = {Demri, St{\'e}phane and Finkel, Alain and Goranko, Valentin
and van Drimmelen, Govert},
title = {Model-checking \(\textsf{CTL}^{*}\) over Flat {P}resburger Counter
Systems},
year = {2010},
volume = {20},
number = {4},
pages = {313-344},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DFGD-jancl10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DFGD-jancl10.pdf},
doi = {10.3166/jancl.20.313-344},
abstract = {This paper studies model-checking of fragments and extensions of
\(\textsf{CTL}^{*}\) on infinite-state counter systems, where the states
are vectors of integers and the transitions are determined by means of
relations definable within Presburger arithmetic. In general, reachability
properties of counter systems are undecidable, but we have identified a
natural class of admissible counter systems (ACS) for which we show that
the quantification over paths in \(\textsf{CTL}^{*}\) can be simulated by
quantification over tuples of natural numbers, eventually allowing
translation of the whole Presburger-\(\textsf{CTL}^{*}\) into Presburger
arithmetic, thereby enabling effective model checking. We provide evidence
that our results are close to optimal with respect to the class of counter
systems described above.}
}
@mastersthesis{cyriac-master,
author = {Cyriac, Aiswarya},
title = {Temporal Logics for Concurrent Recursive Programs},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2010},
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ac-m2.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ac-m2.pdf}
}
@inproceedings{AC-clodem10,
address = {Edinburgh, Scotland, UK},
month = jul,
year = 2010,
acronym = {{CL}o{D}e{M}'10},
booktitle = {{P}roceedings of the {W}orkshop on {C}omparing {L}ogical {D}ecision
{M}ethods ({CL}o{D}e{M}'10)},
author = {Cyriac, Aiswarya},
title = {A~New Version of Focus Games for {LTL} Satisfiability},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ac-clodem10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ac-clodem10.pdf}
}
@comment{{B-arxiv16,
author = Bollig, Benedikt,
affiliation = aff-LSVmexico,
title = One-Counter Automata with Counter Visibility,
institution = Computing Research Repository,
number = 1602.05940,
month = feb,
nmonth = 2,
year = 2016,
type = RR,
axeLSV = mexico,
NOcontrat = "",
url = http://arxiv.org/abs/1602.05940,
PDF = "http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf",
lsvdate-new = 20160222,
lsvdate-upd = 20160222,
lsvdate-pub = 20160222,
lsv-category = "rapl",
wwwpublic = "public and ccsb",
note = 18~pages,
abstract = "In a one-counter automaton (OCA), one can read a letter
from some finite alphabet, increment and decrement the counter by
one, or test it for zero. It is well-known that universality and
language inclusion for OCAs are undecidable. We consider here OCAs
with counter visibility: Whenever the automaton produces a letter,
it outputs the current counter value along with~it. Hence, its
language is now a set of words over an infinite alphabet. We show
that universality and inclusion for that model are in PSPACE, thus
no harder than the corresponding problems for finite automata, which
can actually be considered as a special case. In fact, we show that
OCAs with counter visibility are effectively determinizable and
closed under all boolean operations. As~a~strict generalization, we
subsequently extend our model by registers. The general nonemptiness
problem being undecidable, we impose a bound on the number of
register comparisons and show that the corresponding nonemptiness
problem is NP-complete.",
}}
This file was generated by bibtex2html 1.98.