@article{CD-jar10,
publisher = {Springer},
journal = {Journal of Automated Reasoning},
author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
title = {Decidability and combination results for two notions of
knowledge in security protocols},
volume = 48,
number = {4},
pages = {441-487},
month = apr,
year = 2012,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-jar10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-jar10.pdf},
doi = {10.1007/s10817-010-9208-8},
abstract = {In formal approaches, messages sent over a network are usually
modeled by terms together with an equational theory, axiomatizing the
properties of the cryptographic functions (encryption, exclusive~or,~...).
The analysis of cryptographic protocols requires a precise understanding
of the attacker knowledge. Two standard notions are usually considered:
deducibility and indistinguishability. Those notions are well-studied and
several decidability results already exist to deal with a variety of
equational theories. Most of the existing results are dedicated to
specific equational theories and only few results, especially in the case
of indistinguishability, have been obtained for equational theories with
associative and commutative properties~(AC).\par
In this paper, we show that existing decidability results can be easily
combined for any disjoint equational theories: if the deducibility and
indistinguishability relations are decidable for two disjoint theories,
they are also decidable for their union. We also propose a general setting
for solving deducibility and indistinguishability for an important class
(called \emph{monoidal}) of equational theories involving AC operators.\par
As a consequence of these two results, new decidability and complexity
results can be obtained for many relevant equational theories.}
}
@article{KMT-jar10,
publisher = {Springer},
journal = {Journal of Automated Reasoning},
author = {Kremer, Steve and Mercier, Antoine and Treinen, Ralf},
title = {Reducing Equational Theories for the Decision of Static
Equivalence},
year = 2012,
month = feb,
pages = {197-217},
number = 48,
volume = 2,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KMT-jar10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KMT-jar10.pdf},
doi = {10.1007/s10817-010-9203-0},
abstract = {Static equivalence is a well established notion of
indistinguishability of sequences of terms which is useful in the symbolic
analysis of cryptographic protocols. Static equivalence modulo equational
theories allows for a more accurate representation of cryptographic
primitives by modelling properties of operators by equational axioms. We
develop a method that allows us in some cases to simplify the task of
deciding static equivalence in a multi-sorted setting, by removing a
symbol from the term signature and reducing the problem to several simpler
equational theories. We illustrate our technique at hand of bilinear
pairings.}
}
@article{CDK-jar10,
publisher = {Springer},
journal = {Journal of Automated Reasoning},
author = {Ciob{\^a}c{\u{a}}, {\c{S}}tefan and Delaune, St{\'e}phanie
and Kremer, Steve},
title = {Computing knowledge in security protocols under convergent
equational theories},
year = 2012,
month = feb,
pages = {219-262},
number = 2,
volume = 48,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDK-jar10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDK-jar10.pdf},
doi = {10.1007/s10817-010-9197-7},
abstract = {The analysis of security protocols requires reasoning about the
knowledge an attacker acquires by eavesdropping on network traffic. In
formal approaches, the messages exchanged over the network are modeled by
a term algebra equipped with an equational theory axiomatizing the
properties of the cryptographic primitives (e.g. encryption, signature).
In this context, two classical notions of knowledge, deducibility and
indistinguishability, yield corresponding decision problems.\par
We propose a procedure for both problems under arbitrary convergent
equational theories. Since the underlying problems are undecidable we
cannot guarantee termination. Nevertheless, our procedure terminates on a
wide range of equational theories. In particular, we obtain a new
decidability result for a theory we encountered when studying electronic
voting protocols. We also provide a prototype implementation.}
}
@article{FG-lmcs12,
journal = {Logical Methods in Computer Science},
author = {Finkel, Alain and Goubault{-}Larrecq, Jean},
title = {Forward Analysis for {WSTS}, Part~{II}: Complete {WSTS}},
year = 2012,
month = sep,
volume = 8,
number = {3:28},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FG-lmcs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FG-lmcs12.pdf},
doi = {10.2168/LMCS-8(3:28)2012},
abstract = {We describe a simple, conceptual forward analysis procedure for
\(\infty\)-complete WSTS~\(\mathfrak{S}\). This computes the so-called
\emph{clover} of a state. When \(\mathfrak{S}\) is the completion of a
WSTS~\(\mathfrak{X}\), the clover in~\(\mathfrak{S}\) is a finite
description of the downward closure of the reachability set. We show
that such completions are infinity-complete exactly when
\(\mathfrak{X}\) is an \(\omega^2\)-WSTS, a~new robust class of WSTS.
We show that our procedure terminates in more cases than the
generalized Karp-Miller procedure on extensions of Petri nets and on
lossy channel systems. We characterize the WSTS where our procedure
terminates as those that are \emph{clover-flattable}. Finally, we
apply this to well-structured counter systems.}
}
@article{JGL-lmcs12,
journal = {Logical Methods in Computer Science},
author = {Goubault{-}Larrecq, Jean},
title = {{QRB}-Domains and the Probabilistic Powerdomain},
year = 2012,
volume = 8,
number = {1:14},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-lmcs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-lmcs12.pdf},
doi = {10.2168/LMCS-8(1:14)2012},
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.\par
We introduce a natural class of such quasi-continuous dcpos, the
omega-QRB-domains. We show that they form a category omega-QRB
with pleasing properties: omega-QRB is closed under the
probabilistic powerdomain functor, under finite products, under
taking bilimits of expanding sequences, under retracts, and
even under so-called quasi-retracts. But... omega-QRB is
not Cartesian closed. We conclude by showing that the QRB
domains are just one half of an FS-domain, merely lacking
control.}
}
@article{BGGLP-comp11,
publisher = {Springer},
journal = {Computing},
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},
year = 2012,
month = mar,
volume = 94,
number = {2-4},
pages = {189-201},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGGLP-comp11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGGLP-comp11.pdf},
doi = {10.1007/s00607-011-0182-8},
abstract = {We often need to deal with information that contains
both interval and probabilistic uncertainties. P-boxes and
Dempster-Shafer structures are models that unify both kind of
information, but they suffer from the main defect of intervals,
the wrapping effect. We present here a new arithmetic that
mixes, in a guaranteed manner, interval uncertainty with
probabilities, while using some information about variable
dependencies, hence limiting the loss from not accounting for
correlations. This increases the precision of the result and
decreases the computation time compared to standard p-box
arithmetic.}
}
@inproceedings{BC-post12,
address = {Tallinn, Estonia},
month = mar,
year = 2012,
volume = {7215},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Degano, Pierpaolo and Guttman, Joshua D.},
acronym = {{POST}'12},
booktitle = {{P}roceedings of the 1st {I}nternational {C}onference on
{P}rinciples of {S}ecurity and {T}rust
({POST}'12)},
author = {Bana, Gergei and Comon{-}Lundh, Hubert},
title = {Towards Unconditional Soundness: Computationally Complete Symbolic Attacker},
pages = {189-208},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-post12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-post12.pdf},
doi = {10.1007/978-3-642-28641-4_11},
abstract = {We consider the question of the adequacy of symbolic models
versus computational models for the verification of security protocols. We
neither try to include properties in the symbolic model that reflect the
properties of the computational primitives nor add computational
requirements that enforce the soundness of the symbolic model. We propose
in this paper a different approach: everything is possible in the symbolic
model, unless it contradicts a computational assumption. In this way, we
obtain unconditional soundness almost by construction. And we do not need
to assume the absence of dynamic corruption or the absence of key-cycles,
which are examples of hypotheses that are always used in related works. We
set the basic framework, for arbitrary cryptographic primitives and
arbitrary protocols, however for trace security properties only.}
}
@inproceedings{CCS-post12,
address = {Tallinn, Estonia},
month = mar,
year = 2012,
volume = {7215},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Degano, Pierpaolo and Guttman, Joshua D.},
acronym = {{POST}'12},
booktitle = {{P}roceedings of the 1st {I}nternational {C}onference on
{P}rinciples of {S}ecurity and {T}rust
({POST}'12)},
author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique and Scerri, Guillaume},
title = {Security proof with dishonest keys},
pages = {149-168},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCS-post12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCS-post12.pdf},
doi = {10.1007/978-3-642-28641-4_9},
abstract = {Symbolic and computational models are the two families of models
for rigorously analysing security protocols. Symbolic models are abstract
but offer a high level of automation while computational models are more
precise but security proof can be tedious. Since the seminal work of Abadi
and Rogaway, a new direction of research aims at reconciling the two views
and many soundness results establish that symbolic models are actually
sound w.r.t. computational models.\par
This is however not true for the prominent case of encryption. Indeed, all
existing soundness results assume that the adversary only uses honestly
generated keys. While this assumption is acceptable in the case of
asymmetric encryption, it is clearly unrealistic for symmetric encryption.
In this paper, we provide with several examples of attacks that do not
show-up in the classical Dolev-Yao model, and that do not break the
IND-CPA nor INT-CTXT properties of the encryption scheme.\par
Our main contribution is to show the first soundness result for symmetric
encryption and arbitrary adversaries. We consider arbitrary
indistinguishability properties and an unbounded number of sessions. This
result relies on an extension of the symbolic model, while keeping
standard security assumptions: IND-CPA and IND-CTXT for the encryption
scheme.}
}
@inproceedings{CDD-post12,
address = {Tallinn, Estonia},
month = mar,
year = 2012,
volume = {7215},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Degano, Pierpaolo and Guttman, Joshua D.},
acronym = {{POST}'12},
booktitle = {{P}roceedings of the 1st {I}nternational {C}onference on
{P}rinciples of {S}ecurity and {T}rust
({POST}'12)},
author = {Cortier, V{\'e}ronique and Degrieck, Jan and Delaune, St{\'e}phanie},
title = {Analysing routing protocols: four nodes topologies are sufficient},
pages = {30-50},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDD-post12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDD-post12.pdf},
doi = {10.1007/978-3-642-28641-4_3},
abstract = {Routing protocols aim at establishing a route between nodes on a
network. Secured versions of routing protocols have been proposed in order
to provide more guarantees on the resulting routes. Formal methods have
proved their usefulness when analysing standard security protocols such as
confidentiality or authentication protocols. However, existing results and
tools do not apply to routing protocols. This is due in particular to the
fact that all possible topologies (infinitely many) have to be considered.\par
In this paper, we propose a simple reduction result: when looking for
attacks on properties such as the validity of the route, it is sufficient
to consider topologies with only four nodes, resulting in a number of just
five distinct topologies to consider. As an application, we analyse the
SRP applied to DSR and the SDMSR protocols using the ProVerif tool.}
}
@inproceedings{BHP-tacas12,
address = {Tallinn, Estonia},
month = mar,
year = 2012,
volume = {7214},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Flanagan, Cormac and K{\"o}nig, Barbara},
acronym = {{TACAS}'12},
booktitle = {{P}roceedings of the 18th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'12)},
author = {Barbot, Beno{\^\i}t and Haddad, Serge and Picaronny, Claudine},
title = {Coupling and Importance Sampling for Statistical Model Checking},
pages = {331-346},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHP-tacas12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHP-tacas12.pdf},
doi = {10.1007/978-3-642-28756-5_23},
abstract = {Statistical model-checking is an alternative verification
technique applied on stochastic systems whose size is beyond numerical
analysis ability. Given a model (most often a Markov chain) and a formula,
it provides a confidence interval for the probability that the model
satisfies the formula. One of the main limitations of the statistical
approach is the computation time explosion triggered by the evaluation of
very small probabilities. In order to solve this problem we develop a new
approach based on importance sampling and coupling. The corresponding
algorithms have been implemented in our tool cosmos. We present
experimentation on several relevant systems, with estimated time
reductions reaching a factor of~\(10^{120}\).}
}
@inproceedings{CMV-tacas12,
address = {Tallinn, Estonia},
month = mar,
year = 2012,
volume = {7214},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Flanagan, Cormac and K{\"o}nig, Barbara},
acronym = {{TACAS}'12},
booktitle = {{P}roceedings of the 18th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'12)},
author = {Chadha, Rohit and Madhusudan, P. and Viswanathan, Mahesh},
title = {Reachability under Contextual Locking},
pages = {437-450},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CMV-tacas12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CMV-tacas12.pdf},
doi = {10.1007/978-3-642-28756-5_30},
abstract = {The pairwise reachability problem for a multi-threaded program
asks, given control locations in two threads, whether they can be
simultaneously reached in an execution of the program. The problem is
important for static analysis and is used to detect statements that are
concurrently enabled. This problem is in general undecidable even when
data is abstracted and when the threads (with recursion) synchronize only
using a finite set of locks. Popular programming paradigms that limit the
lock usage patterns have been identified under which the pairwise
reachability problem becomes decidable. In this paper, we consider a new
natural programming paradigm, called contextual locking, which ties the
lock usage to calling patterns in each thread: we assume that locks are
released in the same context that they were acquired and that every lock
acquired by a thread in a procedure call is released before the procedure
returns. Our main result is that the pairwise reachability problem is
polynomial-time decidable for this new programming paradigm as well.}
}
@inproceedings{BCGK-fossacs12,
address = {Tallinn, Estonia},
month = mar,
year = 2012,
volume = 7213,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Birkedal, Lars},
acronym = {{FoSSaCS}'12},
booktitle = {{P}roceedings of the 15th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'12)},
author = {Bollig, Benedikt and Cyriac, Aiswarya and Gastin, Paul and
Narayan Kumar, K.},
title = {Model Checking Languages of Data Words},
pages = {391-405},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGK-fossacs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGK-fossacs12.pdf},
doi = {10.1007/978-3-642-28729-9_26},
abstract = {We consider the model-checking problem for data multi-pushdown
automata (DMPA). DMPA generate data words, i.e, strings enriched with
values from an infinite domain. The latter can be used to represent an
unbounded number of process identifiers so that DMPA are suitable to model
concurrent programs with dynamic process creation. To specify properties
of data words, we use monadic second-order (MSO) logic, which comes with a
predicate to test two word positions for data equality. While
satisfiability for MSO logic is undecidable (even for weaker fragments
such as first-order logic), our main result states that one can decide if
all words generated by a DMPA satisfy a given formula from the full MSO
logic.}
}
@inproceedings{BBMU-fossacs12,
address = {Tallinn, Estonia},
month = mar,
year = 2012,
volume = 7213,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Birkedal, Lars},
acronym = {{FoSSaCS}'12},
booktitle = {{P}roceedings of the 15th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'12)},
author = {Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas and Ummels, Michael},
title = {Concurrent games with ordered objectives},
pages = {301-315},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBMU-fossacs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBMU-fossacs12.pdf},
doi = {10.1007/978-3-642-28729-9_20},
abstract = {We consider concurrent games played on graphs, in which each
player has several qualitative (e.g. reachability or B{\"u}chi)
objectives, and a preorder on these objectives (for instance the counting
order, where the aim is to maximise the number of objectives that are
fulfilled).\par
We study two fundamental problems in that setting: (1)~the \emph{value
problem}, which aims at deciding the existence of a strategy that ensures
a given payoff; (2)~the \emph{Nash equilibrium problem}, where we want to
decide the existence of a Nash equilibrium (possibly with a condition on
the payoffs). We characterise the exact complexities of these problems for
several relevant preorders, and several kinds of objectives.}
}
@article{haar-deds11,
publisher = {Springer},
journal = {Discrete Event Dynamic Systems: Theory and Applications},
author = {Haar, Stefan},
title = {What topology tells us about diagnosability in partial order semantics},
pages = {383-402},
volume = 22,
number = 4,
year = {2012},
month = dec,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-deds11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-deds11.pdf},
doi = {10.1007/s10626-011-0121-z},
abstract = {From a partial observation of the behaviour of a labeled
Discrete Event System, \emph{fault diagnosis} strives to determine whether
or not a given {"}invisible{"} fault event has occurred. The
\emph{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?
When this problem is investigated in the context of 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
{"}\emph{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{CD-lopstr11,
address = {Odense, Denmark},
year = 2012,
volume = {7225},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Vidal, Germ{\'a}n},
acronym = {{LOPSTR}'11},
booktitle = {{P}roceedings of the 21st {I}nternational
{W}orkshop on {L}ogic {P}rogram {S}ynthesis
and {T}ransformation
({LOPSTR}'11)},
author = {Cabalar, Pedro and Demri, St{\'e}phane},
title = {Automata-Based Computation of Temporal Equilibrium Models},
pages = {57-72},
doi = {10.1007/978-3-642-32211-2_5},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-lopstr11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-lopstr11.pdf},
abstract = {Temporal Equilibrium Logic~(TEL) is a formalism for temporal
logic programming that generalizes the paradigm of Answer Set
Programming~(ASP) introducing modal temporal operators from standard
Linear-time Temporal Logic~(LTL). In this paper we solve some problems
that remained open for TEL like decidability, bounds for computational
complexity as well as computation of temporal equilibrium models for
arbitrary theories. We propose a method for the latter that consists in
building a B{\"u}chi automaton that accepts exactly the temporal
equilibrium models of a given theory, providing an automata-based decision
procedure and illustrating the \(\omega\)-regularity of such sets. We show
that TEL satisfiability can be solved in exponential space and it is hard
for polynomial space. Finally, given two theories, we provide a decision
procedure to check if they have the same temporal equilibrium models.}
}
@article{BJ-jal11,
publisher = {Elsevier Science Publishers},
journal = {Journal of Applied Logic},
author = {Bouhoula, Adel and Jacquemard, Florent},
title = {Sufficient completeness verification for conditional and constrained~{TRS}},
year = {2012},
month = mar,
volume = {10},
number = {1},
pages = {127-143},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BJ-jal11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BJ-jal11.pdf},
doi = {10.1016/j.jal.2011.09.001},
abstract = {We present a procedure for checking sufficient completeness of
conditional and constrained term rewriting systems containing axioms for
constructors which may be constrained (by e.g. equalities, disequalities,
ordering, membership,~...). Such axioms allow to specify complex data
structures like e.g. sets, sorted lists or powerlists. Our approach is
integrated into a framework for inductive theorem proving based on tree
grammars with constraints, a formalism which permits an exact
representation of languages of ground constructor terms in normal form.\par
The procedure is presented by an inference system which is shown sound and
complete. A~precondition of one inference of this system refers to a
(undecidable) property called strong ground reducibility which is
discharged to the above inductive theorem proving system. We have
successfully applied our method to several examples, yielding readable
proofs and, in case of negative answer, a counter-example suggesting how
to complete the specification. Moreover, we show that it is a decision
procedure when the TRS is unconditional but constrained, for an expressive
class of constrained constructor axioms.}
}
@article{DDG-jlc11,
publisher = {Oxford University Press},
journal = {Journal of Logic and Computation},
author = {Demri, St{\'e}phane and D'Souza, Deepak and Gascon, R{\'e}gis},
title = {Temporal Logics of Repeating Values},
year = {2012},
month = oct,
volume = 22,
number = 5,
pages = {1059-1096},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDG-jlc11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDG-jlc11.pdf},
doi = {10.1093/logcom/exr013},
abstract = {Various logical formalisms with the freeze quantifier have been
recently considered to model computer systems even though this is a
powerful mechanism that often leads to undecidability. In this paper, we
study a linear-time temporal logic with past-time operators such that the
freeze operator is only used to express that some value from an infinite
set is repeated in the future or in the past. Such a restriction has been
inspired by a recent work on spatio-temporal logics that suggests such a
restricted use of the freeze operator. We show decidability of finitary
and infinitary satisfiability by reduction into the verification of
temporal properties in Petri nets by proposing a symbolic representation
of models. This is a quite surprising result in view of the expressive
power of the logic since the logic is closed under negation, contains
future-time and past-time temporal operators and can express the nonce
property and its negation. These ingredients are known to lead to
undecidability with a more liberal use of the freeze quantifier. The paper
also contains developments about the relationships between temporal logics
with the freeze operator and counter automata as well as reductions into
first-order logics over data words.}
}
@inproceedings{DDS-tosca11,
address = {Saarbr{\"u}cken, Germany},
month = jan,
year = 2012,
volume = 6993,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {M{\"o}dersheim, Sebastian A. and Palamidessi, Catuscia},
acronym = {{TOSCA}'11},
booktitle = {{R}evised {S}elected {P}apaers of the {W}orkshop on {T}heory of {S}ecurity and
{A}pplications ({TOSCA}'11)},
author = {Dahl, Morten and Delaune, St{\'e}phanie and Steel, Graham},
title = {Formal Analysis of Privacy for Anonymous Location Based Services},
pages = {98-112},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-tosca11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-tosca11.pdf},
doi = {10.1007/978-3-642-27375-9_6},
abstract = {We propose a framework for formal analysis of privacy in
location based services such as anonymous electronic toll collection. We
give a formal definition of privacy, and apply it to the VPriv scheme for
vehicular services. We analyse the resulting model using the ProVerif
tool, concluding that our privacy property holds only if certain
conditions are met by the implementation. Our analysis includes some novel
features such as the formal modelling of privacy for a protocol that
relies on interactive zero-knowledge proofs of knowledge and list
permutations. }
}
@inproceedings{JLTV-tosca11,
address = {Saarbr{\"u}cken, Germany},
month = jan,
year = 2012,
volume = 6993,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {M{\"o}dersheim, Sebastian A. and Palamidessi, Catuscia},
acronym = {{TOSCA}'11},
booktitle = {{R}evised {S}elected {P}apaers of the {W}orkshop on {T}heory of {S}ecurity and
{A}pplications ({TOSCA}'11)},
author = {Jacquemard, Florent and Lozes, {\'E}tienne and Treinen, Ralf and
Villard, Jules},
title = {Multiple Congruence Relations, First-Order Theories on
Terms, and the Frames of the Applied Pi-Calculus},
pages = {166-185},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/JLTV-tosca11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JLTV-tosca11.pdf},
doi = {10.1007/978-3-642-27375-9_10},
abstract = {We investigate the problem of deciding first-order theories of
finite trees with several distinguished congruence relations, each of them
given by some equational axioms. We give an automata-based solution for
the case where the different equational axiom systems are linear and
variable-disjoint (this includes the case where all axioms are ground),
and where the logic does not permit to express tree relations
\(x=f(y,z)\). We~show that the problem is undecidable when these
restrictions are relaxed. As motivation and application, we show how to
translate the model-checking problem of \(A\pi\mathcal{L}\), a~spatial
equational logic for the applied pi-calculus, to the validity of
first-order formulas in term algebras with multiple congruence
relations.}
}
@incollection{DG-iis09,
author = {Demri, St{\'e}phane and Gastin, Paul},
title = {Specification and Verification using Temporal Logics},
booktitle = {Modern applications of automata theory},
editor = {D'Souza, Deepak and Shankar, Priti},
series = {IISc Research Monographs},
volume = 2,
publisher = {World Scientific},
chapter = 15,
pages = {457-494},
year = 2012,
month = jul,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DG-iis09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DG-iis09.pdf},
abstract = {This chapter illustrates two aspects of automata theory related
to linear-time temporal logic LTL used for the verification of computer
systems. First, we present a translation from LTL formulae to B{\"u}chi
automata. The aim is to design an elementary translation which is
reasonably efficient and produces small automata so that it can be easily
taught and used by hand on real examples. Our translation is in the spirit
of the classical tableau constructions but is optimized in several ways.
Secondly, we recall how temporal operators can be defined from regular
languages and we explain why adding even a single operator definable by a
context-free language can lead to undecidability.}
}
@inproceedings{CU-fsttcs12,
address = {Hyderabad, India},
month = dec,
year = 2012,
volume = 18,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
acronym = {{FSTTCS}'12},
booktitle = {{P}roceedings of the 32nd {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'12)},
author = {Chadha, Rohit and Ummels, Michael},
title = {The complexity of quantitative information flow in recursive
programs},
pages = {534-545},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-15.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-15.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2012.534},
abstract = {Information-theoretic measures based upon mutual information can
be employed to quantify the information that an \emph{execution} of a
program reveals about its \emph{secret inputs}. The \emph{information
leakage bounding problem} asks whether the information leaked by a program
does not exceed a certain amount. We consider this problem for two
scenarios: a)~the \emph{outputs} of the program are revealed, and b)~the
\emph{timing} (measured in the number of execution steps) of the program
is revealed. For both scenarios, we establish complexity results in the
context of deterministic boolean programs, both for programs with and
without recursion. In particular, we prove that for recursive programs the
information leakage bounding problem is no harder than checking
reachability.}
}
@inproceedings{ASV-www12comp,
address = {Lyon, France},
month = apr,
year = 2012,
publisher = {ACM Press},
editor = {Mille, Alain and Gandon, Fabien L. and Misselis, Jacques and
Rabinovich, Michael and Staab, Steffen},
acronym = {{WWW}'12},
booktitle = {{P}roceedings of the 21st {W}orld {W}ide {W}eb {C}onference
({WWW}'12)~-- {C}ompanion {V}olume},
author = {Abiteboul, Serge and Senellart, Pierre and Vianu, Victor},
title = {The {ERC} webdam on foundations of web data management},
pages = {211-214},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ASV-www12comp.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ASV-www12comp.pdf},
abstract = {The Webdam ERC grant is a five-year project that started
in December~2008. The goal is to develop a formal model for Web
data management that would open new horizons for the development
of the Web in a well-principled way, enhancing its functionality,
performance, and reliability. Specifically, the goal is to develop
a universally accepted formal framework for describing complex and
flexible interacting Web applications featuring notably data
exchange, sharing, integration, querying, and updating. We also
propose to develop formal foundations that will enable peers to
concurrently reason about global data management activities,
cooperate in solving specific tasks, and support services with
desired quality of service. Although the proposal addresses
fundamental issues, its goal is to serve as the basis for future
software development for Web data management.}
}
@inproceedings{ABD-webdb12,
address = {Scottsdale, Arizona, USA},
month = may,
year = 2012,
editor = {Ives, Zachary G. and Velegrakis, Yannis},
acronym = {({W}eb{DB}'12)},
booktitle = {{P}roceedings of the 15th {I}nternational {W}orkshop on the
{W}eb and {D}atabases ({W}eb{DB}'12)},
author = {Abiteboul, Serge and Bienvenu, Meghyn and Deutch, Daniel},
title = {Deduction in the Presence of Distribution and Contradictions},
pages = {31-36},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABD-webdb12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABD-webdb12.pdf},
abstract = {We study deduction, captured by \emph{datalog}-style
rules, in the presence of contradictions, captured by
\emph{functional dependency} (FD) violation. We propose a simple
non-deterministic semantics for datalog with FDs based on
inferring facts one at a time, never violating the FDs. We present
a novel \emph{proof theory} for this semantics. We also discuss a
set-at-a-time semantics, where at each iteration, all facts that
can be inferred are added to the database, and then choices are
made between contradicting facts. We then build upon a distributed
datalog idiom, namely \emph{Webdamlog}, to define a semantics for
the \emph{distributed setting}. Observe that contradictions
naturally arise in such a setting, with different peers having
conflicting information or opinions. We study different semantics
for this setting.}
}
@inproceedings{AAMS-sigmod12,
address = {Scottsdale, Arizona, USA},
month = may,
year = 2012,
publisher = {ACM Press},
editor = {Candan, K. Sel{\c{c}}uk and Chen, Yi and Snodgrass, Richard T. and
Gravano, Luis and Fuxman, Ariel},
acronym = {{SIGMOD}'12},
booktitle = {{P}roceedings of the {ACM} {SIGMOD} {I}nternaitonal
{C}onference on {M}anagement of {D}ata ({SIGMOD}'12)},
author = {Abiteboul, Serge and Amsterdamer, Yael and
Milo, Tova and Senellart, Pierre},
title = {Auto-completion learning for~{XML}},
pages = {669-672},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AAMS-sigmod12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AAMS-sigmod12.pdf},
doi = {10.1145/2213836.2213928},
abstract = {Editing an XML document manually is a complicated task.
While many XML editors exist in the market, we argue that some
important functionalities are missing in all of them. Our goal is
to makes the editing task simpler and faster. We~present ALEX
(Auto-completion Learning Editor for~XML), an editor that assists
the users by providing intelligent autocompletion
suggestions. These suggestions are adapted to the user needs,
simply by feeding ALEX with a set of example XML documents to
learn from. The~suggestions are also guaranteed to be compliant
with a given XML schema, possibly including integrity
constraints. To~fulfill this challenging goal, we rely on novel,
theoretical foundations by us and others, which are combined here
in a system for the first time.}
}
@inproceedings{ABV-icdt12,
address = {Berlin, Germany},
month = mar,
year = 2012,
publisher = {ACM Press},
editor = {Deutsch, Alin},
acronym = {{ICDT}'12},
booktitle = {{P}roceedings of the 15th {I}nternational {C}onference on
{D}atabase {T}heory ({ICDT}'12)},
author = {Abiteboul, Serge and Bourhis, Pierre and Vianu, Victor},
title = {Highly expressive query languages for unordered data trees},
pages = {46-60},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABV-icdt12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABV-icdt12.pdf},
doi = {10.1145/2274576.2274583},
abstract = {We study highly expressive query languages for unordered
data trees, using as formal vehicles Active XML and extensions of
languages in the while family. All languages may be seen as adding
some form of control on top of a set of basic pattern queries. The
results highlight the impact and interplay of different factors:
the expressive power of basic queries, the embedding of
computation into data (as~in Active~XML), and the use of
deterministic vs. nondeterministic control. All languages are
Turing complete, but not necessarily query complete in the sense
of Chandra and Harel. Indeed, we show that some combinations of
features yield serious limitations, analogous to \(FO^{k}\)
definability in the relational context. On the other hand, the
limitations come with benefits such as the existence of powerful
normal forms. Other languages are {"}almost{"} complete, but fall
short because of subtle limitations reminiscent of the copy
elimination problem in object databases.}
}
@inproceedings{AADMS-icdt12,
address = {Berlin, Germany},
month = mar,
year = 2012,
publisher = {ACM Press},
editor = {Deutsch, Alin},
acronym = {{ICDT}'12},
booktitle = {{P}roceedings of the 15th {I}nternational {C}onference on
{D}atabase {T}heory ({ICDT}'12)},
author = {Abiteboul, Serge and Amsterdamer, Yael and Deutch, Daniel and
Milo, Tova and Senellart, Pierre},
title = {Finding optimal probabilistic generators for {XML} collections},
pages = {127-139},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AADMS-icdt12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AADMS-icdt12.pdf},
doi = {10.1145/2274576.2274591},
abstract = {We study the problem of, given a corpus of XML documents
and its schema, finding an optimal (generative) probabilistic
model, where optimality here means maximizing the likelihood of
the particular corpus to be generated. Focusing first on the
structure of documents, we present an efficient algorithm for
finding the best generative probabilistic model, in the absence of
constraints. We further study the problem in the presence of
integrity constraints, namely key, inclusion, and domain
constraints. We study in this case two different kinds of
generators. First, we consider a continuation-test generator that
performs, while generating documents, tests of schema
satisfiability; these tests prevent from generating a document
violating the constraints but, as we will see, they are
computationally expensive. We also study a restart generator that
may generate an invalid document and, when this is the case,
restarts and tries again. Finally, we consider the injection of
data values into the structure, to obtain a full XML document. We
study different approaches for generating these values.}
}
@inproceedings{AAS-icde12,
address = {Washington, D.C., USA},
month = apr,
year = 2012,
publisher = {{IEEE} Computer Society Press},
editor = {Kementsietsidis, Anastasios and Vaz{~}Salles, Marcos Antonio},
acronym = {{ICDE}'12},
booktitle = {{P}roceedings of the 28th {I}nternational {C}onference on
{D}ata {E}ngineering ({ICDE}'12)},
author = {Abiteboul, Serge and Antoine, {\'E}milien and Stoyanovich, Julia},
title = {Viewing the Web as a Distributed Knowledge Base},
pages = {1-4},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AAS-icde12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AAS-icde12.pdf},
doi = {10.1109/ICDE.2012.150},
abstract = {This papers addresses the challenges faced by everyday
Web users, who interact with inherently heterogeneous and
distributed information. Managing such data is currently beyond
the skills of casual users. We describe ongoing work that has as
its goal the development of foundations for declarative
distributed data management. In this approach, we see the Web as a
knowledge base consisting of distributed logical facts and
rules. Our objective is to enable automated reasoning over this
knowledge base, ultimately improving the quality of service and of
data. For this, we use Webdamlog, a Datalog-style language with
rule delegation. We outline ongoing efforts on the WebdamExchange
platform that combines Webdamlog evaluation with communication and
security protocols.}
}
@inproceedings{SA-dl12,
address = {Rome, Italy},
month = jun,
year = 2012,
volume = 846,
series = {CEUR Workshop Proceedings},
publisher = {RWTH Aachen, Germany},
editor = {Kazakov, Yevgeny and Lembo, Domenico and Wolter, Frank },
acronym = {{DL}'12},
booktitle = {{P}roceedings of the 2012 {I}nternational
{W}orkshop {D}escription {L}ogic ({DL}'09)},
author = {Abiteboul, Serge},
title = {Viewing the Web as a Distributed Knowledge Base},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SA-dl12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SA-dl12.pdf}
}
@inproceedings{SA-csl12,
address = {Fontainebleau, France},
month = sep,
year = 2012,
volume = 16,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {C{\'e}gielski, Patrick and Durand, Arnaud},
acronym = {{CSL}'12},
booktitle = {{P}roceedings of the 21st {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'12)},
author = {Abiteboul, Serge},
title = {Sharing Distributed Knowledge on the Web (Invited Talk)},
pages = {6-8},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SA-csl12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SA-csl12.pdf},
doi = {10.4230/LIPIcs.CSL.2012.6},
abstract = {To share information, we propose to see the Web as a
knowledge base consisting of distributed logical facts and
rules. Our objective is to help Web users finding information, as
well as controlling their own, using automated reasoning over
this knowledge base towards improving the quality of service and
of data. For this, we introduce Webdamlog, a Datalog-style
language with rule delegation. We~mention the implementation of a
system to support this language as well as standard communications
and security protocols.}
}
@article{ABV-tods12,
publisher = {ACM Press},
journal = {ACM Transactions on Database Systems},
author = {Abiteboul, Serge and Bourhis, Pierre and Vianu, Victor},
title = {Comparing workflow specification languages: A~matter of views},
volume = 37,
number = {2:10},
nopages = {},
year = 2012,
month = may,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABV-tods12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABV-tods12.pdf},
doi = {10.1145/2188349.2188352},
abstract = {We address the problem of comparing the expressiveness
of workflow specification formalisms using a notion of view of a
workflow. Views allow to compare widely different workflow systems
by mapping them to a common representation capturing the
observables relevant to the comparison. Using this framework, we
compare the expressiveness of several workflow specification
mechanisms, including automata, temporal constraints, and
pre-and-post conditions, with XML and relational databases as
underlying data models. One surprising result shows the
considerable power of static constraints to simulate apparently
much richer workflow control mechanisms.}
}
@article{BSS-lmcs12,
journal = {Logical Methods in Computer Science},
author = {Boja{\'n}czyk, Miko{\l}aj and Segoufin, Luc and Straubing,
Howard},
title = {Piecewise testable tree languages},
volume = 8,
number = {3:26},
nopages = {},
year = 2012,
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BSS-lmcs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BSS-lmcs12.pdf},
doi = {10.2168/LMCS-8(3:26)2012},
abstract = {This paper presents a decidable characterization of tree
languages that can be defined by a boolean combination of \(\Sigma_{1}\)
sentences. This is a tree extension of the Simon theorem, which says that
a string language can be defined by a boolean combination of \(\Sigma_{1}\)
sentences if and only if its syntactic monoid is \(\mathcal{J}\)-trivial.}
}
@article{AMSS-siamjc12,
publisher = {SIAM},
journal = {SIAM Journal on Computing},
author = {Anderson, Matthew and van Melkebeek, Dieter and Schweikardt,
Nicole and Segoufin, Luc},
title = {Locality from Circuit Lower Bounds},
volume = 41,
number = 6,
pages = {1481-1523},
year = {2012},
month = nov,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AMSS-siamjc12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AMSS-siamjc12.pdf},
doi = {10.1137/110856873},
abstract = {We study the locality of an extension of first-order logic that
captures graph queries computable in \(\textsf{AC}^{0}\), i.e., by
families of polynomial-size constant-depth circuits. The extension
considers first-order formulas over relational structures which may use
arbitrary numerical predicates in such a way that their truth value is
independent of the particular interpretation of the numerical predicates.
We refer to such formulas as Arb-invariant first-order. We consider the
two standard notions of locality, Gaifman and Hanf locality. Our main
result gives a Gaifman locality theorem: An Arb-invariant first-order
formula cannot distinguish between two tuples that have the same
neighborhood up to distance \((\log n)^{c}\), where \(n\) represents the
number of elements in the structure and \(c\) is a constant depending on
the formula. When restricting attention to string structures, we achieve
the same quantitative strength for Hanf locality. In both cases we show
that our bounds are tight. We also present an application of our results
to the study of regular languages. Our proof exploits the close connection
between first-order formulas and the complexity class \(\textsf{AC}^{0}\)
and hinges on the tight lower bounds for parity on constant-depth
circuits.}
}
@phdthesis{benzina-phd2012,
author = {Benzina, Hedi},
title = {Enforcing Virtualized Systems Security},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2012,
month = dec,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/benzina-these12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/benzina-these12.pdf}
}
@phdthesis{balaguer-phd2012,
author = {Balaguer, Sandie},
title = {La concurrence dans les syst{\`e}mes distribu{\'e}s temps-r{\'e}el},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2012,
month = dec,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/balaguer-these12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/balaguer-these12.pdf}
}
@book{SA-bookCDF,
author = {Abiteboul, Serge},
title = {Sciences des donn{\'e}es: De la logique du premier ordre {\`a} la Toile},
publisher = {Fayard},
year = {2012},
series = {Le{\c{c}}ons inaugurales du {C}oll{\`e}ge de {F}rance}
}
@techreport{rr-lsv-12-25,
author = {Feld, Gilles and Fribourg, Laurent and Labrousse, Denis and
Revol, Bertrand and Soulat, Romain},
title = {Correct-by-Design Control of 5-level and 7-level Power Converters},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2012},
month = dec,
type = {Research Report},
number = {LSV-12-25},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-25.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-25.pdf},
versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-25-v1.pdf, 20121205},
note = {8~pages},
abstract = {High-power converters based on elementary switching cells are
more and more used in the industry of power electronics owing to various
advantages such as lower voltage stress and reduced power loss. However,
the complexity of controlling such converters is a major challenge that
the power manufacturing industry has to face with. The synthesis of
industrial switching controllers relies today on heuristic rules and
empiric simulation. The state of the system is not guaranteed to stay
within the limits that are admissible for its correct electrical behavior.
We show here how to apply a formal method in order to synthesise a
correct-by-design control that guarantees that the power converter will
always stay within a predened safe zone of variations for its input
parameters. Our method nds local invariants by decomposing the safety
space into smaller zones. The method is applied in order to synthesize
correct-by-design controls for a 5-level and 7-level power converters. We
check the validity of our approach by numerical simulations and physical
experimentations done with a prototype built by SATIE laboratory.}
}
@techreport{rr-lsv-12-24,
author = {Fribourg, Laurent and Soulat, Romain},
title = {Controlled Recurrent Subspaces for Sampled Switched Linear Systems},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2012},
month = dec,
type = {Research Report},
number = {LSV-12-24},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-24.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-24.pdf},
versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-24-v1.pdf, 20121205},
note = {11~pages},
abstract = {Sampled switched linear systems are governed by piecewise linear
dynamics that are periodically sampled with a given period~\(\tau\). At
each sampling time, the {"}mode{"} of the system, i.e., the parameters of
the linear dynamics, are switched according to a control rule. We give
here a procedure for showing that a given area~\(R\) of the state space
has a {"}\(k\)-recurrent decomposition: such a decomposition induces a
control that makes every trajectory starting from~\(R\) go back to~\(R\)
within at most \(k\) steps (i.e, \(k\tau\)\ time). We can then determine
an extended zone that contains all the trajectories issued from~\(R\);
this allows us to check safety properties of the system. We show the
practical interest of our approach on several examples of the literature.
We also give a geometrical condition on~\(R\) that ensures the existence
of a \(k\)-recurrent decomposition.}
}
@techreport{rr-lsv-12-23,
author = {Vester, Steen},
title = {Symmetric {N}ash equilibria},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2012},
month = dec,
type = {Research Report},
number = {LSV-12-23},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-23.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-23.pdf},
versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-23-v1.pdf, 20121204},
note = {51~pages}
}
@mastersthesis{m2-chretien,
author = {Chr{\'e}tien, R{\'e}my},
title = {Trace equivalence of protocols for an unbounded number of sessions},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2012},
month = sep,
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-22.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-22.pdf},
note = {30~pages},
abstract = {The problem of deciding reachability for cryptographic protocols
has been thoroughly studied for an unbounded number of sessions and proven
to be undecidable in general. Nevertheless some fragments were shown to be
decidable, either by tagging or by restricting the number of blind-copies.
On the other hand, trace equivalenc has only been proven to be decidable
for a bounded number of sessions. The objective of this talk is to provide
the first results of decidability of trace equivalence for an unbounded
number of sessions by lifting the approach followed by Comon-Lundh and
Cortier to trace equivalence.\par
Trace equivalence for a first class of protocols was shown undecidable
under scarce restrictions one variable and symmetric encryption are indeed
enough. Consequently, we restrained our class of protocols a step further
by making the protocols deterministic in some sense and preventing it from
disclosing secret keys. This tighter class of protocols was then shown to
be decidable after reduction to an equivalence between deterministic
pushdown automata.}
}
@phdthesis{brenguier-phd2012,
author = {Brenguier, Romain},
title = {{\'E}quilibres de {N}ash dans les Jeux Concurrents~--
{A}pplication aux Jeux Temporis{\'e}s},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2012,
month = nov,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/brenguier-these12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/brenguier-these12.pdf}
}
@phdthesis{cheval-phd2012,
author = {Cheval, Vincent},
title = {Automatic verification of cryptographic protocols: privacy-type properties},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2012,
month = dec,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/cheval-these12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/cheval-these12.pdf}
}
@article{CFM-ijfcs12,
publisher = {World Scientific},
journal = {International Journal of Foundations of Computer Science},
author = {Cadilhac, Micha{\"e}l and Finkel, Alain and McKenzie, Pierre},
title = {Bounded {P}arikh automata},
year = 2012,
month = dec,
volume = {23},
number = {8},
pages = {1691-1710},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-ijfcs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-ijfcs12.pdf},
doi = {10.1142/S0129054112400709},
abstract = {The Parikh finite word automaton model~(PA) was introduced and
studied by Klaedtke and Rue{\ss}. Here, we present some expressiveness
properties of a restriction of the deterministic affine PA recently
introduced, and use them as a tool to show that the bounded languages
recognized by PA are the same as those recognized by deterministic PA.
Moreover, this class of languages is shown equal to the class of bounded
languages with a semilinear iteration set.}
}
@article{CFM-rairo12,
address = {Les Ulis, France},
publisher = {EDP Sciences},
journal = {RAIRO Informatique Th{\'e}orique et Applications},
author = {Cadilhac, Micha{\"e}l and Finkel, Alain and McKenzie, Pierre},
title = {Affine {P}arikh automata},
year = 2012,
month = oct,
volume = 46,
number = 4,
pages = {511-545},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-rairo12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-rairo12.pdf},
doi = {10.1051/ita/2012013},
abstract = {The Parikh finite word automaton (PA) was introduced and studied
in 2003 by Klaedtke and Rue\ss. Natural variants of the PA arise from
viewing a PA equivalently as an automaton that keeps a count of its
transitions and semilinearly constrains their numbers. Here we adopt this
view and define the affine PA, that extends the PA by having each
transition induce an affine transformation on the PA registers, and the PA
on letters, that restricts the PA by forcing any two transitions on the
same letter to affect the registers equally. Then we report on the
expressiveness, closure, and decidability properties of such PA variants.
We note that deterministic PA are strictly weaker than deterministic
reversal-bounded counter machines.}
}
@inproceedings{CFM-dlt12,
address = {Taipei, Taiwan},
month = aug,
year = 2012,
volume = 7410,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Yen, Hsu-Chun and Ibarra, Oscar H.},
acronym = {{DLT}'12},
booktitle = {{P}roceedings of the 16th {I}nternational
{C}onference on {D}evelopments in {L}anguage {T}heory
({DLT}'12)},
author = {Cadilhac, Micha{\"e}l and Finkel, Alain and McKenzie, Pierre},
title = {Unambiguous Constrained Automata},
pages = {239-250},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-dlt12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-dlt12.pdf},
doi = {10.1007/978-3-642-31653-1_22},
abstract = {The class of languages captured by Constrained Automata~(CA)
that are unambiguous is shown to possess more closure properties than the
provably weaker class captured by deterministic~CA. Problems decidable for
deterministic CA are nonetheless shown to remain decidable for unambiguous
CA, and testing for \emph{regularity} is added to this set of decidable
problems. Unambiguous CA are then shown incomparable with deterministic
reversal-bounded machines in terms of expressivity, and a
\emph{deterministic} model equivalent to unambiguous CA is identified.}
}
@article{DDMM-lmcs12,
journal = {Logical Methods in Computer Science},
author = {Darondeau, {\relax Ph}ilippe and Demri, St{\'e}phane and
Meyer, Roland and Morvan, {\relax Ch}ristophe},
title = {{P}etri Net Reachability Graphs: Decidability Status of {FO}
Properties},
volume = 8,
number = {4:9},
nopages = {},
month = oct,
year = 2012,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDMM-lmcs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDMM-lmcs12.pdf},
doi = {10.2168/LMCS-8(4:9)2012},
abstract = {We investigate the decidability and complexity status of
model-checking problems on unlabelled reachability graphs of Petri nets by
considering first-order and modal languages without labels on transitions
or atomic propositions on markings. We consider several parameters to
separate decidable problems from undecidable ones. Not only are we able to
provide precise borders and a systematic analysis, but we also demonstrate
the robustness of our proof techniques.}
}
@techreport{AGL-arxiv12,
author = {Adj{\'e}, Assal{\'e} and Goubault{-}Larrecq, Jean},
title = {Concrete Semantics of Programs with Non-Deterministic and
Random Inputs},
year = {2012},
month = oct,
type = {Research Report},
institution = {Computing Research Repository},
number = {cs.LO/1210.2605},
url = {http://arxiv.org/abs/1210.2605},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGL-arxiv12.pdf},
originalpdf = {http://arxiv.org/pdf/1210.2605},
note = {19~pages},
abstract = {This document gives semantics to programs written in a C-like
programming language, featuring interactions with an external environment
with noisy and imprecise data.}
}
@inproceedings{BHP-simul12,
address = {Lisbon, Portugal},
month = nov,
year = 2012,
publisher = {XPS},
editor = {Dini, Petre and Lorenz, Pascal},
acronym = {{SIMUL}'12},
booktitle = {{P}roceedings of the 4th {I}nternational {C}onference on {A}dvances in
{S}ystem {S}imulation ({SIMUL}'12)},
author = {Barbot, Beno{\^\i}t and Haddad, Serge and Picaronny, Claudine},
title = {Importance Sampling for Model Checking of Continuous Time
{M}arkov Chains},
pages = {30-35},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHP-simul12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHP-simul12.pdf},
abstract = {Model checking real time properties on probabilistic systems
requires computing transient probabilities on continuous time Markov
chains. Beyond numerical analysis ability, a probabilistic framing can
only be obtained using simulation. This statistical approach fails when
directly applied to the estimation of very small probabilities. Here
combining the uniformization technique and extending our previous results,
we design a method which applies to continuous time Markov chains and
formulas of a timed temporal logic. The corresponding algorithm has been
implemented in our tool \textsc{cosmos}. We present experimentations on a
relevant system, with drastic time reductions with respect to standard
statistical model checking.}
}
@misc{verydic-d2,
author = {Iosif, Radu and Habermehl, Peter and Labbe, Sebastien and
Lozes, {\'E}tienne and Yakobowski, Boris},
title = {Concurrent Programs with Simple Data Structures {{\slash}}
Sequential Programs with Composite Data Structures},
howpublished = {Deliverable VERIDYC D~2 (ANR-09-SEGI-016)},
month = mar,
year = {2012},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/veridyc-d2.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/veridyc-d2.pdf}
}
@inproceedings{LV-wsfm11,
address = {Clermont-Ferrand, France},
year = 2012,
volume = 7176,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Carbone, Marco and Petit, Jean-Marc},
acronym = {{WS-FM}'11},
booktitle = {{R}evised {S}elected {P}apers of the 8th {I}nternational {W}orkshop on {W}eb
{S}ervices and {F}ormal {M}ethods ({WS}-{FM}'11)},
author = {Lozes, {\'E}tienne and Villard, Jules},
title = {Reliable Contracts for Unreliable Half-Duplex Communications},
pages = {2-16},
doi = {10.1007/978-3-642-29834-9_2},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LV-wsfm11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LV-wsfm11.pdf},
abstract = {Recent trends in formal models of web services description
languages and session types focus on the asynchronicity of communications.
In this paper, we study a core of these models that arose from our
modelling of the Sing\# programming language, and demonstrate
correspondences between Sing\# contracts, asynchronous session behaviors,
and the subclass of communicating automata with two participants that
satisfy the half-duplex property. This correspondence better explains the
criteria proposed by Stengel and Bultan for Sing\# contracts to be
reliable, and possibly indicate useful criteria for the design of WSDL. We
moreover establish a polynomial-time complexity for the analysis of
communication contracts under arbitrary models of asynchronicity, and we
investigate the model-checking problems against LTL formulas.}
}
@inproceedings{LL-fics12,
address = {Tallinn, Estonia},
month = mar,
year = 2012,
volume = 77,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Miller, Dale and {\'E}sik, Zolt{\'a}n},
acronym = {{FICS}'12},
booktitle = {{P}roceedings of the 8th {W}orkshop on {F}ixed {P}oints in
{C}omputer {S}cience ({FICS}'12)},
author = {Lange, Martin and Lozes, {\'E}tienne},
title = {Model-Checking the Higher-Dimensional Modal \(\mu\)-Calculus},
pages = {39-46},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LL-fics12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LL-fics12.pdf},
doi = {10.4204/EPTCS.77.6},
abstract = {The higher-dimensional modal \(\mu\)-calculus is an extension of
the \(\mu\)-calculus in which formulas are interpreted in tuples of states
of a labeled transition system. Every property that can be expressed in
this logic can be checked in polynomial time, and conversely every
polynomial-time decidable problem that has a bisimulation-invariant
encoding into labeled transition systems can also be defined in the
higher-dimensional modal \(\mu\)-calculus. We exemplify the latter
connection by giving several examples of decision problems which reduce to
model checking of the higher-dimensional modal \(\mu\)-calculus for some fixed
formulas. This way generic model checking algorithms for the logic can
then be used via partial evaluation in order to obtain algorithms for
theses problems which may benefit from improvements that are
well-established in the field of program verification, namely on-the-fly
and symbolic techniques. The aim of this work is to extend such techniques
to other fields as well, here exemplarily done for process equivalences,
automata theory, parsing, string problems, and games.}
}
@inproceedings{CD-lics12,
address = {Dubrovnik, Croatia},
month = jun,
year = 2012,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'12},
booktitle = {{P}roceedings of the 27th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'12)},
author = {Chatterjee, Krishnendu and Doyen, Laurent},
title = {Partial-Observation Stochastic Games: How to Win when Belief Fails},
pages = {175-184},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-lics12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-lics12.pdf},
doi = {10.1109/LICS.2012.28},
abstract = {We consider two-player stochastic games played on finite graphs
with reachability objectives where the first player tries to ensure a
target state to be visited almost-surely (i.e., with probability~\(1\)),
or positively (i.e., with positive probability), no matter the strategy of
the second player.\par
We classify such games according to the information and the power of
randomization available to the players. On the basis of information, the
game can be one-sided with either (a)~player~1, or (b)~player~2 having
partial observation (and the other player has perfect observation), or
two-sided with (c)~both players having partial observation. On the basis
of randomization, the players (a)~may not be allowed to use randomization
(pure strategies), or (b)~may choose a probability distribution over
actions but the actual random choice is external and not visible to the
player (actions invisible), or (c)~may use full randomization.\par
Our main results for pure strategies are as follows. (1)~For one-sided
games with player~1 having partial observation we show that (in contrast
to full randomized strategies) belief-based (subset-construction based)
strategies are not sufficient, and we present an exponential upper bound
on memory both for almost-sure and positive winning strategies; we show
that the problem of deciding the existence of almost-sure and positive
winning strategies for player~1 is EXPTIME-complete. (2)~For one-sided
games with player~2 having partial observation we show that non-elementary
memory is both necessary and sufficient for both almost-sure and positive
winning strategies. (3)~We~show that for the general (two-sided) case
finite-memory strategies are sufficient for both positive and almost-sure
winning, and at least non-elementary memory is required.\par
We establish the equivalence of the almost-sure winning problems for pure
strategies and for randomized strategies with actions invisible. Our
equivalence result exhibits serious flaws in previous results of the
literature: we show a non-elementary memory lower bound for almost-sure
winning whereas an exponential upper bound was previously claimed.}
}
@article{CD-tcs12,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Chatterjee, Krishnendu and Doyen, Laurent},
title = {Energy parity games},
volume = 458,
year = 2012,
month = nov,
pages = {49-60},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-tcs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-tcs12.pdf},
doi = {10.1016/j.tcs.2012.07.038},
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 (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 objectives. 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 \(\textsf{NP} \cap \textsf{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
logspace-equivalent to the problem of deciding the winner in mean-payoff
parity games, which can thus be solved in \(\textsf{NP} \cap
\textsf{coNP}\). As a consequence we also obtain a conceptually simple
algorithm to solve mean-payoff parity games.}
}
@misc{impro-D4.1,
author = {Balaguer, Sandie and Chatain, {\relax Th}omas and Haar, Stefan},
title = {Concurrent semantics for timed distributed systems},
howpublished = {Deliverable ImpRo D~4.1 (ANR-2010-BLAN-0317)},
year = 2012,
month = mar,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d41.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d41.pdf}
}
@misc{impro-D2.1,
author = {Akshay, S. and B{\'e}rard, B{\'e}atrice and Bouyer, Patricia
and Haar, Stefan and Haddad, Serge and Jard, Claude and
Lime, Didier and Markey, Nicolas and Reynier, Pierre-Alain
and Sankur, Ocan and Thierry-Mieg, Yann},
title = {Overview of Robustness in Timed Systems},
howpublished = {Deliverable ImpRo D~2.1 (ANR-2010-BLAN-0317)},
year = 2012,
month = jan,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d21.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d21.pdf}
}
@inproceedings{KS-stm12,
address = {Pisa, Italy},
month = sep,
year = 2012,
volume = 7783,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {J{\o}sang, Audun and Samarati, Pierangela and Petrocchi, Marinella},
acronym = {{STM}'12},
booktitle = {{R}evised {S}elected {P}apers of the 8th {W}orkshop
on {S}ecurity and {T}rust {M}anagement
({STM}'12)},
author = {K{\"u}nnemann, Robert and Steel, Graham},
title = {{Y}ubi{S}ecure? Formal Security Analysis Results for the
{Y}ubikey and {Y}ubi{HSM}},
pages = {257-272 },
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-stm12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-stm12.pdf},
doi = {10.1007/978-3-642-38004-4_17},
abstract = {The Yubikey is a small hardware device designed to authenticate
a user against network-based services. Despite its widespread adoption
(over a million devices have been shipped by Yubico to more than 20~000
customers including Google and Microsoft), the Yubikey protocols have
received relatively little security analysis in the academic literature.
In the first part of this paper, we give a formal model for the operation
of the Yubikey one-time password (OTP) protocol. We prove security
properties of the protocol for an unbounded number of fresh OTPs using a
protocol analysis tool, tamarin.\par
In the second part of the paper, we analyze the security of the protocol
with respect to an adversary that has temporary access to the
authentication server. To address this scenario, Yubico offers a small
Hardware Security Module (HSM) called the YubiHSM, intended to protect
keys even in the event of server compromise. We show if the same YubiHSM
configuration is used both to set up Yubikeys and run the authentication
protocol, then there is inevitably an attack that leaks all of the keys to
the attacker. Our discovery of this attack lead to a Yubico security
advisory in February 2012. For the case where separate servers are used
for the two tasks, we give a configuration for which we can show using the
same verification tool that if an adversary that can compromise the server
running the Yubikey-protocol, but not the server used to set up new
Yubikeys, then he cannot obtain the keys used to produce one-time
passwords.}
}
@article{BGKR-tcs12,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Berwanger, Dietmar and Gr{\"a}del, Erich and Kaiser, {\L}ukasz and
Rabinovich, Roman},
title = {Entanglement and the complexity of directed graphs},
volume = 463,
year = 2012,
month = dec,
pages = {2-25},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGKR-tcs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGKR-tcs12.pdf},
doi = {10.1016/j.tcs.2012.07.010},
abstract = {Entanglement is a parameter for the complexity of
finite directed graphs that measures to which extent the cycles of
the graph are intertwined. It is defined by way of a game
similar in spirit to the cops and robber games used to
describe tree width, directed tree width, and hypertree width.
Nevertheless, on many classes of graphs, there are
significant differences between entanglement
and the various incarnations of tree width.\par
Entanglement is intimately related with the computational and
descriptive complexity of the modal \(\mu\)-calculus.
The number of fixed-point variables needed to
describe a finite graph up to bisimulation is captured by its
entanglement. This plays a crucial role in the proof
that the variable hierarchy of the \(\mu\)-calculus is strict.\par
We study complexity issues for entanglement and compare it to
other structural parameters of directed graphs.
One of our main results is that parity games of
bounded entanglement can be solved in polynomial time.
Specifically, we establish that the
complexity of solving a parity game can be parametrised in terms of
the minimal entanglement of subgames induced by a winning strategy.\par
Furthermore, we discuss the case of graphs of entanglement two.
While graphs of entanglement zero and one are very simple,
graphs of entanglement two allow arbitrary nesting of
cycles, and they form a sufficiently rich class for
modelling relevant classes of structured systems.
We provide characterisations
of this class, and propose decomposition notions similar
to the ones for tree width, DAG-width, and Kelly-width.}
}
@inproceedings{BKL-mfcs12,
address = {Bratislava, Slovakia},
month = aug,
year = 2012,
volume = 7464,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Rovan, Branislav and Sassone, Vladimiro and Widmayer, Peter},
acronym = {{MFCS}'12},
booktitle = {{P}roceedings of the 37th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'12)},
author = {Berwanger, Dietmar and Kaiser, {\L}ukasz and Le{\ss}enich, Simon},
title = {Solving Counter Parity Games},
pages = {160-171},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BKL-mfcs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BKL-mfcs12.pdf},
doi = {10.1007/978-3-642-32589-2_17},
abstract = {We study a class of parity games equipped with counters
that evolve according to arbitrary non-negative
affine functions. These games capture several cost
models for dynamic systems from the literature. We
present an elementary algorithm for computing the
exact value of a counter parity game, which both
generalizes previous results and improves their
complexity. To this end, we introduce a class of
\(\omega\)-regular games with imperfect information
and imperfect recall, solve them using
automata-based techniques, and prove a
correspondence between finite-memory strategies in
such games and strategies in counter parity games.}
}
@proceedings{rp2012-FLP,
title = {{P}roceedings of the 6th
{I}nternational {W}okshop on {R}eachability {P}roblems
({RP}'12)},
booktitle = {{P}roceedings of the 6th
{I}nternational {W}okshop on {R}eachability {P}roblems
({RP}'12)},
acronym = {{RP}'12},
editor = {Finkel, Alain and Leroux, J{\'e}r{\^o}me and Potapov, Igor},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 7550,
year = 2012,
month = sep,
address = {Bordeaux, France},
doi = {10.1007/978-3-642-33512-9},
url = {http://www.springerlink.com/content/978-3-642-33511-2/}
}
@article{BDHKO-jctB12,
publisher = {Elsevier Science Publishers},
journal = {Journal of Combinatorial Theory, Series~B},
author = {Berwanger, Dietmar and Dawar, Anuj and Hunter, Paul and Kreutzer, Staphan
and Obdrz{\'a}lek, Jan},
title = {The {DAG}-width of directed graphs},
volume = 102,
number = 4,
year = 2012,
month = jul,
pages = {900-923},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDHKO-jctB12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDHKO-jctB12.pdf},
doi = {10.1016/j.jctb.2012.04.004},
abstract = {Tree-width is a well-known metric on undirected graphs
that measures how tree-like a graph is and gives a
notion of graph decomposition that proves useful in
algorithm design. Tree-width can be characterised
by a graph searching game where a number of cops
attempt to capture a robber. We consider the
natural adaptation of this game to directed graphs
and show that monotone strategies in the game yield
a measure, called DAG-width, that can be seen to
describe how close a directed graph is to a directed
acyclic graph (DAG). We also provide an associated
decomposition and show how it is useful for
developing algorithms on directed graphs. In
particular, we show that the problem of determining
the winner of a parity game is solvable in
polynomial time on graphs of bounded DAG-width. We
also consider the relationship between DAG-width and
other connectivity measures such as directed
tree-width and path-width. A consequence we obtain
is that certain NP-complete problems such as
Hamiltonicity and disjoint paths are polynomial-time
computable on graphs of bounded DAG-width.}
}
@article{FLC-rts12,
publisher = {Springer},
journal = {Real-Time Systems},
author = {Faggioli, Dario and Lipari, Giuseppe and Cucinotta, Tommaso},
title = {Analysis and Implementation of the Multiprocessor Bandwidth
Inheritance Protocol},
volume = {48},
number = {6},
year = {2012},
month = nov,
pages = {789-825},
doi = {10.1007/s11241-012-9162-0},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FLC-rts12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FLC-rts12.pdf},
abstract = {The Multiprocessor Bandwidth Inheritance (M-BWI) protocol is an
extension of the Bandwidth Inheritance (BWI) protocol for symmetric
multiprocessor systems. Similar to Priority Inheritance, M-BWI lets a task
that has locked a resource execute in the resource reservations of the
blocked tasks, thus reducing their blocking time. The protocol is
particularly suitable for open systems where different kinds of tasks
dynamically arrive and leave, because it guarantees temporal isolation
among independent subsets of tasks without requiring any information on
their temporal parameters. Additionally, if the temporal parameters of the
interacting tasks are known, it is possible to compute an upper bound to
the interference suffered by a task due to other interacting tasks. Thus,
it is possible to provide timing guarantees for a subset of interacting
hard real-time tasks. Finally, the M-BWI protocol is neutral to the
underlying scheduling policy: it can be implemented in global, clustered
and semi-partitioned scheduling.\par
After introducing the M-BWI protocol, in this paper we formally prove its
isolation properties, and propose an algorithm to compute an upper bound
to the interference suffered by a task. Then, we describe our
implementation of the protocol for the LITMUS\textsuperscript{RT}
real-time testbed, and measure its overhead. Finally, we compare M-BWI
against FMLP and OMLP, two other protocols for resource sharing in
multiprocessor systems.}
}
@article{SLBC-rts12,
publisher = {Springer},
journal = {Real-Time Systems},
author = {Santos, Rodrigo M. and
Lipari, Giuseppe and
Bini, Enrico and
Cucinotta, Tommaso},
title = {On-line schedulability tests for adaptive reservations in
fixed priority scheduling},
volume = {48},
number = {5},
year = {2012},
month = sep,
pages = {601-634},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SLBC-rts12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SLBC-rts12.pdf},
doi = {10.1007/s11241-012-9156-y},
abstract = {Adaptive reservation is a real-time scheduling technique in
which each application is associated a fraction of the computational
resource (a reservation) that can be dynamically adapted to the varying
requirements of the application by using appropriate feedback control
algorithms. An adaptive reservation is typically implemented by using an
aperiodic server (e.g. sporadic server) algorithm with fixed period and
variable budget. When the feedback law demands an increase of the
reservation budget, the system must run a schedulability test to check if
there is enough spare bandwidth to accommodate such increase. The
schedulability test must be very fast, as it may be performed at each
budget update, i.e. potentially at each instance of a task; yet, it must
be as efficient as possible, to maximize resource usage.\par
In this paper, we tackle the problem of performing an efficient on-line
schedulability test for adaptive resource reservations in fixed priority
schedulers. In the literature, a number of algorithms have been proposed
for on-line admission control in fixed priority systems. We describe four
of these tests, with increasing complexity and performance. In addition,
we propose a novel on-line test, called Spare-Pot algorithm, which has
been specifically designed for the problem at hand, and which shows a good
cost/performance ratio compared to the other tests.}
}
@proceedings{atpn2012-HP,
title = {{P}roceedings of the 33rd
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({ICATPN}'12)},
booktitle = {{P}roceedings of the 33rd
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({ICATPN}'12)},
acronym = {{ICATPN}'12},
editor = {Haddad, Serge and Pomello, Lucia},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 7347,
year = 2012,
month = jun,
address = {Hamburg, Germany},
doi = {10.1007/978-3-642-31131-4},
url = {http://www.springer.com/978-3-642-31131-4}
}
@inproceedings{FGL-pn12,
address = {Hamburg, Germany},
month = jun,
year = 2012,
volume = 7347,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Haddad, Serge and Pomello, Lucia},
acronym = {{PETRI~NETS}'12},
booktitle = {{P}roceedings of the 33rd
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'12)},
author = {Finkel, Alain and Goubault{-}Larrecq, Jean},
title = {The~Theory of~{WSTS}: The~Case of Complete~{WSTS}},
pages = {3-31},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FGL-atpn12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FGL-atpn12.pdf},
doi = {10.1007/978-3-642-31131-4_2},
abstract = {We describe a simple, conceptual forward analysis procedure for
\(\infty\)-complete WSTS~\(\mathfrak{S}\). This computes the so-called
\emph{clover} of a state. When \(\mathfrak{S}\) is the completion of a
WSTS~\(\mathfrak{X}\), the clover in~\(\mathfrak{S}\) is a finite
description of the downward closure of the reachability set. We show that
such completions are \(\infty\)-complete exactly when \(\mathfrak{X}\) is
an \emph{\(\omega^{2}\)-WSTS}, a new robust class of WSTS. We show that
our procedure terminates in more cases than the generalized Karp-Miller
procedure on extensions of Petri nets. We characterize the WSTS where our
procedure terminates as those that are \emph{clover-flattable}. Finally,
we apply this to well-structured Presburger counter systems.}
}
@inproceedings{BFP-fsttcs12,
address = {Hyderabad, India},
month = dec,
year = 2012,
volume = 18,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
acronym = {{FSTTCS}'12},
booktitle = {{P}roceedings of the 32nd {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'12)},
author = {Bonnet, R{\'e}mi and Finkel, Alain and Praveen, M.},
title = {Extending the {R}ackoff technique to affine nets},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFP-fsttcs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFP-fsttcs12.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2012.301},
abstract = {We study the possibility of extending the Rackoff
technique to Affine nets, which are Petri nets
extended with affine functions. The Rackoff
technique has been used for establishing \textsc{Expspace}
upper bounds for the coverability and boundedness
problems for Petri nets. We show that this technique
can be extended to strongly increasing Affine nets,
obtaining better upper bounds compared to known
results. The possible copies between places of a
strongly increasing Affine net make this extension
non-trivial. One cannot expect similar results for
the entire class of Affine nets since coverability
is Ackermann-hard and boundedness is
undecidable. Moreover, it can be proved that model
checking a logic expressing generalized coverability
properties is undecidable for strongly increasing
Affine nets, while it is known to be
\textsc{Expspace}-complete for Petri nets.}
}
@article{bs-ipl12,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Berwanger, Dietmar and Serre, Olivier},
title = {Parity games on undirected graphs},
volume = 112,
number = 23,
year = 2012,
month = dec,
pages = {928-932},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/bs-ipl12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bs-ipl12.pdf},
doi = {10.1016/j.ipl.2012.08.021},
abstract = {We examine the complexity of solving parity games in the special
case when the underlying game graph is undirected. For strictly
alternating games, that is, when the game graph is bipartite between the
players, we observe that the solution can be computed in linear time. In
contrast, when the assumption of strict alternation is dropped, we show
that the problem is as hard in the undirected case as it is in the
general, directed, case.}
}
@article{bbckrs-tcs12,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Baldan, Paolo and Bruni, Alessandro and Corradini, Andrea
and K{\"o}nig, Barbara and Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan},
title = {Efficient unfolding of contextual {P}etri nets},
volume = 449,
number = 1,
year = 2012,
month = aug,
pages = {2-22},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/bbckrs-tcs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bbckrs-tcs12.pdf},
doi = {10.1016/j.tcs.2012.04.046},
abstract = {A contextual net is a Petri net extended with read arcs, which
allows transitions to check for tokens without consuming them. Contextual
nets allow for better modelling of concurrent read access than Petri nets,
and their unfoldings can be exponentially more compact than those of a
corresponding Petri net. A constructive but abstract procedure for
generating those unfoldings was proposed in previous work. However, it
remained unclear whether the approach was useful in practice and which data
structures and algorithms would be appropriate to implement it. Here, we
address this question. We provide two concrete methods for computing
contextual unfoldings, with a view to efficiency. We report on experiments
carried out on a number of benchmarks. These show that not only are
contextual unfoldings more compact than Petri net unfoldings, but they can
be computed with the same or better efficiency, in particular with respect
to alternative approaches based on encodings of contextual nets into Petri
nets.}
}
@inproceedings{BFKSST-crypto12,
address = {Santa Barbara, California, USA},
month = aug,
year = 2012,
volume = 7417,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Safavi-Naini, Reihaneh and Canetti, Ran},
acronym = {{CRYPTO}'12},
booktitle = {{P}roceedings of the 32nd {A}nnual {I}nternational
{C}ryptology {C}onference ({CRYPTO}'12)},
author = {Bardou, Romain and Focardi, Riccardo and Kawamoto, Yusuke and
Simionato, Lorenzo and Steel, Graham and Tsay, Joe-Kai},
title = {Efficient Padding Oracle Attacks on Cryptographic Hardware},
pages = {608-625},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFKSST-crypto12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFKSST-crypto12.pdf},
doi = {10.1007/978-3-642-32009-5_36},
abstract = {We show how to exploit the encrypted key import functions of a
variety of different cryptographic devices to reveal the imported key. The
attacks are padding oracle attacks, where error messages resulting from
incorrectly padded plaintexts are used as a side channel. In the
asymmetric encryption case, we modify and improve Bleichenbacher's attack
on RSA PKCS\#1v1.5 padding, giving new cryptanalysis that allows us to
carry out the 'million message attack' in a mean of 49 000 and median of
14 500 oracle calls in the case of cracking an unknown valid ciphertext
under a 1024 bit key (the original algorithm takes a mean of 215 000 and a
median of 163 000 in the same case). We show how implementation details of
certain devices admit an attack that requires only 9 400 operations on
average (3 800 median). For the symmetric case, we adapt Vaudenay's CBC
attack, which is already highly efficient. We demonstrate the
vulnerabilities on a number of commercially available cryptographic
devices, including security tokens, smartcards and the Estonian electronic
ID card. The attacks are efficient enough to be practical: we give timing
details for all the devices found to be vulnerable, showing how our
optimisations make a qualitative difference to the practicality of the
attack. We give mathematical analysis of the effectiveness of the attacks,
extensive empirical results, and a discussion of countermeasures.}
}
@article{GS-ipl12,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Gastin, Paul and Sznajder, Nathalie},
title = {Decidability of well-connectedness for distributed synthesis},
pages = {963-968},
volume = {112},
number = {24},
month = dec,
year = 2012,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GS-ipl12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GS-ipl12.pdf},
doi = {10.1016/j.ipl.2012.08.018},
abstract = {Although the synthesis problem is often undecidable for
distributed, synchronous systems, it becomes decidable for the subclass of
uniformly well-connected (UWC) architectures, provided that only robust
specifications are considered. It is then an important issue to be able to
decide whether a given architecture falls in this class. This is the
problem addressed in this paper: we establish the decidability and precise
complexity of checking this property. This problem is in EXPSPACE and
NP-hard in the general case, but falls into PSPACE when restricted to a
natural subclass of architectures.}
}
@inproceedings{BDF-cdc12,
address = {Maui, Hawaii, USA},
month = dec,
year = 2012,
publisher = {{IEEE} Control System Society},
acronym = {{CDC}'12},
booktitle = {{P}roceedings of the 51st {IEEE} {C}onference on
{D}ecision and {C}ontrol ({CDC}'12)},
author = {Bu{\v{s}}i{\'c}, Ana and Djafri, Hilal and Fourneau,
Jean-Michel},
title = {Bounded state space truncation and censored {M}arkov chains},
pages = {5828-5833},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDF-cdc12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDF-cdc12.pdf},
doi = {10.1109/CDC.2012.6426156},
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. However, the stochastic matrix of a CMC may
be difficult to obtain. Dayar \emph{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{jks-ifiptcs12,
address = {Amsterdam, The Netherlands},
month = sep,
year = 2012,
volume = {7604},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baeten, Jos and Ball, Tom and de~Boer, Frank},
acronym = {{IFIP~TCS}'12},
booktitle = {{P}roceedings of the 7th {IFIP} {I}nternational
{C}onference on {T}heoretical {C}omputer
{S}cience
({IFIP~TCS}'12)},
author = {Jan\v{c}ar, Petr and Karandikar, Prateek and Schnoebelen,
{\relax Ph}ilippe},
title = {Unidirectional channel systems can be tested},
pages = {149-163},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/JKS-ifiptcs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JKS-ifiptcs12.pdf},
doi = {10.1007/978-3-642-33475-7_11},
abstract = {{"}Unidirectional channel systems{"} (Chambart~\& Schnoebelen,
CONCUR~2008) are systems where one-way communication from a sender to a
receiver goes via one reliable and one unreliable (unbounded fifo)
channel. Equipping these systems with the possibility of testing regular
properties on the contents of channels makes verification undecidable.
Decidability is preserved when only emptiness and nonemptiness tests are
considered: the proof relies on a series of reductions eventually allowing
us to take advantage of recent results on Post's Embedding Problem.}
}
@techreport{rr-lsv-12-16,
author = {Feld, Gilles and Fribourg, Laurent and Labrousse, Denis and
Revol, Bertrand and Soulat, Romain},
title = {Numerical simulation and physical experimentation of a
5-level and 7-level power converter under a control
designed by a formal method},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2012},
month = jul,
type = {Research Report},
number = {LSV-12-16},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-16.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-16.pdf},
versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-16-v1.pdf, 20120727},
note = {18~pages},
abstract = {High-power converters based on elementary switching cells are
more and more used in the industry of power electronics owing to various
advantages such as lower voltage stress and reduced power loss. However,
the complexity of controlling such converters is a major challenge that
the power manufacturing industry has to face with. The synthesis of
industrial switching controllers relies today on heuristic rules and
empiric simulation. There is no formal guarantee of correctness in zones
around nominal values. In [3], we have applied a backward-oriented formal
method to guarantee the good behavior of the systems within predefined
zones of variations for the input parameters. Here, for numerical
stability reasons, we choose to use a forward-oriented method. We apply
this method to a 5-level and 7-level power converters. We check the
correctness of our approach by numerical simulations and physical
experimentations.}
}
@article{AGG-lmcs12,
journal = {Logical Methods in Computer Science},
author = {Adj{\'e}, Assal{\'e} and Gaubert, St{\'e}phane and Goubault,
{\'E}ric},
title = {Coupling policy iteration with semi-definite relaxation to compute
accurate numerical invariants in static analysis},
year = 2012,
month = jan,
volume = {8},
number = {1:1},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGG-lmcs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGG-lmcs12.pdf},
doi = {10.2168/LMCS-8(1:01)2012},
abstract = {We introduce a new domain for finding precise numerical
invariants of programs by abstract interpretation. This domain, which
consists of level sets of non-linear functions, generalizes the domain of
linear {"}templates{"} introduced by Manna, Sankaranarayanan, and Sipma.
In the case of quadratic templates, we use Shor's semi-definite relaxation
to derive computable yet precise abstractions of semantic functionals, and
we show that the abstract fixpoint equation can be solved accurately by
coupling policy iteration and semi-definite programming. We demonstrate
the interest of our approach on a series of examples (filters, integration
schemes) including a degenerate one (symplectic scheme).}
}
@article{Fig-lmcs12,
journal = {Logical Methods in Computer Science},
author = {Figueira, Diego},
title = {Alternating register automata on finite words and trees},
year = 2012,
volume = {8},
number = {1:22},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/Fig-lmcs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Fig-lmcs12.pdf},
doi = {10.2168/LMCS-8(1:22)2012},
abstract = {We study alternating register automata on data words and data
trees in relation to logics. A data word (resp. data tree) is a word
(resp. tree) whose every position carries a label from a finite alphabet
and a data value from an infinite domain. We investigate one-way automata
with alternating control over data words or trees, with one register for
storing data and comparing them for equality. This is a continuation of
the study started by Demri, Lazi{\'c} and Jurdzi{\'n}ski. From the standpoint of
register automata models, this work aims at two objectives:
(1)~simplifying the existent decidability proofs for the emptiness problem
for alternating register automata; and (2)~exhibiting decidable extensions
for these models. From the logical perspective, we show that (a)~in~the
case of data words, satisfiability of LTL with one register and
quantification over data values is decidable; and (b)~the~satisfiability
problem for the so-called forward fragment of XPath on XML documents is
decidable, even in the presence of DTDs and even of key constraints. The
decidability is obtained through a reduction to the automata model
introduced. This fragment contains the child, descendant, next-sibling and
following-sibling axes, as well as data equality and inequality tests.}
}
@article{BFLZ-lmcs12,
journal = {Logical Methods in Computer Science},
author = {Bonnet, R{\'e}mi and Finkel, Alain and Leroux, J{\'e}r{\^o}me and
Zeitoun, Marc},
title = {Model Checking Vector Addition Systems with one zero-test},
year = 2012,
volume = {8},
number = {2:11},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLZ-lmcs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLZ-lmcs12.pdf},
doi = {10.2168/LMCS-8(2:11)2012},
abstract = {We design a variation of the Karp-Miller algorithm to compute,
in a forward manner, a finite representation of the cover (i.e., the
downward closure of the reachability set) of a vector addition system with
one zero-test. This algorithm yields decision procedures for several
problems for these systems, open until now, such as place-boundedness or
LTL model-checking. The proof techniques to handle the zero-test are based
on two new notions of cover: the refined and the filtered cover. The
refined cover is a hybrid between the reachability set and the classical
cover. It inherits properties of the reachability set: equality of two
refined covers is undecidable, even for usual Vector Addition Systems
(with no zero-test), but the refined cover of a Vector Addition System is
a recursive set. The second notion of cover, called the filtered cover, is
the central tool of our algorithms. It inherits properties of the
classical cover, and in particular, one can effectively compute a finite
representation of this set, even for Vector Addition Systems with one
zero-test.}
}
@phdthesis{lozes-HDR12,
author = {Lozes, {\'E}tienne},
title = {Separation Logic: Expressiveness and Copyless
Message-Passing},
year = 2012,
month = jul,
type = {M{\'e}moire d'habilitation},
school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-el12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-el12.pdf}
}
@techreport{rr-lsv-12-14,
author = {Feld, Gilles and Fribourg, Laurent and Labrousse, Denis and
Lefebvre, St{\'e}phane and Revol, Bertrand
and Soulat, Romain},
title = {Control of Multilevel Power Converters using Formal Methods},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2012},
month = jun,
type = {Research Report},
number = {LSV-12-14},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-14.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-14.pdf},
versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-14-v1.pdf, 20120626},
note = {14~pages},
abstract = {High-power converters based on elementary switching cells are
more and more used in the industry of power electronics owing to various
advantages such as lower voltage stress and reduced power loss. However,
the complexity of controlling such converters is a major challenge that
the power manufacturing industry has to face with. The synthesis of
industrial switching controllers relies today on heuristic rules and
empiric simulation. There is no formal guarantee of correctness in zones
around nominal values. It is therefore interesting to apply formal methods
to guarantee the good behavior of the systems within predefined zones of
variations for the input parameters. As far as we know, such formal
methods have been applied only to small electronic power devices (like
DC-DC boost converters) containing one switching cell. We show in this
paper that one can apply formal methods to more complicated systems, such
as multi-level converters containing several pairs of switching cells.}
}
@inproceedings{GM-ciaa12,
address = {Porto, Portugal},
month = jul,
year = 2012,
volume = {7381},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Moreira, Nelma and Reis, Rog{\'e}rio},
acronym = {{CIAA}'12},
booktitle = {{P}roceedings of the 17th {I}nternational
{C}onference on {I}mplementation and
{A}pplication of {A}utomata
({CIAA}'12)},
author = {Gastin, Paul and Monmege, Benjamin},
title = {Adding Pebbles to Weighted Automata},
pages = {28-51},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GM-ciaa12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GM-ciaa12.pdf},
doi = {10.1007/978-3-642-31606-7_4},
abstract = {We extend weighted automata and weighted rational expressions
with 2-way moves and (reusable) pebbles. We show with examples from
natural language modeling and quantitative model-checking that weighted
expressions and automata with pebbles are more expressive and allow much
more natural and intuitive specifications than classical ones.\par
We extend Kleene-Sch{\"u}tzenberger theorem showing that weighted
expressions and automata with pebbles have the same expressive power. We
focus on an efficient translation from expressions to automata.\par
We also prove that the evaluation problem for weighted automata can be
done very efficiently if the number of (reusable) pebbles is low.}
}
@inproceedings{BGMZ-atva12,
address = {Thiruvananthapuram, India},
month = oct,
year = {2012},
volume = {7561},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Mukund, Madhavan and Chakraborty, Supratik},
acronym = {{ATVA}'12},
booktitle = {{P}roceedings of the 10th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'12)},
author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin and
Zeitoun, Marc},
title = {A Probabilistic {K}leene Theorem},
pages = {400-415},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-atva12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-atva12.pdf},
doi = {10.1007/978-3-642-33386-6_31},
abstract = {We provide a Kleene Theorem for (Rabin) probabilistic automata
over finite words. Probabilistic automata generalize deterministic finite
automata and assign to a word an acceptance probability. We provide
probabilistic expressions with probabilistic choice, guarded choice,
concatenation, and a star operator. We prove that probabilistic
expressions and probabilistic automata are expressively equivalent. Our
result actually extends to two-way probabilistic automata with pebbles and
corresponding expressions.}
}
@phdthesis{djafri-phd2011,
author = {Djafri, Hilal},
title = {Approches num{\'e}riques et statistiques pour le model checking
des processus stochastiques},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2012,
month = jun,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/djafri-these11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/djafri-these11.pdf}
}
@inproceedings{CD-aiml12,
address = {Copenhagen, Denmark},
month = aug,
year = 2012,
publisher = {College Publications},
editor = {Bolander, Thomas and Bra{\"u}ner, Torben and Ghilardi, Silvio and Moss, Lawrence},
acronym = {{AiML}'12},
booktitle = {{S}elected {P}apers from the 9th
{W}orkshop on {A}dvances in {M}odal {L}ogics
({AiML}'12)},
author = {Carreiro, Facundo and Demri, St{\'e}phane},
title = {Beyond Regularity for {P}resburger Modal Logics},
pages = {161-182},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-aiml12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-aiml12.pdf},
abstract = {Satisfiability problem for modal logic~K with quantifier-free
Presburger and regularity constraints~(EML) is known to be
pspace-complete. In this paper, we consider its extension with nonregular
constraints, and more specifically those expressed by visibly pushdown
languages~(VPL). This class of languages behaves nicely, in particular
when combined with Propositional Dynamic Logic~(PDL). By extending EML, we
show that decidability is preserved if we allow at most one positive
VPL-constraint at each modal depth. However, the presence of two
VPL-contraints or the presence of a negative occurrence of a single
VPL-constraint leads to undecidability. These results contrast with the
decidability of PDL augmented with VPL-constraints.}
}
@inproceedings{PHL-tap12,
address = {Prague, Czech Republic},
month = may # {-} # jun,
year = 2012,
volume = 7305,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Brucker, Achim D. and Julliand, Jacques},
acronym = {{TAP}'12},
booktitle = {{P}roceedings of the 6th {I}nternational {C}onference
on {T}ests and {P}roofs ({TAP}'12)},
author = {Ponce{ }de{~}Le{\'o}n, Hern{\'a}n and Haar, Stefan and Longuet, Delphine},
title = {Conformance Relations for Labeled Event Structures},
pages = {83-98},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-tap12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-tap12.pdf},
doi = {10.1007/978-3-642-30473-6_8},
abstract = {We propose a theoretical framework for testing concurrent
systems from true concurrency models like Petri nets or networks of
automata. The underlying model of computation of such formalisms are
labeled event structures, which allow to represent concurrency explicitly.
The activity of testing relies on the definition of a conformance relation
that depends on the observable behaviors on the system under test, which
is given for sequential systems by ioco type relations. However, these
relations are not capable of capturing and exploiting concurrency of non
sequential behavior. We~study different conformance relations for labeled
event structures, relying on different notions of observation, and
investigate their properties and connections.}
}
@inproceedings{HSS-lics2012,
address = {Dubrovnik, Croatia},
month = jun,
year = 2012,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'12},
booktitle = {{P}roceedings of the 27th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'12)},
author = {Haddad, Serge and Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe},
title = {The Ordinal-Recursive Complexity of Timed-Arc {P}etri
Nets, Data Nets, and Other Enriched Nets},
pages = {355-364},
url = {http://hal.archives-ouvertes.fr/hal-00793811},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HSS-lics12.pdf},
doi = {10.1109/LICS.2012.46},
abstract = {We show how to reliably compute fast-growing functions
with timed-arc Petri nets and data nets. This
construction provides ordinal-recursive lower bounds
on the complexity of the main decidable properties
(safety, termination, regular simulation,~etc.) of
these models. Since these new lower bounds match the
upper bounds that one can derive from wqo theory,
they precisely characterise the computational power
of these so-called {"}enriched{"} nets.}
}
@inproceedings{DDS-ijcar12,
address = {Manchester, UK},
month = jun,
year = 2012,
volume = {7364},
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer-Verlag},
editor = {Gramlich, Bernhard and Miller, Dale and Sattler, Uli},
acronym = {{IJCAR}'12},
booktitle = {{P}roceedings of the 6th {I}nternational {J}oint
{C}onference on {A}utomated {R}easoning
({IJCAR}'12)},
author = {Demri, St{\'e}phane and Dhar, Amit Kumar and Sangnier, Arnaud},
title = {Taming Past {LTL} and Flat Counter Systems},
pages = {179-193},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-ijcar12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-ijcar12.pdf},
doi = {10.1007/978-3-642-31365-3_16},
abstract = {Reachability and LTL model-checking problems for flat counter
systems are known to be decidable but whereas the reachability problem can
be shown in NP, the best known complexity upper bound for the latter
problem is made of a tower of several exponentials. Herein, we show that
the problem is only NP-complete even if LTL admits past-time operators and
arithmetical constraints on counters. Actually, the NP upper bound is shown
by adequately combining a new stuttering theorem for Past LTL and the
property of small integer solutions for quantifier-free Presburger
formulae. Other complexity results are proved, for instance for restricted
classes of flat counter systems.}
}
@inproceedings{RS-concur12,
address = {Newcastle, UK},
month = sep,
year = 2012,
volume = 7454,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Koutny, Maciej and Ulidowski, Irek},
acronym = {{CONCUR}'12},
booktitle = {{P}roceedings of the 23rd
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'12)},
author = {Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan},
title = {Verification of {P}etri Nets with Read Arcs},
pages = {471-485},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/RS-concur12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RS-concur12.pdf},
doi = {10.1007/978-3-642-32940-1_33},
abstract = {Recent work studied the unfolding construction for contextual
nets, i.e. nets with read arcs. Such unfoldings are more concise and can
usually be constructed more efficiently than for Petri nets. However,
concrete verification algorithms exploiting these advantages were lacking
so far. We address this question and propose SAT-based verification
algorithms for deadlock and reachability of contextual nets. Moreover, we
study optimizations of the SAT encoding and report on experiments.}
}
@inproceedings{CGN-concur12,
address = {Newcastle, UK},
month = sep,
year = 2012,
volume = 7454,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Koutny, Maciej and Ulidowski, Irek},
acronym = {{CONCUR}'12},
booktitle = {{P}roceedings of the 23rd
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'12)},
author = {Cyriac, Aiswarya and Gastin, Paul and Narayan Kumar, K.},
title = {{MSO} Decidability of Multi-Pushdown Systems via Split-Width},
pages = {547-561},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CGN-concur12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CGN-concur12.pdf},
doi = {10.1007/978-3-642-32940-1_38},
abstract = {Multi-threaded programs with recursion are naturally modeled as
multi-pushdown systems. The behaviors are represented as multiply nested
words (MNWs), which are words enriched with additional binary relations
for each stack matching a push operation with the corresponding pop
operation. Any MNW can be decomposed by two basic and natural operations:
shuffle of two sequences of factors and merge of consecutive factors of a
sequence. We say that the split-width of a MNW is~\(k\) if it admits a
decomposition where the number of factors in each sequence is at most~\(k\).
The MSO theory of MNWs with split-width~\(k\) is decidable. We introduce two
very general classes of MNWs that strictly generalize known decidable
classes and prove their MSO decidability via their split-width and obtain
comparable or better bounds of tree-width of known classes.}
}
@inproceedings{BGS-concur12,
address = {Newcastle, UK},
month = sep,
year = 2012,
volume = 7454,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Koutny, Maciej and Ulidowski, Irek},
acronym = {{CONCUR}'12},
booktitle = {{P}roceedings of the 23rd
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'12)},
author = {Brenguier, Romain and G{\"o}ller, Stefan and Sankur, Ocan},
title = {A~Comparison of Succinctly Represented Finite-State Systems},
pages = {147-161},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGS-concur12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGS-concur12.pdf},
doi = {10.1007/978-3-642-32940-1_12},
abstract = {We study the succinctness of different classes of succinctly
presented finite transition systems with respect to bisimulation
equivalence. Our results show that synchronized product of finite
automata, hierarchical graphs, and timed automata are pairwise
incomparable in this sense. We moreover study the computational complexity
of deciding simulation preorder and bisimulation equivalence on these
classes.}
}
@inproceedings{BHSS-concur12,
address = {Newcastle, UK},
month = sep,
year = 2012,
volume = 7454,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Koutny, Maciej and Ulidowski, Irek},
acronym = {{CONCUR}'12},
booktitle = {{P}roceedings of the 23rd
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'12)},
author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Sassolas,
Mathieu and Sznajder, Nathalie},
title = {Concurrent Games on~{VASS} with Inhibition},
pages = {39-52},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHSS-CONCUR12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHSS-CONCUR12.pdf},
doi = {10.1007/978-3-642-32940-1_5},
abstract = {We propose to study concurrent games on a new extension of
Vector Addition Systems with States, where inhibition conditions are added
for modeling purposes. Games are a well-suited framework to solve control
problems, and concurrent semantics reflect realistic situations where the
environment can always produce a move before the controller, although it
is never required to do so. This is in contrast with previous works, which
focused mainly on turn-based semantics. Moreover, we consider asymmetric
games, where environment and controller do not have the same capabilities,
although they both have restricted power. In this setting, we investigate
reachability and safety objectives, which are not dual to each other
anymore, and we prove that (i)~reachability games are undecidable for
finite targets, (ii)~they are 2-EXPTIME-complete for upward-closed targets
and (iii)~safety games are co-NP-complete for finite, upward-closed and
semi-linear targets. Moreover, for the decidable cases, we build a finite
representation of the corresponding controllers.}
}
@inproceedings{BC-concur12,
address = {Newcastle, UK},
month = sep,
year = 2012,
volume = 7454,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Koutny, Maciej and Ulidowski, Irek},
acronym = {{CONCUR}'12},
booktitle = {{P}roceedings of the 23rd
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'12)},
author = {Balaguer, Sandie and Chatain, {\relax Th}omas},
title = {Avoiding Shared Clocks in Networks of Timed Automata},
pages = {100-114},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-concur12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-concur12.pdf},
doi = {10.1007/978-3-642-32940-1_9},
abstract = {Networks of timed automata~(NTA) are widely used to model
distributed real-time systems. Quite often in the literature, the automata
are allowed to share clocks. This is a problem when one considers
implementing such model in a distributed architecture, since reading
clocks a priori requires communications which are not explicitly described
in the model. We focus on the following question: given a NTA \(A_{1}
\parallel A_{2}\) where \(A_{2}\) reads some clocks reset by~\(A_{1}\),
does there exist a NTA \(A'_{1} \parallel A'_{2}\) without shared clocks
with the same behavior as the initial NTA? For this, we allow the automata
to exchange information during synchronizations only. We discuss a
formalization of the problem and give a criterion using the notion of
contextual timed transition system, which represents the behavior
of~\(A_{2}\) when in parallel with~\(A_{1}\). Finally, we effectively
build \(A'_{1} \parallel A'_{2}\) when it exists.}
}
@inproceedings{DLM-concur12,
address = {Newcastle, UK},
month = sep,
year = 2012,
volume = 7454,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Koutny, Maciej and Ulidowski, Irek},
acronym = {{CONCUR}'12},
booktitle = {{P}roceedings of the 23rd
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'12)},
author = {Da{~}Costa, Arnaud and Laroussinie, Fran{\c{c}}ois and
Markey, Nicolas},
title = {Quantified {CTL}: expressiveness and model checking},
pages = {177-192},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DLM-concur12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DLM-concur12.pdf},
doi = {10.1007/978-3-642-32940-1_14},
abstract = {While it was defined long ago, the extension of CTL with
quantification over atomic propositions has never been studied
extensively. Considering two different semantics (depending whether
propositional quantification refers to the Kripke structure or to its
unwinding tree), we study its expressiveness (showing in particular that
QCTL coincides with Monadic Second-Order Logic for both semantics) and
characterize the complexity of its model-checking problem, depending on
the number of nested propositional quantifiers (showing that the structure
semantics populates the polynomial hierarchy while the tree semantics
populates the exponential hierarchy). We also show how these results apply
to model checking ATL-like temporal logics for games.}
}
@inproceedings{FLMS-time12,
address = {Leicester, UK},
month = sep,
year = 2012,
publisher = {{IEEE} Computer Society Press},
editor = {Reynolds, Mark and Terenziani, Paolo and Moszkowski, Ben},
acronym = {{TIME}'12},
booktitle = {{P}roceedings of the 19th {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'12)},
author = {Fribourg, Laurent and Lesens, David and Moro, Pierre and
Soulat, Romain},
title = {Robustness Analysis for Scheduling Problems using the Inverse
Method},
pages = {73-80},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FLMS-time12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FLMS-time12.pdf},
doi = {10.1109/TIME.2012.10},
abstract = {Given a Parametric Timed Automaton (PTA)~\(\mathcal{A}\) and a
tuple~\(\pi_{0}\) of reference valuations for timings, the \emph{Inverse
Method~(IM)} synthesizes a constraint around~\(\pi_{0}\) where
\(\mathcal{A}\) behaves in the same time-abstract manner. This provides us
with a quantitative measure of robustness of the behavior
of~\(\mathcal{A}\) around~\(\pi_{0}\). We~show in this paper how
\textit{IM} can be applied in a specific way to treat the robustness of
scheduling systems. We also explain how to use the method in order to
synthesize large zones of the timing parameter space where the system is
guaranteed to be schedulable. We illustrate the method on several examples
of the literature as well as a case study originating from an industrial
design project.}
}
@inproceedings{AFKS12,
address = {Paris, France},
month = aug,
year = 2012,
volume = {7436},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Giannakopoulou, Dimitra and M{\'e}ry, Dominique},
acronym = {{FM}'12},
booktitle = {{P}roceedings of the 18th {I}nternational {S}ymposium on {F}ormal
{M}ethods ({FM}'12)},
author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent and K{\"u}hne,
Ulrich and Soulat, Romain},
title = {{IMITATOR}~2.5: A~Tool for Analyzing Robustness in Scheduling
Problems},
pages = {33-36},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AFKS-fm12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AFKS-fm12.pdf},
doi = {10.1007/978-3-642-32759-9_6},
abstract = {The tool \textsc{Imitator} implements the \emph{Inverse
Method~(IM)} for Timed Automata~(TAs). Given a TA~\(\mathcal{A}\) and a
tuple~\(\pi_{0}\) of reference valuations for timings, \textit{IM}
synthesizes a constraint around~\(\pi_{0}\) where \(\mathcal{A}\) behaves
in the same discrete manner. This provides us with a quantitative measure
of robustness of the behavior of~\(\mathcal{A}\) around~\(\pi_{0}\). The
new version \textsc{Imitator}~2.5 integrates the new features of
stopwatches (in~addition to standard clocks) and updates (in addition to
standard clock resets), as well as powerful algorithmic improvements for
state space reduction. These new features make the tool well-suited to
analyze the robustness of solutions in several classes of preemptive
scheduling problems.}
}
@inproceedings{AMH-safep12,
address = {Mexico City, Mexico},
month = aug,
year = 2012,
publisher = {IFAC},
acronym = {{SAFEPROCESS}'12},
booktitle = {{P}roceedings of the 8th {IFAC} {S}ymposium on {F}ault {D}etection,
{S}upervision and {S}afety for {T}echnical {P}rocesses ({SAFEPROCESS}'12)},
author = {Agarwal, Anoopam and Madalinski, Agnes and Haar, Stefan},
title = {Effective Verification of Weak Diagnosability},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AMH-safep12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AMH-safep12.pdf},
doi = {10.3182/20120829-3-MX-2028.00083},
abstract = {The \emph{diagnosability} problem can be stated as follows: does
a given labeled Discrete Event System allow for an outside observer to
determine the occurrence of the {"}invisible{"} fault, no later than a
bounded number of events after that unobservable occurrence, and based on
the partial observation of the behaviour? When this problem is
investigated in the context of concurrent systems, partial order semantics
induces a separation between classical or strong diagnosability on the one
hand, and \emph{weak diagnosability} on the other hand. The present paper
presents the first solution for checking weak diagnosability, via a
\emph{verifier} construction.}
}
@inproceedings{BBJM-qest12,
address = {London, UK},
month = sep,
year = 2012,
publisher = {{IEEE} Computer Society Press},
acronym = {{QEST}'12},
booktitle = {{P}roceedings of the 9th {I}nternational
{C}onference on {Q}uantitative
{E}valuation of {S}ystems
({QEST}'12)},
author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and
Jurdzi{\'n}ski, Marcin and Menet, Quentin},
title = {Almost-Sure Model-Checking of Reactive Timed Automata},
pages = {138-147},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBJM-qest12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBJM-qest12.pdf},
doi = {10.1109/QEST.2012.10},
abstract = {We consider the model of stochastic timed automata, a model in
which both delays and discrete choices are made probabilistically. We are
interested in the almost-sure model-checking problem, which asks whether
the automaton satisfies a given property with probability~\(1\). While
this problem was shown decidable for single-clock automata few years ago,
it was also proven that the algorithm for this decidability result could
not be used for general timed automata. In this paper we describe the
subclass of reactive timed automata, and we prove decidability of the
almost-sure model-checking problem under that restriction. Decidability
relies on the fact that this model is almost-surely fair. As a desirable
property of real systems, we show that reactive automata are almost-surely
non-Zeno. Finally we show that the almost-sure model-checking problem can
be decided for specifications given as deterministic timed automata.}
}
@inproceedings{BLM-qest12,
address = {London, UK},
month = sep,
year = 2012,
publisher = {{IEEE} Computer Society Press},
acronym = {{QEST}'12},
booktitle = {{P}roceedings of the 9th {I}nternational
{C}onference on {Q}uantitative
{E}valuation of {S}ystems
({QEST}'12)},
author = {Bouyer, Patricia and Larsen, Kim G. and Markey, Nicolas},
title = {Lower-Bound Constrained Runs in Weighted Timed Automata},
pages = {128-137},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLM-qest12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLM-qest12.pdf},
doi = {10.1109/QEST.2012.28},
noontract = {},
abstract = {We investigate a number of problems related to infinite runs of
weighted timed automata, subject to lower-bound constraints on the
accumulated weight. Closing an open problem from [Bouyer \textit{et~al.},
{"}Infinite runs in weighted timed automata with energy constraints{"},
FORMATS'08], we show that the existence of an infinite
lower-bound-constrained run is---for us somewhat
unexpectedly---undecidable for weighted timed automata with four or more
clocks.\par
This undecidability result assumes a fixed and know initial credit. We
show that the related problem of existence of an initial credit for which
there ex- ist a feasible run is decidable in PSPACE. We also investigate
the variant of these problems where only bounded-duration runs are
considered, showing that this restriction makes our original problem
decidable in NEXPTIME. Finally, we prove that the universal versions of
all those problems (i.e, checking that all the considered runs satisfy the
lower-bound constraint) are decidable in PSPACE.}
}
@article{BMOSW-fac12,
publisher = {Springer},
journal = {Formal Aspects of Computing},
author = {Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo{\"e}l
and Schnoebelen, {\relax Ph}ilippe and Worrell, James},
title = {On Termination and Invariance for Faulty Channel Systems},
year = 2012,
month = jul,
volume = 24,
number = {4-6},
pages = {595-607},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMOSU-fac12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMOSU-fac12.pdf},
doi = {10.1007/s00165-012-0234-7},
abstract = {A~\emph{channel machine} consists of a finite controller
together with several fifo channels; the controller can read messages from
the head of a channel and write messages to the tail of a channel. In this
paper we focus on channel machines with \emph{insertion errors}, i.e.,
machines in whose channels messages can spontaneously appear. We consider
the invariance problem: does a given insertion channel machine have an
infinite computation all of whose configurations satisfy a given
predicate? We show that this problem is primitive-recursive if the
predicate is closed under message losses. We also give a non-elementary
lower bound for the invariance problem under this restriction. Finally,
using the previous result, we show that the satisfiability problem for the
safety fragment of Metric Temporal Logic is non-elementary.}
}
@inproceedings{BDL-tase12,
address = {Beijing, China},
month = jul,
year = 2012,
publisher = {{IEEE} Computer Society Press},
noeditor = {},
acronym = {{TASE}'12},
booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium
on {T}heoretical {A}spects of {S}oftware {E}ngineering
({TASE}'12)},
author = {Bollig, Benedikt and Decker, Normann and Leucker, Martin},
title = {Frequency Linear-time Temporal Logic},
pages = {85-92},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDL-tase12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDL-tase12.pdf},
doi = {10.1109/TASE.2012.43},
abstract = {We propose fLTL, an extension to linear-time temporal logic
(LTL) that allows for expressing relative frequencies by a generalization
of temporal operators. This facilitates the specification of requirements
such as the deadlines in a real-time system must be met in at least~\(95\%\)
of all cases. For our novel logic, we establish an undecidability result
regarding the satisfiability problem but identify a decidable fragment
which strictly increases the expressiveness of LTL by allowing, e.g., to
express non-context-free properties.}
}
@inproceedings{IL-pairing12,
address = {Cologne, Germany},
month = may,
year = 2012,
volume = 7708,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abdalla, Michel and Lange, Tanja},
acronym = {{PAIRING}'12},
booktitle = {{P}roceedings of the 5th {I}nternational
{C}onference on {P}airing-Based {C}ryptography
({PAIRING}'12)},
author = {Izabach{\`e}ne, Malika and Libert, Beno{\^\i}t},
title = {Divisible E-Cash in the Standard Model},
pages = {314-332},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/IL-pairing12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/IL-pairing12.pdf},
doi = {10.1007/978-3-642-36334-4_20},
abstract = {Off-line e-cash systems are the digital analogue of regular
cash. One of the main desirable properties is anonymity: spending a coin
should not reveal the identity of the spender and, at the same time, users
should not be able to double-spend coins without being detected. Compact
e-cash systems make it possible to store a wallet of \(O(2^{L})\) coins
using \(O(L + \lambda)\) bits, where \(\lambda\) is the security
parameter. They are called \emph{divisible} whenever the user has the
flexibility of spending an amount of~\(2^{\ell}\), for some \(\ell\leq
L\), more efficiently than by repeatedly spending individual coins. This
paper presents the first construction of divisible e-cash in the standard
model (i.e., without the random oracle heuristic). The scheme allows a
user to obtain a wallet of~\(2^{L}\) coins by running a withdrawal
protocol with the bank. Our construction is built on the traditional
binary tree approach, where the wallet is organized in such a way that the
monetary value of a coin depends on how deep the coin is in the tree.}
}
@inproceedings{BMS-icalp12,
address = {Warwick, UK},
month = jul,
year = 2012,
volume = {7392},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Czumaj, Artur and Mehlhorn, Kurt and Pitts, Andrew and Wattenhofer, Roger},
acronym = {{ICALP}'12},
booktitle = {{P}roceedings of the 39th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'12)~-- {P}art~{II}},
author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan},
title = {Robust Reachability in Timed Automata: A~Game-based
Approach},
pages = {128-140},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-icalp12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-icalp12.pdf},
doi = {10.1007/978-3-642-31585-5_15},
abstract = {Reachability checking is one of the most basic problems in
verification. By solving this problem, one synthesizes a strategy that
dictates the actions to be performed for ensuring that the target location
is reached. In this work, we are interested in synthesizing {"}robust{"}
strategies for ensuring reachability of a location in a timed automaton;
with {"}robust{"}, we mean that it must still ensure reachability even
when the delays are perturbed by the environment. We model this perturbed
semantics as a game between the controller and its environment, and solve
the parameterized robust reachability problem: we show that the existence
of an upper bound on the perturbations under which there is a strategy
reaching a target location is EXPTIME-complete.}
}
@incollection{topnoc12-ehh,
year = 2012,
volume = 6900,
series = {Lecture Notes in Computer Science},
editor = {Jensen, Kurt and Donatelli, Susanna and Kleijn, Jetty},
publisher = {Springer},
booktitle = {Transactions on {P}etri Nets and Other Models of Concurrency~{V}},
author = {El{~}Hog{-}Benzina, Dorsaf and Haddad, Serge and Hennicker, Rolf},
title = {Refinement and Asynchronous Composition of Modal {P}etri Nets},
pages = {96-120},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/topnoc12-ehh.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/topnoc12-ehh.pdf},
doi = {10.1007/978-3-642-29072-5_4},
abstract = {We propose a framework for the specification of infinite state
systems based on Petri nets with distinguished \emph{may}- and
\emph{must}-transitions (called modalities) which specify the allowed and
the required behavior of refinements and hence of implementations. For any
modal Petri net, we define its generated modal language specification
which abstracts away silent transitions. On this basis we consider
refinements of modal Petri nets by relating their generated 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 scenario of our approach we
consider I/O-Petri nets and their asynchronous composition which typically
leads to an infinite state system.}
}
@inproceedings{benzina-dictap12,
address = {Bangkok, Thailand},
month = may,
year = 2012,
publisher = {{IEEE} Computer Society Press},
acronym = {{DICTAP}'12},
booktitle = {{P}roceedings of the 2nd {I}nternational {C}onference on {D}igital
{I}nformation and {C}ommunication {T}echnology and its
{A}pplication ({DICTAP}'12)},
author = {Benzina, Hedi},
title = {Towards Designing Secure Virtualized Systems},
pages = {250-255},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HB-dictap12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HB-dictap12.pdf},
doi = {10.1109/DICTAP.2012.6215385},
abstract = {Virtual machine technology is rapidly gaining acceptance as a
fundamental building block in enterprise data centers. It is most known
for improving efficiency and ease of management. However, it also provides
a compelling approach to enhancing system security, offering new ways to
rearchitect todays systems and opening the door for a wide range of future
security technologies. While this technology is meant to enhance the
security of computer systems, some recent attacks show that virtual
machine technology has many weaknesses and becomes exposed to many
security threats. In this paper we present some of these threats and show
how we protect these systems through intrusion detection and security
policies mechanisms.}
}
@article{jcss12-DJLL,
publisher = {Elsevier Science Publishers},
journal = {Journal of Computer and System Sciences},
author = {Demri, St{\'e}phane and Jurdzi{\'n}ski, Marcin and Lachish, Oded and
Lazi{\'c}, Ranko},
title = {The covering and boundedness problems for branching
vector addition systems},
year = {2012},
volume = 79,
number = 1,
pages = {23-38},
month = feb,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/djll-jcss12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/djll-jcss12.pdf},
doi = {10.1016/j.jcss.2012.04.002},
abstract = {The covering and boundedness problems for branching vector
addition systems are shown complete for doubly-exponential time.}
}
@inproceedings{ACD-csf12,
address = {Cambridge Massachusetts, USA},
month = jun,
year = 2012,
publisher = {{IEEE} Computer Society Press},
acronym = {{CSF}'12},
booktitle = {{P}roceedings of the
25th {IEEE} {C}omputer {S}ecurity {F}oundations
{S}ymposium ({CSF}'12)},
author = {Arapinis, Myrto and Cheval, Vincent and Delaune, St{\'e}phanie},
title = {Verifying privacy-type properties in a modular way},
pages = {95-109},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACD-csf12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACD-csf12.pdf},
doi = {10.1109/CSF.2012.16},
abstract = {Formal methods have proved their usefulness for analysing the
security of protocols. In this setting, privacy-type security properties
(e.g. vote-privacy, anonymity, unlinkability) that play an important role
in many modern applications are formalised using a notion of
equivalence.\par
In this paper, we study the notion of trace equivalence and we show how to
establish such an equivalence relation in a modular way. It is well-known
that composition works well when the processes do not share secrets.
However, there is no result allowing us to compose processes that rely on
some shared secrets such as long term keys. We show that composition works
even when the processes share secrets provided that they satisfy some
reasonable conditions. Our composition result allows us to prove various
equivalence-based properties in a modular way, and works in a quite
general setting. In particular, we consider arbitrary cryptographic
primitives and processes that use non-trivial else branches.\par
As an example, we consider the ICAO e-passport standard, and we show how
the privacy guarantees of the whole application can be derived from the
privacy guarantees of its sub-protocols.}
}
@inproceedings{benzina-iscc12,
address = {Nev{\c{s}}ehir, Turkey},
month = jul,
year = 2012,
publisher = {{IEEE} Computer Society Press},
noeditor = {},
acronym = {{ISCC}'12},
booktitle = {{P}roceedings of the 17th {IEEE} {S}ymposium on {C}omputers and
{C}ommunications ({ISCC}'12)},
author = {Benzina, Hedi},
title = {A~Network Policy Model for Virtualized Systems},
pages = {680-683},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/benzina-iscc12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/benzina-iscc12.pdf},
doi = {10.1109/ISCC.2012.6249376},
abstract = {Modern hypervisors offer the ability to build virtual networks
between virtual machines. These networks are very useful in both personal
and professional activities since they offer the same opportunities as
physical networks, but in a much lower cost in terms of hardware and time.
On the other hand, these networks are facing many security threats due to
the absence of rigourous security policies that protect the sensitive
ressources of the network. In this paper, we propose a multilevel security
policy model for these networks, this policy covers not only network
operations, but also operations related to the management of the virtual
architecture.}
}
@inproceedings{DKP-ijcar12,
address = {Manchester, UK},
month = jun,
year = 2012,
volume = {7364},
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer-Verlag},
editor = {Gramlich, Bernhard and Miller, Dale and Sattler, Uli},
acronym = {{IJCAR}'12},
booktitle = {{P}roceedings of the 6th {I}nternational {J}oint
{C}onference on {A}utomated {R}easoning
({IJCAR}'12)},
author = {Delaune, St{\'e}phanie and Kremer, Steve and Pasail{\u{a}}, Daniel},
title = {Security protocols, constraint systems, and
group theories},
pages = {164-178},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DKP-ijcar12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DKP-ijcar12.pdf},
doi = {10.1007/978-3-642-31365-3_15},
abstract = {When formally analyzing security protocols it is often
important to express properties in terms of an
adversary's inability to distinguish two
protocols. It has been shown that this problem
amounts to deciding the equivalence of two
constraint systems, i.e., whether they have the same
set of solutions. In this paper we study this
equivalence problem when cryptographic primitives
are modeled using a group equational theory, a
special case of monoidal equational theories. The
results strongly rely on the isomorphism between
group theories and rings. This allows us to reduce
the problem under study to the problem of solving
systems of equations over rings.\par We provide
several new decidability and complexity results,
notably for equational theories which have
applications in security protocols, such as
exclusive or and Abelian groups which may
additionally admit a unary, homomorphic symbol.}
}
@inproceedings{KS-csr12,
address = {Nizhni Novgorod, Russia},
month = jul,
year = 2012,
volume = {7353},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hirsch, Edward A. and Karhum{\"a}ki, Juhani and Lepist{\"o},
Arto and Prilutskii, Michail},
acronym = {{CSR}'12},
booktitle = {{P}roceedings of the 7th {I}nternational {C}omputer {S}cience
{S}ymposium in {R}ussia ({CSR}'12)},
author = {Karandikar, Prateek and Schnoebelen, {\relax Ph}ilippe},
title = {Cutting Through Regular {P}ost Embedding Problems},
pages = {229-240},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-csr12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-csr12.pdf},
doi = {10.1007/978-3-642-30642-6_22},
abstract = {The Regular Post Embedding Problem extended with partial
(co)directness is shown decidable. This extends to universal and{\slash}or
counting versions. It is also shown that combining directness and
codirectness in Post Embedding problems leads to undecidability.}
}
@phdthesis{doyen-HDR11,
author = {Doyen, Laurent},
title = {Games and Automata: From Boolean to Quantitative Verification},
year = 2012,
month = mar,
type = {M{\'e}moire d'habilitation},
school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-ld.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-ld.pdf},
noslides = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/hdr-ld-slides.pdf}
}
@techreport{rr-lsv-12-05,
author = {Soulat, Romain},
title = {Scheduling with {IMITATOR}: Some Case Studies},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2012},
month = mar,
type = {Research Report},
number = {LSV-12-05},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-05.pdf},
versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-05-v1.pdf, 20120313},
note = {13~pages},
abstract = {The tool IMITATOR implements the \emph{Inverse Method (IM)} for
Timed Automata (TAs). Given a TA~\(\mathcal{A}\) and a tuple~\(\pi_0\) of
reference valuations for timings, IM synthesizes a constraint around pi0
where A behaves in the same discrete manner. This provides us with a
quantitative measure of robustness of the behavior of~\(\mathcal{A}\)
around~\(\pi_0\).\par
The new version IMITATOR~2.5 integrates the new features of stopwatches
(in addition to standard clocks) and updates (in addition to standard
clock resets), as well as powerful algorithmic improvements for state
space reduction. We illustrate on several case studies of preemptive
scheduling problems how such features make the tool well-suited to analyze
robustness.}
}
@article{BCH-fmsd12,
publisher = {Springer},
journal = {Formal Methods in System Design},
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},
year = 2012,
month = jun,
volume = 40,
number = 3,
pages = {330-355},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-fmsd12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-fmsd12.pdf},
doi = {10.1007/s10703-012-0146-4},
abstract = {Several formalisms to model distributed real-time systems
coexist in the literature. This naturally induces a need to compare their
expressiveness and to translate models from one formalism to another when
possible. The first formal comparisons of the expressiveness of these
models focused on the preservation of the sequential behavior of the
models, using notions like timed language equivalence or timed
bisimilarity. They do not consider preservation of concurrency. In~this
paper we define timed traces as a partial order representation of
executions of our models for real-time distributed systems. Timed traces
provide an alternative to timed words, and take the distribution of
actions into account. We propose a translation between two popular
formalisms that describe timed concurrent systems: \(1\)-bounded time Petri
nets~(TPN) and networks of timed automata~(NTA). Our translation preserves
the distribution of actions, that is we require that if the TPN represents
the product of several components (called processes), then each process
should have its counterpart as one timed automaton in the resulting~NTA.}
}
@techreport{rr-lsv-12-04,
author = {Barbot, Beno{\^\i}t and Haddad, Serge and Picaronny, Claudine},
title = {Importance Sampling for Model Checking of Time-Bounded Until},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2012},
month = feb,
type = {Research Report},
number = {LSV-12-04},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-04.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-04.pdf},
versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-04-v1.pdf, 20120227},
note = {14~pages},
abstract = {Statistical model-checking is an alternative verification
technique applied on stochastic systems whose size is beyond numerical
analysis ability. Given a model (most often a Markov chain) and a formula,
it provides a confidence interval for the probability that the model
satisfies the formula. In a previous contribution, we have overtaken the
main limitation of the statistical approach, i.e. the computation time
explosion associated with the evaluation of very small probabilities. This
method was valid only for the standard ``Until'' of temporal logics. We
establish a similar validity condition which applies to the ``Bounded
Until'', using more elaborate arguments. We also address the problem of
additional memory requirements necessary to apply the method and we design
several algorithms depending on the intended trade-off between time and
memory. The corresponding algorithms have been implemented in our tool
Cosmos. We present experimentations on several relevant systems, with
drastic time reductions w.r.t. standard statistical model checking.}
}
@inproceedings{AFS-nfm12,
address = {Norfolk, Virginia, USA},
month = apr,
year = 2012,
volume = 7226,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Goodloe, Alwyn and Person, Suzette},
acronym = {{NFM}'12},
booktitle = {{P}roceedings of the 4th {NASA} {F}ormal {M}ethods {S}ymposium ({NFM}'12)},
author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent and Soulat,
Romain},
title = {Enhancing the Inverse Method with State Merging},
pages = {100-105},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AFS-nfm12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AFS-nfm12.pdf},
doi = {10.1007/978-3-642-28891-3_10},
abstract = {Keeping the state space small is essential when verifying
real-time systems using Timed Automata~(TA). In~the model-checker Uppaal,
the merging operation has been used extensively in order to reduce the
number of states. Actually, Uppaal's merging technique applies within the
more general setting of Parametric Timed Automata (PTA). The \emph{Inverse
Method~(IM)} for a PTA~\(\mathcal{A}\) is a procedure that synthesizes a
zone around a given point~\(\pi^{0}\) (parameter valuation) over which
\(\mathcal{A}\) is guaranteed to behave similarly. We show that the
integration of merging into~\emph{IM} leads to the synthesis of larger
zones around~\(\pi^{0}\). It~also often improves the performance
of~\emph{IM}, both in terms of computational space and time, as shown by
our experimental results.}
}
@article{BHS-fmsd2012,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Sassolas, Mathieu},
title = {Interrupt Timed Automata: Verification and Expressiveness},
year = {2012},
month = feb,
volume = {40},
number = {1},
pages = {41-87},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHS-fmsd12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHS-fmsd12.pdf},
doi = {10.1007/s10703-011-0140-2},
abstract = {We introduce the class of Interrupt Timed Automata (ITA), a
subclass of hybrid automata well suited to the description of timed
multi-task systems with interruptions in a single processor environment.\par
While the reachability problem is undecidable for hybrid automata we show
that it is decidable for ITA. More precisely we prove that the untimed
language of an ITA is regular, by building a finite automaton as a
generalized class graph. We then establish that the reachability problem
for ITA is in NEXPTIME and in PTIME when the number of clocks is fixed. To
prove the first result, we define a subclass ITA\(_{-}\) of ITA, and show
that (1)~any ITA can be reduced to a language-equivalent automaton in
ITA\(_{-}\) and (2)~the reachability problem in this subclass is in NEXPTIME
(without any class graph).\par
In the next step, we investigate the verification of real time properties
over ITA. We prove that model checking SCL, a fragment of a timed linear
time logic, is undecidable. On the other hand, we give model checking
procedures for two fragments of timed branching time logic.\par
We also compare the expressive power of classical timed automata and ITA
and prove that the corresponding families of accepted languages are
incomparable. The result also holds for languages accepted by controlled
real-time automata (CRTA), that extend timed automata. We finally combine
ITA with CRTA, in a model which encompasses both classes and show that the
reachability problem is still decidable. Additionally we show that the
languages of ITA are neither closed under complementation nor under
intersection.}
}
@article{BK-jal12,
publisher = {Elsevier Science Publishers},
journal = {Journal of Applied Logic},
author = {Bollig, Benedikt and Kuske, Dietrich},
title = {An optimal construction of {H}anf sentences},
year = {2012},
month = jun,
volume = {10},
number = {2},
pages = {179-186},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BK-jal12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BK-jal12.pdf},
doi = {10.1016/j.jal.2012.01.002},
abstract = {We give a new construction of formulas in Hanf normal form that
are equivalent to first-order formulas over structures of bounded degree.
This is the first algorithm whose running time is shown to be elementary.
The triply exponential upper bound is complemented by a matching lower
bound.}
}
@article{GMM-fmsd2012,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Ganty, Pierre and Majumdar, Rupak and Monmege, Benjamin},
title = {Bounded underapproximations},
year = {2012},
month = apr,
volume = {40},
number = {2},
pages = {206-231},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GMM-fmsd12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GMM-fmsd12.pdf},
doi = {10.1007/s10703-011-0136-y},
abstract = {We show a new and constructive proof of the following
language-theoretic result: for every context-free language~\(L\), there is
a bounded context-free language \(L'\subseteq L\) which has the same
Parikh (commutative) image as~\(L\). Bounded languages, introduced by
Ginsburg and Spanier, are subsets of regular languages of the form
\(w_{1}^{*}w_{2}^{*}\cdots w_{m}^{*}\) for some \(w_1,\cdots,w_{m}\in
\Sigma^{*}\). In particular bounded context-free languages have nice
structural and decidability properties. Our proof proceeds in two parts.
First, we give a new construction that shows that each context free
language~\(L\) has a subset~\(L_{N}\) that has the same Parikh image
as~\(L\) and that can be represented as a sequence of substitutions on a
linear language. Second, we inductively construct a Parikh-equivalent
bounded context-free subset of~\(L_{N}\).\par
We show two applications of this result in model checking: to
underapproximate the reachable state space of multithreaded procedural
programs and to underapproximate the reachable state space of recursive
counter programs. The bounded language constructed above provides a
decidable underapproximation for the original problems. By iterating the
construction, we get a semi-algorithm for the original problems that
constructs a sequence of underapproximations such that no two
underapproximations of the sequence can be compared. This provides a
progress guarantee: every word~\(w\in L\) is in some underapproximation of
the sequence, and hence, a program bug is guaranteed to be found. In
particular, we show that verification with bounded languages generalizes
context-bounded reachability for multithreaded programs.}
}
@inproceedings{CCK-esop12,
address = {Tallinn, Estonia},
month = mar,
year = 2012,
volume = {7211},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Seidl, Helmut},
acronym = {{ESOP}'12},
booktitle = {{P}rogramming {L}anguages and {S}ystems~---
{P}roceedings of the 22nd
{E}uropean {S}ymposium on {P}rogramming
({ESOP}'12)},
author = {Chadha, Rohit and Ciob{\^a}c{\u{a}}, {\c{S}}tefan and Kremer, Steve},
title = {Automated verification of equivalence properties of
cryptographic protocols},
pages = {108-127},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCK-esop12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCK-esop12.pdf},
doi = {10.1007/978-3-642-28869-2_6},
abstract = {Indistinguishability properties are essential in formal
verification of cryptographic protocols. They are needed to model
anonymity properties, strong versions of confidentiality and resistance to
offline guessing attacks, and can be conveniently modeled using process
equivalences. We present a novel procedure to verify equivalence
properties for bounded number of sessions. Our procedure is able to verify
trace equivalence for determinate cryptographic protocols. On determinate
protocols, trace equivalence coincides with observational equivalence
which can therefore be automatically verified for such processes. When
protocols are not determinate our procedure can be used for both under-
and over-approximations of trace equivalence, which proved successful on
examples. The procedure can handle a large set of cryptographic
primitives, namely those which can be modeled by an optimally reducing
convergent rewrite system. Although, we were unable to prove its
termination, it has been implemented in a prototype tool and has been
effectively tested on examples, some of which were outside the scope of
existing tools.}
}
@article{BDL-icomp12,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Brochenin, R{\'e}mi and Demri, St{\'e}phane and Lozes, {\'E}tienne},
title = {On the Almighty Wand},
year = {2012},
volume = 211,
pages = {106-137},
month = feb,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDL-icomp12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDL-icomp12.pdf},
doi = {10.1016/j.ic.2011.12.003},
abstract = {We investigate decidability, complexity and expressive power
issues for (first-order) separation logic with one record field (herein
called~\texttt{SL}) and its fragments. \texttt{SL}~can specify properties
about the memory heap of programs with singly-linked lists. Separation
logic with two record fields is known to be undecidable by reduction of
finite satisfiability for classical predicate logic with one binary
relation. Surprisingly, we show that second-order logic is as expressive
as \texttt{SL} and as a by-product we get undecidability of~\texttt{SL}.
This is refined by showing that \texttt{SL} without the separating
conjunction is as expressive as~\texttt{SL}, whence undecidable too. As a
consequence, in \texttt{SL} the separating implication (also known as the
magic wand) can simulate the separating conjunction. By~contrast, we
establish that \texttt{SL} without the magic wand is decidable, and
we~prove a non-elementary complexity by reduction from satisfiability for
the first-order theory over finite words. This result is extended with a
bounded use of the magic wand that appears in Hoare-style rules. As a
generalisation, it~is shown that~\(k\texttt{SL}\), the separation logic
over heaps with \(k\geq 1\) record fields, is equivalent
to~\(k\texttt{SO}\), the second-order logic over heaps with \(k\) record
fields.}
}
@inproceedings{BLLJKFSFR-revet12,
address = {Hammamet, Tunisia},
month = mar,
year = 2012,
publisher = {{IEEE} Power~\& Energy Society},
editor = {Neji, Rafik},
acronym = {{REVET}'12},
booktitle = {{P}roceedings of the 1st {I}nternational {C}onference on
{R}enewable {E}nergies and {VE}hicular {T}echnology
({REVET}'12)},
author = {Belkacem, Ghania and Labrousse, Denis and Lefebvre, St{\'e}phane and
Joubert, Pierre-Yves and K{\"u}hne, Ulrich and Fribourg,
Laurent and Soulat, Romain and Florentin, {\'E}ric and Rey,
{\relax Ch}ristian},
title = {Distributed and Coupled Electrothermal Model of Power
Semiconductor Devices},
pages = {84-89},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLLJKFSFR-revet12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLLJKFSFR-revet12.pdf},
doi = {10.1109/REVET.2012.6195253},
abstract = {Electro-thermal model of power semiconductor devices are of key
importance in order to optimize their thermal design and increase their
reliability. The development of such an electro-thermal model for power
MOSFET transistors (COOLMOS\textsuperscript{(TM)}) based on the coupling
between two computation softwares (Matlab and Cast3M) is described in the
paper. The elaborated 2D electro-thermal model is able to predict
i)~the~temperature distribution on chip surface well as in volume,
ii)~the~effect of the temperature on the distribution of the current
flowing within the die and iii)~the~effects of the ageing of the
metallization layer on the current density and the temperature. In the
paper, the used electrical and thermal models are described as well as the
implemented coupling scheme.}
}
@inproceedings{SVMM-sbbd2012,
address = {S{\~a}o~Paulo, Brazil},
month = oct,
year = 2012,
editor = {Casanova, Marco A.},
publisher = {Sociedade Brasileira de Computa{\c{c}}{\~a}o},
acronym = {{SBBD}'12},
booktitle = {{P}roceedings of the 27th {B}razilian {S}ymposium on {D}atabases ({SBBD}'12)},
author = {Sim{\~o}es{ }De{~}Sousa, Diego V. and Viana, Henrique and
Markey, Nicolas and de Mac{\^e}do, Jose Ant{\^o}nio F.},
title = {Querying Trajectories through Model Checking based on Timed
Automata},
pages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SVMM-sbbd2012.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SVMM-sbbd2012.pdf},
abstract = {The popularization of geographical position devices (e.g.~GPS)
creates new opportunities for analyzing behavior of moving objects.
However, such analysis are hindered by a lack of semantic information
associated to the basic information provided by~GPS. Previous works
propose semantic enrichment of trajectories. Through the semantic
enrichment, we~could check which trajectories have a given moving sequence
in an application. Often, this~sequence is expressed according to the
semantic application, using the approach of semantic trajectories proposed
in the literature. This~trajectory can be represented as a sequence of
predicates that holds in some time interval. However, the solutions for
querying moving sequence proposed by previous works have a high
computational cost. In~this paper, we~propose an expressive query language
to semantic trajectories that allows temporal constraints. To~evaluate a
query we will use model checking based on timed automata, that can be
performed in polynomial time. As~this model checking algorithm is not
implemented yet, we propose to use UPPAAL tool, that can be more expensive
theoretically, but we expected that will be ecient for our approach. In
addition, we will present a query example that demonstrates the expressive
power of our language. Although in this paper we will focus on semantic
trajectories data, our approach is general enough for being applied to
other purposes.}
}
@incollection{CD-nato12,
author = {Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie},
title = {Formal Security Proofs},
booktitle = {Software Safety and Security},
pages = {26-63},
editor = {Nipkow, Tobias and Grumberg, Orna and Hauptmann, Benedikt},
series = {NATO Science for Peace and Security Series~-- D:~Information and
Communication Security},
volume = {33},
publisher = {{IOS} Press},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-nato12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-nato12.pdf},
year = 2012,
month = may
}
@inproceedings{CLHKS-ispec12,
address = {Hangzhou, China},
year = 2012,
month = apr,
volume = 7232,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ryan, Mark D. and Smyth, Ben and Wang, Guilin},
acronym = {{ISPEC}'12},
booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on
{I}nformation {S}ecurity {P}ractice and {E}xperience
({ISPEC}'12)},
author = {Comon{-}Lundh, Hubert and Hagiya, Masami and Kawamoto, Yusuke
and Sakurada, Hideki},
title = {Computational Soundness of Indistinguishability
Properties without Computable Parsing},
pages = {63-79},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CHKS-ispec12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CHKS-ispec12.pdf},
doi = {10.1007/978-3-642-29101-2_5},
abstract = {We provide a symbolic model for protocols using public-key
encryption and hash function, and prove that this model is computationally
sound: if there is an attack in the computational world, then there is an
attack in the symbolic (abstract) model. Our original contribution is that
we deal with the security properties, such as anonymity, which cannot be
described using a single execution trace, while considering an unbounded
number of sessions of the protocols in the presence of active and adaptive
adversaries. Our soundness proof is different from all existing studies in
that it does not require a computable parsing function from bit strings to
terms. This allows us to deal with more cryptographic primitives, such as
a preimage-resistant and collision-resistant hash function whose input may
have different lengths.}
}
@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.",
}}
@misc{AG:anr-cpp12,
author = {Adj{\'e}, Assal{\'e} and Goubault-Larrecq, Jean},
howpublished = {Fourniture du projet ANR CPP (Confidence, Proofs, and Probabilities), WP 2, version 1},
month = oct,
title = {Concrete semantics of programs with non-deterministic and random inputs},
year = {2012},
url = {http://arxiv.org/abs/1210.2605}
}
This file was generated by bibtex2html 1.98.