@inproceedings{ltc-GardentPPS11,
address = {Pozna\'n, Poland},
month = nov,
year = 2014,
volume = {8387},
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Vetulani, Zygmunt and Mariani, Joseph},
acronym = {{LTC}'11},
booktitle = {{P}roceedings of the 5th {L}anguage {\&} {T}echnology
{C}onference ({LTC}'11)},
author = {Gardent, Claire and Perrier, Guy and Parmentier, Yannick
and Schmitz, Sylvain},
title = {Lexical Disambiguation in {LTAG} using Left Context},
nopages = {},
url = {http://hal.archives-ouvertes.fr/hal-00629902/},
abstract = {In this paper, we present an automaton-based lexical
disambiguation process for Lexicalized Tree-Adjoining
Grammar (LTAG). This process builds on previous work
of Bonfante \textit{et~al.}~(2004), and extends it by
computing a polarity-based abstraction, which
contains information about left context. This
extension allows for a faster lexical disambiguation
by reducing the filtering automaton.}
}
@inproceedings{ABGGP-vstte13,
address = {Atherton, California, USA},
year = 2014,
volume = 8164,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cohen, Ernie and Rybalchenko, Andrey},
acronym = {{VSTTE}'13},
booktitle = {{R}evised {S}elected {P}apers of the
5th {IFIP} {TC2}\slash{WG2.3} {C}onference {V}erified
{S}oftware---{T}heories, {T}ools, and {E}xperiments
({VSTTE}'13)},
author = {Adj{\'e}, Assal{\'e} and Bouissou, Olivier and
Goubault{-}Larrecq, Jean and
Goubault, {\'E}ric and Putot, Sylvie},
title = {Static Analysis of Programs with Imprecise Probabilistic Inputs},
pages = {22-47},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGGP-vstte13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGGP-vstte13.pdf},
doi = {10.1007/978-3-642-54108-7},
abstract = {Having a precise yet sound abstraction of the inputs of
numerical programs is important to analyze their behavior. For many
programs, these inputs are probabilistic, but the actual distribution used
is only partially known. We present a static analysis framework for
reasoning about programs with inputs given as imprecise probabilities: we
define a collecting semantics based on the notion of previsions and an
abstract semantics based on an extension of Dempster-Shafer structures. We
prove the correctness of our approach and show on some realistic examples
the kind of invariants we are able to infer.}
}
@mastersthesis{m2-lefaucheux,
author = {Lefaucheux, Engel},
title = {D{\'e}tection de fautes dans les syst{\`e}mes probabilistes},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2014},
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-lefaucheux.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-lefaucheux.pdf},
note = {35~pages}
}
@mastersthesis{m2-dubut,
author = {Dubut, J{\'e}r{\'e}my},
title = {{H}omologie dirig{\'e}e},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2014},
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-dubut.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-dubut.pdf},
note = {35~pages}
}
@mastersthesis{m2-halfon,
author = {Halfon, Simon},
title = {Non Primitive Recursive Complexity Classes},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2014},
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-halfon.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-halfon.pdf},
note = {21~pages}
}
@inproceedings{FFLRS-fsfma14,
address = {Singapore},
month = may,
year = 2014,
volume = 156,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Lin, Shang{-}Wei and Petrucci, Laure},
acronym = {{FSFMA}'14},
booktitle = {{P}roceedings of the 2nd {F}rench-{S}ingaporean {W}orkshop
on {F}ormal {M}ethods and {A}pplications ({FSFMA}'14)},
author = {Feld, Gilles and Fribourg, Laurent and Labrousse, Denis and
Revol, Bertrand and Soulat, Romain},
title = {Correct-by-design Control Synthesis for Multilevel
Converters using State Space Decomposition},
pages = {5-16},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FFLRS-fsfma14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FFLRS-fsfma14.pdf},
doi = {10.4204/EPTCS.156.5},
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 synthesize a
correct-by-design control that guarantees that the power converter will
always stay within a predefined safe zone of variations for its input
parameters. The method is applied in order to synthesize a
correct-by-design control for 5-level and 7-level power converters with a
flying capacitor topology. We check the validity of our approach by
numerical simulations for 5 and 7 levels. We also perform physical
experimentations using a prototype built by SATIE laboratory for 5
levels}
}
@misc{reachard-30,
author = {Finkel, Alain},
title = {REACHARD~-- Compte-rendu interm{\'e}diaire},
month = feb,
year = {2014},
note = {18~pages},
type = {Contract Report},
howpublished = {Deliverable~D3 Reachard (ANR-11-BS02-001)}
}
@misc{cassting-D62,
author = {Markey, Nicolas and Valette, Sophie},
title = {Annual report for Year~1},
howpublished = {Cassting deliverable~D6.2 (FP7-ICT-601148)},
month = may,
year = {2014},
note = {38~pages},
type = {Contract Report}
}
@misc{cassting-D31,
author = {Markey, Nicolas and Brihaye, {\relax Th}omas and Larsen, Kim G.},
title = {Robustness of collective adaptive systems},
howpublished = {Cassting deliverable~D3.1 (FP7-ICT-601148)},
month = mar,
year = {2014},
note = {17~pages},
type = {Contract Report},
url = {http://www.cassting-project.eu/wp-content/uploads/2014/05/deliv-31.pdf},
pdf = {http://www.cassting-project.eu/wp-content/uploads/2014/05/deliv-31.pdf}
}
@misc{cassting-D24,
author = {Markey, Nicolas and Chaturvedi, Namit and Geeraerts, Gilles
and Srba, Ji{\v{r}}{\'\i}},
title = {Efficient strategy synthesis for complex objectives},
howpublished = {Cassting deliverable~D2.4 (FP7-ICT-601148)},
month = oct,
year = {2014},
note = {20~pages},
type = {Contract Report},
url = {http://www.cassting-project.eu/wp-content/uploads/2014/10/deliv-24.pdf},
pdf = {http://www.cassting-project.eu/wp-content/uploads/2014/10/deliv-24.pdf}
}
@misc{cassting-D14,
author = {Brihaye, {\relax Th}omas and Markey, Nicolas},
title = {Solution concepts for collective adaptive systems},
howpublished = {Cassting deliverable~D1.4 (FP7-ICT-601148)},
month = mar,
year = {2014},
note = {13~pages},
type = {Contract Report},
url = {http://www.cassting-project.eu/wp-content/uploads/2014/05/deliv-14.pdf},
pdf = {http://www.cassting-project.eu/wp-content/uploads/2014/05/deliv-14.pdf}
}
@article{BFCH-compj14,
publisher = {Oxford University Press},
journal = {The Computer Journal},
author = {Beccuti, Marco and Franceschinis, Giuliana and
Codetta{-}Raiteri, Daniele and Haddad, Serge},
title = {Computing Optimal Repair Strategies by Means of NdRFT
Modeling and Analysis},
volume = 57,
number = 12,
month = dec,
year = 2014,
pages = {1870-1892},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFCH-compj14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFCH-compj14.pdf},
doi = {10.1093/comjnl/bxt134},
abstract = {In this paper, the \emph{Non-deterministic Repairable Fault
Tree}~(NdRFT) formalism is proposed: it allows the modeling of failures of
complex systems in addition to their repair processes. Its originality
with respect to other Fault Tree extensions allows us to address repair
strategy optimization problems: in an NdRFT model, the decision as to
whether to start or not a given repair action is non-deterministic, so
that all the possibilities are left open. The formalism is rather
powerful, it allows: the specification of self-revealing events, the
representation of components degradation, the choice among local repair,
global repair, preventive maintenance, and the specification of the
resources needed to start a repair action. The optimal repair strategy
with respect to some relevant system state function, e.g. system
unavailability, can then be computed by solving an optimization problem on
a Markov Decision Process derived from the NdRFT. Such derivation is
obtained by converting the NdRFT model into an intermediate formalism
called Markov Decision Petri Net~(MDPN). In the paper, the NdRFT syntax
and semantics are formally described, together with the conversion rules
to derive from the NdRFT the corresponding MDPN model. The application of
NdRFT is illustrated through examples.}
}
@article{GLS-tods14,
publisher = {ACM Press},
journal = {ACM Transactions on Database Systems},
author = {Gheerbrant, Am{\'e}lie and Libkin, Leonid and Sirangelo, Cristina},
title = {Na{\"\i}ve Evaluation of Queries over Incomplete Databases},
volume = {39},
number = {4:31},
nopages = {},
month = dec,
year = {2014},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLS-tods14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLS-tods14.pdf},
doi = {10.1145/2691190.2691194},
abstract = {The term na{\"\i}ve evaluation refers to evaluating queries over
incomplete databases as if nulls were usual data values, i.e., to using
the standard database query evaluation engine. Since the semantics of
query answering over incomplete databases is that of certain answers, we
would like to know when na{\"\i}ve evaluation computes them: i.e., when
certain answers can be found without inventing new specialized algorithms.
For relational databases it is well known that unions of conjunctive
queries possess this desirable property, and results on preservation of
formulae under homomorphisms tell us that within relational calculus, this
class cannot be extended under the open-world assumption.\par
Our goal here is twofold. First, we develop a general framework that
allows us to determine, for a given semantics of incompleteness, classes
of queries for which na{\"\i}ve evaluation computes certain answers. Second,
we apply this approach to a variety of semantics, showing that for many
classes of queries beyond unions of conjunctive queries, na{\"\i}ve
evaluation makes perfect sense under assumptions different from
open-world. Our key observations are: (1)~na{\"\i}ve evaluation is equivalent
to monotonicity of queries with respect to a semantics-induced ordering,
and (2)~for most reasonable semantics of incompleteness, such monotonicity
is captured by preservation under various types of homomorphisms. Using
these results we find classes of queries for which na{\"\i}ve evaluation
works, e.g., positive first-order formulae for the closed-world semantics.
Even more, we introduce a general relation-based framework for defining
semantics of incompleteness, show how it can be used to capture many known
semantics and to introduce new ones, and describe classes of first-order
queries for which na{\"\i}ve evaluation works under such semantics.}
}
@inproceedings{BC-ccs14,
address = {Scottsdale, Arizona, USA},
month = nov,
year = 2014,
publisher = {ACM Press},
editor = {Ahn, Gail-Joon and Yung, Moti and Li, Ninghui},
acronym = {{CCS}'14},
booktitle = {{P}roceedings of the 21st {ACM} {C}onference
on {C}omputer and {C}ommunications {S}ecurity
({CCS}'14)},
author = {Bana, Gergei and Comon{-}Lundh, Hubert},
title = {A~Computationally Complete Symbolic Attacker for
Equivalence Properties},
pages = {609-620},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-ccs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-ccs14.pdf},
doi = {10.1145/2660267.2660276},
abstract = {We consider the problem of computational indistinguishability of
protocols. We design a symbolic model, amenable to automated deduction,
such that a successful inconsistency proof implies computational
indistinguishability. Conversely, symbolic models of distinguishability
provide clues for likely computational attacks. We follow the idea we
introduced earlier for reachability properties, axiomatizing what an
attacker cannot violate. This results a computationally complete symbolic
attacker, and ensures unconditional computational soundness for the
symbolic analysis. We present a small library of computationally sound,
modular axioms, and test our technique on an example protocol. Despite
additional difficulties stemming from the equivalence properties, the
models and the soundness proofs turn out to be simpler than they were for
reachability properties.}
}
@phdthesis{ponce-phd2014,
author = {Ponce{ }de{~}Le{\'o}n, Hern{\'a}n},
title = {Testing Concurrent Systems Through Event Structures},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2014,
month = nov,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ponce-phd14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ponce-phd14.pdf}
}
@phdthesis{barbot-phd2014,
author = {Barbot, Beno{\^\i}t},
title = {Acceleration for Statistical Model Checking},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2014,
month = nov,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/barbot-phd14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/barbot-phd14.pdf}
}
@phdthesis{sirangelo-HDR14,
author = {Sirangelo, Cristina},
title = {Representing and querying incomplete information: a~data
interoperability perspective},
year = 2014,
month = dec,
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-CS14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-CS14.pdf}
}
@article{LLV-tcs14,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Lange, Martin and Lozes, {\'E}tienne and Vargas{ }Guzm{\'a}n,
Manuel},
title = {Model-checking process equivalences},
volume = {560},
number = {3},
year = {2014},
month = dec,
pages = {326-347},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LLV-tcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LLV-tcs14.pdf},
doi = {10.1016/j.tcs.2014.08.020},
abstract = {Process equivalences are formal methods that relate programs and
systems which, informally, behave in the same way. Since there is no
unique notion of what it means for two dynamic systems to display the same
behaviour there are a multitude of formal process equivalences, ranging
from bisimulation to trace equivalence, categorised in the linear-time
branching-time spectrum.\par
We present a logical framework based on an expressive modal fixpoint logic
which is capable of defining many process equivalence relations: for each
such equivalence there is a fixed formula which is satisfied by a pair of
processes if and only if they are equivalent with respect to this
relation.\par
We explain how to do model checking for this logic in EXPTIME. This allows
model checking technology to be used for process equivalence checking. We
introduce two fragments of the logic for which it is possible to do
model-checking in PTIME and PSPACE respectively, and show that the
formulas that define the process equivalences we consider are in one of
these fragments. This yields a generic proof technique for establishing
the complexities of these process equivalences.\par
Finally, we show how partial evaluation can be used to obtain decision
procedures for process equivalences from the generic model checking
scheme.}
}
@article{BHLM-lmcs14,
journal = {Logical Methods in Computer Science},
author = {Bollig, Benedikt and Habermehl, Peter and Leucker, Martin
and Monmege, Benjamin},
title = {A~Robust Class of Data Languages and an Application to Learning},
year = {2014},
month = dec,
volume = 10,
number = {4:19},
nopages = {},
url = {http://arxiv.org/abs/1411.6646},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHLM-lmcs14.pdf},
doi = {10.2168/LMCS-10(4:19)2014},
abstract = {We~introduce session automata, an automata model to process data
words, i.e., words over an infinite alphabet. Session automata support the
notion of fresh data values, which are well suited for modeling protocols
in which sessions using fresh values are of major interest, like in
security protocols or ad-hoc networks. Session automata have an
expressiveness partly extending, partly reducing that of classical
register automata. We~show that, unlike register automata and their
various extensions, session automata are robust: They (i)~are closed under
intersection, union, and (resource-sensitive) complementation, (ii)~admit
a symbolic regular representation, (iii)~have a decidable inclusion
problem (unlike register automata), and (iv)~enjoy logical
characterizations. Using these results, we establish a learning algorithm
to infer session automata through membership and equivalence queries.}
}
@article{HSS-lmcs14,
journal = {Logical Methods in Computer Science},
author = {Haase, Christoph and Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe},
title = {The Power of Priority Channel Systems},
year = {2014},
month = dec,
volume = 10,
number = {4:4},
nopages = {},
url = {http://arxiv.org/abs/1301.5500},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HSS-lmcs14.pdf},
doi = {10.2168/LMCS-10(4:4)2014},
abstract = {We introduce Priority Channel Systems, a new class of channel
systems where messages carry a numeric priority and where higher-priority
messages can supersede lower-priority messages preceding them in the fifo
communication buffers. The decidability of safety and inevitability
properties is shown via the introduction of a priority embedding, a
well-quasi-ordering that has not previously been used in well-structured
systems. We then show how Priority Channel Systems can compute
Fast-Growing functions and prove that the aforementioned verification
problems are \(\mathbf{F}_{\epsilon_{0}}\)-complete.}
}
@inproceedings{DSS-pods14,
address = {Snowbird, Utah, USA},
month = jun,
year = 2014,
publisher = {ACM Press},
editor = {Hull, Richard and Grohe, Martin},
acronym = {{PODS}'14},
booktitle = {{P}roceedings of the 33rd {A}nnual
{ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium
on {P}rinciples of {D}atabase {S}ystems
({PODS}'14)},
author = {Durand, Arnaud and Schweikardt, Nicole and Segoufin, Luc},
title = {Enumerating answers to first-order queries over databases of low degree},
pages = {121-131},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DSS-pods14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DSS-pods14.pdf},
doi = {10.1145/2594538.2594539},
abstract = {A~class of relational databases has low degree if for
all~\(\delta\), all but finitely many databases in the class have degree
at most~\(n^{\delta}\), where \(n\) is the size of the database. Typical
examples are databases of bounded degree or of degree bounded by
\(\textrm{log} n\).\par
It is known that over a class of databases having low degree, first-order
boolean queries can be checked in pseudo-linear time, i.e. in time bounded
by \(n^{1+\epsilon}\), for all~\(\epsilon\). We~generalise this result by
considering query evaluation.\par
We show that counting the number of answers to a query can be done in
pseudo-linear time and that enumerating the answers to a query can be done
with constant delay after a pseudo-linear time preprocessing.}
}
@inproceedings{segoufin-stacs14,
address = {Lyon, France},
month = mar,
year = 2014,
volume = 25,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Mayr, Ernst W. and Portier, Natacha},
acronym = {{STACS}'14},
booktitle = {{P}roceedings of the 31st {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'14)},
author = {Segoufin, Luc},
title = {A~glimpse on constant delay enumeration},
pages = {13-27},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/segoufin-stacs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/segoufin-stacs14.pdf},
doi = {10.4230/LIPIcs.STACS.2014.13},
abstract = {We survey some of the recent results about enumerating the
answers to queries over a database. We focus on the case where the
enumeration is performed with a constant delay between any two consecutive
solutions, after a linear time preprocessing. This cannot be always
achieved. It requires restricting either the class of queries or the class
of databases. We describe here several scenarios when this is possible.}
}
@inproceedings{ADV-icdt14,
address = {Athens, Greece},
month = mar,
year = 2014,
editor = {Schweikardt, Nicole and Christophides, Vassilis and Leroy, Vincent},
acronym = {{ICDT}'14},
booktitle = {{P}roceedings of the 17th {I}nternational {C}onference on
{D}atabase {T}heory ({ICDT}'14)},
author = {Abiteboul, Serge and Deutch, Daniel and Vianu, Victor},
title = {Deduction with Contradictions in Datalog},
pages = {143-154},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ADV-icdt14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ADV-icdt14.pdf},
doi = {10.5441/002/icdt.2014.17},
abstract = {We study deduction in the presence of inconsistencies. Following
previous works, we capture deduction via datalog programs and
inconsistencies through violations of functional dependencies (FDs). We
study and compare two semantics for datalog with FDs: the first, of a
logical nature, is based on inferring facts one at a time, while never
violating the FDs; the second, of an operational nature, consists in a
fixpoint computation in which maximal sets of facts consistent with the
FDs are inferred at each stage.\par
Both semantics are nondeterministic, yielding sets of possible worlds. We
introduce a PTIME (in the size of the extensional data) algorithm, that
given a datalog program, a set of FDs and an input instance, produces a
c-table representation of the set of possible worlds. Then, we propose to
quantify nondeterminism with probabilities, by means of a probabilistic
semantics. We consider the problem of capturing possible worlds along with
their probabilities via probabilistic c-tables.\par
We then study classical computational problems in this novel context. We
consider the problems of computing the probabilities of answers, of
identifying most likely supports for answers, and of determining the
extensional facts that are most influential for deriving a particular
fact. We show that the interplay of recursion and FDs leads to novel
technical challenges in the context of these problems.}
}
@inproceedings{JLMX-mfps30,
address = {Ithaca, New~York, USA},
month = jun,
year = 2014,
volume = 308,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Jacobs, Bart and Silva, Alexandra and Staton, Sam},
acronym = {{MFPS}'14},
booktitle = {{P}roceedings of the 30th {C}onference on
{M}athematical {F}oundations of {P}rogramming
{S}emantics ({MFPS}'14)},
author = {Jaziri, Samy and Larsen, Kim G. and Mardare, Radu and Xue, Bingtian},
title = {Adequacy and Complete Axiomatization for Timed Modal Logic},
pages = {183-210},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/JLMX-mfps14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JLMX-mfps14.pdf},
doi = {10.1016/j.entcs.2014.10.011},
abstract = {In this paper we develop the metatheory for Timed Modal
Logic~(TML), which is the modal logic used for the analysis of timed
transition systems~(TTSs). We solve a series of long-standing open
problems related to~TML. Firstly, we prove that TML enjoys the
Hennessy-Milner property and solve one of the open questions in the field.
Secondly, we prove that the set of validities are not recursively
enumerable. Nevertheless, we develop a strongly-complete proof system
for~TML. Since the logic is not compact, the proof system contains
infinitary rules, but only with countable sets of instances. Thus, we~can
involve topological results regarding Stone spaces, such as the
Rasiowa-Sikorski lemma, to complete the proofs.}
}
@inproceedings{GLJ-mfps30,
address = {Ithaca, New~York, USA},
month = jun,
year = 2014,
volume = 308,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Jacobs, Bart and Silva, Alexandra and Staton, Sam},
acronym = {{MFPS}'14},
booktitle = {{P}roceedings of the 30th {C}onference on
{M}athematical {F}oundations of {P}rogramming
{S}emantics ({MFPS}'14)},
author = {Goubault{-}Larrecq, Jean and Jung, Achim},
title = {{QRB}, {QFS}, and the Probabilistic Powerdomain},
pages = {167-182},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLJ-mfps14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLJ-mfps14.pdf},
doi = {10.1016/j.entcs.2014.10.010},
abstract = {We show that the first author's QRB-domains coincide with Li and
Xu's QFS-domains, and also with Lawson-compact quasi-continuous dcpos,
with stably-compact locally finitary compact spaces, with sober
QFS-spaces, and with sober QRB-spaces. The first three coincidences were
discovered independently by Lawson and~Xi. The equivalence with sober
QFS-spaces is then applied to give a novel, direct proof that the
probabilistic powerdomain of a QRB-domain is a QRB-domain. This improves
upon a previous, similar result, which was limited to pointed,
second-countable QRB-domains.}
}
@inproceedings{AG-fsttcs14,
address = {New~Dehli, India},
month = dec,
year = 2014,
volume = {29},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Raman, Venkatesh and Suresh, S.~P.},
acronym = {{FSTTCS}'14},
booktitle = {{P}roceedings of the 34th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'14)},
author = {Aiswarya, C. and Gastin, Paul},
title = {Reasoning about distributed systems: {WYSIWYG}},
pages = {11-30},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AG-fsttcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AG-fsttcs14.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2014.11},
abstract = {There are two schools of thought on reasoning about distributed
systems: one~following interleaving based semantics, and one following
partial-order{{\slash}}graph based semantics. This paper compares these two
approaches and argues in favour of the latter. An~introductory treatment
of the split-width technique is also provided.}
}
@article{BFHP-fi14,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {Bernardinello, Luca and Ferigato, Carlo and
Haar, Stefan and Pomello, Lucia},
title = {Closed Sets in Occurrence Nets with Conflicts},
volume = 133,
number = 4,
year = 2014,
pages = {323-344},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHP-fi14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHP-fi14.pdf},
doi = {10.3233/FI-2014-1079},
abstract = {The semantics of concurrent processes can be defined in terms of
partially ordered sets. Occurrence nets, which belong to the family of
Petri nets, model concurrent processes as partially ordered sets of
occurrences of local states and local events. On the basis of the
associated concurrency relation, a closure operator can be defined, giving
rise to a lattice of closed sets. Extending previous results along this
line, the present paper studies occurrence nets with forward conflicts,
modelling families of processes. It is shown that the lattice of closed
sets is orthomodular, and the relations between closed sets and some
particular substructures of an occurrence net are studied. In particular,
the paper deals with runs, modelling concurrent histories, and trails,
corresponding to possible histories of sequential components. A~second
closure operator is then defined by means of an iterative procedure.
The~corresponding closed sets, here called 'dynamically closed', are shown
to form a complete lattice, which in general is not orthocomplemented.
Finally, it is shown that, if an occurrence net satisfies a property
called B-density, which essentially says that any antichain meets any
trail, then the two notions of closed set coincide, and they form a
complete, algebraic orthomodular lattice.}
}
@inproceedings{BHL-fsttcs14,
address = {New~Dehli, India},
month = dec,
year = 2014,
volume = {29},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Raman, Venkatesh and Suresh, S.~P.},
acronym = {{FSTTCS}'14},
booktitle = {{P}roceedings of the 34th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'14)},
author = {Bertrand, Nathalie and Haddad, Serge and Lefaucheux, Engel},
title = {Foundation of Diagnosis and Predictability in Probabilistic
Systems},
pages = {417-429},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHL-fsttcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHL-fsttcs14.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2014.417},
abstract = {In discrete event systems prone to unobservable faults, a
diagnoser must eventually detect fault occurrences. The diagnosability
problem consists in deciding whether such a diagnoser exists. Here we
investigate diagnosis for probabilistic systems modelled by partially
observed Markov chains also called probabilistic labeled transition
systems (pLTS). First we study different specifications of diagnosability
and establish their relations both in finite and infinite pLTS. Then we
analyze the complexity of the diagnosability problem for finite pLTS: we
show that the polynomial time procedure earlier proposed is erroneous and
that in fact for all considered specifications, the problem is
PSPACE-complete. We also establish tight bounds for the size of
diagnosers. Afterwards we consider the dual notion of predictability which
consists in predicting that in a safe run, a fault will eventually occur.
Predictability is an easier problem than diagnosability: it is
NLOGSPACE-complete. Yet the predictor synthesis is as hard as the
diagnoser synthesis. Finally we introduce and study the more flexible
notion of prediagnosability that generalizes predictability and
diagnosability.}
}
@inproceedings{BGK-fsttcs14,
address = {New~Dehli, India},
month = dec,
year = 2014,
volume = {29},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Raman, Venkatesh and Suresh, S.~P.},
acronym = {{FSTTCS}'14},
booktitle = {{P}roceedings of the 34th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'14)},
author = {Bollig, Benedikt and Gastin, Paul and Kumar, Akshay},
title = {Parameterized Communicating Automata: Complementation and
Model Checking},
pages = {625-637},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGK-fsttcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGK-fsttcs14.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2014.625},
abstract = {We study the language-theoretical aspects of parameterized
communicating automata (PCAs), in which processes communicate via
rendez-vous. A given PCA can be run on any topology of bounded degree such
as pipelines, rings, ranked trees, and grids. We show that, under a
context bound, which restricts the local behavior of each process, PCAs
are effectively complementable. Complementability is considered a key
aspect of robust automata models and can, in particular, be exploited for
verification. In this paper, we use it to obtain a characterization of
context-bounded PCAs in terms of monadic second-order (MSO) logic. As the
emptiness problem for context-bounded PCAs is decidable for the classes of
pipelines, rings, and trees, their model-checking problem wrt. MSO
properties also becomes decidable. While previous work on model checking
parameterized systems typically uses temporal logics without next
operator, our MSO logic allows one to express several natural next
modalities.}
}
@inproceedings{CMS-fsttcs14,
address = {New~Dehli, India},
month = dec,
year = 2014,
volume = {29},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Raman, Venkatesh and Suresh, S.~P.},
acronym = {{FSTTCS}'14},
booktitle = {{P}roceedings of the 34th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'14)},
author = {Chadha, Rohit and Mathur, Umang and Schwoon, Stefan},
title = {Computing Information Flow Using Symbolic Model-Checking},
pages = {505-516},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CMS-fsttcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CMS-fsttcs14.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2014.505},
abstract = {Several measures have been proposed in literature for
quantifying the information leaked by the public outputs of a program with
secret inputs. We consider the problem of computing information leaked by
a deterministic or probabilistic program when the measure of information
is based on (a)~min-entropy and (b)~Shannon entropy. The key challenge in
computing these measures is that we need the total number of possible
outputs and, for each possible output, the number of inputs that lead to
it. A direct computation of these quantities is infeasible because of the
state-explosion problem. We therefore propose symbolic algorithms based on
binary decision diagrams (BDDs). The advantage of our approach is that
these symbolic algorithms can be easily implemented in any BDD-based
model-checking tool that checks for reachability in deterministic
non-recursive programs by computing program summaries. We demonstrate the
validity of our approach by implementing these algorithms in a tool
Moped-QLeak, which is built upon Moped, a model checker for Boolean
programs. Finally, we show how this symbolic approach extends to
probabilistic programs.}
}
@inproceedings{DFM-fsttcs14,
address = {New~Dehli, India},
month = dec,
year = 2014,
volume = {29},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Raman, Venkatesh and Suresh, S.~P.},
acronym = {{FSTTCS}'14},
booktitle = {{P}roceedings of the 34th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'14)},
author = {David, Claire and Francis, Nadime and Murlak, Filip},
title = {Consistency of injective tree patterns},
pages = {279-290},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DFM-fsttcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DFM-fsttcs14.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2014.279},
abstract = {Testing if an incomplete description of an XML document is
consistent, that is, if it describes a real document conforming to the
imposed schema, amounts to deciding if a given tree pattern can be matched
injectively into a tree accepted by a fixed automaton. This problem can be
solved in polynomial time for patterns that use the child relation and the
sibling order, but do not use the descendant relation. For general
patterns the problem is in NP, but no lower bound has been known so far.
We show that the problem is NP-complete already for patterns using only
child and descendant relations. The source of hardness turns out to be the
interplay between these relations: for patterns using only descendant we
give a polynomial algorithm. We also show that the algorithm can be
adapted to patterns using descendant and following-sibling, but combining
descendant and next-sibling leads to intractability.}
}
@inproceedings{DJLMS-fsttcs14,
address = {New~Dehli, India},
month = dec,
year = 2014,
volume = {29},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Raman, Venkatesh and Suresh, S.~P.},
acronym = {{FSTTCS}'14},
booktitle = {{P}roceedings of the 34th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'14)},
author = {Doyen, Laurent and Juhl, Line and Larsen, Kim G. and
Markey, Nicolas and Shirmohammadi, Mahsa},
title = {Synchronizing words for weighted and timed automata},
pages = {121-132},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DJLMS-fsttcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DJLMS-fsttcs14.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2014.121},
abstract = {The problem of synchronizing automata is concerned with the
existence of a word that sends all states of the automaton to one and the
same state. This problem has classically been studied for complete
deterministic finite automata, with the existence problem being
NLOGSPACE-complete.\par
In this paper we consider synchronizing-word problems for weighted and
timed automata. We consider the synchronization problem in several
variants and combinations of these, including deterministic and
non-deterministic timed and weighted automata, synchronization to unique
location with possibly different clock valuations or accumulated weights,
as well as synchronization with a safety condition forbidding the
automaton to visit states outside a safety-set during synchronization
(e.g. energy constraints). For deterministic weighted automata, the
synchronization problem is proven PSPACE-complete under energy
constraints, and in 3-EXPSPACE under general safety constraints. For timed
automata the synchronization problems are shown to be PSPACE-complete in
the deterministic case, and undecidable in the non-deterministic case.}
}
@inproceedings{BMS-fsttcs14,
address = {New~Dehli, India},
month = dec,
year = 2014,
volume = {29},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Raman, Venkatesh and Suresh, S.~P.},
acronym = {{FSTTCS}'14},
booktitle = {{P}roceedings of the 34th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'14)},
author = {Bouyer, Patricia and Markey, Nicolas and Stan, Daniel},
title = {Mixed {N}ash Equilibria in Concurrent Games},
pages = {351-363},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-fsttcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-fsttcs14.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2014.351},
abstract = {We study mixed-strategy Nash equilibria in multiplayer
deterministic concurrent games played on graphs, with terminal-reward
payoffs (that is, absorbing states with a value for each player). We show
undecidability of the existence of a constrained Nash equilibrium (the
constraint requiring that one player should have maximal payoff), with
only three players and 0/1-rewards (i.e., reachability objectives). This
has to be compared with the undecidability result by Ummels and Wojtczak
for turn-based games which requires 14 players and general rewards. Our
proof has various interesting consequences: (i)~the~undecidability of the
existence of a Nash equilibrium with a constraint on the social welfare;
(ii)~the~undecidability of the existence of an (unconstrained) Nash
equilibrium in concurrent games with terminal-reward payoffs.}
}
@article{BBBMBGJ-lmcs14,
journal = {Logical Methods in Computer Science},
author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye,
{\relax Th}omas and Menet, Quentin and Baier, Christel and
Gr{\"o}{\ss}er, Marcus and Jurdzi{\'n}ski, Marcin},
title = {Stochastic Timed Automata},
volume = 10,
number = {4:6},
nopages = {},
month = dec,
year = 2014,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBMBGJ-mfcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBMBGJ-mfcs14.pdf},
doi = {10.2168/LMCS-10(4:6)2014},
abstract = {A~stochastic timed automaton is a purely stochastic process
defined on a timed automaton, in which both delays and discrete choices
are made randomly. We study the almost-sure model-checking problem for
this model, that is, given a stochastic timed automaton~\(\mathcal{A}\)
and a property~\(\varphi\), we want to decide whether \(\mathcal{A}\)
satisfies~\(\varphi\) with probability~\(1\). In this paper, we identify
several classes of automata and of properties for which this can be
decided. The proof relies on the construction of a finite abstraction,
called the thick graph, that we interpret as a finite Markov chain, and
for which we can decide the almost-sure model-checking problem.
Correctness of the abstraction holds when automata are almost-surely fair,
which we show, is the case for two large classes of systems, single-clock
automata and so-called weak-reactive automata. Techniques employed in this
article gather tools from real-time verification and probabilistic
verification, as well as topological games played on timed automata.}
}
@article{BCGZ-jal14,
publisher = {Elsevier Science Publishers},
journal = {Journal of Applied Logic},
author = {Bollig, Benedikt and Cyriac, Aiswarya and Gastin, Paul and
Zeitoun, Marc},
title = {Temporal logics for concurrent recursive programs:
Satisfiability and model checking},
volume = 12,
number = 4,
pages = {395-416},
month = dec,
year = 2014,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGZ-jal14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGZ-jal14.pdf},
doi = {10.1016/j.jal.2014.05.001},
abstract = {We develop a general framework for the design of temporal logics
for concurrent recursive programs. A program execution is modeled as a
partial order with multiple nesting relations. To specify properties of
executions, we consider any temporal logic whose modalities are definable
in monadic second-order logic and which, in addition, allows PDL-like path
expressions. This captures, in a unifying framework, a wide range of
logics defined for ranked and unranked trees, nested words, and
Mazurkiewicz traces that have been studied separately. We show that
satisfiability and model checking are decidable in EXPTIME and 2EXPTIME,
depending on the precise path modalities.}
}
@proceedings{KHY-topnoc2014,
editor = {Koutny, Maciej and Haddad, Serge and Yakovlev, Alex},
title = {Transactions on {P}etri Nets and Other Models of Concurrency~{IX}},
booktitle = {Transactions on {P}etri Nets and Other Models of Concurrency~{IX}},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 8910,
year = {2014},
noaddress = {},
url = {http://www.springer.com/978-3-662-45729-0}
}
@incollection{topnoc14-CH,
year = 2014,
volume = {8910},
series = {Lecture Notes in Computer Science},
editor = {Koutny, Maciej and Haddad, Serge and Yakovlev, Alex},
publisher = {Springer},
booktitle = {Transactions on {P}etri Nets and Other Models of Concurrency~{IX}},
author = {Chatain, {\relax Th}omas and Haar, Stefan},
title = {A Canonical Contraction for Safe {P}etri Nets},
pages = {83-98},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/topnoc14-CH.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/topnoc14-CH.pdf},
doi = {10.1007/978-3-662-45730-6_5},
abstract = {Under maximal semantics, the occurrence of an event~\(a\) in a
concurrent run of an occurrence net may imply the occurrence of other
events, not causally related to~\(a\), in the same run. In recent works,
we have formalized this phenomenon as the reveals relation, and used it to
obtain a contraction of sets of events called facets in the context of
occurrence nets. Here, we extend this idea to propose a canonical
contraction of general safe Petri nets into pieces of partial-order
behaviour which can be seen as {"}macro-transitions{"} since all their
events must occur together in maximal semantics. On occurrence nets, our
construction coincides with the facets abstraction. Our contraction
preserves the maximal semantics in the sense that the maximal processes of
the contracted net are in bijection with those of the original net.}
}
@inproceedings{CHJPS-cmsb14,
address = {Manchester, UK},
month = nov,
year = 2014,
volume = {8859},
series = {Lecture Notes in Bioinformatics},
publisher = {Springer-Verlag},
editor = {Mendes, Pedro},
acronym = {{CMSB}'14},
booktitle = {{P}roceedings of the 12th
{C}onference on
{C}omputational {M}ethods in {S}ystem {B}iology
({CMSB}'14)},
author = {Chatain, {\relax Th}omas and Haar, Stefan and Jezequel,
Lo{\"\i}g and Paulev{\'e}, Lo{\"\i}c and Schwoon, Stefan},
title = {Characterization of Reachable Attractors Using {P}etri Net
Unfoldings},
pages = {129-142},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CHJPS-cmsb14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CHJPS-cmsb14.pdf},
doi = {10.1007/978-3-319-12982-2_10},
abstract = {Attractors of network dynamics represent the long-term
behaviours of the modelled system. Their characterization is therefore
crucial for understanding the response and differentiation capabilities of
a dynamical system. In the scope of qualitative models of interaction
networks, the computation of attractors reachable from a given state of
the network faces combinatorial issues due to the state space explosion.
In this paper, we present a new algorithm that exploits the concurrency
between transitions of parallel acting components in order to reduce the
search space. The algorithm relies on Petri net unfoldings that can be
used to compute a compact representation of the dynamics. We illustrate
the applicability of the algorithm with Petri net models of cell
signalling and regulation networks, Boolean and multi-valued. The proposed
approach aims at being complementary to existing methods for deriving the
attractors of Boolean models, while being generic since they apply to any
safe Petri net.}
}
@inproceedings{BHHP-simul14,
address = {Nice, France},
month = oct,
year = 2014,
publisher = {XPS},
editor = {Arisha, Amr and Bobashev, Georgiy},
acronym = {{SIMUL}'14},
booktitle = {{P}roceedings of the 6th {I}nternational {C}onference on {A}dvances in
{S}ystem {S}imulation ({SIMUL}'14)},
author = {Barbot, Beno{\^\i}t and Haddad, Serge and Heiner, Monika
and Picaronny, Claudine},
title = {Rare Event Handling in Signalling Cascades},
pages = {126-131},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHHP-simul14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHHP-simul14.pdf},
abstract = {Signalling cascades are a recurrent pattern of biological
regulatory systems whose analysis has deserved a lot of attention. It has
been shown that stochastic Petri nets are appropriate to model such
systems and evaluate the probabilities of specific properties. Such an
evaluation can be done numerically when the combinatorial state space
explosion is manageable or statistically otherwise. However, when the
probabilities to be evaluated are too small, random simulation requires
more sophisticated techniques for the handling of rare events. In this
paper, we show how such involved methods can be successfully applied for
signalling cascades. More precisely, we study three relevant properties of
a signalling cascade with the help of the Cosmos tool. Our experiments
point out interesting dependencies between quantitative parameters of the
regulatory system and its transient behaviour. In addition, they
demonstrate that we can go beyond the capabilities of Marcie which
provides one of the most efficient numerical solvers.}
}
@inproceedings{DDS-rp14,
address = {Oxford, UK},
month = sep,
year = 2014,
volume = {8762},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell, James},
acronym = {{RP}'14},
booktitle = {{P}roceedings of the 8th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'14)},
author = {Demri, St{\'e}phane and Dhar, Amit Kumar and Sangnier, Arnaud},
title = {Equivalence Between Model-Checking Flat Counter Systems and
{P}resburger Arithmetic},
pages = {85-97},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-rp14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-rp14.pdf},
doi = {10.1007/978-3-319-11439-2_7},
abstract = {We show that model-checking flat counter systems over
CTL\textsuperscript{*} (with arithmetical constraints on counter values)
has the same complexity as the satisfiability problem for Presburger
arithmetic. The lower bound already holds with the temporal operator EF
only, no~arithmetical constraints in the logical language and with guards
on transitions made of simple linear constraints. This complements our
understanding of model-checking flat counter systems with linear-time
temporal logics, such as LTL for which the problem is already known to be
(only) NP-complete with guards restricted to the linear fragment.}
}
@proceedings{DKW-ijcar2014,
editor = {Demri, St{\'e}phane and Kapur, Deepak and Weidenbach, Christoph},
title = {{P}roceedings of the 7th
{I}nternational {J}oint {C}onference on {A}utomated {R}easoning
({IJCAR}'14)},
booktitle = {{P}roceedings of the 7th
{I}nternational {J}oint {C}onference on {A}utomated {R}easoning
({IJCAR}'14)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 8562,
year = {2014},
month = jul,
address = {Vienna, Austria},
url = {http://www.springer.com/978-3-319-08586-9}
}
@article{CD-interstices14,
publisher = {INRIA},
journal = {Interstices},
author = {Chr{\'e}tien, R{\'e}my and Delaune, St{\'e}phanie},
title = {Le~bitcoin, une monnaie \(100\%\) num{\'e}rique},
month = sep,
year = {2014},
url = {https://interstices.info/jcms/ni_78681/le-bitcoin-une-monnaie-100-numerique},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-interstices14.pdf}
}
@inproceedings{CDR-tgc14,
address = {Rome, Italy},
month = dec,
year = 2014,
volume = {8902},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Maffei, Matteo and Tuosto, Emilio},
acronym = {{TGC}'14},
booktitle = {{R}evised {S}elected {P}apers of the 9th {S}ymposium on {T}rustworthy {G}lobal
{C}omputing ({TGC}'14)},
author = {Cheval, Vincent and Delaune, St{\'e}phanie and Ryan, Mark
D.},
title = {Tests for establishing security properties},
pages = {82-96},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDR-tgc14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDR-tgc14.pdf},
doi = {10.1007/978-3-662-45917-1_6},
abstract = {Ensuring strong security properties in some cases requires
participants to carry out tests during the execution of a protocol.
A~classical example is electronic voting: participants are required to
verify the presence of their ballots on a bulletin board, and to verify
the computation of the election outcome. The notion of certificate
transparency is another example, in which participants in the protocol are
required to perform tests to verify the integrity of a certificate log.\par
We present a framework for modelling systems with such `testable
properties', using the applied pi calculus. We model the tests that are
made by participants in order to obtain the security properties.
Underlying our work is an attacker model called {"}malicious but cautious{"},
which lies in between the Dolev-Yao model and the {"}honest but curious{"}
model. The malicious-but-cautious model is appropriate for cloud computing
providers that are potentially malicious but are assumed to be cautious
about launching attacks that might cause user tests to fail.}
}
@inproceedings{schmitz-rp14,
address = {Oxford, UK},
month = sep,
year = 2014,
volume = {8762},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell, James},
acronym = {{RP}'14},
booktitle = {{P}roceedings of the 8th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'14)},
author = {Schmitz, Sylvain},
title = {Complexity Bounds for Ordinal-Based Termination},
pages = {1-19},
url = {http://arxiv.org/abs/1407.5896},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/schmitz-rp14.pdf},
doi = {10.1007/978-3-319-11439-2_1},
abstract = {`What more than its truth do we know if we have a proof of a
theorem in a given formal system?' We examine Kreisel's question in the
particular context of program termination proofs, with an eye to deriving
complexity bounds on program running times.\par
Our main tool for this are length function theorems, which provide
complexity bounds on the use of well quasi orders. We illustrate how to
prove such theorems in the simple yet until now untreated case of
ordinals. We show how to apply this new theorem to derive complexity
bounds on programs when they are proven to terminate thanks to a ranking
function into some ordinal.}
}
@inproceedings{GLS-pp14,
year = 2014,
volume = 8464,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {van Breugel, Franck and Kashefi, Elham and Palamidessi,
Catuscia and Rutten, Jan},
booktitle = {Horizons of the Mind. A~Tribute to Prakash Panangaden},
author = {Goubault{-}Larrecq, Jean and Segala, Roberto},
title = {Random Measurable Selections},
pages = {343-362},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLS-pp14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLS-pp14.pdf},
doi = {10.1007/978-3-319-06880-0_18},
abstract = {We make the first steps towards showing a general {"}randomness
for free{"} theorem for stochastic automata. The goal of such theorems is
to replace randomized schedulers by averages of pure schedulers. Here, we
explore the case of measurable multifunctions and their measurable
selections. This involves constructing probability measures on the
measurable space of measurable selections of a given measurable
multifunction, which seems to be a fairly novel problem. We then extend
this to the case of IT automata, namely, non-deterministic (infinite)
automata with a history-dependent transition relation. Throughout, we
strive to make our assumptions minimal.}
}
@inproceedings{BGS-rp14,
address = {Oxford, UK},
month = sep,
year = 2014,
volume = {8762},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell, James},
acronym = {{RP}'14},
booktitle = {{P}roceedings of the 8th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'14)},
author = {Bollig, Benedikt and Gastin, Paul and Schubert, Jana},
title = {Parameterized Verification of Communicating Automata under Context Bounds},
pages = {45-57},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGS-rp14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGS-rp14.pdf},
doi = {10.1007/978-3-319-11439-2_4},
abstract = {We study the verification problem for parameterized
communicating automata~(PCA), in which processes synchronize via message
passing. A~given PCA can be run on any topology of bounded degree (such as
pipelines, rings, or ranked trees), and communication may take place
between any two processes that are adjacent in the topology. Parameterized
verification asks if there is a topology from a given topology class that
allows for an accepting run of the given PCA. In general, this problem is
undecidable even for synchronous communication and simple pipeline
topologies. We therefore consider context-bounded verification, which
restricts the behavior of each single process. For several variants of
context bounds, we show that parameterized verification over pipelines,
rings, and ranked trees is decidable. Our approach is automata-theoretic
and uniform. We introduce a notion of graph acceptor that identifies those
topologies allowing for an accepting run. Depending on the given topology
class, the topology acceptor can then be restricted, or adjusted, so that
the verification problem reduces to checking emptiness of finite automata
or tree automata.}
}
@inproceedings{HM-rp14,
address = {Oxford, UK},
month = sep,
year = 2014,
volume = {8762},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell, James},
acronym = {{RP}'14},
booktitle = {{P}roceedings of the 8th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'14)},
author = {Haddad, Serge and Monmege, Benjamin},
title = {Reachability in {MDP}s: Refining Convergence of Value Iteration},
pages = {125-137},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2014-07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2014-07.pdf},
doi = {10.1007/978-3-319-11439-2_10},
abstract = {Markov Decision Processes (MDP) are a widely used model
including both non-deterministic and probabilistic choices. Minimal and
maximal probabilities to reach a target set of states, with respect to a
policy resolving non-determinism, may be computed by several methods
including value iteration. This algorithm, easy to implement and efficient
in terms of space complexity, consists in iteratively finding the
probabilities of paths of increasing length. However, it raises three
issues: (1)~defining a stopping criterion ensuring a bound on the
approximation, (2)~analyzing the rate of convergence, and (3)~specifying
an additional procedure to obtain the exact values once a sufficient
number of iterations has been performed. The first two issues are still
open and for the third one a {"}crude{"} upper bound on the number of
iterations has been proposed. Based on a graph analysis and transformation
of MDPs, we address these problems. First we introduce an interval
iteration algorithm, for which the stopping criterion is straightforward.
Then we exhibit convergence rate. Finally we significantly improve the
bound on the number of iterations required to get the exact values.}
}
@inproceedings{LS-rp14,
address = {Oxford, UK},
month = sep,
year = 2014,
volume = {8762},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell, James},
acronym = {{RP}'14},
booktitle = {{P}roceedings of the 8th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'14)},
author = {Leroux, J{\'e}r{\^o}me and Schnoebelen, {\relax Ph}ilippe},
title = {On Functions Weakly Computable by {P}etri Nets and Vector
Addition Systems},
pages = {190-202},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-rp14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-rp14.pdf},
doi = { 10.1007/978-3-319-11439-2_15},
abstract = {We show that any unbounded function weakly computable by a Petri
net or a VASS cannot be sublinear. This answers a long-standing folklore
conjecture about weakly computing the inverses of some fast-growing
functions. The proof relies on a pumping lemma for sets of runs in Petri
nets or VASSes.}
}
@inproceedings{HH-rp14,
address = {Oxford, UK},
month = sep,
year = 2014,
volume = {8762},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell, James},
acronym = {{RP}'14},
booktitle = {{P}roceedings of the 8th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'14)},
author = {Haase, Christoph and Halfon, Simon},
title = {Integer Vector Addition Systems with States},
pages = {112-124},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HH-rp14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HH-rp14.pdf},
doi = {10.1007/978-3-319-11439-2_9},
abstract = {This paper studies reachability, coverability and
inclusion problems for Integer Vector Addition
Systems with States (\(\mathbb{Z}\)-VASS) and
extensions and restrictions
thereof. A~\(\mathbb{Z}\)-VASS comprises a
finite-state controller with a finite number of
counters ranging over the integers. Although it is
folklore that reachability in \(\mathbb{Z}\)-VASS is
NP-complete, it turns out that despite their
naturalness, from a complexity point of view this
class has received little attention in the
literature. We fill this gap by providing an
in-depth analysis of the computational complexity of
the aforementioned decision problems. Most
interestingly, it turns out that while the addition
of reset operations to ordinary VASS leads to
undecidability and Ackermann-hardness of
reachability and coverability, respectively, they
can be added to \(\mathbb{Z}\)-VASS while retaining
NP-completeness of both coverability and
reachability.}
}
@article{PHL-stvr14,
publisher = {John Wiley \& Sons, Ltd.},
journal = {Software Testing, Verification and Reliability},
author = {Ponce{ }de{~}Le{\'o}n, Hern{\'a}n and Haar, Stefan and
Longuet, Delphine},
title = {Model-Based Testing for Concurrent Systems with Labeled Event
Structures},
volume = 24,
number = 7,
year = {2014},
month = nov,
pages = {558-590},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-stvr14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-stvr14.pdf},
doi = {10.1002/stvr.1543},
abstract = {We propose a theoretical testing framework and a test generation
algorithm for concurrent systems specified with true concurrency models,
such as Petri nets or networks of automata. The semantic model of
computation of such formalisms are labeled event structures, which allow
to represent concurrency explicitly. We introduce the notions of strong
and weak concurrency: strongly concurrent events must be concurrent in the
implementation, while weakly concurrent ones may eventually be ordered.
The ioco type conformance relations for sequential systems rely on the
observation of sequences of actions and blockings, thus they are not
capable of capturing and exploiting concurrency of non sequential
behaviors. We propose an extension of \textbf{ioco} for labeled event
structures, named \textbf{co-ioco}, allowing to deal with strong and weak
concurrency. We~extend the notions of test cases and test execution to
labeled event structures, and give a test generation algorithm building a
complete test suite for \textbf{co-ioco}.}
}
@inproceedings{BMP-dx14,
address = {Graz, Austria},
month = sep,
year = 2014,
editor = {Abreu, Rui and Pill, Ingo and Wotawa, Franz},
acronym = {{DX}'14},
booktitle = {{P}roceedings of the 25th {I}nternational {W}orkshop on
{P}rinciples of {D}iagnosis ({DX}'14)},
author = {Brand{\'a}n{ }Briones, Laura and Madalinski, Agnes and Ponce{ }de{~}Le{\'o}n, Hern{\'a}n},
title = {Distributed Diagnosability Analysis with {P}etri Nets},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMP-dx14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMP-dx14.pdf},
abstract = {We propose a framework to distributed diagnosability analysis of
concurrent systems modeled with Petri nets as a collection of components
synchronizing on common observable transitions, where faults can occur in
several components. The diagnosability analysis of the entire system is
done in parallel by verifying the interaction of each component with the
fault free versions of the other components. Furthermore, we use existing
efficient methods and tools, in particular parallel LTL-X model checking
based on unfoldings, for diagnosability verification.}
}
@article{EM-integers14,
journal = {INTEGERS -- Electronic Journal of Combinatorial Number Theory},
author = {Elias, Yara and McKenzie, Pierre},
title = {On Generalized Addition Chains},
volume = 14,
number = {A16},
nopages = {},
year = 2014,
month = mar,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/EM-integers14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/EM-integers14.pdf},
abstract = {Given integers \(d \geq 1\), and \(g \geq 2\),
a~\(g\)-addition chain for~\(d\) is a sequence of
integers \(a_0 = 1\), \(a_1\), \(a_2\), ... ,
\(a_{r-1}\), \(a_r = d\) where \(a_i = a_{j_{1}} +
a_{j_{2}} + \cdots + a_{j_{k}}\), with \(2 \leq k
\leq g\), and \(0 \leq j_1 \leq j_2 \cdots j_k \leq
i-1\). The length of a \(g\)-addition chain
is~\(r\), the number of terms following~\(1\) in the
sequence. We denote by~\(l_{g}(d)\) the length of a
shortest addition chain for~\(d\). Many results have
been established in the case \(g = 2\). Our aim is
to establish the same sort of results for arbitrary
fixed~\(g\). In~particular, we adapt methods for
constructing \(g\)-addition chains when \(g = 2\) to
the case \(g > 2\) and we study the asymptotic
behavior of~\(l_g\).}
}
@inproceedings{CKM-ncma14,
address = {Kassel, Germany},
month = jul,
year = 2014,
volume = 304,
series = {books@ocg.at},
publisher = {Austrian Computer Society},
editor = {Bensch, Suna and Freund, Rudolf and Otto, Friedrich},
acronym = {{NCMA}'14},
booktitle = {{P}roceedings of the 6th {W}orkshop on {N}on-{C}lassical {M}odels
of {A}utomata and {A}pplications ({NCMA}'14)},
author = {Cadilhac, Micha{\"e}l and Krebs, Andreas and McKenzie, Pierre},
title = {Extremely uniform branching programs},
pages = {73-83},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CKM-ncma14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CKM-ncma14.pdf},
abstract = {We propose a new descriptive complexity notion of
uniformity for branching programs solving problems
defined on structured data. We observe that
FO[=]-uniform (\(n\)-way) branching programs are
unable to solve the tree evaluation problem studied
by Cook, McKenzie, Wehr, Braverman and Santhanam
because such programs possess a variant of their
thriftiness property. Similarly, FO[=]-uniform
(\(n\)-way) branching programs are unable to solve
the P-complete GEN problem because such programs
possess the incremental property studied by G{\'a}l,
Kouck{\'y} and McKenzie.}
}
@inproceedings{AGN-atva14,
address = {Sydney, Australia},
month = nov,
year = {2014},
volume = 8837,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cassez, Franck and Raskin, Jean-Fran{\c{c}}ois},
acronym = {{ATVA}'14},
booktitle = {{P}roceedings of the 12th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'14)},
author = {Aiswarya, C. and Gastin, Paul and Narayan Kumar, K.},
title = {Verifying Communicating Multi-pushdown Systems via Split-width},
pages = {1-17},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGN-atva14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGN-atva14.pdf},
doi = {10.1007/978-3-319-11936-6_1},
abstract = {Communicating multi-pushdown systems model networks of
multi-threaded recursive programs communicating via reliable FIFO
channels. We extend the notion of split-width to this setting, improving
and simplifying the earlier definition. Split-width, while having the same
power of clique-{{\slash}}tree-width, gives a divide-and-conquer technique
to prove the bound of a class, thanks to the two basic operations, shuffle
and merge, of the split-width algebra. We illustrate this technique on
examples. We also obtain simple, uniform and optimal decision procedures
for various verification problems parametrised by split-width.}
}
@article{FKS-fmsd14,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Fribourg, Laurent and K{\"u}hne, Ulrich and Soulat, Romain},
title = {Finite Controlled Invariants for Sampled Switched Systems},
year = 2014,
month = dec,
volume = 45,
number = 3,
pages = {303-329},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FKS-fmsd14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FKS-fmsd14.pdf},
doi = {10.1007/s10703-014-0211-2},
abstract = {We consider in this paper switched systems, a class of hybrid
systems recently used with success in various domains such as automotive
industry and power electronics. We propose a state-dependent control
strategy which makes the trajectories of the analyzed system converge to
finite cyclic sequences of points. Our method relies on a technique of
decomposition of the state space into local regions where the control is
uniform. We have implemented the procedure using zonotopes, and applied it
successfully to several examples of the literature and industrial case
studies in power electronics.}
}
@inproceedings{SLAF-syncop14,
address = {Grenoble, France},
volume = 145,
series = {Electronic Proceedings in Theoretical Computer Science},
month = apr,
year = 2014,
editor = {Andr{\'e}, {\'E}tienne and Frehse, Goran},
acronym = {{SYNCOP}'14},
booktitle = {{P}roceedings of the 1st {I}nternational {W}orkshop on {S}ynthesis
of {C}ontinuous {P}arameters ({SYNCOP}'14)},
author = {Sun, Youcheng and Lipari, Giuseppe and
Andr{\'e}, {\'E}tienne and Fribourg, Laurent},
title = {Toward Parametric Timed Interfaces for Real-Time Components},
pages = {49-64},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SLAF-syncop14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SLAF-syncop14.pdf},
doi = {10.4204/EPTCS.145.6},
abstract = {We propose here a framework to model real-time components
consisting of concurrent real-time tasks running on a single processor,
using parametric timed automata. Our framework is generic and modular, so
as to be easily adapted to different schedulers and more complex task
models. We first perform a parametric schedulability analysis of the
components using the inverse method. We show that the method unfortunately
does not provide satisfactory results when the task periods are considered
as parameters. After identifying and explaining the problem, we present a
solution adapting the model by making use of the worst-case scenario in
schedulability analysis. We show that the analysis with the inverse method
always converges on the modified model when the system load is strictly
less than~\(100\%\). Finally, we show how to use our parametric analysis for
the generation of timed interfaces in compositional system design.}
}
@inproceedings{BGM-atva14,
address = {Sydney, Australia},
month = nov,
year = {2014},
volume = 8837,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cassez, Franck and Raskin, Jean-Fran{\c{c}}ois},
acronym = {{ATVA}'14},
booktitle = {{P}roceedings of the 12th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'14)},
author = {Bouyer, Patricia and Gardy, Patrick and Markey, Nicolas},
title = {Quantitative verification of weighted {K}ripke structures},
pages = {64-80},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-atva14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-atva14.pdf},
doi = {10.1007/978-3-319-11936-6_6},
abstract = {Extending formal verification techniques to handle quantitative
aspects, both for the models and for the properties to be checked, has
become a central research topic over the last twenty years. Following
several recent works, we study model checking for (one-dimensional)
weighted Kripke structures with positive and negative weights, and
temporal logics constraining the total and/or average weight. We prove
decidability when only accumulated weight is constrained, while allowing
average-weight constraints alone already is undecidable.}
}
@inproceedings{MV-atva14,
address = {Sydney, Australia},
month = nov,
year = {2014},
volume = 8837,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cassez, Franck and Raskin, Jean-Fran{\c{c}}ois},
acronym = {{ATVA}'14},
booktitle = {{P}roceedings of the 12th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'14)},
author = {Markey, Nicolas and Vester, Steen},
title = {Symmetry Reduction in Infinite Games with Finite Branching},
pages = {281-296},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/MV-atva14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/MV-atva14.pdf},
doi = {10.1007/978-3-319-11936-6_21},
abstract = {Symmetry reductions have been applied extensively for the
verification of finite-state concurrent systems and hardware designs using
model-checking of temporal logics such as LTL, CTL and
CTL\textsuperscript{*}, as well as real-time and probabilistic-system
model-checking. In this paper we extend the technique to handle
infinite-state games on graphs with finite branching where the objectives
of the players can be very general. As particular applications, it is
shown that the technique can be applied to reduce the state space in
parity games as well as when doing model-checking of the temporal logic
ATL\textsuperscript{*}.}
}
@article{ADK-lmcs14,
journal = {Logical Methods in Computer Science},
author = {Arapinis, Myrto and Delaune, St{\'e}phanie and Kremer, Steve},
title = {Dynamic Tags for Security Protocols},
volume = 10,
number = {2:11},
nopages = {},
month = jun,
year = 2014,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ADK-lmcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ADK-lmcs14.pdf},
doi = {10.2168/LMCS-10(2:11)2014},
abstract = {The design and verification of cryptographic protocols is a
notoriously difficult task, even in symbolic models which take an abstract
view of cryptography. This is mainly due to the fact that protocols may
interact with an arbitrary attacker which yields a verification problem
that has several sources of unboundedness (size of messages, number of
sessions, etc. In this paper, we characterize a class of protocols for
which deciding security for an unbounded number of sessions is decidable.
More precisely, we present a simple transformation which maps a protocol
that is secure for a bounded number of protocol sessions (a~decidable
problem) to a protocol that is secure for an unbounded number of sessions.
The precise number of sessions that need to be considered is a function of
the security property and we show that for several classical security
properties a single session is sufficient. Therefore, in many cases our
results yields a design strategy for security protocols: (i)~design a
protocol intended to be secure for a {single session}; and (ii)~apply our
transformation to obtain a protocol which is secure for an unbounded
number of sessions.}
}
@article{FL-is14,
publisher = {Springer},
journal = {Informatik Spektrum},
author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me},
title = {Neue, einfache {A}lgorithmen f{\"u}r {P}etrinetze},
volume = 37,
number = {3},
month = jun,
year = 2014,
pages = {229-236},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FL-is14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FL-is14.pdf},
doi = {10.1007/s00287-013-0753-5},
abstract = {Wir zeigen, wie die Entscheidungsprobleme der {\"U}berdeckung,
der Beschr{\"a}nktheit und der Erreichbarkeit mithilfe induktiver
Invarianten einfacher l{\"o}sbar sind als mit herk{\"o}mmlichen
Methoden}
}
@article{CD-tocl14,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Chatterjee, Krishnendu and Doyen, Laurent},
title = {Partial-Observation Stochastic Games: How to Win when Belief Fails},
volume = 15,
number = {2:16},
month = apr,
year = 2014,
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-tocl14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-tocl14.pdf},
doi = {10.1145/2579819},
abstract = {In two-player finite-state stochastic games of partial
observation on graphs, in every state of the graph,
the players simultaneously choose an action, and
their joint actions determine a probability
distribution over the successor states. The game is
played for infinitely many rounds and thus the
players construct an infinite path in the graph. We
consider 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 to 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, (a)~the players may not be allowed to
use randomization (pure strategies), or (b)~they may
choose a probability distribution over actions but
the actual random choice is external and not visible
to the player (actions invisible), or (c)~they may
use full randomization.\par
Our main results for pure strategies are as follows:
(1)~For one-sided games with player~2 having perfect
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
and present symbolic algorithms that avoid the
explicit exponential construction. (2)~For one-sided
games with player~1 having perfect observation we
show that non-elementary memory is both necessary
and sufficient for both almost-sure and positive
win- ning 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. We establish the equivalence of the
almost-sure winning problems for pure strategies and
for randomized strategies with actions
invisible. Our equivalence result exhibit 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.}
}
@inproceedings{CS-mfcs14,
address = {Budapest, Hungary},
month = aug,
year = 2014,
volume = {8634},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {{\'E}sik, Zolt{\'a}n and Csuhaj{-}Varj{\'u}, Erzs{\'e}bet and
Dietzfelbinger, Martin},
acronym = {{MFCS}'14},
booktitle = {{P}roceedings of the 39th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'14)~-- {P}art~{I}},
author = {Courtois, Jean-Baptiste and Schmitz, Sylvain},
title = {Alternating Vector Addition Systems with States},
pages = {220-231},
url = {http://hal.inria.fr/hal-00980878},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-mfcs14.pdf},
doi = {10.1007/978-3-662-44522-8_19},
abstract = {Alternating vector addition systems are obtained by equipping
vector addition systems with states (VASS) with 'fork' rules, and provide
a natural setting for infinite-arena games played over a VASS. Initially
introduced in the study of propositional linear logic, they have more
recently gathered attention in the guise of \emph{multi-dimensional
energy} games for quantitative verification and synthesis.\par
We show that establishing who is the winner in such a game with a state
reachability objective is 2-ExpTime-complete. As a further application, we
show that the same complexity result applies to the problem of whether a
VASS is simulated by a finite-state system.}
}
@inproceedings{CGK-concur14,
address = {Rome, Italy},
month = sep,
year = 2014,
volume = 8704,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baldan, Paolo and Gorla, Daniele},
acronym = {{CONCUR}'14},
booktitle = {{P}roceedings of the 25th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'14)},
author = {Cyriac, Aiswarya and Gastin, Paul and Narayan Kumar, K.},
title = {Controllers for the Verification of Communicating Multi-Pushdown Systems},
pages = {297-311},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CGK-concur14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CGK-concur14.pdf},
doi = {10.1007/978-3-662-44584-6_21},
abstract = {Multi-pushdowns communicating via queues are formal models of
multi-threaded programs communicating via channels. They are turing
powerful and much of the work on their verification has focussed on
under-approximation techniques. Any error detected in the
under-approximation implies an error in the system. However the successful
verification of the under-approximation is not as useful if the system
exhibits unverified behaviours. Our aim is to design controllers that
observe/restrict the system so that it stays within the verified
under-approximation. We identify some important properties that a good
controller should satisfy. We consider an extensive under-approximation
class, construct a distributed controller with the desired properties and
also establish the decidability of verification problems for this class.}
}
@inproceedings{CCD-concur14,
address = {Rome, Italy},
month = sep,
year = 2014,
volume = 8704,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baldan, Paolo and Gorla, Daniele},
acronym = {{CONCUR}'14},
booktitle = {{P}roceedings of the 25th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'14)},
author = {Chr{\'e}tien, R{\'e}my and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
title = {Typing messages for free in security protocols:
the~case of equivalence properties},
pages = {372-386},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-concur14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-concur14.pdf},
doi = {10.1007/978-3-662-44584-6_26},
abstract = {Privacy properties such as untraceability, vote secrecy, or
anonymity are typically expressed as behavioural equivalence in a process
algebra that models security protocols. In this paper, we study how to
decide one particular relation, namely trace equivalence, for an unbounded
number of sessions.\par
Our first main contribution is to reduce the search space for attacks.
Specifically, we show that if there is an attack then there is one that is
well-typed. Our result holds for a large class of typing systems and a
large class of determinate security protocols. Assuming finitely many
nonces and keys, we can derive from this result that trace equivalence is
decidable for an unbounded number of sessions for a class of tagged
protocols, yielding one of the first decidability results for the
unbounded case. As an intermediate result, we also provide a novel
decision procedure in the case of a bounded number of sessions.}
}
@inproceedings{DMS-concur14,
address = {Rome, Italy},
month = sep,
year = 2014,
volume = 8704,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baldan, Paolo and Gorla, Daniele},
acronym = {{CONCUR}'14},
booktitle = {{P}roceedings of the 25th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'14)},
author = {Doyen, Laurent and Massart, {\relax Th}ierry and Shirmohammadi, Mahsa},
title = {Robust Synchronization in {M}arkov Decision Processes},
pages = {234-248},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DMS-concur14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DMS-concur14.pdf},
doi = {10.1007/978-3-662-44584-6_17},
abstract = {We consider synchronizing properties of Markov decision
processes (MDP), viewed as generators of sequences of probability
distributions over states. A~probability distribution is \(p\)-synchronizing
if the probability mass is at least~\(p\) in some state, and a sequence of
probability distributions is weakly \(p\)-synchronizing, or strongly
\(p\)-synchronizing if respectively infinitely many, or all but finitely many
distributions in the sequence are \(p\)-synchronizing.\par
For each synchronizing mode, an MDP can be \textit{(i)}~sure winning if
there is a strategy that produces a \(1\)-synchronizing sequence;
\textit{(ii)}~almost-sure winning if there is a strategy that produces a
sequence that is, for all \(\epsilon>0\), a \((1-\epsilon)\)-synchronizing
sequence; \textit{(iii)}~limit-sure winning if for all \(\epsilon>0\),
there is a strategy that produces a \((1-\epsilon)\)-synchronizing
sequence.\par
For each synchronizing and winning mode, we consider the problem of
deciding whether an MDP is winning, and we establish matching upper and
lower complexity bounds of the problems, as well as the optimal memory
requirement for winning strategies: \textit{(a)}~for all winning modes, we
show that the problems are PSPACE-complete for weakly synchronizing, and
PTIME-complete for strongly synchronizing; \textit{(b)}~we~show that for
weakly synchronizing, exponential memory is sufficient and may be
necessary for sure winning, and infinite memory is necessary for
almost-sure winning; for strongly synchronizing, linear-size memory is
sufficient and may be necessary in all modes; \textit{(c)}~we~show a
robustness result that the almost-sure and limit-sure winning modes
coincide for both weakly and strongly synchronizing.}
}
@inproceedings{BMM-concur14,
address = {Rome, Italy},
month = sep,
year = 2014,
volume = 8704,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baldan, Paolo and Gorla, Daniele},
acronym = {{CONCUR}'14},
booktitle = {{P}roceedings of the 25th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'14)},
author = {Bouyer, Patricia and Markey, Nicolas and Matteplackel,
Raj~Mohan},
title = {Averaging in~{LTL}},
pages = {266-280},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMM-concur14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMM-concur14.pdf},
doi = {10.1007/978-3-662-44584-6_19},
abstract = {For the accurate analysis of computerized systems, powerful
quantitative formalisms have been designed, together with efficient
verification algorithms. However, verification has mostly remained
boolean---either a property is~true, or it~is false. We~believe that this
is too crude in a context where quantitative information and constraints
are crucial: correctness should be quantified!\par In a recent line of
works, several authors have proposed quantitative semantics for temporal
logics, using e.g. \emph{discounting} modalities (which give less
importance to distant events). In~the present paper, we define and study a
quantitative semantics of~LTL with \emph{averaging} modalities, either on
the long run or within an until modality. This, in a way, relaxes the
classical Boolean semantics of~LTL, and provides a measure of certain
properties of a model. We~prove that computing and even approximating the
value of a formula in this logic is undecidable.}
}
@inproceedings{PHL-ictac14,
address = {Bucharest, Romania},
month = sep,
year = 2014,
volume = 8687,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ciobanu, Gabriel and M{\'e}ry, Dominique},
acronym = {{ICTAC}'14},
booktitle = {{P}roceedings of the 11th {I}nternational {C}olloquium on
{T}heoretical {A}spects of {C}omputing ({ICTAC}'14)},
author = {Ponce{ }de{~}Le{\'o}n, Hern{\'a}n and Haar, Stefan and
Longuet, Delphine},
title = {Distributed testing of concurrent systems: vector clocks to
the rescue},
pages = {369-387},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-ictac14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-ictac14.pdf},
doi = {10.1007/978-3-319-10882-7_22},
abstract = {The ioco relation has become a standard in model-based
conformance testing. The co-ioco conformance relation is an extension of
this relation to concurrent systems specified with true-concurrency
models. This relation assumes a global control and observation of the
system under test, which is not usually realistic in the case of
physically distributed systems. Such systems can be partially observed at
each of their points of control and observation by the sequences of inputs
and outputs exchanged with their environment. Unfortunately, in general,
global observation cannot be reconstructed from local ones, so global
conformance cannot be decided with local tests. We propose to append time
stamps to the observable actions of the system under test in order to
regain global conformance from local testing.}
}
@inproceedings{KS-dcfs2014,
address = {Turku, Finland},
month = aug,
year = 2014,
volume = {8614},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {J{\"u}rgensen, Helmut and Karhum{\"a}ki, Juhani and Okhotin, Alexander},
acronym = {{DCFS}'14},
booktitle = {{P}roceedings of the 16th {W}orkshop on {D}escriptional
{C}omplexity of {F}ormal {S}ystems ({DCFS}'14)},
author = {Karandikar, Prateek and Schnoebelen, {\relax Ph}ilippe},
title = {On the state complexity of closures and interiors of regular
languages with subwords},
pages = {234-245},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-dcfs2014.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-dcfs2014.pdf},
doi = {10.1007/978-3-319-09704-6_21},
abstract = {We study the state complexity of the set of subwords and
superwords of regular languages, and provide new lower bounds in the case
of languages over a two-letter alphabet. We also consider the dual
interior sets, for which the nondeterministic state complexity has a
doubly-exponential upper bound. We prove a matching doubly-exponential
lower bound for downward interiors in the case of an unbounded alphabet.}
}
@inproceedings{KH-acsd14,
address = {Tunis, Tunisia},
month = jun,
year = 2014,
publisher = {{IEEE} Computer Society Press},
acronym = {{ACSD}'14},
booktitle = {{P}roceedings of the 14th {I}nternational
{C}onference on {A}pplication of {C}oncurrency
to {S}ystem {D}esign
({ACSD}'14)},
author = {Kordon, Fabrice and Hulin{-}Hubard, Francis},
title = {BenchKit, a Tool for Massive Concurrent Benchmarking},
pages = {159-165},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KH-acsd14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KH-acsd14.pdf},
doi = {10.1109/ACSD.2014.12},
abstract = {Benchmarking numerous programs in a reasonable time requires the
use of several (potentially multicore) computers. We experimented such a
situation in the context of the MCC (Model Checking Contest @ Petri net)
where we had to operate more than 52000 runs for the 2013 edition. This
paper presents BenchKit, a tool to operate programs on sets of potentially
parallel machines and to gather monitoring information like CPU or memory
usage. It also samples such data over the execution time. BenchKit has
been elaborated in the context of the MCC and will be used for the 2014
edition.}
}
@inproceedings{GHKS-acsd14,
address = {Tunis, Tunisia},
month = jun,
year = 2014,
publisher = {{IEEE} Computer Society Press},
acronym = {{ACSD}'14},
booktitle = {{P}roceedings of the 14th {I}nternational
{C}onference on {A}pplication of {C}oncurrency
to {S}ystem {D}esign
({ACSD}'14)},
author = {Germanos, Vasileios and Haar, Stefan
and Khomenko, Victor and Schwoon, Stefan},
title = {Diagnosability under Weak Fairness},
pages = {132-141},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GHKS-acsd14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GHKS-acsd14.pdf},
doi = {10.1109/ACSD.2014.9},
abstract = {In partially observed Petri nets, diagnosis is the
task of detecting whether or not the given sequence of
observed labels indicates that some unobservable fault
has occurred. Diagnosability is an associated property of
the Petri net, stating that in any possible execution an
occurrence of a fault can eventually be diagnosed.\par In this
paper we consider diagnosability under the weak fairness (WF)
assumption, which intuitively states that no transition from
a given set can stay enabled forever---it~must eventually
either fire or be disabled. We show that a previous approach
to WF-diagnosability in the literature has a major flaw, and
present a corrected notion. Moreover, we present an efficient
method for verifying WF-diagnosability based on a reduction
to LTL-X model checking. An important advantage of this
method is that the LTL-X formula is fixed---in~particular,
the WF assumption does not have to be expressed as a part of
it (which would make the formula length proportional to the
size of the specification), but rather the ability of existing
model checkers to handle weak fairness directly is exploited.}
}
@inproceedings{SLSFM-rtcsa14,
address = {Chongqing, China},
month = aug,
year = 2014,
publisher = {{IEEE} Computer Society Press},
acronym = {{RTCSA}'14},
booktitle = {{P}roceedings of the 20th {IEEE} {I}nternational {C}onference on {E}mbedded
and {R}eal-{T}ime {C}omputing {S}ystems and {A}pplications
({RTCSA}'14)},
author = {Sun, Youcheng and Lipari, Giuseppe and
Soulat, Romain and Fribourg, Laurent and
Markey, Nicolas},
title = {Component-Based Analysis of Hierarchical Scheduling using Linear Hybrid Automata},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SLSFM-rtcsa14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SLSFM-rtcsa14.pdf},
doi = {10.1109/RTCSA.2014.6910502},
abstract = {Formal methods (e.g. Timed Automata or Linear Hybrid Automata)
can be used to analyse a real-time system by performing a reachability
analysis on the model. The advantage of using formal methods is that they
are more expressive than classical analytic models used in schedulability
analysis. For example, it is possible to express state-dependent
behaviour, arbitrary activation patterns,~etc.\par
In this paper we use the formalism of Linear Hybrid Automata to encode a
hierarchical scheduling system. In particular, we model a dynamic server
algorithm and the tasks contained within, abstracting away the rest of the
system, thus enabling component-based scheduling analysis. We prove the
correctness of the model and the decidability of the reachability analysis
for the case of periodic tasks. Then, we compare the results of our model
against classical schedulability analysis techniques, showing that our
analysis performs better than analytic methods in terms of resource
utilisation. We further present two case studies: a~component with
state-dependent tasks, and a simplified model of a real avionics system.
Finally, through extensive tests with various configurations, we
demonstrate that this approach is usable for medium size components.}
}
@article{BFSP-tcs14,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Bouchy, Florent and Finkel, Alain and San{ }Pietro, Pierluigi},
title = {Dense-choice Counter Machines Revisited},
volume = {542},
month = jul,
year = 2014,
pages = {17-31},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFSP-tcs14.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFSP-tcs14.pdf},
doi = {10.1016/j.tcs.2014.04.029},
abstract = {This paper clarifies the picture about Dense-choice
Counter Machines (DCM), a less studied version of
Counter Machines where counters range on a dense,
rather than discrete, domain. The definition of DCM
is revisited to make it extend (discrete) Counter
Machines, and new undecidability and decidability
results are proved. Using the first-order additive
mixed theory of reals and integers, the paper
presents a logical characterization of the sets of
configurations reachable by reversal-bounded DCM. We
also relate the DCM model to more common models of
systems.}
}
@techreport{rr-lsv-14-06,
author = {Sun, Youcheng and Lipari, Giuseppe},
title = {A Weak Simulation Relation for Real-Time
Schedulability Analysis of Global Fixed
Priority Scheduling Using Linear Hybrid
Automata},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2014},
month = apr,
type = {Research Report},
number = {LSV-14-06},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2014-06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2014-06.pdf},
versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2014-06-v1.pdf, 20140428},
note = {17~pages},
abstract = {In this paper we present an exact schedulability test for
sporadic real-time tasks scheduled by the Global Fixed Priority Fully
Preemptive Scheduler on a multiprocessor system. The analysis consists in
modelling the system as a Linear Hybrid Automaton, and in performing a
reachability analysis for states representing deadline miss conditions. To
mitigate the problem of state space explosion, we propose a partial order
relationship over the symbolic states of the model and we prove that this
is a weak simulation relation. We then present an implementation of the
analysis in a software tool, and we show that the use of the proposed
model permits to analyse larger systems than other exact algorithms in the
literature.}
}
@inproceedings{CD-icalp14,
address = {Copenhagen, Denmark},
month = jul,
year = 2014,
volume = 8573,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Esparza, Javier and Fraigniaud, Pierre and Koutsoupias, Elias},
acronym = {{ICALP}'14},
booktitle = {{P}roceedings of the 41st {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'14)~-- {P}art~{II}},
author = {Chatterjee, Krishnendu and Doyen, Laurent},
title = {Games with a Weak Adversary},
pages = {110-121},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-icalp14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-icalp14.pdf},
doi = {10.1007/978-3-662-43951-7_10},
abstract = {We consider multi-player graph games with partial-observation
and parity objective. While the decision problem for three-player games
with a coalition of the first and second players against the third player
is undecidable in general, we present a decidability result for
partial-observation games where the first and third player are in a
coalition against the second player, thus where the second player is
adversarial but weaker due to partial-observation. We establish tight
complexity bounds in the case where player~1 is less informed than
player~2, namely 2-EXPTIME-completeness for parity objectives. The
symmetric case of player~1 more informed than player~2 is much more
complicated, and we show that already in the case where player~1 has
perfect observation, memory of size non-elementary is necessary in general
for reachability objectives, and the problem is decidable for safety and
reachability objectives. Our results have tight connections with
partial-observation stochastic games for which we derive new complexity
results.}
}
@inproceedings{BFM-icalp14,
address = {Copenhagen, Denmark},
month = jul,
year = 2014,
volume = 8573,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Esparza, Javier and Fraigniaud, Pierre and Koutsoupias, Elias},
acronym = {{ICALP}'14},
booktitle = {{P}roceedings of the 41st {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'14)~-- {P}art~{II}},
author = {Blondin, Michael and Finkel, Alain and McKenzie, Pierre},
title = {Handling Infinitely Branching {WSTS}},
pages = {13-25},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFM-icalp14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFM-icalp14.pdf},
doi = {10.1007/978-3-662-43951-7_2},
abstract = {Most decidability results concerning well-structured
transition systems apply to the \emph{finitely branching}
variant. Yet some models (inserting automata, \(\omega\)-Petri
nets,~...) are naturally infinitely branching. Here
we develop tools to handle infinitely branching WSTS
by exploiting the crucial property that in the
(ideal) completion of a well-quasi-ordered set,
downward-closed sets are finite unions of
ideals. Then, using these tools, we derive
decidability results and we delineate the
undecidability frontier in the case of the
termination, the control-state maintainability and
the coverability problems. Coverability and
boundedness under new effectivity conditions are
shown decidable.}
}
@inproceedings{DD-aiml14,
address = {Groningen, The Netherlands},
month = aug,
year = 2014,
publisher = {College Publications},
editor = {Gor{\'e}, Rajeev and Kooi, Barteld P. and Kurucz, Agi},
acronym = {{AiML}'14},
booktitle = {{P}roceedings of the 10th
{C}onference on {A}dvances in {M}odal {L}ogics
({AiML}'14)},
author = {Demri, St{\'e}phane and Deters, Morgan},
title = {The effects of modalities in separation logics (extended abstract)},
pages = {134-138},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-aiml14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-aiml14.pdf},
abstract = {Like modal logic, temporal logic, or description logic,
separation logic has become a popular class of logical formalisms in
computer science, conceived as assertion languages for Hoare-style proof
systems with the goal to perform automatic program analysis. We present
similarities with modal and temporal logics, and we present landmark
results about decidability, complexity and expressive power.}
}
@inproceedings{DD-csllics14,
address = {Vienna, Austria},
month = jul,
year = 2014,
publisher = {ACM Press},
acronym = {{CSL\slash LICS}'14},
booktitle = {{P}roceedings of the Joint Meeting of the 23rd {EACSL} {A}nnual {C}onference on
{C}omputer {S}cience {L}ogic and the 29th {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({CSL\slash LICS}'14)},
author = {Demri, St{\'e}phane and Deters, Morgan},
title = {Expressive Completeness of Separation Logic With Two
Variables and No Separating Conjunction},
nopages = {},
chapter = {37},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-csllics14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-csllics14.pdf},
doi = {10.1145/2603088.2603142},
abstract = {We show that first-order separation logic with one record field
restricted to two variables and the separating implication (no separating
conjunction) is as expressive as weak second-order logic, substantially
sharpening a previous result. Capturing weak second-order logic with such
a restricted form of separation logic requires substantial updates to
known proof techniques. We develop these, and as a by-product identify the
smallest fragment of separation logic known to be undecidable: first-order
separation logic with one record field, two variables, and no separating
conjunction.}
}
@inproceedings{BGMZ-csllics14,
address = {Vienna, Austria},
month = jul,
year = 2014,
publisher = {ACM Press},
acronym = {{CSL\slash LICS}'14},
booktitle = {{P}roceedings of the Joint Meeting of the 23rd {EACSL} {A}nnual {C}onference on
{C}omputer {S}cience {L}ogic and the 29th {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({CSL\slash LICS}'14)},
author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin and
Zeitoun, Marc},
title = {Logical Characterization of Weighted Pebble Walking Automata},
nopages = {},
chapter = 19,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-csllics14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-csllics14.pdf},
doi = {10.1145/2603088.2603118},
abstract = {Weighted automata are a conservative quantitative extension of
finite automata that enjoys applications, e.g., in language processing and
speech recognition. Their expressive power, however, appears to be
limited, especially when they are applied to more general structures than
words, such as graphs. To address this drawback, weighted automata have
recently been generalized to weighted pebble walking automata, which
proved useful as a tool for the specification and evaluation of
quantitative properties over words and nested words. In this paper, we
establish the expressive power of weighted pebble walking automata in
terms of transitive closure logic, lifting a similar result by Engelfriet
and Hoogeboom from the Boolean case to a quantitative setting. This result
applies to general classes of graphs, including all the aforementioned
classes.}
}
@inproceedings{Haase-csllics14,
address = {Vienna, Austria},
month = jul,
year = 2014,
publisher = {ACM Press},
acronym = {{CSL\slash LICS}'14},
booktitle = {{P}roceedings of the Joint Meeting of the 23rd {EACSL} {A}nnual {C}onference on
{C}omputer {S}cience {L}ogic and the 29th {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({CSL\slash LICS}'14)},
author = {Haase, Christoph},
title = {Subclasses of {P}resburger Arithmetic and the Weak {EXP} Hierarchy},
nopages = {},
chapter = 47,
url = {http://arxiv.org/abs/1401.5266},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Haase-csllics14.pdf},
doi = {10.1145/2603088.2603092},
abstract = {It is shown that for any fixed \(i>0\), the
\(\Sigma_{i+1}\)-fragment of Presburger arithmetic, i.e., its restriction
to \(i+1\) quantifier alternations beginning with an existential
quantifier, is complete for \(\Sigma^{\textsc{EXP}}_{i}\), the \(i\)-th
level of the weak EXP hierarchy, an~analogue to the polynomial-time
hierarchy residing between \textsc{NEXP} and \textsc{EXPSPACE}. This
result completes the computational complexity landscape for Presburger
arithmetic, a~line of research which dates back to the seminal work by
Fischer~\& Rabin in~1974. Moreover, we~apply some of the techniques
developed in the proof of the lower bound in order to establish bounds on
sets of naturals definable in the \(\Sigma_1\)-fragment of Presburger
arithmetic: given a \(\Sigma_1\)-formula \(\Phi(x)\), it~is shown that the
set of non-negative solutions is an ultimately periodic set whose period
is at most doubly-exponentially and that this bound is tight.}
}
@inproceedings{BB-csllics14,
address = {Vienna, Austria},
month = jul,
year = 2014,
publisher = {ACM Press},
acronym = {{CSL\slash LICS}'14},
booktitle = {{P}roceedings of the Joint Meeting of the 23rd {EACSL} {A}nnual {C}onference on
{C}omputer {S}cience {L}ogic and the 29th {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({CSL\slash LICS}'14)},
author = {Bollig, Benedikt},
title = {Logic for Communicating Automata with Parameterized Topology},
nopages = {},
chapter = 18,
exturl = {http://hal.inria.fr/hal-00872807/},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BB-csllics14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BB-csllics14.pdf},
doi = {10.1145/2603088.2603093},
abstract = {We introduce parameterized communicating automata~(PCA) as a
model of systems where finite-state processes communicate through FIFO
channels. Unlike classical communicating automata, a given PCA can be run
on any network topology of bounded degree. The topology is thus a
parameter of the system. We provide various B{\"u}chi-Elgot-Trakhtenbrot
theorems for~PCA, which roughly read as follows: Given a logical
specification~\(\phi\) and a class of topologies~\(T\), there is a~PCA that is
equivalent to~\(\phi\) on all topologies from~\(T\). We~give uniform constructions
which allow us to instantiate~\(T\) with concrete classes such as pipelines,
ranked trees, grids, rings,~etc. The proofs build on a locality theorem
for first-order logic due to Schwentick and Barthelmann, and they exploit
concepts from the non-parameterized case, notably a result by Genest,
Kuske, and Muscholl.}
}
@inproceedings{CDNV-fossacs14,
address = {Grenoble, France},
month = apr,
year = 2014,
volume = {8412},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Muscholl, Anca},
acronym = {{FoSSaCS}'14},
booktitle = {{P}roceedings of the 17th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'14)},
author = {Chatterjee, Krishnendu and Doyen, Laurent and
Nain, Sumit and Vardi, Moshe Y.},
title = {The Complexity of Partial-Observation Stochastic Parity Games
with Finite-Memory Strategies},
pages = {242-257},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDNV-fossacs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDNV-fossacs14.pdf},
doi = {10.1007/978-3-642-54830-7_16},
abstract = { We consider two-player partial-observation stochastic games on
finite-state graphs where player~1 has partial observation and player~2
has perfect observation. The winning condition we study are \(\omega\)-regular
conditions specified as parity objectives. The qualitative-analysis
problem given a partial-observation stochastic game and a parity objective
asks whether there is a strategy to ensure that the objective is satisfied
with probability~1 (resp.~positive probability). These
qualitative-analysis problems are known to be undecidable. However in many
applications the relevant question is the existence of finite-memory
strategies, and the qualitative-analysis problems under finite-memory
strategies was recently shown to be decidable in 2EXPTIME. We improve the
complexity and show that the qualitative-analysis problems for
partial-observation stochastic parity games under finite-memory strategies
are EXPTIME-complete; and also establish optimal (exponential) memory
bounds for finite-memory strategies required for qualitative analysis. }
}
@inproceedings{CDGO-fossacs14,
address = {Grenoble, France},
month = apr,
year = 2014,
volume = {8412},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Muscholl, Anca},
acronym = {{FoSSaCS}'14},
booktitle = {{P}roceedings of the 17th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'14)},
author = {Chatterjee, Krishnendu and Doyen, Laurent and Gimbert, Hugo
and Oualhadj, Youssouf},
title = {Perfect-Information Stochastic Mean-Payoff Parity Games},
pages = {210-225},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDGO-fossacs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDGO-fossacs14.pdf},
doi = {10.1007/978-3-642-54830-7_4},
abstract = {The theory of graph games is the foundation for modeling and
synthesizing reactive processes. In the synthesis of stochastic processes,
we use \(2\frac{1}{2}\)-player games where some transitions of the game
graph are controlled by two adversarial players, the System and the
Environment, and the other transitions are determined probabilistically.
We consider \(2\frac{1}{2}\)-player games where the objective of the
System is the conjunction of a qualitative objective (specified as a
parity condition) and a quantitative objective (specified as a mean-payoff
condition). We establish that the problem of deciding whether the System
can ensure that the probability to satisfy the mean-payoff parity
objective is at least a given threshold is in
\(\textsf{NP}\cap\textsf{coNP}\), matching the best known bound in the
special case of 2-player games (where all transitions are deterministic)
with only parity objectives, or with only mean-payoff objectives. We
present an algorithm running in time~\(O(d \cdot n^{2d} \cdot
\textsf{MeanGame}) to compute the set of almost-sure winning states from
which the objective can be ensured with probability~1, where n is the
number of states of the game, d the number of priorities of the parity
objective, and MeanGame is the complexity to compute the set of
almost-sure winning states in \(2\frac{1}{2}\)-player mean-payoff games.
Our results are useful in the synthesis of stochastic reactive systems
with both functional requirement (given as a qualitative objective) and
performance requirement (given as a quantitative objective).}
}
@inproceedings{DMS-fossacs14,
address = {Grenoble, France},
month = apr,
year = 2014,
volume = {8412},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Muscholl, Anca},
acronym = {{FoSSaCS}'14},
booktitle = {{P}roceedings of the 17th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'14)},
author = {Doyen, Laurent and Massart, {\relax Th}ierry and Shirmohammadi, Mahsa},
title = {Limit Synchronization in Markov Decision Processes},
pages = {58-72},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DMS-fossacs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DMS-fossacs14.pdf},
doi = {10.1007/978-3-642-54830-7_4},
abstract = {Markov decision processes (MDP) are finite-state systems with
both strategic and probabilistic choices. After fixing a strategy, an MDP
produces a sequence of probability distributions over states. The sequence
is eventually synchronizing if the probability mass accumulates in a
single state, possibly in the limit. Precisely, for \(0 \leq p \leq 1\)
the sequence is \(p\)-synchronizing if a probability distribution in the
sequence assigns probability at least~\(p\) to some state, and we
distinguish three synchronization modes: \textit{(i)}~sure winning if
there exists a strategy that produces a 1-synchronizing sequence;
\textit{(ii)}~almost-sure winning if there exists a strategy that produces
a sequence that is, for all \(\varepsilon>0\), a
\((1-\varepsilon)\)-synchronizing sequence; \textit{(iii)}~limit-sure
winning if for all \(\varepsilon>0\), there exists a strategy that
produces a \((1-\varepsilon)\)-synchronizing sequence. We~consider the
problem of deciding whether an MDP is sure, almost-sure, or limit-sure
winning, and we establish the decidability and optimal complexity for all
modes, as well as the memory requirements for winning strategies. Our main
contributions are as follows: \textit{(a)}~for~each winning modes
we~present characterizations that give a PSPACE complexity for the
decision problems, and we establish matching PSPACE lower bounds;
\textit{(b)}~we~show that for sure winning strategies, exponential memory
is sufficient and may be necessary, and that in general infinite memory is
necessary for almost-sure winning, and unbounded memory is necessary for
limit-sure winning; \textit{(c)}~along with our results, we establish new
complexity results for alternating finite automata over a one-letter
alphabet.}
}
@inproceedings{FSS-icdt14,
address = {Athens, Greece},
month = mar,
year = 2014,
editor = {Schweikardt, Nicole and Christophides, Vassilis and Leroy, Vincent},
acronym = {{ICDT}'14},
booktitle = {{P}roceedings of the 17th {I}nternational {C}onference on
{D}atabase {T}heory ({ICDT}'14)},
author = {Francis, Nadime and Segoufin, Luc and Sirangelo, Cristina},
title = {Datalog Rewritings of Regular Path Queries using Views},
pages = {107-118},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FSS-icdt14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FSS-icdt14.pdf},
doi = {10.5441/002/icdt.2014.14},
abstract = {We consider query answering using views on graph databases, i.e.
databases structured as edge-labeled graphs. We consider views and queries
specified by Regular Path Queries. These are queries selecting pairs of
nodes in a graph database that are connected via a path whose sequence of
edge labels belongs to some regular language.\par
A~view~\(\mathbf{V}\) determines a query~\(Q\) if for all graph
databases~\(D\), the view image~\(\mathbf{V}(D)\) always contains enough
information to answer~\(Q\) on~\(D\). In other words, there is a well defined
function from~\(\mathbf{V}(D)\) to~\(Q(D)\).\par
Our main result shows that when this function is monotone, there exists a
rewriting of~\(Q\) as a Datalog query over the view
instance~\(\mathbf{V}(D)\). In~particular the query can be evaluated in
time polynomial in the size of~\(\mathbf{V}(D)\).\par
As a side result we also prove that it is decidable whether an RPQ query
can be rewritten in Datalog using RPQ views.}
}
@techreport{BB-arxiv14,
author = {Brault{-}Baron, Johann},
title = {Hypergraph Acyclicity Revisited},
institution = {Computing Research Repository},
number = {1403.7076},
year = {2014},
month = feb,
type = {Research Report},
url = {http://arxiv.org/abs/1403.7076},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BB-arxiv14.pdf},
note = {32~pages},
abstract = {The notion of graph acyclicity has been extended to several
different notions of hypergraph acyclicity, in increasing order of generality:
\emph{gamma} acyclicity, \emph{beta} acyclicity, and \emph{alpha} acyclicity, that
have met a great
interest in many fields. \parWe prove the equivalence between the numerous
characterizations of each notion with a new, simpler proof, in a self-contained
manner. For that purpose, we introduce new notions of alpha, beta and gamma leaf
that allow to define new {"}rule-based{"} characterizations of each notion.\par
The~combined presentation of the notions is completed with a study of their
respective closure properties. New closure results are established, and alpha,
beta and gamma acyclicity are proved optimal w.r.t. their closure properties.}
}
@article{LM-lmcs14,
journal = {Logical Methods in Computer Science},
author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas},
title = {Quantified {CTL}: Expressiveness and Complexity},
volume = 10,
number = {4:17},
nopages = {},
month = dec,
year = 2014,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LM-lmcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LM-lmcs14.pdf},
doi = {10.2168/LMCS-10(4:17)2014},
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
characterise the complexity of its model-checking and satisfiability
problems, 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).}
}
@article{NM-ercim14,
publisher = {European Research Consortium for Informatics and Mathematics},
journal = {ERCIM News},
author = {Markey, Nicolas},
title = {Cassting: Synthesizing Complex Systems Using Non-Zero-Sum Games},
volume = 97,
pages = {25-26},
year = 2014,
month = apr,
url = {http://ercim-news.ercim.eu/en97/special/cassting-synthesizing-complex-systems-using-non-zero-sum-games},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/NM-ercim14.pdf}
}
@inproceedings{DGLM-csr14,
address = {Moscow, Russia},
month = jun,
year = 2014,
volume = {8476},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Pin, Jean-{\'E}ric},
acronym = {{CSR}'14},
booktitle = {{P}roceedings of the 9th {I}nternational {C}omputer {S}cience
{S}ymposium in {R}ussia ({CSR}'14)},
author = {Demri, St{\'e}phane and Galmiche, Didier and
Larchey-Wendling, Dominique and M{\'e}ry, Daniel},
title = {Separation Logic with One Quantified Variable},
pages = {125-138},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DGLM-csr14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DGLM-csr14.pdf},
doi = {10.1007/978-3-319-06686-8_10},
abstract = {We investigate first-order separation logic with one record
field restricted to a unique quantified variable (1SL1). Undecidability is
known when the number of quantified variables is unbounded and the
satisfiability problem is PSPACE-complete for the propositional fragment.
We show that the satisfiability problem for 1SL1 is PSPACE-complete and we
characterize its expressive power by showing that every formula is
equivalent to a Boolean combination of atomic properties. This contributes
to our understanding of fragments of first-order separation logic that can
specify properties about the memory heap of programs with singly-linked
lists. When the number of program variables is fixed, the complexity drops
to polynomial time. All the fragments we consider contain the magic wand
operator and first-order quantification over a single variable.}
}
@phdthesis{mahsa-phd2014,
author = {Shirmohammadi, Mahsa},
title = {Qualitative Analysis of Synchronizing Probabilistic Systems},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France and Universit\'e Libre de Bruxelles, Belgium},
type = {Th{\`e}se de doctorat},
year = 2014,
month = dec,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/mahsa-phd14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/mahsa-phd14.pdf}
}
@phdthesis{soulat-phd2014,
author = {Soulat, Romain},
title = {Synthesis of Correct-by-Design Schedulers for Hybrid Systems},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2014,
month = feb,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/soulat-phd14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/soulat-phd14.pdf}
}
@techreport{rr-lsv-14-03,
author = {Fribourg, Laurent and Goubault, {\'E}ric and Mohamed, Sameh
and Putot, Sylvie and Soulat, Romain},
title = {Synthesis of robust boundary control for systems
governed by semi-discrete differential equations},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2014},
month = feb,
type = {Research Report},
number = {LSV-14-03},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2014-03.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2014-03.pdf},
versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2014-03-v1.pdf, 20140228},
note = {8~pages},
abstract = {The topic of boundary control of PDEs has been the subject of a
considerable literature since the seminal works of J.-L. Lions in the 90s.
In this paper, we consider the boundary control of systems represented by
spatial discretizations of~PDEs (i.e.,~semi-discrete equations). We~focus
on control laws which are sampled and piecewise constant: periodically, at
every sampling time, a fixed control amplitude is applied to the system
until the next sampling instant. We show that, under some conditions,
sampled piecewise-constant boundary control allows to achieve
{"}approximate controllability{"}: Given a time \(T>0\), the controlled system
evolves to a neighborhood of a given final state. The result is
illustrated on the boundary control of the semi-discrete version of the
heat equation.}
}
@inproceedings{CDFR-vmcai14,
address = {San~Diego, California, USA},
month = jan,
year = 2014,
volume = 8318,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {McMillan, Kenneth and Rival, Xavier},
acronym = {{VMCAI}'14},
booktitle = {{P}roceedings of the 15th {I}nternational {C}onference on
{V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation
({VMCAI}'14)},
author = {Chatterjee, Krishnendu and Doyen, Laurent and Filiot,
Emmanuel and Raskin, Jean-Fran{\c{c}}ois},
title = {Doomsday Equilibria for Omega-Regular Games},
pages = {78-97},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDFR-vmcai14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDFR-vmcai14.pdf},
doi = {10.1007/978-3-642-54013-4_5},
abstract = {Two-player games on graphs provide the theoretical framework for
many important problems such as reactive synthesis. While the traditional
study of two-player zero-sum games has been extended to multi-player games
with several notions of equilibria, they are decidable only for
perfect-information games, whereas several applications require
imperfect-information games.\par
In this paper we propose a new notion of equilibria, called doomsday
equilibria, which is a strategy profile such that all players satisfy
their own objective, and if any coalition of players deviates and violates
even one of the players objective, then the objective of every player is
violated.\par
We present algorithms and complexity results for deciding the existence of
doomsday equilibria for various classes of \(\omega\)-regular objectives,
both for imperfect-information games, and for perfect-information games.We
provide optimal complexity bounds for imperfect-information games, and in
most cases for perfect-information games.}
}
@inproceedings{Schmitz-rta14,
address = {Vienna, Austria},
month = jul,
year = 2014,
volume = {8560},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Dowek, Gilles},
acronym = {{RTA\slash TLCA}'14},
booktitle = {{P}roceedings of the {J}oint 25th {I}nternational {C}onference on
{R}ewriting {T}echniques and {A}pplications and 12th
{I}nternational {C}onference on {T}yped {L}ambda-{C}alculi
and {A}pplications ({RTA\slash TLCA}'14)},
author = {Schmitz, Sylvain},
title = {Implicational Relevance Logic is 2-{E}xp{T}ime-Complete},
pages = {395-409},
url = {http://arxiv.org/abs/1402.0705},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Schmitz-rta14.pdf},
doi = {10.1007/978-3-319-08918-8_27},
abstract = {We show that provability in the implicational fragment of
relevance logic is complete for doubly exponential time,
using reductions to and from coverability in branching
vector addition systems.}
}
@inproceedings{LS-csllics14,
address = {Vienna, Austria},
month = jul,
year = 2014,
publisher = {ACM Press},
acronym = {{CSL\slash LICS}'14},
booktitle = {{P}roceedings of the Joint Meeting of the 23rd {EACSL} {A}nnual {C}onference on
{C}omputer {S}cience {L}ogic and the 29th {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({CSL\slash LICS}'14)},
author = {Lazi{\'c}, Ranko and Schmitz, Sylvain},
title = {Non-Elementary Complexities for Branching {VASS},
{MELL}, and Extensions},
nopages = {},
chapter = 61,
url = {http://arxiv.org/abs/1401.6785},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-csllics14.pdf},
doi = {10.1145/2603088.2603129},
abstract = {We study the complexity of reachability problems on branching
extensions of vector addition systems, which allows us to
derive new non-elementary complexity bounds for fragments
and variants of propositional linear logic. We show that
provability in the multiplicative exponential fragment is
Tower-hard already in the affine case---and hence
non-elementary. We match this lower bound for the full
propositional affine linear logic, proving its
Tower-completeness. We also show that provability in
propositional contractive linear logic is
Ackermann-complete.}
}
@inproceedings{BDH-post14,
address = {Grenoble, France},
month = apr,
year = 2014,
volume = {8414},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abadi, Mart{\'\i}n and Kremer, Steve},
acronym = {{POST}'14},
booktitle = {{P}roceedings of the 3rd {I}nternational {C}onference on
{P}rinciples of {S}ecurity and {T}rust
({POST}'14)},
author = {Baelde, David and Delaune, St{\'e}phanie and Hirschi, Lucca},
title = {A~reduced semantics for deciding trace equivalence using constraint systems},
pages = {1-21},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDH-post14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDH-post14.pdf},
doi = {10.1007/978-3-642-54792-8_1},
abstract = {Many privacy-type properties of security protocols can be
modelled using trace equivalence properties in suitable process algebras.
It has been shown that such properties can be decided for interesting
classes of finite processes (i.e.,~without replication) by means of symbolic
execution and constraint solving. However, this does not suffice to obtain
practical tools. Current prototypes suffer from a classical combinatorial
explosion problem caused by the exploration of many interleavings in the
behaviour of processes. Modersheim et~al. have tackled this problem for
reachability properties using partial order reduction techniques. We
revisit their work, generalize it and adapt it for equivalence checking.
We obtain an optimization in the form of a reduced symbolic semantics that
eliminates redundant interleavings on the fly.}
}
@inproceedings{BM-sr14,
address = {Grenoble, France},
month = apr,
year = 2014,
volume = 146,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Mogavero, Fabio and Murano, Aniello},
acronym = {{SR}'14},
booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {S}trategic
{R}easoning ({SR}'14)},
author = {Berwanger, Dietmar and Mathew, Anup Basil},
title = {Games with Recurring Certainty},
pages = {91-96},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BM-sr14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BM-sr14.pdf},
doi = {10.4204/EPTCS.146.12},
abstract = {Infinite games where several players seek to coordinate under
imperfect information are known to be intractable, unless the information
flow is severely restricted. Examples of undecidable cases typically
feature a situation where players become uncertain about the current state
of the game, and this uncertainty lasts forever.\par
Here we consider games where the players attain certainty about the
current state over and over again along any play. For finite-state games,
we note that this kind of \emph{recurring} certainty implies a stronger condition
of \emph{periodic} certainty, that is, the events of state certainty ultimately
occur at uniform, regular intervals. We show that it is decidable whether
a given game presents recurring certainty, and that, if so, the problem of
synthesising coordination strategies under \(\omega\)-regular winning conditions is
solvable.}
}
@inproceedings{CDFR-sr14,
address = {Grenoble, France},
month = apr,
year = 2014,
volume = 146,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Mogavero, Fabio and Murano, Aniello},
acronym = {{SR}'14},
booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {S}trategic
{R}easoning ({SR}'14)},
author = {Chatterjee, Krishnendu and Doyen, Laurent and Filiot, Emmanuel and
Raskin, Jean-Fran{\c{c}}ois},
title = {Doomsday Equilibria for Omega-Regular Games},
pages = {43-48},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDFR-sr14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDFR-sr14.pdf},
doi = {10.4204/EPTCS.146.6},
abstract = {Two-player games on graphs provide the theoretical framework for
many important problems such as reactive synthesis. While the traditional
study of two-player zero-sum games has been extended to multi-player games
with several notions of equilibria, they are decidable only for
perfect-information games, whereas several applications require
imperfect-information games.\par
In this paper we propose a new notion of equilibria, called doomsday
equilibria, which is a strategy profile such that all players satisfy
their own objective, and if any coalition of players deviates and violates
even one of the players objective, then the objective of every player is
violated.\par
We present algorithms and complexity results for deciding the existence of
doomsday equilibria for various classes of \(\omega\)-regular objectives,
both for imperfect-information games, and for perfect-information games.
We provide optimal complexity bounds for imperfect-information games, and
in most cases for perfect-information games.}
}
@inproceedings{BMV-sr14,
address = {Grenoble, France},
month = apr,
year = 2014,
volume = 146,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Mogavero, Fabio and Murano, Aniello},
acronym = {{SR}'14},
booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {S}trategic
{R}easoning ({SR}'14)},
author = {Bouyer, Patricia and Markey, Nicolas and Vester, Steen},
title = {Nash Equilibria in Symmetric Games with Partial Observation},
pages = {49-55},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-sr14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-sr14.pdf},
doi = {10.4204/EPTCS.146.7},
abstract = {We investigate a model for representing large multiplayer games,
which satisfy strong symmetry properties. This model is made of multiple
copies of an arena; each player plays in his own arena, and can partially
observe what the other players do. Therefore, this game has partial
information and symmetry constraints, which make the computation of Nash
equilibria difficult. We show several undecidability results, and for
bounded-memory strategies, we precisely characterize the complexity of
computing pure Nash equilibria (for qualitative objectives) in this game
model.}
}
@phdthesis{cyriac-phd2014,
author = {Cyriac, Aiswarya},
title = {Verification of Communicating Recursive Programs via Split-width},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2014,
month = jan,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/cyriac-phd14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/cyriac-phd14.pdf}
}
@inproceedings{AGHKO-fossacs14,
address = {Grenoble, France},
month = apr,
year = 2014,
volume = {8412},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Muscholl, Anca},
acronym = {{FoSSaCS}'14},
booktitle = {{P}roceedings of the 17th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'14)},
author = {Antonopoulos, Timos and Gorogiannis, Nikos and Haase, Christoph
and Kanovich, Max and Ouaknine, Jo{\"e}l},
title = {Foundations for Decision Problems in Separation Logic with
General Inductive Predicates},
pages = {411-425},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGHKO-fossacs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGHKO-fossacs14.pdf},
doi = {10.1007/978-3-642-54830-7_27},
abstract = {We establish foundational results on the computational
complexity of deciding entailment in Separation Logic with general
inductive predicates whose underlying base language allows for pure
formulas, pointers and existentially quantified variables. We show that
entailment is in general undecidable, and \textsc{ExpTime}-hard in a
fragment recently shown to be decidable by Iosif~\emph{et~al.} Moreover,
entailment in the base language is \(\Pi_2^{\text{P}}\)-complete, the
upper bound even holds in the presence of list predicates. We additionally
show that entailment in essentially any fragment of Separation Logic
allowing for general inductive predicates is intractable even when strong
syntactic restrictions are imposed.}
}
@inproceedings{BFHHH-fossacs14,
address = {Grenoble, France},
month = apr,
year = 2014,
volume = {8412},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Muscholl, Anca},
acronym = {{FoSSaCS}'14},
booktitle = {{P}roceedings of the 17th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'14)},
author = {Bertrand, Nathalie and Fabre, {\'E}ric and Haar, Stefan and
Haddad, Serge and H{\'e}lou{\"e}t, Lo{\"\i}c},
title = {Active diagnosis for probabilistic systems},
pages = {29-42},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHHH-fossacs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHHH-fossacs14.pdf},
doi = {10.1007/978-3-642-54830-7_4},
abstract = {The diagnosis problem amounts to deciding whether some specific
{"}fault{"} event occurred or not in a system, given the observations
collected on a run of this system. This system is then diagnosable if the
fault can always be detected, and the active diagnosis problem consists in
controlling the system in order to ensure its diagnosability. We consider
here a stochastic framework for this problem: once a control is selected,
the system becomes a stochastic process. In this setting, the active
diagnosis problem consists in deciding whether there exists some
observation-based strategy that makes the system diagnosable with
probability one. We prove that this problem is EXPTIME-complete, and that
the active diagnosis strategies are belief-based. The safe active
diagnosis problem is similar, but aims at enforcing diagnosability while
preserving a positive probability to non faulty runs, i.e. without
enforcing the occurrence of a fault. We prove that this problem requires
non belief-based strategies, and that it is undecidable. However, it
belongs to NEXPTIME when restricted to belief-based strategies. Our work
also refines the decidability/undecidability frontier for verification
problems on partially observed Markov decision processes.}
}
@article{ABGMN-fi13,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {Akshay, S. and Bollig, Benedikt and Gastin, Paul and
Mukund, Madhavan and Narayan Kumar, K.},
title = {Distributed Timed Automata with Independently Evolving Clocks},
volume = {130},
number = {4},
month = apr,
year = 2014,
pages = {377-407},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGMN-fi13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGMN-fi13.pdf},
doi = {10.3233/FI-2014-996},
abstract = {We propose a model of distributed timed systems where each
component is a timed automaton with a set of local clocks that evolve at a
rate independent of the clocks of the other components. A~clock can be
read by any component in the system, but it can only be reset by the
automaton it belongs~to.\par
There are two natural semantics for such systems. The \emph{universal}
semantics captures behaviors that hold under any choice of clock rates for
the individual components. This is a natural choice when checking that a
system always satisfies a positive specification. To check if a system
avoids a negative specification, it is better to use the
\emph{existential} semantics—the set of behaviors that the system
can possibly exhibit under some choice of clock rates.\par
We show that the existential semantics always describes a regular set of
behaviors. However, in the case of universal semantics, checking emptiness
or universality turns out to be undecidable. As an alternative to the
universal semantics, we propose a \emph{reactive} semantics that allows us
to check positive specifications and yet describes a regular set of
behaviors.}
}
@article{BGMZ-tocl13,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin and Zeitoun, Marc},
title = {Pebble Weighted Automata and Weighted Logics},
volume = 15,
number = {2:15},
month = apr,
year = 2014,
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-tocl13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-tocl13.pdf},
doi = {10.1145/2579819},
abstract = {We introduce new classes of weighted automata on words. Equipped
with pebbles, they go beyond the class of recognizable formal power
series: they capture weighted first-order logic enriched with a
quantitative version of transitive closure. In contrast to previous work,
this calculus allows for unrestricted use of existential and universal
quantifications over positions of the input word. We actually consider
both two-way and one-way pebble weighted automata. The latter class
constrains the head of the automaton to walk left-to-right, resetting it
each time a pebble is dropped. Such automata have already been considered
in the Boolean setting, in the context of data words. Our main result
states that two-way pebble weighted automata, one-way pebble weighted
automata, and our weighted logic are expressively equivalent. We also give
new logical characterizations of standard recognizable series.}
}
@article{SBM-ic14,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Sankur, Ocan and Bouyer, Patricia and Markey, Nicolas},
title = {Shrinking Timed Automata},
volume = 234,
month = feb,
year = 2014,
pages = {107-132},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SBM-ic14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SBM-ic14.pdf},
doi = {10.1016/j.ic.2014.01.002},
abstract = {We define and study a new approach to the implementability of
timed automata, where the semantics is perturbed by imprecisions and
finite frequency of the hardware. In order to circumvent these effects, we
introduce \emph{parametric shrinking} of clock constraints, which
corresponds to tightening the guards. We propose symbolic procedures to
decide the existence of (and then compute) parameters under which the
shrunk version of a given timed automaton is non-blocking and can
time-abstract simulate the exact semantics. We then define an
implementation semantics for timed automata with a digital clock and
positive reaction times, and show that for shrinkable timed automata,
non-blockingness and time-abstract simulation are preserved in
implementation.}
}
@article{GM-tcs14,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Gastin, Paul and Monmege, Benjamin},
title = {Adding Pebbles to Weighted Automata~-- Easy Specification
{\&} Efficient Evaluation},
volume = {534},
month = may,
year = 2014,
pages = {24-44},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GM-tcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GM-tcs14.pdf},
doi = {10.1016/j.tcs.2014.02.034},
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. 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. We also prove that the
evaluation problem for weighted automata can be done very efficiently if
the number of reusable pebbles is low.}
}
@article{BLM-peva13,
publisher = {Elsevier Science Publishers},
journal = {Performance Evaluation},
author = {Bouyer, Patricia and Larsen, Kim G. and Markey, Nicolas},
title = {Lower-Bound Constrained Runs in Weighted Timed Automata},
volume = 73,
month = mar,
year = 2014,
pages = {91-109},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLM-peva13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLM-peva13.pdf},
doi = { 10.1016/j.peva.2013.11.002},
abstract = {We investigate a number of problems related to infinite runs of
weighted timed automata (with a single weight variable), subject to
lower-bound constraints on the accumulated weight. Closing an open problem
from an earlier paper, 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 known initial credit. We
show that the related problem of existence of an initial credit for which
there exists 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. 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.\par
Finally, we extend this study to multi-weighted timed automata: the
existence of a feasible run becomes undecidable even for bounded duration,
but the existence of initial credits remains decidable (in~PSPACE).}
}
@inproceedings{KL-pdp14,
address = {Turin, Italy},
month = feb,
year = 2014,
publisher = {{IEEE} Computer Society Press},
editor = {Aldinucci, Marco and D'Agostino, Daniele and Kilpatrick, Peter},
acronym = {{PDP}'14},
booktitle = {{P}roceedings of the 22nd {E}uromicro {I}nternational {C}onference
on {P}arallel, {D}istributed, and {N}etwork-{B}ased
{P}rocessing ({PDP}'14)},
author = {Kumar, Sunil and Lipari, Giuseppe},
title = {Latency Analysis of Network-On-Chip-based Many-Core Processors},
pages = {432-439},
doi = {10.1109/PDP.2014.107},
abstract = {The next generation of processor will contain an increasing
number of cores, connected to the main memory and to each other using fast
Network-on-Chip (NoC) organised in complex mesh structures. In order to
analyse real-time programs running on such architectures, it is necessary
to estimate the communication latency between processes running on
different cores. The goal of this paper is to propose an analytic model
for bounding the communication latency on NoC for many-core architectures.
In particular, we introduce a new approach to analyse the communication
latency on NoC with wormhole switching and credit-based virtual channel
flow control. The proposed model is evaluated by comparing the results
predicted by the model with real measurements obtained running a set of
experiments on an Intel SCC platform.}
}
@article{ACD-icomp13,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Arnaud, Mathilde and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
title = {Modeling and Verifying Ad~Hoc Routing Protocols},
volume = 238,
pages = {30-67},
month = nov,
year = 2014,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACD-icomp13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACD-icomp13.pdf},
doi = {10.1016/j.ic.2014.07.004},
abstract = {Mobile ad hoc networks consist of mobile wireless devices which
autonomously organize their infrastructure. In such networks, a central
issue, ensured by routing protocols, is to find a route from one device to
another. Those protocols use cryptographic mechanisms in order to prevent
malicious nodes from compromising the discovered route.\par
Our contribution is twofold. We first propose a calculus for modeling and
reasoning about security protocols, including in particular secured
routing protocols. Our calculus extends standard symbolic models to take
into account the characteristics of routing protocols and to model
wireless communication in a more accurate way. Our second main
contribution is a decision procedure for analyzing routing protocols for
any network topology. By using constraint solving techniques, we show that
it is possible to automatically discover (in~NPTIME) whether there exists
a network topology that would allow malicious nodes to mount an attack
against the protocol, for a bounded number of sessions. We also provide a
decision procedure for detecting attacks in case the network topology is
given a priori. We demonstrate the usage and usefulness of our approach by
analyzing protocols of the literature, such as SRP applied to DSR and
SDMSR.}
}
@inproceedings{HHM-tgc13,
address = {Buenos Aires, Argentina},
month = mar,
year = 2014,
volume = {8358},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abadi, Mart{\'\i}n and Lluch{ }Lafuente, Alberto},
acronym = {{TGC}'13},
booktitle = {{R}evised {S}elected {P}apers of the 8th {S}ymposium on {T}rustworthy {G}lobal
{C}omputing ({TGC}'13)},
author = {Haddad, Serge and Hennicker, Rolf and M{\o}ller, Mikael H.},
title = {Specification of Asynchronous Component Systems with
Modal {I}{{\slash}}{O}-{P}etri Nets},
pages = {219-234},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HHM-tgc13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HHM-tgc13.pdf},
doi = {10.1007/978-3-319-05119-2_13},
abstract = {We consider Petri nets with distinguished labels for
inputs, outputs, internal communications and silent actions and
with {"}must{"} and {"}may{"} modalities for transitions. The
input\slash output labels show the interaction capabilities of a
net to the outside used to build larger nets by asynchronous
composition via communication channels. The modalities express
constraints for Petri net refinement taking into account
observational abstraction from silent transitions. Modal
I\slash O-Petri nets are equipped with a modal transition system
semantics. We show that refinement is preserved by asynchronous
composition and by hiding of communication channels. We study
conformance properties which express communication requirements
for composed systems and we show that those properties are
preserved by refinement. On this basis we propose a methodology
for the specification of distributed systems in terms of modal
I\slash O-Petri nets which supports incremental design, encapsulation of
components and stepwise refinement. Finally we show that our
communication properties are decidable.}
}
@article{GL-acs13,
publisher = {Springer},
journal = {Applied Categorical Structures},
author = {Goubault{-}Larrecq, Jean},
title = {Exponentiable streams and prestreams},
volume = {22},
number = {3},
year = 2014,
month = jun,
pages = {515-549},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GL-acs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GL-acs13.pdf},
corrigendumpdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GL-acs13-erratum.pdf},
doi = { 10.1007/s10485-013-9315-x},
note = {Errata 1: \url{http://www.lsv.fr/Publis/PAPERS/PDF/GL-acs13-erratum.pdf};
Errata 2: \url{http://www.lsv.fr/Publis/PAPERS/PDF/GL-acs13-erratum2.pdf}},
abstract = {Inspired by a construction of Escard{\'o}, Lawson, and Simpson,
we give a general construction of \(\mathcal C\)-generated objects in a
topological construct. When \(\mathcal C\) consists of exponentiable
objects, the resulting category is Cartesian-closed. This generalizes the
familiar construction of compactly-generated spaces, and we apply this to
Krishnan's categories of streams and prestreams, as well as to Haucourt
streams. For that, we need to identify the exponentiable objects in these
categories: for prestreams, we show that these are the preordered
core-compact topological spaces, and for streams, these are the
core-compact streams.}
}
@article{BCD-icomp13,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Bursuc, Sergiu and Comon{-}Lundh, Hubert and Delaune,
St{\'e}phanie},
title = {Deducibility constraints and blind signatures},
year = {2014},
month = nov,
volume = 238,
pages = {106-127},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCD-icomp13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCD-icomp13.pdf},
nonote = {32~pages},
doi = {10.1016/j.ic.2014.07.006},
abstract = {Deducibility constraints represent in a symbolic way the
infinite set of possible executions of a finite protocol. Solving a
deducibility constraint amounts to finding all possible ways of filling
the gaps in a proof. For finite local inference systems, there is an
algorithm that reduces any deducibility constraint to a finite set of
solved forms. This allows one to decide any trace security property of
cryptographic protocols.\par
We investigate here the case of infinite local inference systems, through
the case study of blind signatures. We show that, in this case again, any
deducibility constraint can be reduced to finitely many solved forms
(hence we can decide trace security properties). We sketch also another
example to which the same method can be applied.}
}
@article{BCGMNTW-jfr14,
publisher = {University of Bologna},
journal = {Journal of Formalized Reasoning},
author = {Baelde, David and Chaudhuri, Kaustuv and Gacek, Andrew and
Miller, Dale and Nadathur, Gopalan and Tiu, Alwen and Wang,
Yuting},
title = {Abella: A~System for Reasoning about Relational Specifications},
volume = {7},
number = {2},
year = {2014},
pages = {1-89},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGMNTW-jfr14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGMNTW-jfr14.pdf},
doi = {10.6092/issn.1972-5787/4650},
abstract = {The Abella interactive theorem prover is based on an
intuitionistic logic that allows for inductive and co-inductive reasoning
over relations. Abella supports the \(\lambda\)-tree approach to treating
syntax containing binders: it~allows simply typed \(\lambda\)-terms to be
used to represent such syntax and it provides higher-order (pattern)
unification, the \(\nabla\) quantifier, and nominal constants for
reasoning about these representations. As such, it is a suitable vehicle
for formalizing the meta-theory of formal systems such as logics and
programming languages. This tutorial exposes Abella incrementally,
starting with its capabilities at a first-order logic level and gradually
presenting more sophisticated features, ending with the support it offers
to the \emph{two-level logic approach} to meta-theoretic reasoning. Along
the way, we show how Abella can be used prove theorems involving natural
numbers, lists, and automata, as well as involving typed and untyped
\(\lambda\)-calculi and the \(\pi\)-calculus.}
}
@techreport{KNS-arxiv14,
author = {Karandikar, Prateek and Niewerth, Matthias and Schnoebelen, {\relax Ph}ilippe},
title = {On the state complexity of closures and interiors of regular languages with subwords},
institution = {Computing Research Repository},
number = {1406.0690},
year = {2014},
month = nov,
type = {Research Report},
url = {http://arxiv.org/abs/1406.0690},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KNS-arxiv14.pdf},
note = {24~pages},
abstract = {We study the state complexity of the set of subwords and
superwords of regular languages, and provide new lower bounds in the case
of languages over a two-letter alphabet. We also consider the dual
interior sets, for which the nondeterministic state complexity has a
doubly-exponential upper bound. We prove a matching doubly-exponential
lower bound for downward interiors in the case of an unbounded alphabet.}
}
@article{AFG-sif15,
publisher = {SIF},
journal = {1024~-- Bulletin de la soci{\'e}t{\'e} informatique de France},
author = {Abiteboul, Serge and Fribourg, Laurent and
Goubault{-}Larrecq, Jean},
title = {{G}{\'e}rard {B}erry~: un~informaticien m{\'e}daille d'or du {CNRS}~2014},
volume = 4,
pages = {139-142},
month = oct,
year = 2014,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AFG-sif15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AFG-sif15.pdf},
abstract = {C'est un chercheur en informatique qui vient de recevoir la
m{\'e}daille d'or du CNRS, la plus haute distinction scientifique fran{\c
c}aise toutes disciplines confondues. Les informaticiens sont rares {\`a}
avoir {\'e}t{\'e} ainsi honor{\'e}s : ce n'est que la seconde fois
apr{\`e}s Jacques Stern en~2006.}
}
@inproceedings{MA-bda14,
address = {Autrans, France},
month = oct,
year = 2014,
editor = {Gross-Amblard, David and Collet, {\relax Ch}ristine and
Bobineau, {\relax Ch}ristophe and Jouanot, Fabrice},
acronym = {{BDA}'14},
booktitle = {{A}ctes de la 30{\`e}me {C}onf{\'e}rence sur la {G}estion de
{D}onn{\'e}es~-- {P}rincipes, {T}echnologies et
{A}pplications ({BDA}'14)},
author = {Montoya, David and Abiteboul, Serge},
title = {Inf{\'e}rence d'itin{\'e}raires multimodaux {\`a}~partir de donn{\'e}es
smartphone},
pages = {38-42},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/MA-bda14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/MA-bda14.pdf},
abstract = {We designed a system to infer the multimodal itineraries
traveled by a user from a combination of smartphone sensor data (e.g.,
GPS, Wi-Fi, inertial sensors), personal information, and knowledge of the
transport network topology (e.g., maps, transportation timetables). The
system operates with a Multimodal Transport Network that captures the set
of admissible multimodal itineraries, i.e., paths of this network with
weights providing the statistics (expected time and variance) of the
paths. The network takes into account public transportation schedules. Our
Multimodal Transport Network is constructed from publicly available
transport data of Paris and its neighbourhoods published by different
transport agencies and map organizations. The system models sensor
uncertainty with probabilities, and the likelihood that a multimodal
itinerary was taken by the user is captured in a Dynamic Bayesian Network.
For this demonstration, we captured data from users travelling over the
Paris region who were asked to record data for different trips via an
Android application. After uploading their data into our system, a set of
most likely itineraries is computed for each trip. For each trip, the
system displays recognized multimodal itineraries and their estimated
likelihood over an interactive map.}
}
@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{mcc:2014,
author = {F. Kordon and H. Garavel and L.-M. Hillah and Hulin{-}Hubard, Francis
and A. Linard and M. Beccuti and S. Evangelista and A. Hamez and N.
Lohmann and E. Lopez and E. Paviot-Adet and C. Rodriguez and C. Rohr and
J. Srba},
month = jun,
title = {{Results for the MCC @ Petri Nets 2014}},
year = {2014},
url = {http://mcc.lip6.fr/2014}
}
@mastersthesis{m2-doumane,
author = {Doumane, Amina},
title = {{\'E}tudes des automates en ludique},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2014},
month = sep
}
@misc{JGL:lls14,
author = {Goubault{-}Larrecq, Jean},
howpublished = {Matinale de l'innovation Logiciels Libres et S{\'e}curit{\'e}, Paris, France},
month = dec,
title = {D{\'e}tection d'intrusions avec {OrchIDS}},
year = {2014}
}
@misc{JGL:ccc14,
author = {Goubault{-}Larrecq, Jean},
howpublished = {Invited talk, Continuity, Computability, Constructivity workshop (CCC), Ljubljana, Slovenia},
month = sep,
title = {Noetherian spaces},
year = {2014}
}
@misc{JGL:cps14,
author = {Goubault{-}Larrecq, Jean},
howpublished = {CPS Summer School, Grenoble, France},
month = jul,
title = {{OrchIDS}: on the value of rigor in intrusion detection},
year = {2014}
}
@misc{GSM:dga-inria-2-14,
author = {Goubault-Larrecq, Jean and Sentucq, Pierre-Arnaud and Majorczyk, Fr{\'e}d{\'e}ric},
howpublished = {Fourniture 2 du contrat DGA-INRIA Orchids},
month = may,
title = {Techniques et m{\'e}thodes de g{\'e}n{\'e}ration de signatures pour la d{\'e}tection d'intrusions},
year = {2014}
}
@misc{GSM:dga-inria-1-14,
author = {Goubault-Larrecq, Jean and Sentucq, Pierre-Arnaud and Majorczyk, Fr{\'e}d{\'e}ric},
howpublished = {Fourniture 1 du contrat DGA-INRIA Orchids},
month = may,
title = {Politiques de s{\'e}curit{\'e} syst{\`e}me},
year = {2014}
}
@mastersthesis{m2-Jaziri,
author = {Jaziri, Samy},
title = {{Robustness issues in priced timed automata}},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2014},
month = sep
}
This file was generated by bibtex2html 1.98.