@article{JKS-lmcs14,
journal = {Logical Methods in Computer Science},
author = {Jancar, Petr and Karandikar, Prateek and Schnoebelen, {\relax Ph}ilippe},
title = {On Reachability for Unidirectional Channel Systems Extended
with Regular Tests},
year = {2015},
volume = 11,
number = {{2:2}},
month = apr,
nopages = {},
url = {http://arxiv.org/abs/1406.5067},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JKS-lmcs14.pdf},
doi = {10.2168/LMCS-11(2:2)2015},
abstract = {{"}Unidirectional channel systems{"} (Chambart~\& Schnoebelen,
CONCUR~2008) are finite-state systems where one-way communication from a
Sender to a Receiver goes via one reliable and one unreliable unbounded
fifo channel. While reachability is decidable for these systems, equipping
them with the possibility of testing regular properties on the contents of
channels makes it undecidable. Decidability is preserved when only
emptiness and nonemptiness tests are considered: the proof relies on an
elaborate reduction to a generalized version of Post's Embedding Problem.}
}
@article{KKS-ipl14,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Karandikar, Prateek and Kufleitner, Manfred and Schnoebelen, {\relax Ph}ilippe},
title = {On the index of {S}imon's congruence for piecewise testability},
year = {2015},
month = apr,
volume = {15},
number = {4},
pages = {515-519},
url = {http://arxiv.org/abs/1310.1278},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KKS-ipl14.pdf},
doi = {10.1016/j.ipl.2014.11.008},
abstract = {Simon's congruence, denoted \(\sim_{n}\), relates words having
the same subwords of length up to~\(n\). We~show that, over a
\(k\)-letter alphabet, the~number of words modulo~\(\sim_{n}\) is in
\(2^{\Theta(n^{k-1}\cdot\log n)}\).}
}
@article{ABV-tocsys15,
publisher = {Springer},
journal = {Theory of Computing Systems},
author = {Abiteboul, Serge and Bourhis, Pierre and Vianu, Victor},
title = {Highly Expressive Query Languages for Unordered Data Trees},
pages = {927-966},
year = 2015,
month = nov,
volume = {57},
number = {4},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABV-tocsys15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABV-tocsys15.pdf},
doi = {10.1007/s00224-015-9617-5},
abstract = {We study highly expressive query languages for unordered data
trees, using as formal vehicles Active XML and extensions of languages in
the while family. All languages may be seen as adding some form of control
on top of a set of basic pattern queries. The results highlight the impact
and interplay of different factors: the expressive power of basic queries,
the embedding of computation into data (as in Active XML), and the use of
deterministic vs. nondeterministic control. All languages are Turing
complete, but not necessarily query complete in the sense of Chandra and
Harel. Indeed, we show that some combinations of features yield serious
limitations, analogous to FO\(^{k}\) definability in the relational context. On
the other hand, the limitations come with benefits such as the existence
of powerful normal forms providing opportunities for optimization. Other
languages are {"}almost{"} complete, but fall short because of subtle
limitations reminiscent of the copy elimination problem in object
databases.}
}
@article{AADMS-tocsys14,
publisher = {Springer},
journal = {Theory of Computing Systems},
author = {Abiteboul, Serge and Amsterdamer, Yael and Deutch, Daniel
and Milo, Tova and Senellart, Pierre},
title = {Optimal Probabilistic Generation of {XML} Documents},
pages = {806-842},
year = 2015,
month = nov,
volume = {57},
number = {4},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AADMS-tocsys14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AADMS-tocsys14.pdf},
doi = {10.1007/s00224-014-9581-5},
abstract = {We study the problem of, given a corpus of XML documents and its
schema, finding an optimal (generative) probabilistic model, where
optimality here means maximizing the likelihood of the particular corpus
to be generated. Focusing first on the structure of documents, we present
an efficient algorithm for finding the best generative probabilistic
model, in the absence of constraints. We further study the problem in the
presence of integrity constraints, namely key, inclusion, and domain
constraints. We study in this case two different kinds of generators.
First, we consider a continuation-test generator that performs, while
generating documents, tests of schema satisfiability; these tests prevent
from generating a document violating the constraints but, as we will see,
they are computationally expensive. We also study a restart generator that
may generate an invalid document and, when this is the case, restarts and
tries again. Finally, we consider the injection of data values into the
structure, to obtain a full XML document. We study different approaches
for generating these values.}
}
@article{CDGH-ic15,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Chatterjee, Krishnendu and Doyen, Laurent and Gimbert, Hugo
and Henzinger, Thomas A.},
title = {Randomness for free},
volume = {245},
month = dec,
year = 2015,
pages = {3-16},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDGH-ic15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDGH-ic15.pdf},
doi = {10.1016/j.ic.2015.06.003},
abstract = {We consider two-player zero-sum games on finite-state graphs.
These games can be classified on the basis of the information of the
players and on the mode of interaction between them. On the basis of
information the classification is as follows: (a)~partial-observation
(both players have partial view of the game); (b)~one-sided
complete-observation (one player has complete observation); and
(c)~complete-observation (both players have complete view of the game).
On~the basis of mode of interaction we have the following classification:
(a)~concurrent (players interact simultaneously); and (b)~turn-based
(players interact in turn). The~two sources of randomness in these games
are randomness in the transition function and randomness in the
strategies. In general, randomized strategies are more powerful than
deterministic strategies, and probabilistic transitions give more general
classes of games. We present a complete characterization for the classes
of games where randomness is not helpful~in: (a)~the transition function
(probabilistic transitions can be simulated by deterministic transitions);
and (b)~strategies (pure strategies are as powerful as randomized
strategies). As~a consequence of our characterization we obtain new
undecidability results for these games.}
}
@article{LM-ic14,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas},
title = {Augmenting {ATL} with strategy contexts},
volume = {245},
month = dec,
year = 2015,
pages = {98-123},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2014-05.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2014-05.pdf},
doi = {10.1016/j.ic.2014.12.020},
abstract = {We study the extension of the alternating-time temporal logic
(ATL) with strategy contexts: contrary to the original semantics, in this
semantics the strategy quantifiers do not reset the previously selected
strategies.\par
We show that our extension ATLsc is very expressive, but that its decision
problems are quite hard: model checking is \(k\)-EXPTIME-complete when the
formula has k nested strategy quantifiers; satisfiability is undecidable,
but we prove that it is decidable when restricting to turn-based games.
Our algorithms are obtained through a very convenient translation to QCTL
(the~computation-tree logic CTL extended with atomic quantification),
which we show also applies to Strategy Logic, as well as when strategy
quantification ranges over memoryless strategies.}
}
@article{jgl-jlap14,
publisher = {Elsevier Science Publishers},
journal = {Journal of Logic and Algebraic Methods in Programming},
author = {Goubault{-}Larrecq, Jean},
title = {Full Abstraction for Non-Deterministic and Probabilistic
Extensions of {PCF}~{I}: the~Angelic Cases},
volume = 84,
number = 1,
year = 2015,
month = jan,
pages = {155-184},
opteditor = {Berger, Ulrich},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/jgl-jlap14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/jgl-jlap14.pdf},
doi = {10.1016/j.jlamp.2014.09.003},
abstract = {We examine several extensions and variants of Plotkin's
language~PCF, including non-deterministic and probabilistic choice
constructs. For~each, we give an operational and a denotational semantics,
and compare them. In each case, we show soundness and computational
adequacy: the two semantics compute the same values at ground types.
Beyond this, we establish full abstraction (the~observational preorder
coincides with the denotational preorder) in a number of cases. In~the
probabilistic cases, this requires the addition of so-called statistical
termination testers to the language.}
}
@article{BMS-tcs14,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan},
title = {Robust Reachability in Timed Automata and Games: A~Game-based Approach},
volume = 563,
year = {2015},
month = jan,
pages = {43-74},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-tcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-tcs14.pdf},
doi = {10.1016/j.tcs.2014.08.014 },
abstract = {Reachability checking is one of the most basic problems in
verification. By solving this problem in a game, one can synthesize a
strategy that dictates the actions to be performed for ensuring that the
target location is reached. In this work, we are interested in
synthesizing {"}robust{"} strategies for ensuring reachability of a location
in timed automata. By robust, we mean that it must still ensure
reachability even when the delays are perturbed by the environment. We
model this perturbed semantics as a game between the controller and its
environment, and solve the parameterized robust reachability problem: we
show that the existence of an upper bound on the perturbations under which
there is a strategy reaching a target location is EXPTIME-complete. We
also extend our algorithm, with the same complexity, to turn-based timed
games, where the successor state is entirely determined by the environment
in some locations.}
}
@article{FL-sosym14,
publisher = {Springer},
journal = {Software~\& System Modeling},
author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me},
title = {Recent and simple algorithms for {P}etri nets},
volume = 14,
number = 2,
year = {2015},
month = may,
pages = {719-725},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FL-sosym14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FL-sosym14.pdf},
doi = {10.1007/s10270-014-0426-0},
abstract = {We show how inductive invariants can be used to solve
coverability, boundedness and reachability problems for Petri nets. This
approach provides algorithms that are conceptually simpler than previously
pblished ones.}
}
@article{KS-msttocs14,
publisher = {Springer},
journal = {Theory of Computing Systems},
author = {Karandikar, Prateek and Schnoebelen, {\relax Ph}ilippe},
title = {Generalized {P}ost Embedding Problems},
year = {2015},
volume = 56,
number = 4,
pages = {697-716},
month = may,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-msttocs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-msttocs14.pdf},
doi = {10.1007/s00224-014-9561-9},
abstract = {The Regular Post Embedding Problem extended with partial
(co)directness is shown decidable. This extends to universal and\slash or
counting versions. It is also shown that combining directness and
codirectness in Post Embedding problems leads to undecidability.}
}
@article{BBMU-lmcs14,
journal = {Logical Methods in Computer Science},
author = {Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas
and Ummels, Michael},
title = {Pure {N}ash Equilibria in Concurrent Games},
volume = {11},
number = {2:9},
nopages = {},
month = jun,
year = 2015,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBMU-lmcs15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBMU-lmcs15.pdf},
doi = {10.2168/LMCS-11(2:9)2015},
abstract = {We study pure-strategy Nash equilibria in multiplayer concurrent
games, for a variety of omega-regular objectives. For simple objectives
(e.g. reachability, B{\"u}chi objectives), we transform the problem of
deciding the existence of a Nash equilibrium in a given concurrent game
into that of deciding the existence of a winning strategy in a turn-based
two-player game (with a refined objective). We use that transformation to
design algorithms for computing Nash equilibria, which in most cases have
optimal worst-case complexity. For automata-defined objectives, we extend
the above algorithms using a simulation relation which allows us to
consider the product of the game with the automata defining the
objectives. Building on previous algorithms for simple qualitative
objectives, we define and study a semi-quantitative framework, where all
players have several boolean objectives equipped with a preorder; a player
may for instance want to satisfy all her objectives, or to maximise the
number of objectives that she achieves. In most cases, we prove that the
algorithms we obtain match the complexity of the problem they address.}
}
@article{GL-mscs13,
publisher = {Cambridge University Press},
journal = {Mathematical Structures in Computer Science},
author = {Goubault{-}Larrecq, Jean},
title = {A~short proof of the {S}chr{\"o}der-{S}impson theorem},
volume = 25,
number = 1,
year = 2015,
month = jan,
pages = {1-5},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GL-mscs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GL-mscs13.pdf},
doi = {10.1017/S0960129513000467},
abstract = {We give a short and elementary proof of the
Schr{\"o}der-Simpson Theorem, which states that the space of all
continuous maps from a given space~\(X\) to the non-negative reals with their
Scott topology is the cone-theoretic dual of the probabilistic powerdomain
on~\(X\).}
}
@inproceedings{Lozes-fics15,
address = {Berlin, Germany},
month = sep,
year = 2015,
volume = 191,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Matthes, Ralph and Mio, Matteo},
acronym = {{FICS}'15},
booktitle = {{P}roceedings of the 10th {W}orkshop on {F}ixed {P}oints in
{C}omputer {S}cience ({FICS}'15)},
author = {Lozes, {\'{E}}tienne},
title = {A Type-Directed Negation Elimination},
pages = {132-142},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/Lozes-fics15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Lozes-fics15.pdf},
doi = {10.4204/EPTCS.191.12},
abstract = {In the modal mu-calculus, a formula is well-formed if each recursive variable occurs
underneath an even number of negations. By means of De Morgan's laws, it is easy to transform any
well-formed formula into an equivalent formula without negations - its negation normal form. Moreover,
if the formula is of size n, its negation normal form of is of the same size O(n). The full modal
mu-calculus and the negation normal form fragment are thus equally expressive and concise. In this paper
we extend this result to the higher-order modal fixed point logic (HFL), an extension of the modal
mu-calculus with higher-order recursive predicate transformers. We present a procedure that converts a
formula into an equivalent formula without negations of quadratic size in the worst case and of linear
size when the number of variables of the formula is fixed.}
}
@article{LV-scp15,
publisher = {Elsevier Science Publishers},
journal = {Science of Computer Programming},
author = {Lozes, {\'{E}}tienne and
Villard, Jules},
title = {Shared contract-obedient channels},
year = 2015,
month = mar,
volume = {100},
pages = {28-60},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LV-scp15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LV-scp15.pdf},
doi = {10.1016/j.scico.2014.09.008},
abstract = {Recent advances in the formal verification of message-passing programs are based on proving
that programs correctly implement a given protocol. Many existing verification techniques for
message-passing programs assume that at most one thread may attempt to send or receive on a channel
endpoint at any given point in time, and expressly forbid endpoint sharing. Approaches that do allow such
sharing often do not prove that channels obey their protocols. In this paper, we identify two principles
that can guarantee obedience to a communication protocol even in the presence of endpoint sharing. Firstly,
threads may concurrently use an endpoint in any way that does not advance the state of the protocol.
Secondly, threads may compete for receiving on an endpoint provided that the successful reception
of the message grants them ownership of that endpoint retrospectively. We develop a program logic
based on separation logic that unifies these principles and allows fine-grained reasoning about
endpoint-sharing programs. We demonstrate its applicability on a number of examples.
The program logic is shown sound against an operational semantics of programs, and
proved programs are guaranteed to follow the given protocols and to be free of data races, memory leaks,
and communication errors.}
}
@inproceedings{LL-fct15,
address = {Gda{\'{n}}sk, Poland},
month = aug,
year = 2015,
volume = 9210,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Kosowski, Adrian and Walukiewicz, Igor},
acronym = {{FCT}'15},
booktitle = {{P}roceedings of the 20th {I}nternational {S}ymposium
on {F}undamentals of {C}omputation {T}heory
({FCT}'15)},
author = {Lange, Martin and
Lozes, {\'{E}}tienne},
title = {Conjunctive Visibly-Pushdown Path Queries},
pages = {327-338},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LL-fct15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LL-fct15.pdf},
doi = {10.1007/978-3-319-22177-9_25},
abstract = {Weinvestigateanextensionofconjunctiveregularpathqueries in which path properties and path
relations are defined by visibly push- down automata. We study the problem of query evaluation for
extended conjunctive visibly pushdown path queries and their subclasses, and give a complete picture
of their combined and data complexity. In particular, we introduce a weaker notion called extended
conjunctive reachability queries for which query evaluation has a polynomial data complexity.
We also show that query containment is decidable in 2-EXPTIME for (non-extended) conjunctive visibly
pushdown path queries.}
}
@mastersthesis{m2-dallon,
author = {Dallon, Antoine},
title = {Verification of Cryptographic Protocols : a bound on the number
of agents},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2015},
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-dallon.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-dallon.pdf},
note = {38~pages}
}
@proceedings{KDH-topnoc2015,
editor = {Koutny, Maciej and Desel, J{\"o}rg and Haddad, Serge},
title = {Transactions on {P}etri Nets and Other Models of Concurrency~{X}},
booktitle = {Transactions on {P}etri Nets and Other Models of Concurrency~{X}},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 9410,
year = {2015},
noaddress = {},
url = {http://www.springer.com/978-3-662-48649-8}
}
@misc{cassting-D13,
author = {Markey, Nicolas and Doyen, Laurent and Berwanger, Dietmar},
title = {Models for large-scale systems},
howpublished = {Cassting deliverable~D1.3 (FP7-ICT-601148)},
month = sep,
year = {2015},
note = {17~pages},
type = {Contract Report},
url = {http://www.cassting-project.eu/wp-content/uploads/deliv-13.pdf},
pdf = {http://www.cassting-project.eu/wp-content/uploads/deliv-13.pdf}
}
@misc{cassting-D21,
author = {Geeraerts, Gilles and Dehouck, Samuel and Markey, Nicolas and Larsen, Kim G.},
title = {Efficient algorithms for multi-player games with quantitative aspects},
howpublished = {Cassting deliverable~D2.1 (FP7-ICT-601148)},
month = mar,
year = {2015},
note = {22~pages},
type = {Contract Report},
url = {http://www.cassting-project.eu/wp-content/uploads/deliv-21.pdf},
pdf = {http://www.cassting-project.eu/wp-content/uploads/deliv-21.pdf}
}
@misc{cassting-D63,
author = {Markey, Nicolas and Delaborde, Arthur},
title = {Annual report for Year~2},
howpublished = {Cassting deliverable~D6.3 (FP7-ICT-601148)},
month = may,
year = {2015},
note = {34~pages},
type = {Contract Report},
nourlnote = {confidentiel}
}
@article{GHKS-tecs15,
publisher = {ACM Press},
journal = {ACM Transactions in Embedded Computing Systems},
author = {Germanos, Vasileios and Haar, Stefan
and Khomenko, Victor and Schwoon, Stefan},
title = {Diagnosability under Weak Fairness},
volume = 14,
number = {4:69},
nopages = {},
month = dec,
year = 2015,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GHKS-tecs15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GHKS-tecs15.pdf},
doi = {10.1145/2832910},
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{BGHLM-fsttcs15,
address = {Bangalore, India},
month = dec,
year = 2015,
volume = {45},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Harsha, Prahladh and Ramalingam, G.},
acronym = {{FSTTCS}'15},
booktitle = {{P}roceedings of the 35th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'15)},
author = {Brihaye, {\relax Th}omas and Geeraerts, Gilles and Haddad,
Axel and Lefaucheux, Engel and Monmege, Benjamin},
title = {Simple Priced Timed Games Are Not That Simple},
pages = {278-292},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGHLM-fsttcs15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGHLM-fsttcs15.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2015.278},
abstract = {Priced timed games are two-player zero-sum games played on
priced timed automata (whose locations and transitions are labeled by
weights modeling the costs of spending time in a state and executing an
action, respectively). The goals of the players are to minimise and
maximise the cost to reach a target location, respectively. We consider
priced timed games with one clock and arbitrary (positive and negative)
weights and show that, for an important subclass of theirs (the so-called
simple priced timed games), one can compute, in exponential time, the
optimal values that the players can achieve, with their associated optimal
strategies. As side results, we also show that one-clock priced timed
games are determined and that we can use our result on simple priced timed
games to solve the more general class of so-called reset-acyclic priced
timed games (with arbitrary weights and one-clock).}
}
@inproceedings{MLBHB-vecos15,
address = {Bucharest, Romania},
month = sep,
year = 2015,
volume = {1431},
series = {CEUR Workshop Proceedings},
publisher = {RWTH Aachen, Germany},
editor = {Ben{~}Hedia, Belgacem and Popentiu{ }Vladicescu, Florin},
acronym = {{VECoS}'15},
booktitle = {{P}roceedings of the 9th {W}orkshop on {V}erification and
{E}valuation of {C}omputer and {C}ommunication
{S}ystems({VECoS}'15)},
author = {Methni, Amira and Lemerre, Matthieu and Ben{~}Hedia,
Belgacem and Haddad, Serge and Barkaoui, Kamel},
title = {State Space Reduction Strategie for Model Checking
Concurrent {C}~Programs},
pages = {65-76},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/MLBHB-vecos15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/MLBHB-vecos15.pdf},
abstract = {Model checking is an effective technique for uncovering subtle
errors in concurrent systems. Unfortunately, the state space explosion is
the main bottleneck in model checking tools. Here we propose a state space
reduction technique for model checking concurrent programs written in~C.
The reduction technique consists in an analysis phase, which defines an
approximate agglomeration predicate. This latter states whether a
statement can be agglomerated or~not. We~implement this predicate using a
syntactic analysis, as well as a semantic analysis based on abstract
interpretation. We show the usefulness of using agglomeration technique to
reduce the state space, as well as to generate an abstract TLA+
specification from a~C~program.}
}
@inproceedings{BHHHS-cdc15,
address = {Osaka, Japan},
month = dec,
year = 2015,
publisher = {{IEEE} Control System Society},
noeditor = {},
acronym = {{CDC}'15},
booktitle = {{P}roceedings of the 54th {IEEE} {C}onference on
{D}ecision and {C}ontrol ({CDC}'15)},
author = {B{\"o}hm, Stanislav and Haar, Stefan and Haddad, Serge and
Hofman, Piotr and Schwoon, Stefan},
title = {Active Diagnosis with Observable Quiescence},
pages = {1663-1668},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHHHS-cdc15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHHHS-cdc15.pdf},
doi = {10.1109/CDC.2015.7402449},
abstract = {Active diagnosis of a discrete-event system consists in
controlling the system such that faults can be detected. Here we extend
the framework of active diagnosis by introducing modalities for actions
and states and a new capability for the controller, namely observing that
the system is quiescent. We design a game-based construction for both the
decision and the synthesis problems that is computationally optimal.
Furthermore we prove that the size and the delay provided by the active
diagnoser (when it exists) are almost optimal.}
}
@article{AGMN-tcs15,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Akshay, S. and Gastin, Paul and Mukund,
Madhavan and Kumar, K. Narayan},
title = {Checking conformance for time-constrained scenario-based specifications},
volume = {594},
pages = {24-43},
month = aug,
year = {2015},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGMN-tcs15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGMN-tcs15.pdf},
doi = {10.1016/j.tcs.2015.03.030},
abstract = {We consider the problem of model checking message-passing
systems with real-time requirements. As behavioral specifications, we use
message sequence charts (MSCs) annotated with timing constraints. Our
system model is a network of communicating finite state machines with
local clocks, whose global behavior can be regarded as a timed automaton.
Our goal is to verify that all timed behaviors exhibited by the system
conform to the timing constraints imposed by the specification. In
general, this corresponds to checking inclusion for timed languages, which
is an undecidable problem even for timed regular languages. However, we
show that we can translate regular collections of time-constrained MSCs
into a special class of event-clock automata that can be determinized and
complemented, thus permitting an algorithmic solution to the model
checking/conformance problem.}
}
@inproceedings{BV-fsttcs15,
address = {Bangalore, India},
month = dec,
year = 2015,
volume = {45},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Harsha, Prahladh and Ramalingam, G.},
acronym = {{FSTTCS}'15},
booktitle = {{P}roceedings of the 35th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'15)},
author = {Berwanger, Dietmar and Van{ }den{ }Bogaard, Marie},
title = {Games with Delays. A~{F}rankenstein Approach},
pages = {307-319},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BV-fsttcs15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BV-fsttcs15.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2015.307},
abstract = {We investigate infinite games on finite graphs where the
information flow is perturbed by non-deterministic signalling delays. It
is known that such perturbations make synthesis problems virtually
unsolvable, in the general case. On the classical model where signals are
attached to states, tractable cases are rare and difficult to identify. In
this paper, we propose a model where signals are detached from control
states, and we identify a subclass on which equilibrium outcomes can be
preserved, even if signals are delivered with a delay that is finitely
bounded. To offset the perturbation, our solution procedure combines
responses from a collection of virtual plays following an equilibrium
strategy in the instant-signalling game to synthesise, in a
Dr.~Frankenstein manner, an equivalent equilibrium strategy for the
delayed-signalling game.}
}
@inproceedings{KS-fsttcs15,
address = {Bangalore, India},
month = dec,
year = 2015,
volume = {45},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Harsha, Prahladh and Ramalingam, G.},
acronym = {{FSTTCS}'15},
booktitle = {{P}roceedings of the 35th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'15)},
author = {Karandikar, Prateek and Schnoebelen, {\relax Ph}ilippe},
title = {Decidability in the logic of subsequences and supersequences},
pages = {84-97},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-fsttcs15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-fsttcs15.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2015.84},
abstract = {We consider first-order logics of sequences ordered by the
subsequence ordering, aka sequence embedding. We show that the
\(\Sigma_{2}\)-theory is undecidable, answering a question left open by
Kuske. Regarding fragments with a bounded number of variables, we show
that the \(\textsf{FO}^{2}\)-theory is decidable while the
\(\textsf{FO}^{3}\)-theory is undecidable.}
}
@inproceedings{BGM-fsttcs15,
address = {Bangalore, India},
month = dec,
year = 2015,
volume = {45},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Harsha, Prahladh and Ramalingam, G.},
acronym = {{FSTTCS}'15},
booktitle = {{P}roceedings of the 35th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'15)},
author = {Bouyer, Patricia and Gardy, Patrick and Markey, Nicolas},
title = {Weighted strategy logic with boolean goals over one-counter games},
pages = {69-83},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-fsttcs15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-fsttcs15.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2015.69},
abstract = {Strategy Logic is a powerful specification language for
expressing non-zero-sum properties of multi-player games. SL conveniently
extends the logic ATL with explicit quantification and assignment of
strategies. In this paper, we consider games over one-counter automata,
and a quantitative extension 1cSL of SL with assertions over the value of
the counter. We prove two results: we first show that, if decidable, model
checking the so-called Boolean-goal fragment of 1cSL has non-elementary
complexity; we actually prove the result for the Boolean-goal fragment of
SL over finite-state games, which was an open question in (Mogavero
\emph{et~al.} Reasoning about strategies: On the model-checking problem.
2014). As a first step towards proving decidability, we then show that the
Boolean-goal fragment of 1cSL over one-counter games enjoys a nice
periodicity property.}
}
@inproceedings{adhs15-HT,
address = {Atlanta, Georgia, USA},
month = oct,
year = 2015,
number = 27,
volume = 48,
series = {IFAC-PapersOnLine},
publisher = {Elsevier Science Publishers},
editor = {Lennartson, Bengt and Tabuada, Paulo},
acronym = {{ADHS}'15},
booktitle = {{P}roceedings of the 5th {IFAC} {C}onference on {A}nalysis and
{D}esign of {H}ybrid {S}ystems ({ADHS}'15)},
author = {Haar, Stefan and Theissing, Simon},
title = {A~Hybrid-Dynamical Model for Passenger-flow in Transportation
Systems},
pages = {236-241},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/adhs15-HT.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/adhs15-HT.pdf},
doi = {10.1016/j.ifacol.2015.11.181},
abstract = {In a network with different transportation modes, or multimodal
public transportation system (MPTS), modes are linked among one another
not by resources or infrastructure elements---which are not shared, e.g.,
between different metro lines---but by the flow of passengers between
them. Now, the movements of passengers are steered by the destinations
that individual passengers have, and by which they can be grouped into
trip profiles. To use the strength of fluid dynamics, we therefore
introduce a multiphase hybrid Petri net model, in which the vehicle
dynamics is rendered by individual tokens moving in an infrastructure net,
while passenger quantities are given as vectors---whose components
correspond to trip profiles---and evolve at stations according to fluid
dynamics. This model is intended as a building block for obtaining
supervisory control, via transport operator actions, to mitigate
congestion.}
}
@inproceedings{ncma2015-bou,
address = {Porto, Portugal},
month = aug,
year = 2015,
volume = 318,
series = {books@ocg.at},
publisher = {Austrian Computer Society},
editor = {Freund, Rudolf and Holzer, Markus and Moreira, Nelma and Reis, Rog{\'e}rio},
acronym = {{NCMA}'15},
booktitle = {{P}roceedings of the 7th {W}orkshop on {N}on-{C}lassical {M}odels
of {A}utomata and {A}pplications ({NCMA}'15)},
author = {Bouyer, Patricia},
title = {On the optimal reachability problem in weighted timed automata and
games},
pages = {11-36},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ncma15-bou.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ncma15-bou.pdf},
abstract = {In these notes, we survey works made on the models of weighted
timed automata and games, and more specifically on the optimal
reachability problem.}
}
@inproceedings{MAS-sigspatial15,
address = {Seattle, Washington, USA},
month = nov,
year = 2015,
editor = {Ali, Mohamed and Huang Yan and Gertz, Michael and Renz,
Matthias and Sankaranarayanan, Jagan},
acronym = {{GIS}'15},
booktitle = {{P}roceedings of the 23rd {ACM} {SIGSPATIAL}
{I}nternational {C}onference on {A}dvances
in {G}eographic {I}nformation {S}ystems
({GIS}'15)},
author = {Montoya, David and Abiteboul, Serge and Senellart, Pierre},
title = {Hup-Me: Inferring and Reconciling a Timeline of User Activity
with Smartphone and Personal Data},
pages = {62:1-4},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/MAS-sigspatial15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/MAS-sigspatial15.pdf},
doi = {10.1145/2820783.2820852},
abstract = {We designed a system to infer multimodal itineraries traveled by
a user from a combination of smartphone sensor data (e.g., GPS, Wi-Fi,
accelerometer) and knowledge of the transport network infrastructure
(e.g., road and rail maps, public transportation timetables). The system
uses a Transportation network that captures the set of possible paths of
this network for the modes, e.g., foot, bicycle, road_vehicle, and rail.
This Transportation network is constructed from OpenStreetMap data and
public transportation routes published online by transportation agencies
in GTFS format. The system infers itineraries from a sequence of
smartphone observations in two phases. The first phase uses a dynamic
Bayesian network that models the probabilistic relationship between paths
in Transportation network and sensor data. The second phase attempts to
match portions recognized as road_vehicle or rail with possible public
transportation routes of type bus, train, metro, or tram extracted from
the GTFS source. We evaluated the performance of our system with data from
users traveling over the Paris area who were asked to record data for
different trips via an Android application. Itineraries were annotated
with modes and public transportation routes taken and we report on the
results of the recognition.}
}
@article{CCD-tocl15,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Chr{\'e}tien, R{\'e}my and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
title = {From security protocols to pushdown automata},
volume = {17},
number = {1:3},
nopages = {},
year = 2015,
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-tocl15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-tocl15.pdf},
doi = {10.1145/2811262},
abstract = {Formal methods have been very successful in analyzing security
protocols for reachability properties such as secrecy or authentication.
In contrast, there are very few results for equivalence-based properties,
crucial for studying e.g. privacy-like properties such as anonymity or
vote secrecy.\par
We study the problem of checking equivalence of security protocols for an
unbounded number of sessions. Since replication leads very quickly to
undecidability (even in the simple case of secrecy), we focus on a limited
fragment of protocols (standard primitives but pairs, one variable per
protocol's rules) for which the secrecy preservation problem is known to
be decidable. Surprisingly, this fragment turns out to be undecidable for
equivalence. Then, restricting our attention to deterministic protocols,
we propose the first decidability result for checking equivalence of
protocols for an unbounded number of sessions. This result is obtained
through a characterization of equivalence of protocols in terms of
equality of languages of (generalized, real-time) deterministic pushdown
automata. We further show that checking for equivalence of protocols is
actually equivalent to checking for equivalence of generalized, real-time
deterministic pushdown automata.\par
Very recently, the algorithm for checking for equivalence of deterministic
pushdown automata has been implemented. We have implemented our
translation from protocols to pushdown automata, yielding the first tool
that decides equivalence of (some class of) protocols, for an unbounded
number of sessions. As an application, we have analyzed some protocols of
the literature including a simplified version of the basic access control
(BAC) protocol used in biometric passports.}
}
@inproceedings{CCD-esorics15,
address = {Vienna, Austria},
month = sep,
year = 2015,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ryan, Peter and Weippl, Edgar},
acronym = {{ESORICS}'15},
booktitle = {{P}roceedings of the 20th {E}uropean {S}ymposium on
{R}esearch in {C}omputer {S}ecurity ({ESORICS}'15)},
author = {Chr{\'e}tien, R{\'e}my and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
title = {Checking trace equivalence: How to get rid of nonces?},
pages = {230-251},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-esorics15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-esorics15.pdf},
doi = {10.1007/978-3-319-24177-7_12},
abstract = {Security protocols can be successfully analysed using formal
methods. When proving security in symbolic settings for an unbounded
number of sessions, a typical technique consists in abstracting away fresh
nonces and keys by a bounded set of constants. While this abstraction is
clearly sound in the context of secrecy properties (for protocols without
else branches), this is no longer the case for equivalence properties.\par
In this paper, we study how to soundly get rid of nonces in the context of
equivalence properties. We show that nonces can be replaced by constants
provided that each nonce is associated to two constants (instead of
typically one constant for secrecy properties). Our result holds for
deterministic (simple) protocols and a large class of primitives that
includes e.g. standard primitives, blind signatures, and zero-knowledge
proofs.}
}
@phdthesis{karandikar-phd15,
author = {Karandikar, Prateek},
title = {Subwords: automata, embedding problems, and verification},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France and Chennai Mathematical Institute, India},
type = {Th{\`e}se de doctorat},
year = 2015,
month = feb,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/karandikar-phd15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/karandikar-phd15.pdf}
}
@phdthesis{francis-phd15,
author = {Francis, Nadime},
title = {View-based Query Determinacy and Rewritings over Graph Databases},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2015,
month = dec,
url = {https://tel.archives-ouvertes.fr/tel-01247115}
}
@phdthesis{reichert-phd15,
author = {Reichert, Julien},
title = {D{\'e}cidabilit{\'e} et complexit{\'e} de jeux
d'accessibilit{\'e} sur des syst{\`e}mes {\`a} compteurs},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2015,
month = jul,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/reichert-phd15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/reichert-phd15.pdf}
}
@inproceedings{FGMMP-rp15,
address = {Warsaw, Poland},
month = sep,
year = 2015,
volume = {9328},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Boja{\'n}czyk, Miko{\l}aj and Lasota, S{\l}awomir and Potapov, Igor},
acronym = {{RP}'15},
booktitle = {{P}roceedings of the 9th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'15)},
author = {Fribourg, Laurent and Goubault, {\'E}ric and Mohamed, Sameh
and Mrozek, Marian and Putot, Sylvie},
title = {A~Topological Method for Finding Invariants of
Continuous Systems},
pages = {63-75},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FGMMP-rp15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FGMMP-rp15.pdf},
doi = {10.1007/978-3-319-24537-9_7},
abstract = {A~usual way to find positive invariant sets of ordinary
differential equations is to restrict the search to predefined finitely
generated shapes, such as linear templates, or ellipsoids as in classical
quadratic Lyapunov function based approaches. One then looks for
generators or parameters for which the corresponding shape has the
property that the flow of the ODE goes inwards on its border. But for
non-linear systems, where the structure of invariant sets may be very
complicated, such simple predefined shapes are generally not well suited.
The present work proposes a more general approach based on a topological
property, namely Wa\.{z}ewski's property. Even for complicated non-linear
dynamics, it is possible to successfully restrict the search for isolating
blocks of simple shapes, that are bound to contain non-empty invariant
sets. This approach generalizes the Lyapunov-like approaches, by allowing
for inwards and outwards flow on the boundary of these shapes, with extra
topological conditions. We developed and implemented an algorithm based on
Wa\.{z}ewski's property, SOS optimization and some extra combinatorial and
algebraic properties, that shows very nice results on a number of
classical polynomial dynamical systems.}
}
@inproceedings{LS-rp15,
address = {Warsaw, Poland},
month = sep,
year = 2015,
volume = {9328},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Boja{\'n}czyk, Miko{\l}aj and Lasota, S{\l}awomir and Potapov, Igor},
acronym = {{RP}'15},
booktitle = {{P}roceedings of the 9th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'15)},
author = {Lazi{\'c}, Ranko and Schmitz, Sylvain},
title = {The Ideal View on {R}ackoff's Coverability Technique},
pages = {76-88},
url = {https://hal.inria.fr/hal-01176755},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-rp15.pdf},
doi = {10.1007/978-3-319-24537-9_8},
abstract = {Rackoff's small witness property for the coverability problem
is the standard means to prove tight upper bounds in vector addition
systems (VAS) and many extensions. We show how to derive the same bounds
directly on the computations of the VAS instantiation of the generic
backward coverability algorithm. This relies on a dual view of the
algorithm using ideal decompositions of downwards-closed sets, which
exhibits a key structural invariant in the VAS case. The same reasoning
readily generalises to several VAS extensions.}
}
@inproceedings{BHPSS-rp15,
address = {Warsaw, Poland},
month = sep,
year = 2015,
volume = {9328},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Boja{\'n}czyk, Miko{\l}aj and Lasota, S{\l}awomir and Potapov, Igor},
acronym = {{RP}'15},
booktitle = {{P}roceedings of the 9th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'15)},
author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Picaronny,
Claudine and Safey{ }El{~}Din, Mohab and Sassolas, Mathieu},
title = {Polynomial Interrupt Timed Automata},
pages = {20-32},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHPSS-rp15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHPSS-rp15.pdf},
doi = {10.1007/978-3-319-24537-9_3},
abstract = {Interrupt Timed Automata (ITA) form a subclass of stopwatch
automata where reachability and some variants of timed model checking are
decidable even in presence of parameters. They are well suited to model
and analyze real-time operating systems. Here we extend ITA with
polynomial guards and updates, leading to the class of polynomial ITA
(PolITA). We prove that reachability is decidable in 2EXPTIME on PolITA,
using an adaptation of the cylindrical decomposition method for the
first-order theory of reals. Compared to previous approaches, our
procedure handles parameters and clocks in a unified way. We also obtain
decidability for the model checking of a timed version of CTL and for
reachability in several extensions of PolITA.}
}
@inproceedings{BFM-avocs15,
address = {Edinburgh, UK},
month = sep,
year = {2015},
volume = 72,
series = {Electronic Communications of the EASST},
publisher = {European Association of Software Science and Technology},
editor = {Grov, Gudmund and Ireland, Andrew},
acronym = {{AVoCS}'15},
booktitle = {{P}roceedings of the 15th {I}nternational
{W}orkshop on {A}utomated {V}erification
of {C}ritical {S}ystems
({AVoCS}'15)},
author = {Bouyer, Patricia and Fang, Erwin and Markey, Nicolas},
title = {Permissive strategies in timed automata and games},
nopages = {263-277},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFM-avocs15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFM-avocs15.pdf},
doi = {10.14279/tuj.eceasst.72.1015},
abstract = {Timed automata are a convenient framework for modelling and
reasoning about real-time systems. While these models are now very
well-understood, they do not offer a convenient way of taking timing
imprecisions into account. Several solutions (e.g. parametric guard
enlargement) have recently been proposed over the last ten years to take
such imprecisions into account. In this paper, we propose a new approach
for handling robust reachability, based on permissive strategies. While
classical strategies propose to play an action at an exact point in time,
permissive strategies return an interval of possible dates when to play
the selected action. With such a permissive strategy, we associate a
penalty, which is the inverse of the length of the proposed interval, and
accumulates along the run. We show that in that setting, optimal
strategies can be computed in polynomial time for one-clock timed
automata.}
}
@inproceedings{B-time15,
address = {Kassel, Germany},
month = sep,
year = 2015,
publisher = {{IEEE} Computer Society Press},
editor = {Grandi, Fabio and Lange, Martin and Lomuscio, Alessio},
acronym = {{TIME}'15},
booktitle = {{P}roceedings of the 22nd {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'15)},
author = {Bollig, Benedikt},
title = {Towards Formal Verification of Distributed Algorithms},
pages = {3},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/B-time15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/B-time15.pdf},
doi = {10.1109/TIME.2015.23}
}
@inproceedings{B-ciaa15,
address = {Ume{\aa}, Sweden},
month = aug,
year = 2015,
volume = {9223},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Drewes, Frank},
acronym = {{CIAA}'15},
booktitle = {{P}roceedings of the 20th {I}nternational
{C}onference on {I}mplementation and
{A}pplication of {A}utomata
({CIAA}'15)},
author = {Bollig, Benedikt},
title = {Automata and Logics for Concurrent Systems: Five Models in Five
Pages},
pages = {3-12},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/B-ciaa15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/B-ciaa15.pdf},
doi = {10.1007/978-3-319-22360-5_1},
abstract = {We~survey various automata models of concurrent systems and
their connection with monadic second-order logic: finite automata, class
memory automata, nested-word automata, asynchronous automata, and
message-passing automata.}
}
@inproceedings{RG-bda15,
address = {{\^I}le de Porquerolles, France},
month = sep,
year = 2015,
noeditor = {},
acronym = {{BDA}'15},
booktitle = {{A}ctes de la 31{\`e}me {C}onf{\'e}rence sur la {G}estion de
{D}onn{\'e}es~-- {P}rincipes, {T}echnologies et
{A}pplications ({BDA}'15)},
author = {Rafes, Karima and Germain, C{\'e}cile},
title = {A~platform for scientific data sharing},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/RG-bda15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RG-bda15.pdf},
abstract = {In this paper, we use the semantic web technology, notably RDF,
SPARQL and Linked Open Data in the context of scientific data sharing.
More precisely, we present the LinkedWiki platform that is being developed
at the Center for Data Science of Paris-Saclay University for scientific
data integration. The~goal is to facilitate the discovery and exploitation
of scientists' datasets by their colleagues. For this, we notably rely on
the use by scientists of Wikipedia for specifying the semantics of
datasets, and the use of Wikidata (the~Wikipedia's knowledge base)
identifiers for annotating these datasets and thereby facilitating their
discovery.}
}
@inproceedings{BMRLL-gandalf15,
address = {Genova, Italy},
month = sep,
year = 2015,
volume = {193},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Esparza, Javier and Tronci, Enrico},
acronym = {{GandALF}'15},
booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
({GandALF}'15)},
author = {Bouyer, Patricia and Markey, Nicolas and Randour, Mickael
and Larsen, Kim G. and Laursen, Simon},
title = {Average-energy games},
pages = {1-15},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMRLL-gandalf15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMRLL-gandalf15.pdf},
doi = {10.4204/EPTCS.193.1},
abstract = {Two-player quantitative zero-sum games provide a natural
framework to synthesize controllers with performance guarantees for
reactive systems within an uncontrollable environment. Classical settings
include mean-payoff games, where the objective is to optimize the long-run
average gain per action, and energy games, where the system has to avoid
running out of energy.\par
We study \emph{average-energy} games, where the goal is to optimize the
long-run average of the accumulated energy. We show that this objective
arises naturally in several applications, and that it yields interesting
connections with previous concepts in the literature. We prove that
deciding the winner in such games is in
\textsf{NP}{{\(\cap\)}}\textsf{coNP} and at least as hard as solving
mean-payoff games, and we establish that memoryless strategies suffice to
win. We also consider the case where the system has to minimize the
average-energy while maintaining the accumulated energy within predefined
bounds at all times: this corresponds to operating with a finite-capacity
storage for energy. We give results for one-player and two-player games,
and establish complexity bounds and memory requirements.}
}
@inproceedings{LMS-gandalf15,
address = {Genova, Italy},
month = sep,
year = 2015,
volume = {193},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Esparza, Javier and Tronci, Enrico},
acronym = {{GandALF}'15},
booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
({GandALF}'15)},
author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and
Sangnier, Arnaud},
title = {{{\(\textsf{ATL}_{\textsf{sc}}\)}} with partial observation},
pages = {43-57},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LMS-gandalf15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LMS-gandalf15.pdf},
doi = {10.4204/EPTCS.193.4},
abstract = {Alternating-time temporal logic with strategy contexts
({{\(\textsf{ATL}_{\textsf{sc}}\)}}) is a powerful formalism for
expressing properties of multi-agent systems: it~extends \textsf{CTL} with
\emph{strategy quantifiers}, offering a convenient way of expressing both
collaboration and antagonism between several agents. Incomplete
observation of the state space is a desirable feature in such a framework,
but it quickly leads to undecidable verification problems. In this paper,
we prove that \emph{uniform} incomplete observation (where all players
have the same observation) preserves decidability of the model checking
problem, even for very expressive logics such as
{{\(\textsf{ATL}_{\textsf{sc}}\)}}.}
}
@inproceedings{BV-dlt15,
address = {Liverpool, UK},
month = jul,
year = 2015,
volume = {9168},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Potapov, Igor},
acronym = {{DLT}'15},
booktitle = {{P}roceedings of the 19th {I}nternational
{C}onference on {D}evelopments in {L}anguage {T}heory
({DLT}'15)},
author = {Berwanger, Dietmar and Van{ }den{ }Bogaard, Marie},
title = {Consensus Game Acceptors},
pages = {108-119},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BV-dlt15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BV-dlt15.pdf},
doi = {10.1007/978-3-319-21500-6_8},
abstract = {We study a game for recognising formal languages, in which two
players with imperfect information need to coordinate on a common
decision, given private input strings correlated by a finite graph. The
players have a joint objective to avoid an inadmissible decision, in spite
of the uncertainty induced by the input.\par
We show that the acceptor model based on consensus games characterises
context-sensitive languages, and conversely, that winning strategies in
such games can be described by context-sensitive languages. We also
discuss consensus game acceptors with a restricted observation pattern
that describe nondeterministic linear-time languages.}
}
@inproceedings{BMV-atva15,
address = {Shanghai, China},
month = oct,
year = {2015},
volume = {9364},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Finkbeiner, Bernd and Pu, Geguang and Zhang, Lijun},
acronym = {{ATVA}'15},
booktitle = {{P}roceedings of the 13th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'15)},
author = {Berwanger, Dietmar and Mathew, Anup Basil and
Van{ }den{ }Bogaard, Marie},
title = {Hierarchical Information Patterns and Distributed Strategy Synthesis},
pages = {378-393},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-atva15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-atva15.pdf},
doi = {10.1007/978-3-319-24953-7_28},
abstract = {Infinite games with imperfect information tend to be
undecidable unless the information flow is severely restricted. One
fundamental decidable case occurs when there is a total ordering among
players, such that each player has access to all the information that the
following ones receive.\par
In this paper we consider variations of this hierarchy principle for
synchronous games with perfect recall, and identify new decidable classes
for which the distributed synthesis problem is solvable with finite-state
strategies. In particular, we show that decidability is maintained when
the information hierarchy may change along the play, or when transient
phases without hierarchical information are allowed.}
}
@inproceedings{PRCHH-atva15,
address = {Shanghai, China},
month = oct,
year = {2015},
volume = {9364},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Finkbeiner, Bernd and Pu, Geguang and Zhang, Lijun},
acronym = {{ATVA}'15},
booktitle = {{P}roceedings of the 13th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'15)},
author = {Ponce{ }de{~}Le{\'o}n, Hern{\'a}n and Rodr{\'\i}guez,
C{\'e}sar and Carmona, Josep and Heljanko, Keijo and Haar, Stefan},
title = {Unfolding-Based Process Discovery},
pages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/PRCHH-atva15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PRCHH-atva15.pdf},
doi = {10.1007/978-3-319-24953-7_4},
abstract = {This paper presents a novel technique for process discovery. In
contrast to the current trend, which only considers an event log for
discovering a process model, we assume two additional inputs: an
independence relation on the set of logged activities, and a collection of
negative traces. After deriving an intermediate net unfolding from them,
we perform a controlled folding giving rise to a Petri net which contains
both the input log and all independence-equivalent traces arising from~it.
Remarkably, the derived Petri net cannot execute any trace from the
negative collection. The entire chain of transformations is fully
automated. A tool has been developed and experimental results are provided
that witness the significance of the contribution of this paper.}
}
@inproceedings{BDS-csl15,
address = {Berlin, Germany},
month = sep,
year = 2015,
volume = {41},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Kreuzer, Stephan},
acronym = {{CSL}'15},
booktitle = {{P}roceedings of the 24th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'15)},
author = {Baelde, David and Doumane, Amina and Saurin, Alexis},
title = {Least and Greatest Fixed Points in Ludics},
pages = {549-566},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDS-csl15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDS-csl15.pdf},
doi = {10.4230/LIPIcs.CSL.2015.549},
abstract = {Various logics have been introduced in order to reason over
(co)inductive specifications and, through the Curry-Howard correspondence,
to study computation over inductive and coinductive data. The logic mu-MALL
is one of those logics, extending multiplicative and additive linear logic
with least and greatest fixed point operators.\par
In this paper, we investigate the semantics of mu-MALL proofs in
(computational) ludics. This framework is built around the notion of
design, which can be seen as an analogue of the strategies of game
semantics. The infinitary nature of designs makes them particularly well
suited for representing computations over infinite data.\par
We provide mu-MALL with a denotational semantics, interpreting proofs by
designs and formulas by particular sets of designs called behaviours. Then
we prove a completeness result for the class of {"}essentially finite
designs{"}, which are those designs performing a finite computation followed
by a copycat. On the way to completeness, we investigate semantic
inclusion, proving its decidability (given two formulas, we can decide
whether the semantics of one is included in the other's) and completeness
(if semantic inclusion holds, the corresponding implication is provable in
mu-MALL).}
}
@article{CLMT-dagstuhl15,
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
journal = {Dagstuhl Reports},
editor = {Chatterjee, Krishnendu and Lafortune, St{\'e}phane and
Markey, Nicolas and Thomas, Wolfgang},
author = {Chatterjee, Krishnendu and Lafortune, St{\'e}phane and
Markey, Nicolas and Thomas, Wolfgang},
title = {Non-Zero-Sum-Games and Control ({D}agstuhl Seminar~15061)},
pages = {1-25},
year = {2015},
volume = {5},
number = {2},
month = jun,
url = {http://drops.dagstuhl.de/opus/volltexte/2015/5042},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CLMT-dagstuhl15.pdf},
doi = {10.4230/DagRep.5.2.1},
abstract = {In this report, the program, research issues, and results of
Dagstuhl Seminar 15061 {"}Non-Zero-Sum-Games and Control{"} are described.
The area of non-zero-sum games is addressed in a wide range of topics:
multi-player games, partial-observation games, quantitative game models,
and---as~a special focus---connections with control engineering
(supervisory control).}
}
@inproceedings{HPRV-ppdp15,
address = {Siena, Italy},
month = jul,
year = 2015,
publisher = {ACM Press},
editor = {Albert, Elvira},
acronym = {{PPDP}'15},
booktitle = {{P}roceedings of the 17th {I}nternational
{C}onference on {P}rinciples and {P}ractice of {D}eclarative
{P}rogramming ({PPDP}'15)},
author = {Haar, Stefan and Perchy, Salim and Rueda, Camilo and
Valencia, Franck},
title = {An Algebraic View of Space{{\slash}}Belief and
Extrusion{{\slash}}Utterance for
Concurrency{{\slash}}Epistemic Logic},
pages = {161-172},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HPRV-ppdp15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HPRV-ppdp15.pdf},
doi = {10.1007/978-3-319-19488-2_6},
abstract = {We enrich spatial constraint systems with operators to specify
information and processes moving from a space to another. We shall refer
to these news structures as spatial constraint systems with extrusion. We
shall investigate the properties of this new family of constraint systems
and illustrate their applications. From a computational point of view the
new operators provide for process\slash information extrusion, a central
concept in formalisms for mobile communication. From an epistemic point of
view extrusion corresponds to a notion we shall call utterance; a~piece of
information that an agent communicates to others but that may be
inconsistent with the agent's beliefs. Utterances can then be used to
express instances of epistemic notions, which are common place in social
media, such as hoaxes or intentional lies. Spatial constraint systems with
extrusion can be seen as complete Heyting algebras equipped with maps to
account for spatial and epistemic specifications.}
}
@inproceedings{BMPS-formats15,
address = {Madrid, Spain},
month = sep,
year = 2015,
volume = {9268},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Sankaranarayanan, Sriram and Vicario, Enrico},
acronym = {{FORMATS}'15},
booktitle = {{P}roceedings of the 13th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'15)},
author = {Bouyer, Patricia and Markey, Nicolas and Perrin, Nicolas
and Schlehuber, Philipp},
title = {Timed automata abstraction of switched dynamical systems
using control funnels},
pages = {60-75},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMPS-formats15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMPS-formats15.pdf},
doi = {10.1007/978-3-319-22975-1_5},
abstract = {The~development of formal methods for control design is an
important challenge with potential applications in a wide range of
safety-critical cyber-physical systems. Focusing on switched dynamical
systems, we~propose a new abstraction, based on time-varying regions of
invariance (the~\emph{control funnels}), that models behaviors of systems as
timed automata. The main advantage of this method is that it allows
automated verification of formal specifications and reactive controller
synthesis without discretizing the evolution of the state of the system.
Efficient constructions are possible in the case of linear dynamics.
We~demonstrate the potential of our approach with two examples.}
}
@inproceedings{AM-formats15,
address = {Madrid, Spain},
month = sep,
year = 2015,
volume = {9268},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Sankaranarayanan, Sriram and Vicario, Enrico},
acronym = {{FORMATS}'15},
booktitle = {{P}roceedings of the 13th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'15)},
author = {Andr{\'e}, {\'E}tienne and Markey, Nicolas},
title = {Language Preservation Problems in Parametric Timed Automata},
pages = {27-43},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AM-formats15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AM-formats15.pdf},
doi = {10.1007/978-3-319-22975-1_3},
abstract = {Parametric timed automata (PTA) are a powerful formalism to
model and reason about concurrent systems with some unknown timing delays.
In this paper, we address the (untimed) language- and trace-preservation
problems: given a reference parameter valuation, does there exist another
parameter valuation with the same untimed language (or trace)? We show
that these problems are undecidable both for general PTA, and even for the
restricted class of L/U-PTA. On the other hand, we exhibit decidable
subclasses: 1-clock PTA, and 1-parameter deterministic L-PTA and U-PTA.}
}
@inproceedings{ABG-concur15,
address = {Madrid, Spain},
month = sep,
year = 2015,
volume = {42},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Aceto, Luca and de Frutos-Escrig, David},
acronym = {{CONCUR}'15},
booktitle = {{P}roceedings of the 26th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'15)},
author = {Aiswarya, C. and Bollig, Benedikt and Gastin, Paul},
title = {An Automata-Theoretic Approach to the Verification of Distributed Algorithms},
pages = {340-353},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-concur15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-concur15.pdf},
doi = {10.4230/LIPIcs.CONCUR.2015.340},
abstract = {We introduce an automata-theoretic method for the verification
of distributed algorithms running on ring networks. In a distributed
algorithm, an arbitrary number of processes cooperate to achieve a common
goal (e.g., elect a leader). Processes have unique identifiers (pids) from
an infinite, totally ordered domain. An algorithm proceeds in synchronous
rounds, each round allowing a process to perform a bounded sequence of
actions such as send or receive a pid, store it in some register, and
compare register contents wrt. the associated total order. An algorithm is
supposed to be correct independently of the number of processes. To
specify correctness properties, we introduce a logic that can reason about
processes and pids. Referring to leader election, it may say that, at the
end of an execution, each process stores the maximum pid in some dedicated
register. Since the verification of distributed algorithms is undecidable,
we propose an underapproximation technique, which bounds the number of
rounds. This is an appealing approach, as the number of rounds needed by a
distributed algorithm to conclude is often exponentially smaller than the
number of processes. We provide an automata-theoretic solution, reducing
model checking to emptiness for alternating two-way automata on words.
Overall, we show that round-bounded verification of distributed algorithms
over rings is PSPACE-complete.}
}
@inproceedings{BDH-concur15,
address = {Madrid, Spain},
month = sep,
year = 2015,
volume = {42},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Aceto, Luca and de Frutos-Escrig, David},
acronym = {{CONCUR}'15},
booktitle = {{P}roceedings of the 26th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'15)},
author = {Baelde, David and Delaune, St{\'e}phanie and Hirschi,
Lucca},
title = {Partial Order Reduction for Security Protocols},
pages = {497-510},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDH-concur15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDH-concur15.pdf},
doi = {10.4230/LIPIcs.CONCUR.2015.497},
abstract = {Security protocols are concurrent processes that communicate
using cryptography with the aim of achieving various security properties.
Recent work on their formal verification has brought procedures and tools
for deciding trace equivalence properties (\textit{e.g.},~anonymity,
unlinkability, vote secrecy) for a bounded number of sessions. However,
these procedures are based on a naive symbolic exploration of all traces
of the considered processes which, unsurprisingly, greatly limits the
scalability and practical impact of the verification tools.\par
In this paper, we mitigate this difficulty by developing partial order
reduction techniques for the verification of security protocols. We
provide reduced transition systems that optimally elim- inate redundant
traces, and which are adequate for model-checking trace equivalence
properties of protocols by means of symbolic execution. We have
implemented our reductions in the tool \textsf{Apte}, and demonstrated
that it achieves the expected speedup on various protocols.}
}
@inproceedings{BJM-concur15,
address = {Madrid, Spain},
month = sep,
year = 2015,
volume = {42},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Aceto, Luca and de Frutos-Escrig, David},
acronym = {{CONCUR}'15},
booktitle = {{P}roceedings of the 26th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'15)},
author = {Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas},
title = {On~the Value Problem in Weighted Timed Games},
pages = {311-324},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BJM-concur15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BJM-concur15.pdf},
doi = {10.4230/LIPIcs.CONCUR.2015.311},
abstract = {A~weighted timed game is a timed game with extra quantitative
information representing e.g. energy consumption. Optimizing the cost for
reaching a target is a natural question, which has been investigated for
ten years. Existence of optimal strategies is known to be undecidable in
general, and only very restricted classes of games have been described for
which optimal cost and almost-optimal strategies can be computed.\par
In this paper, we show that the value problem is undecidable in general
weighted timed games. The undecidability proof relies on that for the
existence of optimal strategies and on a diagonalization construction
recently designed in the context of quantitative temporal logics. We then
provide an algorithm to compute arbitrary approximations of the value in a
game, and almost-optimal strategies. The algorithm applies in a large
subclass of weighted timed games, and is the first approximation scheme
which is designed in the current context.}
}
@inproceedings{CDV-icalp15,
address = {Kyoto, Japan},
month = jul,
year = 2015,
volume = {9135},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Halld{\'o}rsson, Magnus M. and Iwama, Kazuo and Kobayashi,
Naoki and Speckmann, Bettina},
acronym = {{ICALP}'15},
booktitle = {{P}roceedings of the 42nd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'15)~-- {P}art~{II}},
author = {Chatterjee, Krishnendu and Doyen, Laurent and Vardi, Moshe},
title = {The Complexity of Synthesis from Probabilistic Components},
pages = {108-120},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDV-icalp15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDV-icalp15.pdf},
doi = {10.1007/978-3-662-47666-6_9},
abstract = {The synthesis problem asks for the automatic construction of a
system from its specification. In the traditional setting, the system is
{"}constructed from scratch{"} rather than composed from reusable
components. However, this is rare in practice, and almost every
non-trivial software system relies heavily on the use of libraries of
reusable components. Recently, Lustig and Vardi introduced dataflow and
controlflow synthesis from libraries of reusable components. They proved
that dataflow synthesis is undecidable, while controlflow synthesis is
decidable. The problem of controlflow synthesis from libraries of
probabilistic components was considered by Nain, Lustig and Vardi, and was
shown to be decidable for qualitative analysis (that asks that the
specification be satisfied with probability~1). Our main contribution for
controlflow synthesis from probabilistic components is to establish better
complexity bounds for the qualitative analysis problem, and to show that
the more general quantitative problem is undecidable. For the qualitative
analysis, we show that the problem (i)~is EXPTIME-complete when the
specification is given as a deterministic parity word automaton, improving
the previously known 2EXPTIME upper bound; and (ii)~belongs to
UP\(\cap\)coUP and is parity-games hard, when the specification is given
directly as a parity condition on the components, improving the previously
known EXPTIME upper bound.}
}
@inproceedings{JLS-icalp15,
address = {Kyoto, Japan},
month = jul,
year = 2015,
volume = {9135},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Halld{\'o}rsson, Magnus M. and Iwama, Kazuo and Kobayashi,
Naoki and Speckmann, Bettina},
acronym = {{ICALP}'15},
booktitle = {{P}roceedings of the 42nd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'15)~-- {P}art~{II}},
author = {Jurdzi{\'n}ski, Marcin and Lazi{\'c}, Ranko and Schmitz, Sylvain},
title = {Fixed-Dimensional Energy Games are in Pseudo Polynomial Time},
pages = {260-272},
url = {http://arxiv.org/abs/1502.06875},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JLS-arxiv15.pdf},
doi = {10.1007/978-3-662-47666-6_21},
abstract = {We generalise the hyperplane separation technique (Chatterjee
and Velner,~2013) from multi-dimensional mean-payoff to energy games, and
achieve an algorithm for solving the latter whose running time is
exponential only in the dimension, but not in the number of vertices of
the game graph. This answers an open question whether energy games with
arbitrary initial credit can be solved in pseudo-polynomial time for fixed
dimensions~\(3\) or larger (Chaloupka,~2013). It~also improves the complexity
of solving multi-dimensional energy games with given initial credit from
non-elementary (Br\'azdil, Jan\v{c}ar, and Ku\v{c}era,~2010) to 2EXPTIME,
thus establishing their 2EXPTIME-completeness.}
}
@phdthesis{bollig-HDR15,
author = {Bollig, Benedikt},
title = {Automata and Logics for Concurrent Systems: Realizability and Verification},
year = 2015,
month = jun,
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-bollig15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-bollig15.pdf}
}
@inproceedings{CCD-csf15,
address = {Verona, Italy},
month = jul,
year = 2015,
publisher = {{IEEE} Computer Society Press},
acronym = {{CSF}'15},
booktitle = {{P}roceedings of the
28th {IEEE} {C}omputer {S}ecurity {F}oundations
{S}ymposium ({CSF}'15)},
author = {Chr{\'e}tien, R{\'e}my and Cortier, V{\'e}ronique and
Delaune, St{\'e}phanie},
title = {Decidability of trace equivalence for protocols with nonces},
pages = {170-184},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-csf15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-csf15.pdf},
doi = {10.1109/CSF.2015.19},
abstract = {Privacy properties such as anonymity, unlinkability, or vote
secrecy are typically expressed as equivalence properties.\par
In this paper, we provide the first decidability result for trace
equivalence of security protocols, for an unbounded number of sessions and
unlimited fresh nonces. Our class encompasses most symmetric key protocols
of the literature, in their tagged variant.}
}
@inproceedings{MLBHB-ftscs15,
address = {Luxembourg},
optnmonth = 11,
optmonth = nov,
year = 2015,
volume = {476},
series = {Communications in Computer and Information Science},
publisher = {Springer},
editor = {Artho, Cyrille and {\"O}lveczky, Peter Csaba},
acronym = {{FTSCS}'14},
booktitle = {{P}roceedings of the 3rd {I}nternational {W}orkshop on {F}ormal {T}echniques for
{S}afety-{C}ritical {S}ystems, Nov. 2014 ({FTSCS}'14)},
author = {Methni, Amira and Lemerre, Matthieu and Ben{~}Hedia, Belgacem and
Haddad, Serge and Barkaoui, Kamel},
title = {Specifying and Verifying Concurrent {C}~Programs with {TLA+}},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/MLBHB-ftscs15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/MLBHB-ftscs15.pdf},
doi = {10.1007/978-3-319-17581-2_14},
pages = {206-222},
nonote = {17~pages},
abstract = {Verifying software systems automatically from their source code
rather than modelling them in a dedicated language gives more confidence
in establishing their properties. Here we propose a formal specification
and verification approach for concurrent C programs directly based on the
semantics of~C. We define a set of translation rules and implement it in a
tool~(C2TLA+) that automatically translates C code into a TLA+
specification. The~TLC model checker can use this specification to
generate a model, allowing to check the absence of runtime errors and dead
code in the C program in a given configuration. In addition, we show how
translated specifications interact with manually written ones~to: check
the C code against safety or liveness properties; provide concurrency
primitives or model hardware that cannot be expressed in~C; and use
abstract versions of translated C functions to address the state explosion
problem. All these verifications have been conducted on an industrial case
study, which is a part of the microkernel of the PharOS real-time
system.}
}
@article{FH-fundi15,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {Fraca, Est{\'\i}baliz and Haddad, Serge},
title = {Complexity Analysis of Continuous Petri Nets},
volume = 137,
number = {1},
pages = {1-28},
year = 2015,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FH-fundi15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FH-fundi15.pdf},
doi = {10.3233/FI-2015-1168},
abstract = {At the end of the eighties, continuous Petri nets were
introduced for: (1)~alleviating the combinatory explosion triggered by
discrete Petri nets (i.e. usual Petri nets) and, (2)~modelling the
behaviour of physical systems whose state is composed of continuous
variables. Since then several works have established that the
computational complexity of deciding some standard behavioural properties
of Petri nets is reduced in this framework. Here we first establish the
decidability of additional properties like coverability, boundedness and
reachability set inclusion. We also design new decision procedures for
reachability and lim-reachability problems with a better computational
complexity. Finally we provide lower bounds characterising the exact
complexity class of the reachability, the coverability, the boundedness,
the deadlock freeness and the liveness problems. A~small case study is
introduced and analysed with these new procedures.}
}
@article{BHHP-ijasm15,
publisher = {IARIA},
journal = {International Journal on Advances in Systems and Measurements},
author = {Barbot, Beno{\^\i}t and Haddad, Serge and Heiner, Monika and
Picaronny, Claudine},
title = {Rare Event Handling in Signalling Cascades},
volume = 8,
number = {1-2},
pages = {69-79},
year = 2015,
month = jun,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHHP-ijasm15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHHP-ijasm15.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{RNG-ldq15,
address = {Portoro{\v z}, Slovenia},
month = jun,
year = 2015,
volume = {1376},
series = {CEUR Workshop Proceedings},
publisher = {RWTH Aachen, Germany},
editor = {Rula, Anisa and Zaveri, Amrapali and Knuth, Magnus and
Kontokostas, Dimitris},
acronym = {{LDQ}'15},
booktitle = {{P}roceedings of the 2nd {W}orkshop on {L}inked {D}ata {Q}uality
({LDQ}'15)},
author = {Rafes, Karima and Nauroy, Julien and Germain, C{\'e}cile},
title = {Certifying the interoperability of {RDF} database systems},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/RNG-ldq15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RNG-ldq15.pdf},
abstract = {In~March~2013, the W3C recommended SPARQL~1.1 to retrieve and
manipulate decentralized RDF data. Real-world usage requires advanced
features of SPARQL~1.1. recommendations As these are not consistently
implemented, we propose a test framework named TFT (Tests for Triple
stores) to test the interoperability of the SPARQL end-point of RDF
database systems. This framework can execute the W3C's SPARQL~1.1 test
suite and also its own tests of interoperability. To help the developers
and end-users of RDF databases, we perform daily tests on Jena-Fuseki,
Marmotta-KiWistore, 4Store and three other commercial databases. With
these tests, we have built a scoring system named SPARQLScore and share
our results on the website \url{http://sparqlscore.com}.}
}
@inproceedings{RRS-cav15,
address = {San Francisco, CA, USA},
month = jul,
year = 2015,
volume = 9206,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Kroening, Daniel and Pasareanu, Corina},
acronym = {{CAV}'15},
booktitle = {{P}roceedings of the 27th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'15)~-- Part~{I}},
author = {Randour, Mickael and Raskin, Jean-Fran{\c{c}}ois and Sankur, Ocan},
title = {Percentile Queries in Multi-Dimensional {M}arkov Decision Processes},
pages = {123-139},
url = {http://arxiv.org/abs/1410.4801},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RRS-arxiv14.pdf},
doi = {10.1007/978-3-319-21690-4_8},
abstract = {Multi-dimensional weighted Markov decision processes (MDPs) are
useful to analyze systems with multiple objectives that are potentially
conflicting and make necessary the analysis of trade-offs. In this paper,
we study the complexity of percentile queries in such MDPs and provide
algorithms to synthesize strategies that enforce such constraints. Given a
multi-dimensional weighted MDP and a quantitative payoff function~\(f\),
quantitative thresholds~\(v_i\) (one per dimension), and probability
thresholds~\(\alpha_{i}\), we show how to compute a single strategy that
enforces that for all dimension~\(i\), the probability that an
outcome~\(\rho\) satisfies \(f_{i}(\rho) \geq v_{i}\) is at
least~\(\alpha_{i}\). We study this problem for the classical quantitative
payoffs studied in the literature (sup, inf, lim sup, lim inf,
mean-payoff, truncated sum, discounted sum). So our work can be seen as an
extension to the quantitative case of the multi-objective model checking
problem on MDPs studied by Etessami et al. in unweighted MDPs.}
}
@inproceedings{HK-icalp15,
address = {Kyoto, Japan},
month = jul,
year = 2015,
volume = {9135},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Halld{\'o}rsson, Magnus M. and Iwama, Kazuo and Kobayashi,
Naoki and Speckmann, Bettina},
acronym = {{ICALP}'15},
booktitle = {{P}roceedings of the 42nd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'15)~-- {P}art~{II}},
author = {Haase, Christoph and Kiefer, Stefan},
title = {The Odds of Staying on Budget},
pages = {234-246},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HK-icalp15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HK-icalp15.pdf},
doi = {10.1007/978-3-662-47666-6_19},
abstract = {Given Markov chains and Markov decision processes (MDPs) whose
transitions are labelled with non-negative integer costs, we study the
computational complexity of deciding whether the probability of paths
whose accumulated cost satisfies a Boolean combination of inequalities
exceeds a given threshold. For acyclic Markov chains, we show that this
problem is PP-complete, whereas it is hard for the POSSLP problem and in
PS PACE for general Markov chains. Moreover, for acyclic and general MDPs,
we prove PSPACE- and EXP-completeness, respectively. Our results have
direct implications on the complexity of computing reward quantiles in
succinctly represented stochastic systems.}
}
@inproceedings{DGGL-icalp15,
address = {Kyoto, Japan},
month = jul,
year = 2015,
volume = {9135},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Halld{\'o}rsson, Magnus M. and Iwama, Kazuo and Kobayashi,
Naoki and Speckmann, Bettina},
acronym = {{ICALP}'15},
booktitle = {{P}roceedings of the 42nd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'15)~-- {P}art~{II}},
author = {Dubut, J{\'e}r{\'e}my and Goubault, {\'E}ric and
Goubault{-}Larrecq, Jean},
title = {Natural Homology},
pages = {171-183},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DGGL-icalp15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DGGL-icalp15.pdf},
doi = {10.1007/978-3-662-47666-6_14},
abstract = {We propose a notion of homology for directed algebraic topology,
based on so-called natural systems of abelian groups, and which we call
natural homology. Contrarily to previous proposals, and as we show,
natural homology has many desirable properties: it~is invariant under
isomorphisms of directed spaces, it is invariant under refinement
(subdivision), and it is computable on cubical complexes.}
}
@inproceedings{LS-lics15,
address = {Kyoto, Japan},
month = jul,
year = 2015,
publisher = {{IEEE} Press},
acronym = {{LICS}'15},
booktitle = {{P}roceedings of the 30th {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'15)},
author = {Leroux, J{\'e}r{\^o}me and Schmitz, Sylvain},
title = {Demystifying Reachability in Vector Addition Systems},
pages = {56-67},
url = {http://arxiv.org/abs/1503.00745},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-arxiv15.pdf},
doi = {10.1109/LICS.2015.1},
abstract = {More than 30 years after their inception, the decidability
proofs for reachability in vector addition systems (VAS) still retain much
of their mystery. These proofs rely crucially on a decomposition of runs
successively refined by Mayr, Kosaraju, and Lambert, which appears rather
magical, and for which no complexity upper bound is known.\par
We first offer a justification for this decomposition technique, by
showing that it emerges naturally in the study of the ideals of a well
quasi ordering of VAS runs. In a second part, we apply recent results on
the complexity of termination thanks to well quasi orders and well orders
to obtain fast-growing complexity upper bounds for the decomposition
algorithms, thus providing the first known upper bounds for general VAS
reachability.}
}
@inproceedings{BFGHM-lics15,
address = {Kyoto, Japan},
month = jul,
year = 2015,
publisher = {{IEEE} Press},
acronym = {{LICS}'15},
booktitle = {{P}roceedings of the 30th {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'15)},
author = {Blondin, Michael and Finkel, Alain and G{\"o}ller, Stefan
and Haase, Christoph and McKenzie, Pierre},
title = {Reachability in Two-Dimensional Vector Addition
Systems with States is {PSPACE}-Complete},
pages = {32-43},
url = {http://arxiv.org/abs/1412.4259},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFGHM-lics15-long.pdf},
doi = {10.1109/LICS.2015.14},
abstract = {Determining the complexity of the reachability problem for
vector addition systems with states (VASS) is a long-standing open problem
in computer science. Long known to be decidable, the problem to this day
lacks any complexity upper bound whatsoever. In this paper, reachability
for two-dimensional VASS is shown PSPACE-complete. This improves on a
previously known doubly exponential time bound established by Howell,
Rosier, Huynh and Yen in~1986. The coverability and boundedness problems
are also noted to be PSPACE-complete. In addition, some complexity results
are given for the reachability problem in two-dimensional VASS and in
integer VASS when numbers are encoded in unary.}
}
@inproceedings{ACR-acsd15,
address = {Brussels, Belgium},
month = jun,
year = 2015,
publisher = {{IEEE} Computer Society Press},
editor = {Haar, Stefan and Meyer, Roland},
acronym = {{ACSD}'15},
booktitle = {{P}roceedings of the 15th {I}nternational
{C}onference on {A}pplication of {C}oncurrency
to {S}ystem {D}esign
({ACSD}'15)},
author = {Andr{\'e}, {\'E}tienne and Chatain, {\relax Th}omas and
Rodr{\'\i}guez, C{\'e}sar},
title = {Preserving Partial Order Runs in Parametric Time {P}etri Nets},
pages = {120-129},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACR-acsd15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACR-acsd15.pdf},
doi = {10.1109/ACSD.2015.16},
abstract = {Parameter synthesis for timed systems aims at deriving parameter
valuations satisfying a given property. In this paper we target concurrent
systems; it is well known that concurrency is a source of state-space
explosion, and partial order techniques were defined to cope with this
problem. Here we use partial order semantics for parametric time Petri
nets as a way to significantly enhance the result of an existing synthesis
algorithm. Given a reference parameter valuation, our approach synthesizes
other valuations preserving, up to interleaving, the behavior of the
reference parameter valuation. We show the applicability of our approach
using acyclic asynchronous circuits.}
}
@inproceedings{CHKS-pn15,
address = {Brussels, Belgium},
month = jun,
year = 2015,
volume = {9115},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Devillers, Raymond and Valmari, Antti},
acronym = {{PETRI~NETS}'15},
booktitle = {{P}roceedings of the 36th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'15)},
author = {Chatain, {\relax Th}omas and Haar, Stefan and Koutny,
Maciej and Schwoon, Stefan},
title = {Non-Atomic Transition Firing in Contextual Nets},
pages = {117-136},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CHKS-pn15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CHKS-pn15.pdf},
doi = {10.1007/978-3-319-19488-2_6},
abstract = {The firing rule for Petri nets assumes instantaneous and
simultaneous consumption and creation of tokens. In the context of
ordinary Petri nets, this poses no particular problem because of the
system's asynchronicity, even if token creation occurs later than token
consumption in the firing. With read arcs, the situation changes, and
several different choices of semantics are possible. The step semantics
introduced by Janicki and Koutny can be seen as imposing a two-phase
firing scheme: first, the presence of the required tokens is checked, then
consumption and production of tokens happens. Pursuing this approach
further, we develop a more general framework based on explicitly splitting
the phases of firing, allowing to synthesize coherent steps. This turns
out to define a more general non-atomic semantics, which has important
potential for safety as it allows to detect errors that were missed by the
previous semantics. Then we study the characterization of partial-order
processes feasible under one or the other semantics.}
}
@incollection{BH-im15,
year = 2015,
publisher = {CNRS \'Editions},
editor = {Ollinger, Nicolas},
booktitle = {Informatique Math{\'e}matique. Une~photographie en~2015},
author = {Bertrand, Nathalie and Haddad, Serge},
title = {Contr{\^o}le, probabilit{\'e}s et observation partielle},
chapter = 5,
pages = {177-227},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BH-im15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BH-im15.pdf}
}
@article{DDS-ic15,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Demri, St{\'e}phane and Dhar, Amit Kumar and Sangnier, Arnaud},
title = {Taming Past {LTL} and Flat Counter Systems},
volume = {242},
month = jun,
year = 2015,
pages = {306-339},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-ic15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-ic15.pdf},
doi = {10.1016/j.ic.2015.03.007},
abstract = {Reachability and LTL model-checking problems for flat counter
systems are known to be decidable but whereas the reachability problem can
be shown in NP, the best known complexity upper bound for the latter
problem is made of a tower of several exponentials. Herein, we show that
this problem is only NP-complete even if LTL admits past-time operators
and arithmetical constraints on counters. As far as past-time operators
are concerned, their addition to LTL immediately leads to complications
and hence an NP upper bound cannot be deduced by translating formulae into
LTL and studying the problem only for this latter logic. Actually, the NP
upper bound is shown by adequately combining a new stuttering theorem for
Past LTL and the property of small integer solutions for quantifier-free
Presburger formulae. This latter complexity bound extends known and recent
results on model-checking weak Kripke structures with LTL formulae as
well as reachability problems for flat counter systems. We also provide
other complexity results obtained by restricting further the class of flat
counter systems.}
}
@article{BBDHP-peva15,
publisher = {Elsevier Science Publishers},
journal = {Performance Evaluation},
author = {Ballarini, Paolo and Barbot, Beno{\^\i}t and Duflot, Marie and
Haddad, Serge and Pekergin, Nihal},
title = {{HASL}: A~New Approach for Performance Evaluation and Model
Checking from Concepts to Experimentation},
year = {2015},
month = aug,
volume = 90,
pages = {53-77},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2015-04.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2015-04.pdf},
doi = {10.1016/j.peva.2015.04.003},
abstract = {We introduce the Hybrid Automata Stochastic Language (HASL), a
new temporal logic formalism for the verification of Discrete Event
Stochastic Processes (DESP). HASL employs a Linear Hybrid Automaton (LHA)
to select prefixes of relevant execution paths of a DESP. LHA allows
rather elaborate information to be collected \emph{on-the-fly} during path
selection, providing the user with powerful means to express sophisticated
measures. A~formula of HASL consists of an LHA and an expression~\(Z\)
referring to moments of \emph{path random variables}. A~simulation-based
statistical engine is employed to obtain a confidence interval estimate
of the expected value of~\(Z\). In~essence, HASL~provides a unifying
verification framework where temporal reasoning is naturally blended with
elaborate reward-based analysis. Moreover, we have implemented a tool,
named COSMOS, for performing analysis of HASL formula for DESP modelled by
Petri nets. Using this tool we have developed two detailed case studies: a
flexible manufacturing system and a genetic oscillator.}
}
@article{LS-tocl15,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Lazi{\'c}, Ranko and Schmitz, Sylvain},
title = {Non-Elementary Complexities for Branching~{VASS}, {MELL}, and Extensions},
volume = {16},
number = {3:20},
nopages = {},
month = jul,
year = 2015,
url = {http://arxiv.org/abs/1401.6785},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-tocl15.pdf},
doi = {10.1145/2733375},
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{FKM-syncop15,
address = {London, UK},
volume = 44,
series = {Open Access Series in Informatics},
month = apr,
year = 2015,
editor = {Andr{\'e}, {\'E}tienne and Frehse, Goran},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
acronym = {{SYNCOP}'15},
booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {S}ynthesis
of {C}ontinuous {P}arameters ({SYNCOP}'15)},
author = {Fribourg, Laurent and K{\"u}hne, Ulrich and Markey, Nicolas},
title = {Game-based Synthesis of Distributed Controllers for Sampled Switched Systems},
pages = {47-61},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FKM-syncop15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FKM-syncop15.pdf},
doi = {10.4230/OASIcs.SynCoP.2015.47},
abstract = {Switched systems are a convenient formalism for modeling
physical processes interacting with a digital controller. Unfortunately,
the formalism does not capture the distributed nature encountered e.g. in
cyber-physical systems, which are organized as networks of elements
interacting with each other and with local controllers. Most current
methods for control synthesis can only produce a centralized controller,
which is assumed to have complete knowledge of all the component states
and can interact with all of them. In~this paper, we~consider a controller
synthesis method based on state space decomposition, and propose a
game-based approach in order to extend it within a distributed framework.}
}
@inproceedings{LDRCF-syncop15,
address = {London, UK},
volume = 44,
series = {Open Access Series in Informatics},
month = apr,
year = 2015,
editor = {Andr{\'e}, {\'E}tienne and Frehse, Goran},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
acronym = {{SYNCOP}'15},
booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {S}ynthesis
of {C}ontinuous {P}arameters ({SYNCOP}'15)},
author = {Le{~}Co{\"e}nt, Adrien and De{~}Vuyst, Florian and Rey,
{\relax Ch}ristian and Chamoin, Ludovic and Fribourg, Laurent},
title = {Guaranteed control of switched control systems
using model order reduction and state-space bisection},
pages = {32-46},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LDCRF-syncop15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LDCRF-syncop15.pdf},
doi = {10.4230/OASIcs.SynCoP.2015.32},
abstract = {This paper considers discrete-time linear systems controlled by
a quantized law, i.e., a piecewise constant time function taking a finite
set of values. We show how to generate the control by, first, applying
model reduction to the original system, then using a {"}state-space
bisection{"} method for synthesizing a control at the reduced-order
level, and finally computing an upper bound to the deviations between the
controlled output trajectories of the reduced-order model and those of the
original model. The effectiveness of our approach is illustrated on
several examples of the literature.}
}
@inproceedings{ACD-post15,
address = {London, UK},
month = apr,
year = 2015,
volume = {9036},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Focardi, Riccardo and Myers, Andrew},
acronym = {{POST}'15},
booktitle = {{P}roceedings of the 4th {I}nternational {C}onference on
{P}rinciples of {S}ecurity and {T}rust
({POST}'15)},
author = {Arapinis, Myrto and Cheval, Vincent and Delaune, St{\'e}phanie},
title = {Composing security protocols: from confidentiality to privacy},
pages = {324-343},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACD-post15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACD-post15.pdf},
doi = {10.1007/978-3-662-46666-7_17},
abstract = {Security protocols are used in many of our daily-life
applications, and our privacy largely depends on their design. Formal
verification techniques have proved their usefulness to analyse these
protocols, but they become so complex that modular techniques have to be
developed. We propose several results to safely compose security
protocols. We consider arbitrary primitives modeled using an equational
theory, and a rich process algebra close to the applied pi calculus.\par
Relying on these composition results, we derive some security properties
on a protocol from the security analysis performed on each of its
sub-protocols individually. We consider parallel composition and the case
of key-exchange protocols. Our results apply to deal with confidentiality
but also privacy-type properties (e.g. anonymity) expressed using a notion
of equivalence. We illustrate the usefulness of our composition results on
protocols from the 3G phone application and electronic passport.}
}
@phdthesis{scerri-phd15,
author = {Scerri, Guillaume},
title = {Proofs of security protocols revisited},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2015,
month = jan,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/scerri-phd15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/scerri-phd15.pdf}
}
@article{DD-jancl15,
publisher = {Taylor \& Francis},
journal = {Journal of Applied Non-Classical Logics},
author = {Demri, St{\'e}phane and Deters, Morgan},
title = {Separation Logics and Modalities: A~Survey},
volume = 25,
number = 1,
pages = {50-99},
year = 2015,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-jancl15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-jancl15.pdf},
doi = {10.1080/11663081.2015.1018801},
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. In a broad
sense, separation logic is often understood as a programming language, an
assertion language and a family of rules involving Hoare triples. In this
survey, we present similarities between separation logic as an assertion
language and modal and temporal logics. Moreover, we propose a selection
of landmark results about decidability, complexity and expressive power.}
}
@article{DD-tocl15,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Demri, St{\'e}phane and Deters, Morgan},
title = {Two-variable separation logic and its inner circle},
volume = 16,
number = {2:15},
nopages = {},
month = mar,
year = 2015,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-tocl15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-tocl15.pdf},
doi = {10.1145/2724711},
abstract = {Separation logic is a well-known assertion language for
Hoare-style proof systems. We show that first-order separation logic with
a unique record field restricted to two quantified variables and no
program variables is undecidable. This is among the smallest fragments of
separation logic known to be undecidable, and this contrasts with
decidability of two-variable first-order logic. We also investigate its
restriction by dropping the magic wand connective, known to be decidable
with non-elementary complexity, and we show that the satisfiability
problem with only two quantified variables is not yet elementary
recursive. Furthermore, we establish insightful and concrete relationships
between two-variable separation logic and propositional in- terval
temporal logic (PITL), data logics, and modal logics, providing an inner
circle of closely-related logics.}
}
@inproceedings{KV-icdt15,
address = {Brussels, Belgium},
month = mar,
year = 2015,
volume = 31,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Arenas, Marcelo},
acronym = {{ICDT}'15},
booktitle = {{P}roceedings of the 18th {I}nternational {C}onference on
{D}atabase {T}heory ({ICDT}'15)},
author = {Koutsos, Adrien and Vianu, Victor},
title = {Process-Centric Views of Data-Driven Business Artifacts},
pages = {247-264},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KV-icdt15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KV-icdt15.pdf},
doi = {10.4230/LIPIcs.ICDT.2015.247},
abstract = {Declarative, data-aware workflow models are becoming
increasingly pervasive. While these have numerous benefits, classical
process-centric specifications retain certain advantages. Workflow
designers are used to development tools such as BPMN or UML diagrams, that
focus on control flow. Views describing valid sequences of tasks are also
useful to provide stake-holders with high-level descriptions of the
workflow, stripped of the accompanying data. In this paper we study the
problem of recovering process-centric views from declarative, data-aware
workflow specifications in a variant of IBM's business artifact model. We
focus on the simplest and most natural process-centric views, specified by
finite-state transition systems, and describing regular languages. The
results characterize when process-centric views of artifact systems are
regular, using both linear and branching-time semantics. We also study the
impact of data dependencies on regularity of the views.}
}
@inproceedings{NF-icdt15,
address = {Brussels, Belgium},
month = mar,
year = 2015,
volume = 31,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Arenas, Marcelo},
acronym = {{ICDT}'15},
booktitle = {{P}roceedings of the 18th {I}nternational {C}onference on
{D}atabase {T}heory ({ICDT}'15)},
author = {Francis, Nadime},
title = {Asymptotic Determinacy of Path Queries using Union-of-Paths Views},
pages = {44-59},
note = {Best student paper award},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/NF-icdt15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/NF-icdt15.pdf},
doi = {10.4230/LIPIcs.ICDT.2015.44},
abstract = {We consider the view determinacy problem over graph databases
for queries defined as (possibly infinite) unions of path queries. These
queries select pairs of nodes in a graph that are connected through a path
whose length falls in a given set. A~view specification is a set of such
queries. We~say that a view specification~\(\textbf{V}\) determines a
query~\(Q\) if, for all databases~\(D\), the answers to~\(\textbf{V}\)
on~\(D\) contain enough information to answer~\(Q\).\par
Our main result states that, given a view~\(\textbf{V}\), there exists an
explicit bound that depends on~\(\textbf{V}\) such that we can decide the
determinacy problem for all queries that ask for a path longer than this
bound, and provide first-order rewritings for the queries that are
determined. We call this notion asymptotic determinacy. As a corollary, we
can also compute the set of almost all path queries that are determined
by~\(\textbf{V}\).}
}
@inproceedings{RRS-vmcai15,
address = {Mumbai, India},
month = jan,
year = 2015,
volume = 8931,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {D'Souza, Deepak and Lal, Akash and Larsen, Kim Guldstrand},
acronym = {{VMCAI}'15},
booktitle = {{P}roceedings of the 16th {I}nternational {C}onference on
{V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation
({VMCAI}'15)},
author = {Randour, Mickael and Raskin, Jean-Fran{\c{c}}ois and
Sankur, Ocan},
title = {Variations on the Stochastic Shortest Path Problem},
pages = {1-18},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/RRS-vmcai15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RRS-vmcai15.pdf},
doi = {10.1007/978-3-662-46081-8_1},
abstract = {In this invited contribution, we revisit the stochastic shortest
path problem, and show how recent results allow one to improve over the
classical solutions: we present algorithms to synthesize strategies with
multiple guarantees on the distribution of the length of paths reaching a
given target, rather than simply minimizing its expected value. The
concepts and algorithms that we propose here are applications of more
general results that have been obtained recently for Markov decision
processes and that are described in a series of recent papers.}
}
@article{VCDHRR-icomp15,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Velner, Yaron and Chatterjee, Krishnendu and Doyen, Laurent
and Henzinger, Thomas A. and Rabinovich, Alexander Moshe and
Raskin, Jean-Fran{\c{c}}ois},
title = {The complexity of multi-mean-payoff and multi-energy games},
year = 2015,
month = apr,
volume = 241,
pages = {177-196},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDRR-icomp15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDRR-icomp15.pdf},
doi = {10.1016/j.ic.2015.03.001},
abstract = {In mean-payoff games, the objective of the protagonist is to
ensure that the limit average of an infinite sequence of numeric weights
is nonnegative. In energy games, the objective is to ensure that the
running sum of weights is always nonnegative. Multi-mean-payoff and
multi-energy games replace individual weights by tuples, and the limit
average (resp., running sum) of each coordinate must be (resp.,~remain)
nonnegative. We prove finite-memory determinacy of multi-energy games and
show inter-reducibility of multi-mean-payoff and multi-energy games for
finite-memory strategies. We improve the computational complexity for
solving both classes with finite-memory strategies: we prove
coNP-completeness improving the previous known \textsf{EXPSPACE} bound.
For memoryless strategies, we show that deciding the existence of a
winning strategy for the protagonist is NP-complete. We present the first
solution of multi-mean-payoff games with infinite-memory strategies: we
show that mean-payoff-sup objectives can be decided in
\textsf{NP}{{\(\cap\)}}\textsf{coNP}, whereas mean-payoff-inf objectives
are coNP-complete.}
}
@article{CDRR-icomp15,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Chatterjee, Krishnendu and Doyen, Laurent and Randour, Mickael and
Raskin, Jean-Fran{\c{c}}ois},
title = {Looking at Mean-Payoff and Total-Payoff through Windows},
year = 2015,
month = jun,
volume = 242,
pages = {25-52},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDRR-icomp15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDRR-icomp15.pdf},
doi = {10.1016/j.ic.2015.03.010},
abstract = {We consider two-player games played on weighted directed graphs
with mean-payoff and total-payoff objectives, two classical quantitative
objectives. While for single-dimensional games the complexity and memory
bounds for both objectives coincide, we show that in contrast to
multi-dimensional mean-payoff games that are known to be coNP-complete,
multi-dimensional total-payoff games are undecidable. We introduce
conservative approximations of these objectives, where the payoff is
considered over a local finite window sliding along a play, instead of the
whole play. For single dimension, we show that (i)~if the window size is
polynomial, deciding the winner takes polynomial time, and (ii)~the
existence of a bounded window can be decided in
\(\textsf{NP}\cap\textsf{coNP}\), and is at least as hard as solving
mean-payoff games. For multiple dimensions, we show that (i)~the problem
with fixed window size is EXPTIME-complete, and (ii)~there is no
primitive-recursive algorithm to decide the existence of a bounded
window.}
}
@article{GJL-tocl15,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {G{\"o}ller, Stefan and Jung, Jean Christoph and Lohrey,
Markus},
title = {The Complexity of Decomposing Modal and First-Order
Theories},
volume = 16,
number = {1:9},
nopages = {},
month = mar,
year = 2015,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GJL-tocl15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GJL-tocl15.pdf},
doi = {10.1145/2699918},
abstract = {We study the satisfiability problem of the logic
\(\textbf{K}^{2}=\textbf{K}\times\textbf{K}\), i.e., the two-dimensional
variant of unimodal logic, where models are restricted to asynchronous
products of two Kripke frames. Gabbay and Shehtman proved in 1998 that
this problem is decidable in a tower of exponentials. So far the best
known lower bound is NEXP-hardness shown by Marx and Mikul\'as in~2001.\par
Our first main result closes this complexity gap: We show that
satisfiability in~\(\textbf{K}^{2}\) is nonelementary. More precisely, we
prove that it is \(k\)-NEXP-complete, where \(k\) is the switching depth
(the~minimal modal rank among the two dimensions) of the input formula,
hereby solving a conjecture of Marx and Mikul\'as. Using our lower-bound
technique allows us to derive also nonelementary lower bounds for the
two-dimensional modal logics \(\textbf{K}^{4}\times\textbf{K}\) and
\(\textbf{S5}_{2}\times\textbf{K}\) for which only elementary
lower bounds were previously known.\par
Moreover, we apply our technique to prove nonelementary lower bounds for
the sizes of Feferman-Vaught decompositions with respect to product for
any decomposable logic that is at least as expressive as unimodal\(\textbf{K}\),
generalizing a recent result by the first author and~Lin. For the
three-variable fragment \(\textsf{FO}^3\) of first-order logic, we obtain the following
immediate corollaries: (i)~the~size of Feferman-Vaught decompositions with
respect to disjoint sum are inherently nonelementary and (ii)~equivalent
formulas in Gaifman normal form are inherently nonelementary.\par
Our second main result consists in providing effective elementary (more
precisely, doubly exponential) upper bounds for the two-variable fragment
\(\textsf{FO}^2\) of first-order logic both for Feferman-Vaught
decompositions and for equivalent formulas in Gaifman normal form.}
}
@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.",
}}
@techreport{CHH-arxiv16,
author = {Chistikov, Dmitry and Haase, Christoph and Halfon, Simon},
title = {Context-Free Commutative Grammars with Integer Counters and Resets},
institution = {Computing Research Repository},
number = {1511-04893},
year = {2015},
month = nov,
type = {Research Report},
url = {http://arxiv.org/abs/1511.04893},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CHH-arxiv16.pdf},
note = {31~pages},
abstract = {We study the computational complexity of reachability,
coverability and inclusion for extensions of context-free commutative
grammars with integer counters and reset operations on them. Those
grammars can alternatively be viewed as an extension of communication-free
Petri nets. Our main results are that reachability and coverability are
inter-reducible and both NP-complete. In particular, this class of
commutative grammars enjoys semi-linear reachability sets. We also show
that the inclusion problem is, in general, coNEXP-complete and already
\(\Pi^{P}_{2}\)-complete for grammars with only one non-terminal symbol.
Showing the lower bound for the latter result requires us to develop a
novel \(\Pi^{P}_{2}\)-complete variant of the classic subset sum
problem.}
}
@misc{vip-D32,
author = {Baelde, David and Delaune, St{\'e}phanie and Kremer, Steve},
title = {Decision procedures for equivalence based properties (part~{II})},
howpublished = {Deliverable VIP~3.2 (ANR-11-JS02-0006)},
month = sep,
year = {2015},
note = {9~pages},
type = {Contract Report},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/vip-d32.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/vip-d32.pdf}
}
@misc{vip-D41,
author = {Delaune, St{\'e}phanie and Kremer, Steve},
title = {Composition results for equivalence-based security properties},
howpublished = {Deliverable VIP~3.1 (ANR-11-JS02-0006)},
month = sep,
year = {2015},
note = {6~pages},
type = {Contract Report},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/vip-d41.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/vip-d41.pdf}
}
@article{LS-sigmodrec15,
publisher = {ACM Press},
journal = {SIGMOD Records},
author = {Segoufin, Luc},
title = {Constant Delay Enumeration for Conjunctive Queries},
year = 2015,
volume = {44},
number = {1},
pages = {10-17},
month = mar,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-sigmodrec15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-sigmodrec15.pdf},
doi = {10.1145/2783888.2783894},
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.\par
This cannot be always achieved. It requires restricting either the class
of queries or the class of databases.\par
We consider conjunctive queries and describe several scenarios when this
is possible.}
}
@article{PS-lmcs15,
journal = {Logical Methods in Computer Science},
author = {Place, {\relax Th}omas and Segoufin, Luc},
title = {Deciding definability in
{{\(\textrm{FO}^{2}(<_{\textbf{h}},<_{\textbf{v}})\)}} on
trees},
year = 2015,
volume = {11},
number = {3:5},
nopages = {},
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/PS-lmcs15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PS-lmcs15.pdf},
doi = {10.2168/LMCS-11(3:5)2015},
abstract = {We provide a decidable characterization of regular forest
languages definable in \(\textrm{FO}^{2}(<_{\textbf{h}},<_{\textbf{v}})\).
By~\(\textrm{FO}^{2}(<_{\textbf{h}},<_{\textbf{v}})\) we refer to the two
variable fragment of first order logic built from the descendant relation
and the following sibling relation. In terms of expressive power it
corresponds to a fragment of the navigational core of XPath that contains
modalities for going up to some ancestor, down to some descendant, left to
some preceding sibling, and right to some following sibling.\par
We also show that our techniques can be applied to other two variable
first-order logics having exactly the same vertical modalities as
\(\textrm{FO}^{2}(<_{\textbf{h}},<_{\textbf{v}})\) but having different
horizontal modalities.}
}
@article{FSS-lmcs15,
journal = {Logical Methods in Computer Science},
author = {Francis, Nadime and Segoufin, Luc and Sirangelo, Cristina},
title = {Datalog Rewritings of Regular Path Queries using Views},
year = 2015,
volume = {11},
number = {4:14},
nopages = {},
month = dec,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FSS-lmcs15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FSS-lmcs15.pdf},
doi = {10.2168/LMCS-11(4:14)2015},
abstract = {We consider query answering using views on graph databases, i.e.
databases structured as edge-labeled graphs. We mainly consider views and
queries specified by Regular Path Queries~(RPQ). 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. We say
that a view~\(\textbf{V}\) determines a query~\(Q\) if for all graph
databases~\(D\), the~view image~\(\textbf{V}(D)\) always contains enough
information to answer~\(Q\) on~\(D\). In~other words, there is a well
defined function from~\(\textbf{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~\(\textbf{V}(D)\). In particular the rewriting query can be
evaluated in time polynomial in the size of~\(\textbf{V}(D)\). Moreover
this implies that it is decidable whether an RPQ query can be rewritten in
Datalog using RPQ views.}
}
@article{BCS-jacm15,
publisher = {ACM Press},
journal = {Journal of the~{ACM}},
author = {B{\'a}r{\'a}ny, Vince and ten Cate, Balder and Segoufin, Luc},
title = {Guarded nagation},
year = 2015,
volume = {62},
number = {3:22},
nopages = {},
month = jun,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCS-jacm15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCS-jacm15.pdf},
doi = {10.1145/2701414},
abstract = { We consider restrictions of first-order logic and of fixpoint
logic in which all occurrences of negation are required to be guarded by
an atomic predicate. In terms of expressive power, the logics in question,
called GNFO and GNFP, extend the guarded fragment of first-order logic and
the guarded least fixpoint logic, respectively. They also extend the
recently introduced unary negation fragments of first-order logic and of
least fixpoint logic.\par
We show that the satisfiability problem for GNFO and for GNFP is
2ExpTime-complete, both on arbitrary structures and on finite structures.
We also study the complexity of the associated model checking problems.
Finally, we show that GNFO and GNFP are not only computationally well
behaved, but also model theoretically: we~show that GNFO and GNFP have the
tree-like model property and that GNFO has the finite model property, and
we characterize the expressive power of GNFO in terms of invariance for an
appropriate notion of bisimulation.\par
Our complexity upper bounds for GNFO and GNFP hold true even for their
{"}clique-guarded{"} extensions CGNFO and CGNFP, in which clique guards are
allowed in the place of guards.}
}
@inproceedings{DS-flc2,
noaddress = {Berlin, Germany},
month = sep,
year = 2015,
volume = 9300,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
noacronym = {},
booktitle = {Fields of Logic and Computation~{II}~-- Essays Dedicated to {Y}uri
{G}urevich on the Occasion of His 75th Birthday},
editor = { Beklemishev, Lev D. and Blass, Andreas and Dershowitz,
Nachum and Finkbeiner, Bernd and Schulte, Wolfram},
author = {Dawar, Anuj and Segoufin, Luc},
title = {Capturing {MSO} with one quantifier},
pages = {142-152},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DS-flc2.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DS-flc2.pdf},
doi = {10.1007/978-3-319-23534-9_8},
abstract = {We construct a single Lindstr{\"o}m quantifier~\(Q\) such that
\(\textrm{FO} (Q)\), the extension of first-order logic with~\(Q\) has the same
expressive power as monadic second-order logic on the class of binary
trees (with distinct left and right successors) and also on unranked trees
with a sibling order. This resolves a conjecture by ten~Cate and Segoufin.
The quantifier~\(Q\) is a variation of a quantifier expressing the Boolean
satisfiability problem.}
}
@inproceedings{SA-adbis15,
address = {Poitiers, France},
month = sep,
year = 2015,
nmnote = {post-proceedings published by LNCS, to appear},
editor = {Bellatreche, Ladjel},
acronym = {{ADBIS}'15},
booktitle = {{P}roceedings of the 19th {E}ast-{E}uropean {C}onference on {A}dvances in
{D}atabases and {I}nformation {S}ystems ({ADBIS}'15)},
author = {Abiteboul, Serge},
title = {The Story of Webdamlog},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SA-adbis15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SA-adbis15.pdf},
abstract = {We~summarize in this paper works about the management of data in
a distributed manner based on Webdamlog, a datalog-extension. We~point to
relevant articles on these works. More references may be found there.}
}
@proceedings{HM-acsd2015,
editor = {Haar, Stefan and Meyer, Roland},
title = {{P}roceedings of the 15th {I}nternational
{C}onference on {A}pplication of {C}oncurrency
to {S}ystem {D}esign
({ACSD}'15)},
booktitle = {{P}roceedings of the 15th {I}nternational
{C}onference on {A}pplication of {C}oncurrency
to {S}ystem {D}esign
({ACSD}'15)},
acronym = {{ACSD}'15},
publisher = {{IEEE} Computer Society Press},
year = 2015,
month = jun,
address = {Brussels, Belgium},
url = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=7352411}
}
@inproceedings{ADESWSS-webdb15,
address = {Melbourne, Australia},
month = may,
year = 2015,
publisher = {ACM Press},
editor = {Stoyanovich, Julia and Suchanek, Fabian M},
acronym = {({W}eb{DB}'15)},
booktitle = {{P}roceedings of the 18th {I}nternational {W}orkshop on the
{W}eb and {D}atabases ({W}eb{DB}'15)},
author = {Abiteboul, Serge and Dong, Xin Luna and Etzioni, Oren and
Srivastava, Divesh and Weikum, Gerhard and Stoyanovich,
Julia and Suchanek, Fabian M.},
title = {The elephant in the room: getting value from Big Data},
pages = {1-5},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ADESWSS-webdb15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ADESWSS-webdb15.pdf},
doi = {10.1145/2767109.2770014}
}
@inproceedings{MSAM-sigmod15,
address = {Melbourne, Australia},
month = may # {-} # jun,
year = 2015,
publisher = {ACM Press},
editor = {Sellis, Timos K. and Davidson, Susan B. and Ives,Zachary G.},
acronym = {{SIGMOD}'15},
booktitle = {{P}roceedings of the {ACM} {SIGMOD} {I}nternaitonal
{C}onference on {M}anagement of {D}ata ({SIGMOD}'15)},
author = {Moffitt, Vera Zaychik and Stoyanovich, Julia and Abiteboul,
Serge and Miklau, Gerome},
title = {Collaborative Access Control in {W}ebdam{L}og},
pages = {197-211},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/MSAM-sigmod15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/MSAM-sigmod15.pdf},
doi = {10.1109/DSAA.2015.7344775},
abstract = {The management of Web users' personal information is
increasingly distributed across a broad array of applications and systems,
including online social networks and cloud-based services. Users wish to
share data using these systems, but avoiding the risks of unintended
disclosures or unauthorized access by applications has become a major
challenge.\par
We propose a novel access control model that operates within a distributed
data management framework based on datalog. Using this model, users can
control access to data they own and control applications they run. They
can conveniently specify access control policies providing flexible
tuple-level control derived using provenance information. We present a
formal specification of the model, an implementation built using an
open-source distributed datalog engine, and an extensive experimental
evaluation showing that the computational cost of access control is
modest.}
}
@article{cacm15-AAK,
publisher = {ACM Press},
journal = {Communications of the~{ACM}},
author = {Abiteboul, Serge and Andr{\'e}, Benjamin and Kaplan, Daniel},
title = {Managing your digital life},
volume = {58},
number = {5},
pages = {32-35},
year = 2015,
month = may,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/cacm15-AAK.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/cacm15-AAK.pdf},
doi = {10.1145/2670528},
abstract = {Everyone should be able to manage their personal data
with a personal information management system.}
}
@inproceedings{APS-tap15,
address = {L'Aquila, Italy},
month = jul,
year = 2015,
volume = 9154,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = { Blanchette, Jasmin Christian and Kosmatov, Nikolai},
acronym = {{TAP}'15},
booktitle = {{P}roceedings of the 9th {I}nternational {C}onference
on {T}ests and {P}roofs ({TAP}'15)},
author = {Athanasiou, Konstantinos and Ponce{ }de{~}Le{\'o}n, Hern\'an
and Schwoon, Stefan},
title = {Test Case Generation for Concurrent Systems
Using Event Structures},
pages = {19-37},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/APS-tap15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/APS-tap15.pdf},
doi = {10.1007/978-3-319-21215-9_2},
abstract = {This paper deals with the test-case generation problem for
concurrent systems that are specified by true-concurrency models such as
Petri nets. We show that using true-concurrency models reduces both the
size and the number of test cases needed for achieving certain coverage
criteria. We present a test-case generation algorithm based on Petri net
unfoldings and a SAT encoding for solving controllability problems in test
cases. Finally, we evaluate our algorithm against traditional test-case
generation methods under interleaving semantics.}
}
@misc{mcc:2015,
author = {F. Kordon and H. Garavel and L. M. Hillah and Hulin{-}Hubard, Francis
and A. Linard and M. Beccuti and A. Hamez and E. Lopez-Bobeda and L.
Jezequel and J. Meijer and E. Paviot-Adet and C. Rodriguez and C. Rohr
and J. Srba and Y. Thierry-Mieg and K. Wolf},
month = jun,
title = {{Complete Results for the 2015 Edition of the Model Checking Contest}},
year = {2015},
url = {http://mcc.lip6.fr/2015/results.php}
}
@misc{JGL:dom15,
author = {Goubault{-}Larrecq, Jean},
howpublished = {Invited talk, Domains XII workshop, Cork, Ireland},
month = aug,
title = {Formal balls},
year = {2015}
}
@misc{GSM:dga-inria15,
author = {Goubault-Larrecq, Jean and Sentucq, Pierre-Arnaud and Majorczyk, Fr{\'e}d{\'e}ric},
howpublished = {Rapport interm{\'e}diaire du contrat DGA-INRIA Orchids},
month = may,
title = {Etat d'avancement interm{\'e}diaire des travaux engag{\'e}s sur {OrchIDS}},
year = {2015}
}
@mastersthesis{m2-Gonzalez,
author = {Gonz{\'a}lez, Mauricio},
title = {{Constructions d'Information Parfaite pour certains Jeux {\`a} Information Imparfaite. Quelques Algorithmes.}},
school = {Universit{\'e} Pierre et Marie Curie, Paris, France},
type = {Rapport de {M}aster},
year = {2015},
month = dec
}
@mastersthesis{m2-Fortin,
author = {Fortin, Marie},
title = {{Verification of distributed systems with parameterized network topology}},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2015},
month = sep
}
This file was generated by bibtex2html 1.98.