@article{BFRR-ic15,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Bruy{\`e}re, V{\'e}ronique and Filiot, Emmanuel and
Randour, Mickael and Raskin, Jean-Fran{\c{c}}ois},
title = {Meet Your Expectations With Guarantees: Beyond Worst-Case
Synthesis in Quantitative Games},
volume = {254},
number = {2},
month = jun,
year = 2017,
pages = {259-295},
note = {To appear},
doi = {10.1016/j.ic.2016.10.011},
abstract = {Classical analysis of two-player quantitative games involves an adversary (modeling the environment of the system) which is purely antagonistic and asks for strict guarantees while Markov decision processes model systems facing a purely randomized environment: the aim is then to optimize the expected payoff, with no guarantee on individual outcomes. We introduce the beyond worst-case synthesis problem, which is to construct strategies that guarantee some quantitative requirement in the worst-case while providing a higher expected value against a particular stochastic model of the environment given as input.
We study the beyond worst-case synthesis problem for two important quantitative settings: the mean-payoff and the shortest path. In both cases, we show how to decide the existence of finite-memory strategies satisfying the problem and how to synthesize one if one exists. We establish algorithms and we study complexity bounds and memory requirements.}
}
@inproceedings{BJ-fossacs17,
address = {Uppsala, Sweden},
month = apr,
year = 2017,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Esparza, Javier and Murawski, Andrzej},
acronym = {{FoSSaCS}'17},
booktitle = {{P}roceedings of the 20th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'17)},
author = {Bouyer, Patricia and Jug{\'e}, Vincent},
title = {Dynamic Complexity of the {D}yck Reachability},
pages = {265-280},
url = {https://arxiv.org/abs/1610.07499},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BJ-fossacs17.pdf},
doi = {10.1007/978-3-662-54458-7_16},
abstract = {Dynamic complexity is concerned with updating the output of a problem when the input is slightly changed. We study the dynamic complexity of Dyck reachability problems in directed and undirected graphs, where updates may add or delete edges. We show a strong dichotomy between such problems, based on the size of the Dyck alphabet. Some of them are P-complete (under a strong notion of reduction) while the others lie either in DynFO or in NL.}
}
@inproceedings{BHMRZ-fossacs17,
address = {Uppsala, Sweden},
month = apr,
year = 2017,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Esparza, Javier and Murawski, Andrzej},
acronym = {{FoSSaCS}'17},
booktitle = {{P}roceedings of the 20th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'17)},
author = {Bouyer, Patricia and Hofman, Piotr and Markey, Nicolas and Randour, Mickael and Zimmermann, Martin},
title = {Bounding Average-energy Games},
pages = {179-195},
url = {https://arxiv.org/abs/1610.07858},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHMRZ-fossacs17.pdf},
doi = {10.1007/978-3-662-54458-7_11},
abstract = {We consider average-energy games, where the goal is to minimize the long-run average of the accumulated energy. Decidability of average-energy games with a lower-bound constraint on the energy level (but no upper bound) is an open problem; in particular, there is no known upper bound on the memory that is required for winning strategies.
By reducing average-energy games with lower-bounded energy to infinite-state mean-payoff games and analyzing the frequency of low-energy configurations, we show an almost tight doubly-exponential upper bound on the necessary memory, and that the winner of average-energy games with lower-bounded energy can be determined in doubly-exponential time. We also prove EXPSPACE-hardness of this problem.
Finally, we consider multi-dimensional extensions of all types of average-energy games: without bounds, with only a lower bound, and with both a lower and an upper bound on the energy. We show that the fully-bounded version is the only case to remain decidable in multiple dimensions.}
}
@article{J-ijac16,
publisher = {World Scientific},
journal = {International Journal of Algebra and Computation},
author = {Jug{\'e}, Vincent},
title = {The Relaxation Normal Form of Braids is Regular},
volume = {27},
number = {1},
year = {2017},
pages = {61-106},
month = feb,
url = {https://arxiv.org/abs/1507.03248},
doi = {10.1142/S0218196717500059},
abstract = {Braids can be represented geometrically as laminations of punctured disks. The geometric complexity of a braid is the minimal complexity of a lamination that represents it, and tight laminations are representatives of minimal complexity. These laminations give rise to a normal form of braids, via a relaxation algorithm. We study here this relaxation algorithm and the associated normal form. We prove that this normal form is regular and prefix-closed. We provide an effective construction of a deterministic automaton that recognizes this normal form.}
}
@inproceedings{BGHH-stacs17,
address = {Hannover, Germany},
month = mar,
year = 2017,
volume = {},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Vall{\'e}e, Brigitte and Vollmer, Heribert},
acronym = {{STACS}'17},
booktitle = {{P}roceedings of the 34th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'17)},
author = {B{\"o}hm, Stanislav and G{\"o}ller, Stefan and Halfon, Simon and Hofman, Piotr},
title = {On B{\"u}chi one-counter automata},
pages = {14:1-14:13},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7019},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7019/pdf/LIPIcs-STACS-2017-14.pdf},
doi = {10.4230/LIPIcs.STACS.2017.14},
abstract = {Equivalence of deterministic pushdown automata is a famous problem in theoretical computer science whose decidability has been shown by S{\'e}nizergues. Our first result shows that decidability no longer holds when moving from finite words to infinite words. This solves an open problem that has recently been raised by L{\"o}ding. In fact, we show that already the equivalence problem for deterministic B{\"u}chi one-counter automata is undecidable. Hence, the decidability border is rather tight when taking into account a recent result by L{\"o}ding and Repke that equivalence of deterministic weak parity pushdown automata (a subclass of deterministic B{\"u}chi pushdown automata) is decidable. Another known result on finite words is that the universality problem for vector addition systems is decidable. We show undecidability when moving to infinite words. In fact, we prove that already the universality problem for nondeterministic B{\"u}chi one-counter nets (or equivalently vector addition systems with one unbounded dimension) is undecidable.}
}
@inproceedings{CG-stacs17,
address = {Hannover, Germany},
month = mar,
year = 2017,
volume = {},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Vall{\'e}e, Brigitte and Vollmer, Heribert},
acronym = {{STACS}'17},
booktitle = {{P}roceedings of the 34th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'17)},
author = {Carayol, Arnaud and G{\"o}ller, Stefan},
title = {On long words avoiding Zimin patterns},
pages = {19:1-19:13},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7014},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7014/pdf/LIPIcs-STACS-2017-19.pdf},
doi = {10.4230/LIPIcs.STACS.2017.19},
abstract = {A pattern is encountered in a word if some infix of the word is the image of the pattern under some non-erasing morphism. A pattern p is unavoidable if, over every finite alphabet, every sufficiently long word encounters p. A theorem by Zimin and independently by Bean, Ehrenfeucht and McNulty states that a pattern over n distinct variables is unavoidable if, and only if, p itself is encountered in the n-th Zimin pattern. Given an alphabet size k, we study the minimal length f(n,k) such that every word of length f(n,k) encounters the n-th Zimin pattern. It is known that f is upper-bounded by a tower of exponentials. Our main result states that f(n,k) is lower-bounded by a tower of n-3 exponentials, even for k=2. To the best of our knowledge, this improves upon a previously best-known doubly-exponential lower bound. As a further result, we prove a doubly-exponential upper bound for encountering Zimin patterns in the abelian sense.}
}
@inproceedings{LZ-stacs17,
address = {Hannover, Germany},
month = mar,
year = 2017,
volume = {},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Vall{\'e}e, Brigitte and Vollmer, Heribert},
acronym = {{STACS}'17},
booktitle = {{P}roceedings of the 34th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'17)},
author = {Lohrey, Markus and Zetzsche, Georg},
title = {The Complexity of Knapsack in Graph Groups},
pages = {52:1-52:14},
doi = {10.4230/LIPIcs.STACS.2017.52},
abstract = {Myasnikov et al. have introduced the knapsack problem for arbitrary finitely generated groups. In LohreyZ16 the authors proved that for each graph group, the knapsack problem can be solved in NP. Here, we determine the exact complexity of the problem for every graph group. While the problem is TC0-complete for complete graphs, it is LogCFL-complete for each (non-complete) transitive forest. For every remaining graph, the problem is NP-complete.}
}
@article{HHMS-jcss16,
publisher = {Elsevier Science Publishers},
journal = {Journal of Computer and System Sciences},
author = {Stefan Haar and
Serge Haddad and
Tarek Melliti and
Stefan Schwoon},
title = {Optimal constructions for active diagnosis},
pages = {101-120},
volume = {83},
number = {1},
year = {2017},
doi = {10.1016/j.jcss.2016.04.007},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HHMS-jcss16.pdf},
abstract = {Diagnosis is the task of detecting fault occurrences in a partially observed sys- tem. Depending on the possible observations, a discrete-event system may be diagnosable or not. Active diagnosis aims at controlling the system to render it diagnosable. Past research has proposed solutions for this problem, but their complexity remains to be improved. Here, we solve the decision and synthesis problems for active diagnosability, proving that (1) our procedures are optimal with respect to computational complexity, and (2) the memory required for our diagnoser is minimal. We then study the delay between a fault occurrence and its detection by the diagnoser. We construct a memory-optimal diagnoser whose delay is at most twice the minimal delay, whereas the memory required to achieve optimal delay may be highly greater. We also provide a solution for parametrized active diagnosis, where we automatically construct the most permissive controller respecting a given delay.}
}
@article{BKM-tocs17,
publisher = {Springer},
journal = {Theory of Computing Systems},
author = {Bollig, Benedikt and
Kuske, Dietrich and
Mennicke, Roy},
title = {The Complexity of Model Checking Multi-Stack Systems},
volume = {60},
number = {4},
pages = {695-736},
year = {2017},
url = {http://link.springer.com/article/10.1007/s00224-016-9700-6?wt_mc=Internal.Event.1.SEM.ArticleAuthorOnlineFirst},
doi = {10.1007/s00224-016-9700-6},
abstract = {We study the linear-time model checking problem for boolean concurrent programs with recursive procedure calls. While sequential recursive programs are usually modeled as pushdown automata, concurrent recursive programs involve several processes and can be naturally abstracted as pushdown automata with multiple stacks. Their behavior can be understood as words with multiple nesting relations, each relation connecting a procedure call with its corresponding return. To reason about multiply nested words, we consider the class of all temporal logics as defined in the book by Gabbay, Hodkinson, and Reynolds. The unifying feature of these temporal logics is that their modalities are defined in monadic second-order (MSO) logic. In particular, this captures numerous temporal logics over concurrent and/or recursive programs that have been defined so far. Since the general model checking problem is undecidable, we restrict attention to phase bounded executions as proposed by La Torre, Madhusudan, and Parlato. While the MSO model checking problem in this case is non-elementary, our main result states that the model checking (and satisfiability) problem for all MSO-definable temporal logics is decidable in elementary time. More precisely, it is solvable in time exponential in the formula and (n+2)-fold exponential in the number of phases where n is the maximal level of the MSO modalities in the monadic quantifier alternation hierarchy (which is a vast improvement over the conference version of this paper from LICS 2013 where the space was also (n+2)-fold exponential in the size of the temporal formula). We complement this result and provide, for each level n, a temporal logic whose model checking problem is n-EXPSPACE-hard.}
}
@article{BMPS-rts16,
publisher = {Kluwer Academic Publishers},
journal = {Real-Time Systems},
author = {Bouyer, Patricia and Markey, Nicolas and Perrin,
Nicolas and Schlehuber{-}Caissier, Philipp},
title = {Timed automata abstraction of switched dynamical
systems using control funnels},
volume = {53},
number = {3},
year = {2017},
pages = {327-353},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMPS-rts16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMPS-rts16.pdf},
doi = {10.1007/s11241-016-9262-3},
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 (control
funnels), that models behaviors of systems as timed
automata. The~main advantage of this method is that
it allows for the automated verification and
reactive controller synthesis without discretizing
the evolution of the state of the system. Efficient
and analytic constructions are possible in the case
of linear dynamics whereas bounding funnels with
conjectured properties based on numerical
simulations can be used for general nonlinear
dynamics. We~demonstrate the potential of our
approach with three examples.}
}
@article{DGG-acs16,
publisher = {Springer},
journal = {Applied Categorical Structures},
author = {Dubut, J{\'e}r{\'e}my and Goubault, {\'E}ric and
Goubault{-}Larrecq, Jean},
title = {Directed homology theories and {E}ilenberg-{S}teenrod
axioms},
year = 2017,
month = oct,
volume = {25},
number = {5},
pages = {775-807},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DGG-acs16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DGG-acs16.pdf},
doi = {doi:10.1007/s10485-016-9438-y},
abstract = {In this paper, we define and study a homology theory, that
we call {"}natural homology{"}, which associates a natural system of
abelian groups to every space in a large class of directed spaces
and precubical sets. We show that this homology theory enjoys many
important properties, as an invariant for directed homotopy. Among
its properties, we show that subdivided precubical sets have the
same homology type as the original ones ; similarly, the natural
homology of a precubical set is of the same type as the natural
homology of its geometric realization. By same type we mean
equivalent up to some form of bisimulation, that we define using the
notion of open map. Last but not least, natural homology, for the
class of spaces we consider, exhibits very important properties such
as Hurewicz theorems, and most of Eilenberg-Steenrod axioms, in
particular the dimension, homotopy, additivity and exactness axioms.
This last axiom is studied in a general framework of (generalized)
exact sequences.}
}
@article{BMV-ic16,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Bouyer, Patricia and Markey, Nicolas and Vester, Steen},
title = {{N}ash Equilibria in Symmetric Graph Games with Partial Observation},
volume = {254},
number = {2},
month = jun,
year = 2017,
pages = {238-258},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-ic16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-ic16.pdf},
doi = {10.1016/j.ic.2016.10.010},
abstract = {We investigate a model for representing large multiplayer games,
which satisfy strong symmetry properties. This model is made of multiple
copies of an arena; each player plays in his own arena, and can partially
observe what the other players do. Therefore, this game has partial
information and symmetry constraints, which make the computation of Nash
equilibria difficult. We show several undecidability results, and for
bounded-memory strategies, we precisely characterize the complexity of
computing pure Nash equilibria (for qualitative objectives) in this game
model.}
}
@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.",
}}
@article{DGLM-tocs16,
publisher = {Springer},
journal = {Theory of Computing Systems},
author = {Demri, St{\'e}phane and Galmiche, Didier and
Larchey-Wendling, Dominique and Mery, Daniel},
title = {Separation Logic with One Quantified Variable},
year = 2017,
volume = {61},
number = {2},
pages = {371-461},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DGLM-tocs16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DGLM-tocs16.pdf},
doi = {10.1007/s00224-016-9713-1},
abstract = {We investigate first-order separation logic with one record
field restricted to a unique quantified variable (1SL1). Undecidability is
known when the number of quantified variables is unbounded and the
satisfiability problem is pspace-complete for the propositional fragment.
We show that the satisfiability problem for 1SL1 is pspace-complete and we
characterize its expressive power by showing that every formula is
equivalent to a Boolean combination of atomic properties. This contributes
to our understanding of fragments of first-order separation logic that can
specify properties about the memory heap of programs with singly-linked
lists. All the fragments we consider contain the magic wand operator and
first-order quantification over a single variable.}
}
@article{JGL-mscs16,
publisher = {Cambridge University Press},
journal = {Mathematical Structures in Computer Science},
author = {Goubault{-}Larrecq, Jean},
title = {Isomorphism theorems between models of mixed choice},
volume = {27},
number = {6},
pages = {1032-1067},
month = sep,
year = 2017,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-mscs16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-mscs16.pdf},
doi = {10.1017/S0960129515000547},
abstract = {We relate the so-called powercone models of mixed
non-deterministic and probabilistic choice proposed by Tix, Keimel,
Plotkin, Mislove, Ouaknine, Worrell, Morgan, and McIver, to our own models
of previsions. Under suitable topological assumptions, we show that they
are isomorphic. We rely on Keimel's cone-theoretic variants of the
classical Hahn-Banach separation theorems, using functional analytic
methods, and on the Schr{\"o}der-Simpson Theorem.}
}
@misc{mcc:2017,
author = {F. Kordon and H. Garavel and L. M. Hillah and Hulin{-}Hubard, Francis
and B. Berthomieu and G. Ciardo and M. Colange and S. {Dal Zilio} and E.
Amparore and M. Beccuti and T. Liebke and J. Meijer and A. Miner and C.
Rohr and J. Srba and Y. Thierry-Mieg and J. van de Pol and K. Wolf},
month = jun,
title = {{Complete Results for the 2017 Edition of the Model Checking Contest}},
year = {2017},
url = {http://mcc.lip6.fr/2017/results.php}
}
@phdthesis{montoya-phd2017,
author = {Montoya, David},
title = {Une base de connaissance personnelle int\'egrant les donn\'ees d'un utilisateur et une chronologie de ses activit\'es},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2017,
month = mar,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/montoya-phd17.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/montoya-phd17.pdf}
}
@article{CMRZZ-dmtcs2017,
journal = {Discrete Mathematics \& Theoretical Computer Science},
author = {Czerwi{\'{n}}ski, Wojciech and Martens, Wim and van Rooijen, Lorijn and Zeitoun, Marc and Zetzsche, Georg},
title = {A Characterization for Decidable Separability by Piecewise Testable Languages},
volume = {19},
number = {4},
year = {2017},
month = dec,
nopages = {},
doi = {10.23638/DMTCS-19-4-1},
url = {https://dmtcs.episciences.org/4131},
pdf = {https://arxiv.org/pdf/1410.1042.pdf}
}
@article{HKZ-sf2017,
publisher = {Springer},
journal = {Semigroup Forum},
author = {Huschenbett, Martin and Kuske, Dietrich and Zetzsche, Georg},
title = {The Monoid of Queue Actions},
volume = {95},
number = {3},
year = {2017},
month = dec,
pages = {475-508},
doi = {10.1007/s00233-016-9835-4},
abstract = {We model the behavior of a fifo-queue as a monoid of transformations that are induced by sequences of writing and reading. We describe this monoid by means of a confluent and terminating semi-Thue system and study some of its basic algebraic properties such as conjugacy. Moreover, we show that while several properties concerning its rational subsets are undecidable, their uniform membership problem is NL-complete. Furthermore, we present an algebraic characterization of this monoid's recognizable subsets. Finally, we prove that it is not Thurston-automatic.}
}
@article{ZKL-tocs17,
publisher = {Springer},
journal = {Theory of Computing Systems},
author = {Zetzsche, Georg and Kuske, Dietrich and Lohrey, Markus},
title = {On {Boolean} closed full trios and rational {Kripke} frames},
volume = {60},
number = {3},
year = {2017},
month = apr,
pages = {438-472},
doi = {10.1007/s00224-016-9694-0}
}
@mastersthesis{m2-riesner,
author = {Riesner, M{\'e}lissa},
title = {Regularity of deterministic pushdown automata},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2017},
month = aug
}
@inproceedings{D-lics17,
address = {Reykjavik, Iceland},
month = jun,
publisher = {{IEEE} Press},
editor = {Ouaknine, Jo{\"e}l},
acronym = {{LICS}'17},
booktitle = {{P}roceedings of the 32nd {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'17)},
author = {Doumane, Amina},
title = {Constructive completeness for the linear-time {\(\mu\)}-calculus},
pages = {1-12},
year = {2017},
doi = {10.1109/LICS.2017.8005075},
abstract = {Modal \(\mu\)-calculus is one of the central logics for verification. In his seminal paper, Kozen proposed an axiomatization for this logic, which was proved to be complete, 13 years later, by Kaivola for the linear-time case and by Walukiewicz for the branching-time one. These proofs are based on complex, non-constructive arguments, yielding no reasonable algorithm to construct proofs for valid formulas. The problematic of constructiveness becomes central when we consider proofs as certificates, supporting the answers of verification tools. In our paper, we provide a new completeness argument for the linear-time \(\mu\)-calculus which is constructive, i.e. it builds a proof for every valid formula. To achieve this, we decompose this difficult problem into several easier ones, taking advantage of the correspondence between the \(\mu\)-calculus and automata theory. More precisely, we lift the well-known automata transformations (non-determinization for instance) to the logical level. To solve each of these smaller problems, we perform first a proof-search in a circular proof system, then we transform the obtained circular proofs into proofs of Kozen's axiomatization.}
}
@inproceedings{G-fossacs17,
address = {Uppsala, Sweden},
month = apr,
year = 2017,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Esparza, Javier and Murawski, Andrzej},
acronym = {{FoSSaCS}'17},
booktitle = {{P}roceedings of the 20th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'17)},
author = {Gilbert, Fr{\'e}d{\'e}ric},
title = {Automated Constructivization of Proofs},
pages = {480-495},
url = {https://hal.inria.fr/hal-01516788},
pdf = {https://hal.inria.fr/hal-01516788/file/constructivization.pdf},
doi = {10.1007/978-3-662-54458-7_28},
abstract = {No computable function can output a constructive proof from a classical one whenever its associated theorem also holds constructively. We show in this paper that it is however possible, in practice, to turn a large amount of classical proofs into constructive ones. We describe for this purpose a linear-time constructivization algorithm which is provably complete on large fragments of predicate logic.}
}
@inproceedings{G-itp17,
address = {Bras{\'{\i}}lia, Brazil},
year = 2017,
month = sep,
volume = 10499,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ayala{-}Rinc{\'{o}}n, Mauricio and Mu{\~{n}}oz, C{\'{e}}sar A.},
acronym = {{ITP}'17},
booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on
{I}nteractive {T}heorem {P}roving ({ITP}'17)},
author = {Gilbert, Fr{\'e}d{\'e}ric},
title = {Proof Certificates in {PVS}},
pages = {262-268},
url = {https://hal.inria.fr/hal-01673517},
pdf = {https://hal.inria.fr/hal-01673517/file/main.pdf},
doi = {10.1007/978-3-319-66107-0_17},
abstract = {The purpose of this work is to allow the proof system PVS to export proof certificates that can be checked externally. This is done through the instrumentation of PVS to record detailed proofs step by step during the proof search process. At the current stage of this work, proofs can be built for any PVS theory. However, some reasoning steps rely on unverified assumptions. For a restricted fragment of PVS, the proofs are exported to the universal proof checker Dedukti, and the unverified assumptions are proved externally using the automated theorem prover MetiTarski.}
}
@inproceedings{B-ocaml17,
author = {Bury, Guillaume},
title = {{mSAT: An OCaml SAT Solver}},
booktitle = {{OCaml Users and Developers Workshop}},
nopages = {},
noeditor = {},
month = sep,
year = 2017,
address = {Oxford, UK},
url = {https://hal.inria.fr/hal-01670765},
pdf = {https://hal.inria.fr/hal-01670765/file/poster.pdf},
abstract = {mSAT: a SAT solving library in OCaml. It solves the satisfibility of propositional clauses. It is Modular: the user provides the theory. And it produces formal proofs.},
note = {Poster}
}
@inproceedings{JS-lpar17,
address = {Maun, Botswana},
month = may,
volume = {46},
series = {EPiC Series in Computing},
publisher = {EasyChair},
editor = {Eiter, Thomas and Sands, David},
acronym = {{LPAR}'17},
booktitle = {{P}roceedings of the 21st {I}nternational
{C}onference on {L}ogic for {P}rogramming,
{A}rtificial {I}ntelligence, and {R}easoning
({LPAR}'17)},
author = {Jouannaud, Jean-Pierre and Strub, Pierre-Yves},
title = {{Coq without Type Casts: A Complete Proof of Coq Modulo Theory}},
pages = {474-489},
year = {2017},
pdf = {https://hal.inria.fr/hal-01664457/file/final-version.pdf},
url = {https://easychair.org/publications/paper/BKQ},
abstract = {Incorporating extensional equality into a dependent intensional type system such as the Calculus of Constructions provides with stronger type-checking capabilities and makes the proof development closer to intuition. Since strong forms of extensionality lead to undecidable type-checking, a good trade-off is to extend intensional equality with a decidable first-order theory T, as done in CoqMT, which uses matching modulo T for the weak and strong elimination rules, we call these rules T-elimination. So far, type-checking in CoqMT is known to be decidable in presence of a cumulative hierarchy of universes and weak T-elimination. Further, it has been shown by Wang with a formal proof in Coq that consistency is preserved in presence of weak and strong elimination rules, which actually implies consistency in presence of weak and strong T-elimination rules since T is already present in the conversion rule of the calculus.
\par
We justify here CoqMT's type-checking algorithm by showing strong normalization as well as the Church-Rosser property of \(\beta\)-reductions augmented with CoqMT's weak and strong T-elimination rules. This therefore concludes successfully the meta-theoretical study of CoqMT.}
}
@article{BFM-lmcs17,
journal = {Logical Methods in Computer Science},
author = {Blondin, Michael and Finkel, Alain and McKenzie, Pierre},
title = {Well Behaved Transition Systems},
volume = {13},
number = {3},
year = {2017},
month = sep,
pages = {1-19},
doi = {10.23638/LMCS-13(3:24)2017},
url = {https://doi.org/10.23638/LMCS-13(3:24)2017}
}
@article{FS-lmcs17,
journal = {Logical Methods in Computer Science},
author = {Figueira, Diego and Segoufin, Luc},
title = {Bottom-up automata on data trees and vertical {XP}ath},
volume = {13},
number = {4:5},
year = {2017},
month = nov,
doi = {10.23638/LMCS-13(4:5)2017},
abstract = {A data tree is a finite tree whose every node
carries a label from a finite alphabet and a datum
from some infinite domain. We introduce a new model
of automata over unranked data trees with a
decidable emptiness problem. It is essentially a
bottom-up alternating automaton with one register
that can store one data value and can be used to
perform equality tests with the data values
occurring within the subtree of the current node. We
show that it captures the expressive power of the
vertical fragment of XPath - containing the child,
descendant, parent and ancestor axes - obtaining
thus a decision procedure for its satisfiability
problem.}
}
@phdthesis{schmitz-hdr2017,
author = {Schmitz, Sylvain},
title = {Algorithmic Complexity of Well-Quasi-Orders},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {M{\'e}moire d'habilitation},
year = 2017,
month = nov,
url = {http://tel.archives-ouvertes.fr/tel-01663266}
}
@inproceedings{PhS-mfcs17,
address = {Aalborg, Denmark},
month = aug,
year = 2017,
volume = {83},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Fran{\c{c}}ois},
acronym = {{MFCS}'17},
booktitle = {{P}roceedings of the 42nd
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'17)},
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Ideal-Based Algorithms for the Symbolic Verification of Well-Structured Systems (Invited Talk)},
pages = {85:1-85:4},
url = {http://drops.dagstuhl.de/opus/volltexte/2017/8139/},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/8139/pdf/LIPIcs-MFCS-2017-85.pdf},
doi = {10.4230/LIPIcs.MFCS.2017.85},
abstract = {We explain how the downward-closed subsets of a well-quasi-ordering (\(X,\leq\)) can be represented via the ideals of \(X\) and how this leads to simple and efficient algorithms for the verification of well-structured systems.}
}
@article{JGL-minimax17,
publisher = {Heldermann Verlag},
journal = {Minimax Theory and its Applications},
author = {Goubault{-}Larrecq, Jean},
title = {A Non-{H}ausdorff Minimax Theorem},
volume = {3},
number = {1},
year = {2017},
pages = {73-80}
}
@inproceedings{MHP-cmsb17,
address = {Darmstadt, Germany},
month = sep,
year = 2017,
volume = {10545},
series = {Lecture Notes in Bioinformatics},
publisher = {Springer-Verlag},
editor = {Feret, J{\'e}r{\^o}me and Koeppl, Heinz},
acronym = {{CMSB}'17},
booktitle = {{P}roceedings of the 15th
{C}onference on
{C}omputational {M}ethods in {S}ystem {B}iology
({CMSB}'17)},
author = {Mandon, Hugues and Haar, Stefan and Paulev{\'e}, Lo{\"i}c},
title = {{Temporal Reprogramming of Boolean Networks}},
pages = {179-195},
pdf = {https://hal.inria.fr/hal-01589251/document},
doi = {10.1007/978-3-319-67471-1\_11},
abstract = {Cellular reprogramming, a technique that opens huge opportunities in modern and regenerative medicine, heavily relies on identifying key genes to perturb. Most of computational methods focus on finding mutations to apply to the initial state in order to control which attractor the cell will reach. However, it has been shown, and is proved in this article, that waiting between the perturbations and using the transient dynamics of the system allow new reprogramming strategies. To identify these temporal perturbations, we consider a qualitative model of regulatory networks, and rely on Petri nets to model their dynamics and the putative perturbations. Our method establishes a complete characterization of temporal perturbations, whether permanent (mutations) or only temporary, to achieve the existential or inevitable reachability of an arbitrary state of the system. We apply a prototype implementation on small models from the literature and show that we are able to derive temporal perturbations to achieve trans-differentiation.}
}
@techreport{CDD-hal17,
author = {Cortier, V{\'e}ronique and Dallon, Antoine and Delaune, St{\'e}phanie},
institution = {HAL},
month = oct,
number = {hal-01615265},
type = {Research Report},
title = {A typing result for trace inclusion (for pair and symmetric encryption only)},
year = {2017},
url = {https://hal.archives-ouvertes.fr/hal-01615265},
pdf = {https://hal.archives-ouvertes.fr/hal-01615265/document},
abstract = {Privacy-type properties such as vote secrecy, anonymity, or untraceability are typically expressed using the notion of trace equivalence in a process algebra that models security protocols. In this paper, we propose some results to reduce the search space when we are looking for an attack regarding trace equivalence. Our work is strongly inspired from [10], which establishes that, if there is a witness of non trace equivalence, then there is one that is well-typed.\par
Our main contribution is to establish a similar result for trace inclusion. Our motivation is twofolds: first, this small attack property is needed for proving soundness of the tool SatEquiv [13]. Second, we revisit the proof in order to simplify it. Specifically, we show two results. First, if there is a witness of non-inclusion then there is one that is well-typed. We establish this result by providing a decision procedure for trace inclusion similar to the one proposed in [10] for trace equivalence. We also show that we can reduce the search space when considering the notion of static inclusion. Acutally, if there is a witness of static non-inclusion there is one of a specific shape.\par
Even if our setting slightly differs from the one considered in [10], our proofs essentially follow the same ideas than the existing proof for trace equivalence. Nevertheless, we hope that this proof will be easier to extend to other primitives such as asymmetric encryption or signatures.}
}
@article{DDS-tcs17,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Demri, St{\'e}phane and Dhar, Amit and Sangnier, Arnaud},
title = {Equivalence Between Model-Checking Flat Counter Systems and Presburger Arithmetic},
volume = {735},
optnumber = {},
year = {2017},
pages = {2-23},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-tcs17.pdf}
}
@article{GLN-lmcs17,
journal = {Logical Methods in Computer Science},
author = {Goubault{-}Larrecq, Jean and Ng, Kok Min},
title = {A Few Notes on Formal Balls},
volume = {13},
number = {4},
year = {2017},
month = nov,
pages = {1-34},
doi = {10.23638/LMCS-13(4:18)2017},
url = {https://lmcs.episciences.org/4100},
pdf = {https://lmcs.episciences.org/4100/pdf},
note = {Special Issue of the Domains XII Workshop}
}
@incollection{CDH-kimfest17,
author = {Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, {\relax Th}omas~A.},
title = {The Cost of Exactness in Quantitative Reachability},
editor = {Aceto, Luca and Bacci, Giorgio and Bacci, Giovani
and Ing{\'o}lfsd{\'o}ttir, Anna and Legay, Axel and
Mardare, Radu},
booktitle = {Models, Algorithms, Logics and Tools: Essays
Dedicated to Kim Guldstrand Larsen on the Occasion
of His 60th Birthday},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {10460},
year = {2017},
pages = {367-381},
month = aug,
doi = {10.1007/978-3-319-63121-9_18},
abstract = {In the analysis of reactive systems a quantitative objective assigns a real value to every trace of the system. The value decision problem for a quantitative objective requires a trace whose value is at least a given threshold, and the exact value decision problem requires a trace whose value is exactly the threshold. We compare the compu- tational complexity of the value and exact value decision problems for classical quantitative objectives, such as sum, discounted sum, energy, and mean-payoff for two standard models of reactive systems, namely, graphs and graph games.},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDH-2017.pdf}
}
@article{CDFR-ic17,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Krishnendu Chatterjee and Laurent Doyen and Emmanuel Filiot and Jean{-}Fran{\c{c}}ois Raskin},
title = {Doomsday equilibria for omega-regular games},
volume = {254},
year = {2017},
pages = {296-315},
doi = {10.1016/j.ic.2016.10.012},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDFR-ic2017.pdf},
abstract = {Two-player games on graphs provide the theoretical framework for many important problems such as reactive synthesis. While the traditional study of two-player zero-sum games has been extended to multi-player games with several notions of equilibria, they are decidable only for perfect-information games, whereas several applications require imperfect-information games.\par
In this paper we propose a new notion of equilibria, called doomsday equilibria, which is a strategy profile such that all players satisfy their own objective, and if any coalition of players deviates and violates even one of the players objective, then the objective of every player is violated.\par
We present algorithms and complexity results for deciding the existence of doomsday equilibria for various classes of ?-regular objectives, both for imperfect-information games, and for perfect-information games. We provide optimal complexity bounds for imperfect-information games, and in most cases for perfect- information games.}
}
@inproceedings{D-rp17,
address = {London, UK},
month = sep,
year = 2017,
volume = {10506},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Matthew Hague and Igor Potapov},
acronym = {{RP}'17},
booktitle = {{P}roceedings of the 11th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'17)},
author = {Doyen, Laurent},
title = {The Multiple Dimensions of Mean-Payoff Games},
pages = {1-8},
url = {https://doi.org/10.1007/978-3-319-67089-8_1},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Doyen-rp2017.pdf},
doi = {10.1007/978-3-319-67089-8_1},
abstract = {We consider quantitative game models for the design of reactive systems working in resource-constrained environment. The game is played on a finite weighted graph where some resource (e.g., battery) can be consumed or recharged along the edges of the graph.}
}
@article{LS-siglog17,
publisher = {ACM Press},
journal = {SIGLOG News},
abstract = {We consider a logical framework building on
existential positive formulas and then adding
guarded negations and guarded fixpoints, where the
guards are atomic formulas containing all free
variables. The resulting first-order and fixpoint
logics turn out to have nice algorithmic properties
and nice expressive power. We survey some of them.},
author = {Segoufin, Luc},
doi = {10.1145/3129173.3129178},
month = jul,
number = {3},
pages = {12-26},
title = {A survey on guarded negation},
volume = {4},
year = {2017}
}
@inproceedings{TFL-async17,
address = {San Diego, California, USA},
month = may,
publisher = {{IEEE} Computer Society},
editor = {Beign{\'e}, Edith and Stevens, Ken},
acronym = {{ASYNC}'17},
booktitle = {{P}roceedings of the 23rd {IEEE} {I}nternational {S}ymposium on {A}synchronous {C}ircuits and {S}ystems ({ASYNC}'17)},
author = {Ghaith Tarawneh and Matthias F{\"u}gger and Christoph Lenzen},
title = {Metastability Tolerant Computing},
pages = {25-32},
year = {2017},
doi = {10.1109/ASYNC.2017.9},
pdf = {http://www.lsv.fr/~mfuegger/papers/TFL17_async.pdf},
url = {http://ieeexplore.ieee.org/abstract/document/8097381/},
abstract = {Synchronization using flip-flop chains imposes a latency of a few clock cycles when transferring data and control signals between clock domains. We propose a design scheme that avoids this latency by performing synchronization as part of state/data computations while guaranteeing that metastability is contained and its effects tolerated (with an acceptable failure probability). We present a theoretical framework for modeling synchronous state machines in the presence of metastability and use it to prove properties that guarantee some form of reliability. Specifically, we show that the inevitable state/data corruption resulting from propagating metastable states can be confined to a subset of computations. Applications that can tolerate certain failures can exploit this property to leverage low-latency and quasi-reliable operation simultaneously. We demonstrate the approach by designing a Network-on-Chip router with zero- latency asynchronous ports and show via simulation that it outperforms a variant with two flip-flop synchronizers at a negligible cost in packet transfer reliability.}
}
@inproceedings{FKLP-async17,
address = {San Diego, California, USA},
month = may,
publisher = {{IEEE} Computer Society},
editor = {Beign{\'e}, Edith and Stevens, Ken},
acronym = {{ASYNC}'17},
booktitle = {{P}roceedings of the 23rd {IEEE} {I}nternational {S}ymposium on {A}synchronous {C}ircuits and {S}ystems ({ASYNC}'17)},
author = {Matthias F{\"u}gger and Attila Kinali and Christoph Lenzen and Thomas Polzer},
title = {Metastability-Aware Memory-Efficient Time-to-Digital Converter},
pages = {49-56},
year = {2017},
doi = {10.1109/ASYNC.2017.12},
pdf = {http://www.lsv.fr/~mfuegger/pub/FKLP17.pdf},
url = {https://doi.org/10.1109/ASYNC.2017.12},
abstract = {We propose a novel method for transforming delay- line time-to-digital converters (TDCs) into TDCs that output Gray code without relying on synchronizers. We formally prove that the inevitable metastable memory upsets (Marino, TC'81) do not induce an additional time resolution error. Our modified design provides suitable inputs to the recent metastability-containing sorting networks by Lenzen and Medina (ASYNC'16) and Bund et al. (DATE'17). In contrast, employing existing TDCs would require using thermometer code at the TDC output (followed by conversion to Gray code) or resolving metastability inside the TDC. The former is too restrictive w.r.t. the dynamic range of the TDCs, while the latter loses the advantage of enabling (accordingly much faster) computation without having to first resolve metastability.\par
Our all-digital designs are also of interest in their own right: they support high sample rates and large measuring ranges at nearly optimal bit-width of the output, yet maintain the original delay-line?s time resolution. No previous approach unifies all these properties in a single device.}
}
@inproceedings{FNS-disc17,
address = {Vienna, Austria},
month = oct,
year = 2017,
volume = 91,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Richa, Andr{\'e}a},
acronym = {{DISC}'17},
booktitle = {{P}roceedings of the 31st {I}nternational
{S}ymposium on {D}istributed {C}omputing
({DISC}'17)},
author = {Matthias F{\"u}gger and {\relax Th}omas Nowak and Manfred Schwarz},
title = {Brief Announcement: Lower Bounds for Asymptotic Consensus in Dynamic Networks},
pages = {51:1-51:3},
url = {http://drops.dagstuhl.de/opus/volltexte/2017/7992/},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7992/pdf/LIPIcs-DISC-2017-51.pdf},
doi = {10.4230/LIPIcs.DISC.2017.51},
abstract = {In this work we study the performance of asymptotic and approximate consensus algorithms in dynamic networks. The asymptotic consensus problem requires a set of agents to repeatedly set their outputs such that the outputs converge to a common value within the convex hull of initial values. This problem, and the related approximate consensus problem, are fundamental building blocks in distributed systems where exact consensus among agents is not required, e.g., man- made distributed control systems, and have applications in the analysis of natural distributed systems, such as flocking and opinion dynamics. We prove new nontrivial lower bounds on the contraction rates of asymptotic consensus algorithms, from which we deduce lower bounds on the time complexity of approximate consensus algorithms. In particular, the obtained bounds show optimality of asymptotic and approximate consensus algorithms presented in [Charron-Bost et al., ICALP’16] for certain classes of networks that include classical failure assumptions, and confine the search for optimal bounds in the general case.
Central to our lower bound proofs is an extended notion of valency, the set of reachable limits of an asymptotic consensus algorithm starting from a given configuration. We further relate topological properties of valencies to the solvability of exact consensus, shedding some light on the relation of these three fundamental problems in dynamic networks.}
}
@article{BCMW-fi17,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {David Baelde and Arnaud Carayol and Ralph Matthes and Igor Walukiewicz},
title = {Preface: Special Issue of {Fixed Points in Computer Science} ({FICS}'13)},
volume = {150},
number = {3-4},
pages = {i-ii},
year = {2017},
url = {https://doi.org/10.3233/FI-2017-1468},
doi = {10.3233/FI-2017-1468}
}
@inproceedings{BDGK-csf17,
address = {Santa Barbara, California, USA},
month = aug,
publisher = {{IEEE} Computer Society Press},
editor = {K{\"o}pf, Boris and Chong, Steve},
acronym = {{CSF}'17},
booktitle = {{P}roceedings of the
30th {IEEE} {C}omputer {S}ecurity {F}oundations
{S}ymposium ({CSF}'17)},
author = {Baelde, David and Delaune, St{\'e}phanie and Gazeau, Ivan and Kremer, Steve},
title = {Symbolic Verification of Privacy-Type Properties for Security Protocols with {XOR}},
pages = {234-248},
year = {2017},
doi = {10.1109/CSF.2017.22},
pdf = {https://hal.inria.fr/hal-01533694/document},
url = {https://hal.inria.fr/hal-01533694},
abstract = {In symbolic verification of security protocols, process equivalences have recently been used extensively to model strong secrecy, anonymity and unlinkability properties. However, tool support for automated analysis of equivalence properties is limited compared to trace properties, e.g., modeling authentication and weak notions of secrecy. In this paper, we present a novel procedure for verifying equivalences on finite processes, i.e., without replication, for protocols that rely on various cryptographic primitives including exclusive or (xor). We have implemented our procedure in the tool AKISS, and successfully used it on several case studies that are outside the scope of existing tools, e.g., unlinkability on various RFID protocols, and resistance against guessing attacks on protocols that use xor.}
}
@inproceedings{CDD-csf17,
address = {Santa Barbara, California, USA},
month = aug,
publisher = {{IEEE} Computer Society Press},
editor = {K{\"o}pf, Boris and Chong, Steve},
acronym = {{CSF}'17},
booktitle = {{P}roceedings of the
30th {IEEE} {C}omputer {S}ecurity {F}oundations
{S}ymposium ({CSF}'17)},
author = {Cortier, V{\'e}ronique and Dallon, Antoine and Delaune, St{\'e}phanie},
title = {{SAT-Equiv}: An Efficient Tool for Equivalence Properties},
pages = {481-494},
year = {2017},
doi = {10.1109/CSF.2017.15},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDD-csf17.pdf},
url = {http://ieeexplore.ieee.org/document/8049740/},
abstract = {Automatic tools based on symbolic models have been successful in analyzing security protocols. Such tools are particularly adapted for trace properties (e.g. secrecy or authentication), while they often fail to analyse equivalence properties.Equivalence properties can express a variety of security properties, including in particular privacy properties (vote privacy, anonymity, untraceability). Several decision procedures have already been proposed but the resulting tools are rather inefficient.In this paper, we propose a novel algorithm, based on graph planning and SAT-solving, which significantly improves the efficiency of the analysis of equivalence properties. The resulting implementation, SAT-Equiv, can analyze several sessions where most tools have to stop after one or two sessions.}
}
@inproceedings{CCV-er17,
address = {Valencia, Spain},
month = nov,
volume = 10650,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Mayr, Heinrich C. and Guizzardi, Giancarlo and Ma, Hui and Pastor, Oscar},
booktitle = {{P}roceedings of the 36th {I}nternational {C}onference on {C}onceptual {M}odeling ({ER}'17)},
author = {Chatain, {\relax Th}omas and Carmona, Josep and van Dongen, Boudewijn},
title = {Alignment-Based Trace Clustering},
pages = {295-308},
year = {2017},
doi = {10.1007/978-3-319-69904-2_24},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCV-er17.pdf},
url = {https://doi.org/10.1007/978-3-319-69904-2_24},
abstract = {A novel method to cluster event log traces is presented in this paper. In contrast to the approaches in the literature, the clustering approach of this paper assumes an additional input: a process model that describes the current process. The core idea of the algorithm is to use model traces as centroids of the clusters detected, computed from a generalization of the notion of alignment. This way, model explanations of observed behavior are the driving force to compute the clusters, instead of current model agnostic approaches, e.g., which group log traces merely on their vector-space similarity. We believe alignment-based trace clustering provides results more useful for stakeholders. Moreover, in case of log incompleteness, noisy logs or concept drift, they can be more robust for dealing with highly deviating traces. The technique of this paper can be combined with any clustering technique to provide model explanations to the clusters computed. The proposed technique relies on encoding the individual alignment problems into the (pseudo-)Boolean domain, and has been implemented in our tool DarkSider that uses an open-source solver.},
note = {To appear}
}
@phdthesis{doumane-phd2017,
author = {Doumane, Amina},
title = {On the infinitary proof theory of logics with fixed points},
school = {Universit{\'e} Paris-Diderot, Paris, France},
type = {Th{\`e}se de doctorat},
year = 2017,
month = jun,
url = {https://www.irif.fr/~doumane/these.pdf},
pdf = {https://www.irif.fr/~doumane/these.pdf}
}
@inproceedings{LDCF-snr17,
address = {Uppsala, Sweden},
month = apr,
year = 2017,
volume = 247,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Erika {\'{A}}brah{\'{a}}m and Sergiy Bogomolov},
acronym = {{SNR}'17},
booktitle = {{P}roceedings of the 3rd {I}nternational {W}orkshop
on {S}ymbolic and {N}umerical {M}ethods for
{R}eachability {A}nalysis ({SNR}'17)},
author = {Adrien Le{ }Co{\"e}nt and
Florian De{ }Vuyst and
Ludovic Chamoin and
Laurent Fribourg},
title = {Control Synthesis of Nonlinear Sampled Switched Systems using Euler's Method},
pages = {18-33},
url = {https://arxiv.org/abs/1704.03102v1},
pdf = {https://arxiv.org/pdf/1704.03102v1.pdf},
doi = {10.4204/EPTCS.247.2},
abstract = {In this paper, we propose a symbolic control synthesis method for nonlinear sampled switched systems whose vector fields are one-sided Lipschitz. The main idea is to use an approximate model obtained from the forward Euler method to build a guaranteed control. The benefit of this method is that the error introduced by symbolic modeling is bounded by choosing suitable time and space discretizations. The method is implemented in the interpreted language Octave. Several examples of the literature are performed and the results are compared with results obtained with a previous method based on the Runge-Kutta integration method.}
}
@inproceedings{F-formats17,
address = {Berlin, Germany},
month = sep,
year = 2017,
volume = {10419},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abate, Alessandro and Geeraerts, Gilles},
acronym = {{FORMATS}'17},
booktitle = {{P}roceedings of the 15th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'17)},
author = {Fribourg, Laurent},
title = {Euler's Method Applied to the Control of Switched Systems},
pages = {3-21},
url = {https://doi.org/10.1007/978-3-319-65765-3_1},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/F-formats17.pdf},
doi = {10.1007/978-3-319-65765-3_1},
abstract = {Hybrid systems are a powerful formalism for modeling and reasoning about cyber-physical systems. They mix the continuous and discrete natures of the evolution of computerized systems. Switched systems are a special kind of hybrid systems, with restricted discrete behaviours: those systems only have finitely many different modes of (continuous) evolution, with isolated switches between modes. Such systems provide a good balance between expressiveness and controllability, and are thus in widespread use in large branches of industry such as power electronics and automotive control. The control law for a switched system defines the way of selecting the modes during the run of the system. Controllability is the problem of (automatically) synthesizing a control law in order to satisfy a desired property, such as safety (maintaining the variables within a given zone) or stabilisation (confinement of the variables in a close neighborhood around an objective point). In order to compute the control of a switched system, we need to compute the solutions of the differential equations governing the modes. Euler's method is the most basic technique for approximating such solutions. We present here an estimation of the Euler's method local error, using the notion of ''one-sided Lispchitz constant'' for modes. This yields a general control synthesis approach which can encompass several features such as bounded disturbance and compositionality.}
}
@inproceedings{BLL-rp17,
address = {London, UK},
month = sep,
year = 2017,
volume = {10506},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Matthew Hague and Igor Potapov},
acronym = {{RP}'17},
booktitle = {{P}roceedings of the 11th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'17)},
author = {Florian Bruse and
Martin Lange and
{\'E}tienne Lozes},
title = {Space-Efficient Fragments of Higher-Order Fixpoint Logic},
pages = {26-41},
url = {https://doi.org/10.1007/978-3-319-67089-8_3},
doi = {10.1007/978-3-319-67089-8_3},
abstract = {Higher-Order Fixpoint Logic (HFL) is a modal specification language whose expressive power reaches far beyond that of Monadic Second-Order Logic, achieved through an incorporation of a typed \(\lambda\)-calculus into the modal \(\mu\)-calculus. Its model checking problem on finite transition systems is decidable, albeit of high complexity, namely \(k\)-EXPTIME-complete for formulas that use functions of type order at most \(k>0\). In this paper we present a fragment with a presumably easier model checking problem. We show that so-called tail-recursive formulas of type order \(k\) can be model checked in \((k-1)\)-EXPSPACE, and also give matching lower bounds. This yields generic results for the complexity of bisimulation-invariant non-regular properties, as these can typically be defined in HFL.}
}
@inproceedings{LACFDC-rp17,
address = {London, UK},
month = sep,
year = 2017,
volume = {10506},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Matthew Hague and Igor Potapov},
acronym = {{RP}'17},
booktitle = {{P}roceedings of the 11th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'17)},
author = {Adrien Le{ }Co{\"{e}}nt and
Julien {Alexandre dit Sandretto} and
Alexandre Chapoutot and
Laurent Fribourg and
Florian De{ }Vuyst and
Ludovic Chamoin},
title = {Distributed Control Synthesis Using Euler's Method},
pages = {118-131},
url = {https://link.springer.com/chapter/10.1007/978-3-319-67089-8_9},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LACFDC-rp17.pdf},
doi = {10.1007/978-3-319-67089-8_9},
abstract = {In a previous work, we explained how Euler's method for computing approximate solutions of systems of ordinary differential equations can be used to synthesize safety controllers for sampled switched systems. We continue here this line of research by showing how Euler's method can also be used for synthesizing safety controllers in a distributed manner. The global system is seen as an interconnection of two (or more) sub-systems where, for each component, the sub-state corresponding to the other component is seen as an ?input?; the method exploits (a variant of) the notions of incremental input-to-state stability (\(\delta\)-ISS) and ISS Lyapunov function. We illustrate this distributed control synthesis method on a building ventilation example.}
}
@inproceedings{BHL-msr17,
address = {Marseille, France},
month = nov,
year = 2017,
futureseries = {Journal Europ{\'e}en des Syst{\`e}mes Automatis{\'e}s},
publisher = {HAL},
editor = {Demongodin, Isabel and Reynier, Pierre-Alain},
acronym = {{MSR}'17},
booktitle = {{A}ctes du 11{\`e}me {C}olloque sur la
{M}od{\'e}lisation des {S}yst{\`e}mes
{R}{\'e}actifs
({MSR}'17)},
author = {Nathalie Bertrand and Serge Haddad and Engel Lefaucheux},
title = {Diagnostic et contr{\^o}le de la d{\'e}gradation des syst{\`e}mes probabilistes},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHL-msr17.pdf},
abstract = {Le diagnostic actif est op{\'e}r{\'e} par un contr{\^o}leur en vue de rendre un syst{\`e}me diagnosticable. Afin d'{\'e}viter que le contr{\^o}leur ne d{\'e}grade trop fortement le syst{`e}me, on lui affecte g{\'e}n{\'e}ralement un second objectif en termes de qualit{\'e} de service. Dans le cadre des syst{\`e}mes probabilistes, une sp{\'e}cification possible consiste {\`a} assurer une probabilit{\'e} positive qu'une ex{\'e}cution infinie soit correcte, ce qu'on appelle le diagnostic
actif s{\^u}r. Nous introduisons ici deux sp{\'e}cifications alternatives. La gamma-correction du syst{\`e}me affecte {\`a} une ex{\'e}cution une valeur de correction d{\'e}pendant d'un facteur de d{\'e}cote gamma et le contr{\^o}leur doit assurer une valeur moyenne sup{\'e}rieure {\`a} un seuil fix{\'e}. La alpha-d{\'e}gradation requiert qu'asymptotiquement, {\`a} chaque unit{\'e} de temps une proportion sup{\'e}rieure {\`a} alpha des ex{\'e}cutions jusqu'alors correctes le demeure. D'un point de vue s{\'e}mantique, nous explicitons des liens significatifs entre les diff{\'e}rentes notions. Algorithmiquement, nous {\'e}tablissons la fronti{\`e}re entre d{\'e}cidabilit{\'e} et ind{\'e}cidabilit{\'e} des probl{\`e}mes et dans le cas positif nous exhibons la complexit{\'e} pr{\'e}cise ainsi qu'une synth{\`e}se, potentiellement {\`a} m{\'e}moire infinie.}
}
@inproceedings{BHL-fsttcs17,
address = {Kanpur, India},
month = dec,
year = 2017,
volume = {93},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Satya Lokam and R. Ramanujam},
acronym = {{FSTTCS}'17},
booktitle = {{P}roceedings of the 37th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'17)},
author = {B{\'e}atrice B{\'e}rard and Serge Haddad and Engel Lefaucheux},
title = {Probabilistic Disclosure: Maximisation vs. Minimisation},
pages = {13:1-13:14},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=8384},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/8384/pdf/LIPIcs-FSTTCS-2017-13.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2017.13},
abstract = {We consider opacity questions where an observation function provides to an external attacker a view of the states along executions and secret executions are those visiting some state from a fixed subset. Disclosure occurs when the observer can deduce from a finite observation that the execution is secret, the epsilon-disclosure variant corresponding to the execution being secret with probability greater than 1 - epsilon. In a probabilistic and non deterministic setting, where an internal agent can choose between actions, there are two points of view, depending on the status of this agent: the successive choices can either help the attacker trying to disclose the secret, if the system has been corrupted, or they can prevent disclosure as much as possible if these choices are part of the system design. In the former situation, corresponding to a worst case, the disclosure value is the supremum over the strategies of the probability to disclose the secret (maximisation), whereas in the latter case, the disclosure is the infimum (minimisation). We address quantitative problems (comparing the optimal value with a threshold) and qualitative ones (when the threshold is zero or one) related to both forms of disclosure for a fixed or finite horizon. For all problems, we characterise their decidability status and their complexity. We discover a surprising asymmetry: on the one hand optimal strategies may be chosen among deterministic ones in maximisation problems, while it is not the case for minimisation. On the other hand, for the questions addressed here, more minimisation problems than maximisation ones are decidable.}
}
@inproceedings{BFG-fsttcs17,
address = {Kanpur, India},
month = dec,
year = 2017,
volume = {93},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Satya Lokam and R. Ramanujam},
acronym = {{FSTTCS}'17},
booktitle = {{P}roceedings of the 37th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'17)},
author = {Michael Blondin and Alain Finkel and Jean Goubault{-}Larrecq},
title = {Forward Analysis for {WSTS}, {Part III}: {Karp-Miller} Trees},
pages = {16:1-16:15},
url = {https://hal.archives-ouvertes.fr/hal-01736704/},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/8403/pdf/LIPIcs-FSTTCS-2017-16.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2017.16},
abstract = {This paper is a sequel of ''Forward Analysis for WSTS, Part I: Completions'' [STACS 2009, LZI Intl. Proc. in Informatics 3, 433-444] and ''Forward Analysis for WSTS, Part II: Complete WSTS'' [Logical Methods in Computer Science 8(3), 2012]. In these two papers, we provided a framework to conduct forward reachability analyses of WSTS, using finite representations of downwards-closed sets. We further develop this framework to obtain a generic Karp-Miller algorithm for the new class of very-WSTS. This allows us to show that coverability sets of very-WSTS can be computed as their finite ideal decompositions. Under natural assumptions on positive sequences, we also show that LTL model checking for very-WSTS is decidable. The termination of our procedure rests on a new notion of acceleration levels, which we study. We characterize those domains that allow for only finitely many accelerations, based on ordinal ranks.}
}
@inproceedings{DLL-fsttcs17,
address = {Kanpur, India},
month = dec,
year = 2017,
volume = {93},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Satya Lokam and R. Ramanujam},
acronym = {{FSTTCS}'17},
booktitle = {{P}roceedings of the 37th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'17)},
author = {St{\'e}phane Demri and {\'E}tienne Lozes and Denis Lugiez},
title = {On Symbolic Heaps Modulo Permission Theories},
pages = {25:1-25:14},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DLL-fsttcs17.pdf},
url = {https://doi.org/10.4230/LIPIcs.FSTTCS.2017.25},
doi = {10.4230/LIPIcs.FSTTCS.2017.25}
}
@phdthesis{dubut-phd2017,
author = {Dubut, J{\'e}r{\'e}my},
title = {Directed homotopic and homologic theories for geometric models of true concurrency},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2017,
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/dubut-phd17.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/dubut-phd17.pdf}
}
@phdthesis{gardy-phd2017,
author = {Gardy, Patrick},
title = {Semantics of {S}trategy {L}ogic},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2017,
month = jun,
url = {https://tel.archives-ouvertes.fr/tel-01561802},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/gardy-phd17.pdf}
}
@inproceedings{GBBLM-gretsi17,
address = {Juan-les-Pins, France},
month = sep,
year = 2017,
publisher = {},
editor = {},
acronym = {{GRETSI}'17},
booktitle = {Actes du XXVI$^{\text{\`eme}}$ colloque GRETSI},
author = {Mauricio Gonz{\'a}lez and Olivier Beaude and
Patricia Bouyer and Samson Lasaulce and Nicolas
Markey},
title = {Strat{\'e}gies d'ordonnancement de consommation
d'{\'e}nergie en pr{\'e}sence d'information
imparfaite de pr{\'e}vision},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GBBLM-gretsi17.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GBBLM-gretsi17.pdf}
}
@techreport{Haddad-hal17,
author = {Haddad, Serge},
title = {Memoryless Determinacy of Finite Parity Games: Another Simple Proof},
institution = {HAL-inria},
number = {hal-01541508},
month = jun,
year = {2017},
type = {Research Report},
url = {https://hal.inria.fr/hal-01541508},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Haddad-hal17.pdf},
note = {7~pages},
abstract = {Memoryless determinacy of (infinite) parity games is an important result with numerous applications. It was first independently established by Emerson and Jutla [1] and Mostowski [2] but their proofs involve elaborate developments. The elegant and simpler proof of Zielonka [3] still requires a nested induction on the finite number of priorities and on ordinals for sets of vertices. There are other proofs for finite games like the one of Bj{\"o}rklund, Sandberg and Vorobyovin [4] that relies on relating infinite and finite duration games. We present here another simple proof that finite parity games are determined with memoryless strategies using induction on the number of relevant states. The closest proof that relies on induction over non absorbing states is the one of Graedel [5]. However instead of focusing on a single appropriate vertex for induction as we do here, he considers two reduced games per vertex, for all the vertices of the game. The idea of reasoning about a single state has been inspired to me by the analysis of finite stochastic priority games by Karelovic and Zielonka [6].}
}
@techreport{BJM-arxiv17,
author = {Bouyer, Patricia and Markey, Nicolas and
Jug{\'e}, Vincent},
institution = {Computing Research Repository},
month = feb,
note = {14~pages},
number = {1702.05183},
type = {Research Report},
title = {Courcelle's Theorem Made Dynamic},
year = {2017},
url = {https://arxiv.org/abs/1702.05183},
pdf = {https://arxiv.org/abs/1702.05183}
}
@inproceedings{CP-concur17,
address = {Berlin, Germany},
month = sep,
year = 2017,
volume = {85},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Meyer, Roland and Nestmann, Uwe},
acronym = {{CONCUR}'17},
booktitle = {{P}roceedings of the 28th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'17)},
author = {Chatain, {\relax Th}omas and Paulev{\'e}, Lo{\"i}c},
title = {Goal-Driven Unfolding of {P}etri Nets},
pages = {18:1-18:16},
url = {http://drops.dagstuhl.de/opus/volltexte/2017/7773},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7773/pdf/LIPIcs-CONCUR-2017-18.pdf},
doi = {10.4230/LIPIcs.CONCUR.2017.18},
abstract = {Unfoldings provide an efficient way to avoid the state-space explosion due to interleavings of concurrent transitions when exploring the runs of a Petri net. The theory of adequate orders allows one to define finite prefixes of unfoldings which contain all the reachable markings. In this paper we are interested in reachability of a single given marking, called the goal. We propose an algorithm for computing a finite prefix of the unfolding of a 1-safe Petri net that preserves all minimal configurations reaching this goal. Our algorithm combines the unfolding technique with on-the-fly model reduction by static analysis aiming at avoiding the exploration of branches which are not needed for reaching the goal. We present some experimental results.}
}
@inproceedings{BHJ-concur17,
address = {Berlin, Germany},
month = sep,
year = 2017,
volume = {85},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Meyer, Roland and Nestmann, Uwe},
acronym = {{CONCUR}'17},
booktitle = {{P}roceedings of the 28th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'17)},
author = {Bouyer, Patricia and Haddad, Serge and Jug{\'e}, Vincent},
title = {Unbounded product-form {P}etri nets},
pages = {31:1--31:16},
url = {http://drops.dagstuhl.de/opus/volltexte/2017/7795},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7795/pdf/LIPIcs-CONCUR-2017-31.pdf},
doi = {10.4230/LIPIcs.CONCUR.2017.31},
abstract = {Computing steady-state distributions in infinite-state stochastic systems is in general a very difficult task. Product-form Petri nets are those Petri nets for which the steady-state distribution can be described as a natural product corresponding, up to a normalising constant, to an exponentiation of the markings. However, even though some classes of nets are known to have a product-form distribution, computing the normalising constant can be hard. The class of (closed) \(\Pi^3\)-nets has been proposed in an earlier work, for which it is shown that one can compute the steady-state distribution efficiently. However these nets are bounded. In this paper, we generalise queuing Markovian networks and closed \(\Pi^3\)-nets to obtain the class of open \(\Pi^3\)-nets, that generate infinite-state systems. We show interesting properties of these nets: (1) we prove that liveness can be decided in polynomial time, and that reachability in live \(\Pi^3\)-nets can be decided in polynomial time; (2) we show that we can decide ergodicity of such nets in polynomial time as well; (3) we provide a pseudo-polynomial time algorithm to compute the normalising constant.}
}
@inproceedings{AGKS-concur17,
address = {Berlin, Germany},
month = sep,
year = 2017,
volume = {85},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Meyer, Roland and Nestmann, Uwe},
acronym = {{CONCUR}'17},
booktitle = {{P}roceedings of the 28th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'17)},
author = {Akshay, S. and Gastin, Paul and Krishna, Shankara Narayanan and Sarkar, Ilias},
title = {Towards an Efficient Tree Automata based technique for Timed Systems},
pages = {39:1--39:15},
url = {http://drops.dagstuhl.de/opus/volltexte/2017/7801},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7801/pdf/LIPIcs-CONCUR-2017-39.pdf},
doi = {10.4230/LIPIcs.CONCUR.2017.39},
abstract = {The focus of this paper is the analysis of real-time systems with recursion, through the development of good theoretical techniques which are implementable. Time is modeled using clock variables, and recursion using stacks. Our technique consists of modeling the behaviours of the timed system as graphs, and interpreting these graphs on tree terms by showing a bound on their tree-width. We then build a tree automaton that accepts exactly those tree terms that describe realizable runs of the timed system. The emptiness of the timed system thus boils down to emptiness of a finite tree automaton that accepts these tree terms. This approach helps us in obtaining an optimal complexity, not just in theory (as done in earlier work e.g.[concur16]), but also in going towards an efficient implementation of our technique. To do this, we make several improvements in the theory and exploit these to build a first prototype tool that can analyze timed systems with recursion.}
}
@inproceedings{BQS-concur17,
address = {Berlin, Germany},
month = sep,
year = 2017,
volume = {85},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Meyer, Roland and Nestmann, Uwe},
acronym = {{CONCUR}'17},
booktitle = {{P}roceedings of the 28th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'17)},
author = {Bollig, Benedikt and Quaas, Karin and Sangnier, Arnaud},
title = {The Complexity of Flat Freeze LTL},
pages = {33:1--33:16},
url = {http://drops.dagstuhl.de/opus/volltexte/2017/7799},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7799/pdf/LIPIcs-CONCUR-2017-33.pdf},
doi = {10.4230/LIPIcs.CONCUR.2017.33},
abstract = {We consider the model-checking problem for freeze LTL on one-counter automata (OCAs). Freeze LTL extends LTL with the freeze quantifier, which allows one to store different counter values of a run in registers so that they can be compared with one another. As the model-checking problem is undecidable in general, we focus on the flat fragment of freeze LTL, in which the usage of the freeze quantifier is restricted. Recently, Lechner et al. showed that model checking for flat freeze LTL on OCAs with binary encoding of counter updates is decidable and in 2NEXPTIME. In this paper, we prove that the problem is, in fact, NEXPTIME-complete no matter whether counter updates are encoded in unary or binary. Like Lechner et al., we rely on a reduction to the reachability problem in OCAs with parameterized tests (OCAPs). The new aspect is that we simulate OCAPs by alternating two-way automata over words. This implies an exponential upper bound on the parameter values that we exploit towards an NP algorithm for reachability in OCAPs with unary updates. We obtain our main result as a corollary.}
}
@inproceedings{BJM-formats17,
address = {Berlin, Germany},
month = sep,
year = 2017,
volume = {10419},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abate, Alessandro and Geeraerts, Gilles},
acronym = {{FORMATS}'17},
booktitle = {{P}roceedings of the 15th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'17)},
author = {Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas},
title = {On the Determinization of Timed Systems},
pages = {25-41},
url = {https://hal.archives-ouvertes.fr/hal-01566436/},
doi = {10.1007/978-3-319-65765-3_2},
abstract = {We introduce a new formalism called automata over a timed domain which provides an adequate framework for the determinization of timed systems. In this formalism, determinization w.r.t. timed language is always possible at the cost of changing the timed domain. We give a condition for determinizability of automata over a timed domain without changing the timed domain, which allows us to recover several known determinizable classes of timed systems, such as strongly-non-zeno timed automata, integer-reset timed automata, perturbed timed automata, etc. Moreover in the case of timed automata this condition encompasses most determinizability conditions from the literature.}
}
@inproceedings{GMS-mfcs17,
address = {Aalborg, Denmark},
month = aug,
year = 2017,
volume = {83},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Fran{\c{c}}ois},
acronym = {{MFCS}'17},
booktitle = {{P}roceedings of the 42nd
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'17)},
author = {Grosshans, Nathan and McKenzie, Pierre and Segoufin, Luc},
title = {The power of programs over monoids in {DA}},
pages = {2:1--2:20},
url = {http://drops.dagstuhl.de/opus/volltexte/2017/8090/},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/8090/pdf/LIPIcs-MFCS-2017-2.pdf},
doi = {10.4230/LIPIcs.MFCS.2017.2},
abstract = {The program-over-monoid model of computation originates with Barrington's proof that it captures the complexity class NC^1. Here we make progress in understanding the subtleties of the model. First, we identify a new tameness condition on a class of monoids that entails a natural characterization of the regular languages recognizable by programs over monoids from the class. Second, we prove that the class known as DA satisfies tameness and hence that the regular languages recognized by programs over monoids in DA are precisely those recognizable in the classical sense by morphisms from QDA. Third, we show by contrast that the well studied class of monoids called J is not tame and we exhibit a regular language, recognized by a program over a monoid from J, yet not recognizable classically by morphisms from the class QJ. Finally, we exhibit a program-length-based hierarchy within the class of languages recognized by programs over monoids from DA.}
}
@article{BDH-lmcs17,
journal = {Logical Methods in Computer Science},
author = {Baelde, David and Delaune, St{\'e}phanie and Hirschi, Lucca},
title = {{A Reduced Semantics for Deciding Trace Equivalence}},
volume = {13},
number = {2:8},
year = {2017},
pages = {1-48},
doi = {10.23638/LMCS-13(2:8)2017},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDH-lmcs17.pdf},
url = {https://lmcs.episciences.org/3703},
abstract = {Many privacy-type properties of security protocols can be modelled using trace equivalence properties in suitable process algebras. It has been shown that such properties can be decided for interesting classes of finite processes (i.e. without replication) by means of symbolic execution and constraint solving. However, this does not suffice to obtain practical tools. Current prototypes suffer from a classical combinatorial explosion problem caused by the exploration of many interleavings in the behaviour of processes. M{\"o}dersheim et al. [40] have tackled this problem for reachability properties using partial order reduction techniques. We revisit their work, generalize it and adapt it for equivalence checking. We obtain an optimisation in the form of a reduced symbolic semantics that eliminates redundant interleavings on the fly. The obtained partial order reduction technique has been integrated in a tool called Apte. We conducted complete benchmarks showing dramatic improvements.}
}
@article{BFHH-tocl17,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Blondin, Michael and Finkel, Alain and Haase, Christoph and
Haddad, Serge},
title = {The Logical View on Continuous {P}etri Nets},
volume = {18},
number = {3},
year = {2017},
pages = {24:1--24:28},
url = {http://doi.acm.org/10.1145/3105908},
doi = {10.1145/3105908},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHH-tocl17.pdf},
abstract = {Continuous Petri nets are a relaxation of classical discrete Petri nets in which transitions can be fired a fractional number of times, and consequently places may contain a fractional number of tokens. Such continuous Petri nets are an appealing object to study since they over approximate the set of reachable configurations of their discrete counterparts, and their reachability problem is known to be decidable in polynomial time. The starting point of this paper is to show that the reachability relation for continuous Petri nets is definable by a sentence of linear size in the existential theory of the rationals with addition and order. Using this characterization, we obtain decidability and complexity results for a number of classical decision problems for continuous Petri nets. In particular, we settle the open problem about the precise complexity of reachability set inclusion. Finally, we show how continuous Petri nets can be incorporated inside the classical backward coverability algorithm for discrete Petri nets as a pruning heuristic in order to tackle the symbolic state explosion problem. The cornerstone of the approach we present is that our logical characterization enables us to leverage the power of modern SMT-solvers in order to yield a highly performant and robust decision procedure for coverability in Petri nets. We demonstrate the applicability of our approach on a set of standard benchmarks from the literature.}
}
@phdthesis{hirschi-phd2017,
author = {Hirschi, Lucca},
title = {{Automated Verification of Privacy in Security Protocols: Back and Forth Between Theory \& Practice}},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2017,
month = apr,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/hirschi-phd17.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/hirschi-phd17.pdf}
}
@inproceedings{SV-icdt17,
address = {Venice, Italy},
month = mar,
year = 2017,
volume = 68,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Benedikt, Michael and Orsi, Georgio},
acronym = {{ICDT}'17},
booktitle = {{P}roceedings of the 18th {I}nternational {C}onference on
{D}atabase {T}heory ({ICDT}'17)},
author = {Segoufin, Luc and Vigny, Alexandre},
title = {Constant Delay Enumeration for FO Queries over Databases with Local Bounded Expansion},
pages = {20:1-20:16},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7060},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7060/pdf/LIPIcs-ICDT-2017-20.pdf},
doi = {10.4230/LIPIcs.ICDT.2017.20},
abstract = {We consider the evaluation of first-order queries over classes of databases with local bounded expansion. This class was introduced by Nesetril and Ossona de Mendez and generalizes many well known classes of databases, such as bounded degree, bounded tree width or bounded expansion. It is known that over classes of databases with local bounded expansion, first-order sentences can be evaluated in pseudo-linear time (pseudo-linear time means that for all \(\epsilon\) there exists an algorithm working in time \(O(n^{1+\epsilon})\)). Here, we investigate other scenarios, where queries are not sentences. We show that first-order queries can be enumerated with constant delay after a pseudo-linear preprocessing over any class of databases having locally bounded expansion. We also show that, in this context, counting the number of solutions can be done in pseudo-linear time.}
}
@phdthesis{stan-phd2017,
author = {Stan, Daniel},
title = {Randomized Strategies in Concurrent Games},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2017,
month = mar,
url = {https://hal.archives-ouvertes.fr/tel-01519354},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/stan-phd17.pdf}
}
@inproceedings{CK-csf17,
address = {Santa Barbara, California, USA},
month = aug,
publisher = {{IEEE} Computer Society Press},
editor = {K{\"o}pf, Boris and Chong, Steve},
acronym = {{CSF}'17},
booktitle = {{P}roceedings of the
30th {IEEE} {C}omputer {S}ecurity {F}oundations
{S}ymposium ({CSF}'17)},
author = {Comon, Hubert and Koutsos, Adrien},
title = {Formal Computational Unlinkability Proofs of RFID Protocols},
pages = {100-114},
year = {2017},
doi = {10.1109/CSF.2017.9},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CK-csf17.pdf},
url = {http://ieeexplore.ieee.org/document/8049714/},
abstract = {We set up a framework for the formal proofs of
RFID protocols in the computational model. We rely on the
so-called computationally complete symbolic attacker model. Our
contributions are:
1) To design (and prove sound) axioms reflecting the proper-
ties of hash functions (Collision-Resistance, PRF).
2) To formalize computational unlinkability in the model.
3) To illustrate the method, providing the first formal proofs
of unlinkability of RFID protocols, in the computational
model.}
}
@inproceedings{CGKM-csf17,
address = {Santa Barbara, California, USA},
month = aug,
publisher = {{IEEE} Computer Society Press},
editor = {K{\"o}pf, Boris and Chong, Steve},
acronym = {{CSF}'17},
booktitle = {{P}roceedings of the
30th {IEEE} {C}omputer {S}ecurity {F}oundations
{S}ymposium ({CSF}'17)},
author = {Calzavara, Stefano and Grishchenko, Ilya and Koutsos, Adrien and Maffei, Matteo},
title = {A Sound Flow-Sensitive Heap Abstraction for the Static Analysis of Android Applications},
pages = {22-36},
year = {2017},
doi = {10.1109/CSF.2017.19},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CGKM-csf17.pdf},
url = {http://ieeexplore.ieee.org/document/8049649/},
abstract = {The present paper proposes the first static analysis
for Android applications which is both flow-sensitive on the heap
abstraction and provably sound with respect to a rich formal
model of the Android platform. We formulate the analysis as a
set of Horn clauses defining a sound over-approximation of the
semantics of the Android application to analyse, borrowing ideas
from recency abstraction and extending them to our concurrent
setting. Moreover, we implement the analysis in HornDroid, a
state-of-the-art information flow analyser for Android applica-
tions. Our extension allows HornDroid to perform strong updates
on heap-allocated data structures, thus significantly increasing its
precision, without sacrificing its soundness guarantees. We test
our implementation on DroidBench, a popular benchmark of
Android applications developed by the research community, and
we show that our changes to HornDroid lead to an improvement
in the precision of the tool, while having only a moderate cost in
terms of efficiency. Finally, we assess the scalability of our tool
to the analysis of real applications.}
}
@article{KV-jcss17,
publisher = {Elsevier Science Publishers},
journal = {Journal of Computer and System Sciences},
author = {Koutsos, Adrien and Vianu, Victor},
title = {{Process-centric views of data-driven business artifacts}},
volume = {86},
number = {1},
year = {2017},
pages = {82-107},
doi = {10.1016/j.jcss.2016.11.012},
month = jun,
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KV-jcss17.pdf},
url = {http://dx.doi.org/10.1016/j.jcss.2016.11.012},
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 stakeholders 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 process-centric views, specified by finite-state transition systems, 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. As a side effect, we obtain several new results on verification of business artifacts, including a decidability result for branching-time properties.}
}
@inproceedings{FL-icalp17,
address = {Warsaw, Poland},
month = jul,
volume = {80},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chatzigiannakis, Ioannis and Indyk, Piotr and Muscholl, Anca and Kuhn, Fabian},
acronym = {{ICALP}'17},
booktitle = {{P}roceedings of the 44th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'17)},
author = {Finkel, Alain and Lozes, {\'E}tienne},
title = {Synchronizability of Communicating Finite State Machines is not Decidable},
pages = {122:1-122:14},
year = {2017},
doi = {10.4230/LIPIcs.ICALP.2017.122},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7402/pdf/LIPIcs-ICALP-2017-122.pdf},
url = {http://drops.dagstuhl.de/opus/volltexte/2017/7402},
abstract = {A system of communicating finite state machines is synchronizable if its send trace semantics, i.e. the set of sequences of sendings it can perform, is the same when its communications are FIFO asynchronous and when they are just rendez-vous synchronizations. This property was claimed to be decidable in several conference and journal papers for either mailboxes or peer-to-peer communications, thanks to a form of small model property. In this paper, we show that this small model property does not hold neither for mailbox communications, nor for peer-to-peer communications, therefore the decidability of synchronizability becomes an open question. We close this question for peer-to-peer communications, and we show that synchronizability is actually undecidable. We show that synchronizability is decidable if the topology of communications is an oriented ring. We also show that, in this case, synchronizability implies the absence of unspecified receptions and orphan messages, and the channel-recognizability of the reachability set.}
}
@inproceedings{Dowek-icalp17,
address = {Warsaw, Poland},
month = jul,
volume = {80},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chatzigiannakis, Ioannis and Indyk, Piotr and Muscholl, Anca and Kuhn, Fabian},
acronym = {{ICALP}'17},
booktitle = {{P}roceedings of the 44th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'17)},
author = {Dowek, Gilles},
title = {Models and termination of proof reduction in the \(\lambda\Pi\)-calculus modulo theory},
pages = {109:1-109:14},
year = {2017},
doi = {10.4230/LIPIcs.ICALP.2017.109},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7391/pdf/LIPIcs-ICALP-2017-109.pdf},
url = {http://drops.dagstuhl.de/opus/volltexte/2017/7391},
abstract = {We define a notion of model for the \(\lambda\Pi\)-calculus modulo theory and prove a soundness theorem. We then use this notion to define a notion of super-consistent theory and prove that proof reduction terminates in the \(\lambda\Pi\)-calculus modulo any super-consistent theory. We prove this way the termination of proof reduction in several theories including Simple type theory and the Calculus of constructions.}
}
@inproceedings{FMW-cav17,
address = {Heidelberg, Germany},
month = jul,
volume = {10427},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Kuncak, Viktor and Majumdar, Rupak},
acronym = {{CAV}'17},
booktitle = {{P}roceedings of the 29th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'17)},
author = {Fortin, Marie and Muscholl, Anca and Walukiewicz, Igor},
title = {Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems},
pages = {155-175},
year = {2017},
doi = {10.1007/978-3-319-63390-9_9},
url = {https://arxiv.org/abs/1606.08707},
abstract = {}
}
@inproceedings{HSZ-lics17,
address = {Reykjavik, Iceland},
month = jun,
publisher = {{IEEE} Press},
editor = {Ouaknine, Jo{\"e}l},
acronym = {{LICS}'17},
booktitle = {{P}roceedings of the 32nd {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'17)},
author = {Halfon, Simon and Schnoebelen, {\relax Ph}ilippe and Zetzsche, Georg},
title = {Decidability, complexity, and expressiveness of first-order logic over the subword ordering},
pages = {1-12},
year = {2017},
doi = {10.1109/LICS.2017.8005141},
url = {https://arxiv.org/abs/1701.07470},
abstract = {We consider first-order logic over the subword ordering on finite words, where each word is available as a constant. Our first result is that the \(\Sigma_1\) theory is undecidable (already over two letters).\par
We investigate the decidability border by considering fragments where all but a certain number of variables are alternation bounded, meaning that the variable must always be quantified over languages with a bounded number of letter alternations. We prove that when at most two variables are not alternation bounded, the \(\Sigma_1\) fragment is decidable, and that it becomes undecidable when three variables are not alternation bounded. Regarding higher quantifier alternation depths, we prove that the \(\Sigma_2\) fragment is undecidable already for one variable without alternation bound and that when all variables are alternation bounded, the entire first-order theory is decidable.}
}
@inproceedings{CJLS-lics17,
address = {Reykjavik, Iceland},
month = jun,
publisher = {{IEEE} Press},
editor = {Ouaknine, Jo{\"e}l},
acronym = {{LICS}'17},
booktitle = {{P}roceedings of the 32nd {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'17)},
author = {Colcombet, {\relax Th}omas and Jurdzi{\'n}ski,
Marcin and Lazi{\'c}, Ranko and Schmitz, Sylvain},
title = {Perfect Half Space Games},
pages = {1--11},
year = {2017},
doi = {10.1109/LICS.2017.8005105},
url = {http://arxiv.org/abs/1704.05626},
abstract = {We introduce perfect half space games,
in which the goal of Player 2
is to make the sums of encountered multi-dimensional weights diverge in
a direction which is consistent with a chosen sequence of perfect half spaces (chosen dynamically by Player 2).
We establish that the bounding games of
Jurdzinski et al. (ICALP 2015) can be reduced to perfect half space games, which in turn can be translated to the lexicographic
energy games of Colcombet and Niwinski, and are positionally determined in a strong sense (Player 2 can play without knowing the current perfect half space).
We finally show how perfect half space games and bounding games can be employed
to solve multi-dimensional energy parity games in pseudo-polynomial time
when both the numbers of energy dimensions and of priorities are fixed, regardless of whether the initial credit is given as part of the input or existentially quantified. This also yields an optimal 2EXP complexity
with given initial credit, where the best known upper bound was non-elementary.}
}
@inproceedings{HPV-icsc17,
address = {San Diego, CA, USA},
month = jan,
volume = 11,
series = {IEEE ICSC},
publisher = {{IEEE} Press},
todoeditor = {D?Auria, Daniela and Liu, Jianquan and Pilato, Giovanni},
acronym = {{ICSC}'17},
booktitle = {{P}roceedings of the 11th International Conference on Semantic Computing ({ICSC}'17)},
author = {Haar, Stefan and Perchy, Salim and Valencia, Frank},
title = {{D-SPACES: Implementing Declarative Semantics for Spatially Structured Information}},
pages = {227-233},
year = {2017},
doi = {10.1109/ICSC.2017.34},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HPV-icsc17.pdf},
url = {https://hal.inria.fr/hal-01328189},
abstract = {We introduce in this paper D-SPACES, an implementation of constraint systems with space and extrusion operators. Constraint systems are algebraic models that allow for a semantic language-like representation of information in systems where the concept of space is a primary structural feature. We give this information mainly an epistemic interpretation and consider various agents as entities acting upon it. D-SPACES is coded as a c++11 library providing implementations for constraint systems, space functions and extrusion functions. The interfaces to access each implementation are minimal and thoroughly documented. D-SPACES also provides property-checking methods as well as an implementation of a specific type of constraint systems (a boolean algebra). This last implementation serves as an entry point for quick access and proof of concept when using these models. Furthermore, we offer an illustrative example in the form of a small social network where users post their beliefs and utter their opinions.}
}
@article{GHPRV-jlamp17,
publisher = {Elsevier Science Publishers},
journal = {Journal of Logic and Algebraic Methods in Programming},
author = {Guzm{\'a}n, Michell and Haar, Stefan and Perchy, Salim and Rueda, Camilo and Valencia, Frank},
title = {{Belief, Knowledge, Lies and Other Utterances in an Algebra for Space and Extrusion}},
volume = {86},
number = {1},
year = {2017},
pages = {107-133},
doi = {10.1016/j.jlamp.2016.09.001},
month = jan,
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GHPRV-jlamp17.pdf},
url = {https://hal.inria.fr/hal-01257113},
abstract = {The notion of constraint system (cs) is central to declarative formalisms from concurrency theory such as process calculi for concurrent constraint programming (ccp). Constraint systems are often represented as lattices: their elements, called constraints, represent partial information and their order corresponds to entailment. Recently a notion of n-agent spatial cs was introduced to represent information in concurrent constraint programs for spatially distributed multi-agent systems. From a computational point of view a spatial constraint system can be used to specify partial information holding in a given agent's space (local information). From an epistemic point of view a spatial cs can be used to specify information that a given agent considers true (beliefs). Spatial constraint systems, however, do not provide a mechanism for specifying the mobility of information/processes from one space to another. Information mobility is a fundamental aspect of concurrent systems. In this article we develop the theory of spatial constraint systems with operators to specify information and processes moving from a space to another. 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/information extrusion, a central concept in formalisms for mobile communication. From an epistemic point of view extrusion corresponds I to a notion we shall call utterance; a piece of information that an agent communicate to others but that may be inconsistent with the agent's beliefs. Utterances can then be used to express instances of epistemic notions such as hoaxes or intentional lies which are common place in social media. Spatial constraint system can express the epistemic notion of belief by means of space functions that specify local information. We shall also show that spatial constraint can also express the epistemic notion of knowledge by means of a derived spatial operator that specifies global information.}
}
@inproceedings{OBH-most17,
address = {San Jose, CA, USA},
month = may,
editor = {Chen, Hao and Koved, Larry},
booktitle = {{P}roceedings of Mobile Security Technologies (MoST'17), held as part of the {IEEE} Computer Society Security and Privacy Workshops},
author = {{O'Hanlon}, Piers and Borgaonkar, Ravishankar and Hirschi, Lucca},
title = {Mobile subscriber WiFi privacy},
todopages = {252-261},
year = {2017},
tododoi = {},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/OBH-most17.pdf},
abstract = {This paper investigates and analyses the insufficient protections afforded to mobile identities when using today?s operator backed WiFi services. Specifically we detail a range of attacks, on a set of widely deployed authentication protocols, that enable a malicious user to obtain and track a user?s International Mobile Subscriber Identity (IMSI) over WiFi. These attacks are possible due to a lack of sufficient privacy protection measures, which are exacerbated by preconfigured device profiles. We provide a formal analysis of the protocols involved, examine their associated configuration profiles, and document our experiences with reporting the issues to the relevant stakeholders. We detail a range of potential countermeasures to tackle these issues to ensure that privacy is better protected in the future.}
}
@inproceedings{VCCT-caise17,
address = {Essen, Germany},
month = jun,
volume = 10253,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Dubois, Eric and Pohl, Klaus},
acronym = {{CAiSE}'17},
booktitle = {{P}roceedings of the 29th {I}nternational {C}onference on {A}dvanced {I}nformation {S}ystems {E}ngineering ({CAiSE}'17)},
author = {{van Dongen}, Boudewijn and Carmona, Josep and Chatain, {\relax Th}omas and Taymouri, Farbod},
title = {Aligning Modeled and Observed Behavior: A Compromise Between Complexity and Quality},
pages = {94-109},
year = {2017},
doi = {10.1007/978-3-319-59536-8_7},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/VCCT-caise17.pdf},
abstract = {Certifying that a process model is aligned with the real process executions is perhaps the most desired feature a process model may have: aligned process models are crucial for organizations, since strategic decisions can be made easier on models instead of on plain data. In spite of its importance, the current algorithmic support for computing alignments is limited: either techniques that explicitly explore the model behavior (which may be worst-case exponential with respect to the model size), or heuristic approaches that cannot guarantee a solution, are the only alternatives. In this paper we propose a solution that sits right in the middle in the complexity spectrum of alignment techniques; it can always guarantee a solution, whose quality depends on the exploration depth used and local decisions taken at each step. We use linear algebraic techniques in combination with an iterative search which focuses on progressing towards a solution. The experiments show a clear reduction in the time required for reaching a solution, without sacrificing significantly the quality of the alignment obtained.}
}
@inproceedings{BBDH-sia17,
address = {Montigny-le-Bretonneux, France},
month = mar,
editor = {{Di Valentin}, Laurent and Landel, Eric},
acronym = {SIA Simulation Num{\'e}rique},
booktitle = {SIA Simulation Num{\'e}rique},
author = {Barbot, Beno{\^i}t and B{\'e}rard, B{\'e}atrice and Duplouy, Yann and Haddad, Serge},
title = {Statistical Model-Checking for Autonomous Vehicle Safety Validation},
todopages = {},
year = {2017},
todolsvdate-pub = 20170320,
tododoi = {},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBDH-sia17.pdf},
url = {https://hal.archives-ouvertes.fr/hal-01491064},
abstract = {We present an application of statistical
model-checking to the verification of an autonomous
vehicle controller. Our goal is to check safety properties
in various traffic situations. More specifically, we
focus on a traffic jam situation.\par
The controller is specified by a C++ program. Using
sensors, it registers positions and velocities of nearby
vehicles and modifies the position and velocity of the
controlled vehicle to avoid collisions. We model the environment
using a stochastic high level Petri net, where
random behaviors of other vehicles can be described.
We use HASL, a quantitative variant of linear temporal
logic, to express the desired properties. A large family
of performance indicators can be specified in HASL
and we target in particular the expectation of travelled
distance or the collision probability.\par
We evaluate the properties of this model using COSMOS1.
This simulation tool implements numerous statistical
techniques such as sequential hypothesis testing
and most confidence range computation methods.
Its efficiency allowed us to conduct several experiments
with success.}
}
@inproceedings{BHSS-pn17,
address = {Zaragoza, Spain},
month = jun,
volume = {10258},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {van der Aalst, Wifred and Best, Eike},
acronym = {{PETRI~NETS}'17},
booktitle = {{P}roceedings of the 38th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'17)},
author = {B{\'e}rard, B{\'e}atrice and Haar, Stefan and
Schmitz, Sylvain and Schwoon, Stefan},
title = {The Complexity of Diagnosability and Opacity
Verification for {P}etri Nets},
pages = {200-220},
year = {2017},
doi = {10.1007/978-3-319-57861-3_13},
url = {https://hal.inria.fr/hal-01484476},
abstract = {Diagnosability and opacity are two well-studied problems in discrete-event systems. We revisit these two problems with respect to expressiveness and complexity issues. We first relate different notions of diagnosability and opacity. We consider in particular fairness issues and extend the definition of Germanos et al. [ACM TECS, 2015] of weakly fair diagnosability for safe Petri nets to general Petri nets and to opacity questions. Second, we provide a global picture of complexity results for the verification of diagnosability and opacity. We show that diagnosability is NL-complete for finite state systems, PSPACE-complete for safe Petri nets (even with fairness), and EXPSPACE-complete for general Petri nets without fairness, while non diagnosability is inter-reducible with reachability when fault events are not weakly fair. Opacity is ESPACE-complete for safe Petri nets (even with fairness) and undecidable for general Petri nets already without fairness.}
}
@article{ABH-ijfcs17,
publisher = {World Scientific},
journal = {International Journal of Foundations of Computer Science},
author = {Atig, Mohamed Faouzi and Bollig, Benedikt and Habermehl, Peter},
title = {Emptiness of ordered multi-pushdown automata is {2ETIME}-complete},
volume = {28},
number = {8},
year = {2017},
pages = {945-975},
doi = {10.1142/S0129054117500332},
url = {http://www.worldscientific.com/doi/abs/10.1142/S0129054117500332},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABH-ijfcs17.pdf},
abstract = {We consider ordered multi-pushdown automata, a multi-stack extension
of pushdown automata that comes with a constraint on stack operations: a pop
can only be performed on the first non-empty stack (which implies that we
assume a linear ordering on the collection of stacks). We show that the
emptiness problem for multi-pushdown automata is 2ETIME-complete.
Containment in 2ETIME is shown by translating an automaton
into a grammar for which we can check if the generated language is empty.
The lower bound is established by simulating the behavior of an alternating
Turing machine working in exponential space. We also compare ordered
multi-pushdown automata with the model of bounded-phase (visibly)
multi-stack pushdown automata, which do not impose an ordering on stacks,
but restrict the number of alternations of pop operations on different
stacks.}
}
@article{DKP-jar2017,
publisher = {Springer},
journal = {Journal of Automated Reasoning},
author = {Demri, St{\'e}phane and Kapur, Deepak and Weidenbach, Christoph},
editor = {Demri, St{\'e}phane and Kapur, Deepak and Weidenbach, Christoph},
title = {Special Issue of Selected Extended Papers of IJCAR 2014},
url = {http://link.springer.com/journal/10817/58/1/page/1},
volume = {58},
number = {1},
year = {2017}
}
@article{ACR-tecs17,
publisher = {ACM Press},
journal = {ACM Transactions in Embedded Computing Systems},
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},
volume = {16},
number = {2},
year = {2017},
pages = {43:1-43:26},
doi = {10.1145/3012283},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACR-tecs17.pdf},
abstract = {Parameter synthesis for timed systems aims at deriving parameter valuations satisfying a given property. In this article, we target concurrent systems. We use partial-order semantics for parametric time Petri nets as a way to both cope with the well-known state-space explosion due to concurrency and significantly enhance the result of an existing synthesis algorithm. Given a reference parameter valuation, our approach synthesizes other valuations preserving the partial-order executions of the reference parameter valuation. We show the applicability of our approach using a tool applied to asynchronous circuits.}
}
@incollection{BLMOW-kimfest17,
author = {Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois and
Markey, Nicolas and Ouaknine, Jo{\"e}l and Worrell,
James},
title = {Timed temporal logics},
editor = {Aceto, Luca and Bacci, Giorgio and Bacci, Giovani
and Ing{\'o}lfsd{\'o}ttir, Anna and Legay, Axel and
Mardare, Radu},
booktitle = {Models, Algorithms, Logics and Tools: Essays
Dedicated to Kim Guldstrand Larsen on the Occasion
of His 60th Birthday},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {10460},
year = {2017},
pages = {211-230},
month = aug,
doi = {10.1007/978-3-319-65764-6_11},
abstract = {Since the early 1990's, classical temporal logics
have been extended with timing constraints. While
temporal logics only express contraints on the order
of events, their timed extensions can add
quantitative constraints on delays between those
events. We survey expressiveness and algorithmic
results on those logics, and discuss semantic
choices that may look unimportant but do have an
impact on the questions we consider.},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLMOW-kimfest17.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLMOW-kimfest17.pdf}
}
@inproceedings{CHKP-valuetools17,
address = {Venice, Italy},
month = dec,
year = 2017,
acronym = {{VALUETOOLS}'17},
booktitle = {{P}roceedings of the 11th {I}nternational {C}onference
on {P}erformance {E}valuation {M}ethodologies and {T}ools
({VALUETOOLS}'17)},
author = {Chatzikokolakis, Kostas and Haddad, Serge and Kassem, Ali and Palamidessi, Catuscia},
title = {{Trading Optimality for Performance in Location Privacy}},
pages = {221-222},
url = {https://arxiv.org/abs/1710.05524},
pdf = {https://arxiv.org/pdf/1710.05524.pdf},
doi = {10.1145/3150928.3150962},
abstract = {Location-Based Services (LBSs) provide invaluable aid in the everyday activities of many individuals, however they also pose serious threats to the user' privacy. There is, therefore, a growing interest in the development of mechanisms to protect location privacy during the use of LBSs. Nowadays, the most popular methods are probabilistic, and the so-called optimal method achieves an optimal trade-off between privacy and utility by using linear optimization techniques. Unfortunately, due to the complexity of linear programming, the method is unfeasible for a large number n of locations, because the constraints are \(O(n^3)\). In this paper, we propose a technique to reduce the number of constraints to \(O(n^2)\), at the price of renouncing to perfect optimality. We show however that on practical situations the utility loss is quite acceptable, while the gain in performance is significant.}
}
@mastersthesis{m2-LeenaSubramaniam,
author = {Chaitanya Leena Subramaniam},
title = {{Cubical Type Theory in Dedukti}},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2017},
month = sep
}
@techreport{Thire-hal17,
author = {Thir{\'e}, Fran{\c{c}}ois},
institution = {HAL Research Report},
number = {hal-01668250},
type = {Research Report},
title = {{Exporting an Arithmetic Library from Dedukti to HOL}},
year = {2017},
month = dec,
url = {https://hal.inria.fr/hal-01668250},
pdf = {https://hal.inria.fr/hal-01668250/file/sttforall-fscd.pdf},
abstract = {Today, we observe a large diversity of proof systems. This diversity has the negative consequence that a lot of theorems are proved many times. Unlike programming languages, it is difficult for these systems to cooperate because they do not implement the same logic. Logical frameworks are a class of theorems provers that overcome this issue by their capacity of implementing various logics. In this work, we study the STT\(\forall_{\beta\delta}\) logic, an extension of the Simple Type Theory that has been encoded in the logical framework Dedukti. We show that this new logic is a good candidate to export proofs to other provers. As an example, we show how this logic has been encoded into Dedukti and how we used it to export proofs to the HOL family provers via OpenTheory.}
}
@mastersthesis{m2-genestier,
author = {Genestier, Guillaume},
title = {Termination checking in the \(\lambda\Pi\)-calculus modulo theory},
school = {Universit{\'e} Paris~7, Paris, France},
type = {Rapport de {M}aster},
year = {2017},
month = sep,
url = {https://hal.inria.fr/hal-01676409},
pdf = {https://hal.inria.fr/hal-01676409/file/Genestier_RapportLMFI.pdf}
}
@mastersthesis{m2-defourne,
author = {Defourn{\'e}, Antoine},
title = {{Proof Tactics in Dedukti}},
school = {Inria Saclay},
type = {Rapport de {M}aster},
year = {2017},
month = sep,
url = {https://hal.inria.fr/hal-01661872},
pdf = {https://hal.inria.fr/hal-01661872/file/rapport_pfe_ensimag.pdf}
}
@article{AM-prd17,
publisher = {American Physical Society},
journal = {Physical Review D},
author = {Arrighi, Pablo and Martiel, Simon},
title = {Quantum causal graph dynamics},
volume = {96},
number = {2},
year = {2017},
pdf = {https://arxiv.org/pdf/1607.06700.pdf},
abstract = {Consider a graph having quantum systems lying at each node. Suppose that the whole thing evolves in discrete time steps, according to a global, unitary causal operator. By causal we mean that information can only propagate at a bounded speed, with respect to the distance given by the graph. Suppose, moreover, that the graph itself is subject to the evolution, and may be driven to be in a quantum superposition of graphs—in accordance to the superposition principle. We show that these unitary causal operators must decompose as a finite-depth circuit of local unitary gates. This unifies a result on Quantum Cellular Automata with another on Reversible Causal Graph Dynamics. Along the way we formalize a notion of causality which is valid in the context of quantum superpositions of time-varying graphs, and has a number of good properties.
}
}
@book{AD18,
title = {{Le temps des algorithmes}},
author = {Abiteboul, Serge and Dowek, Gilles},
url = {https://hal.inria.fr/hal-01502505},
publisher = {{Editions Le Pommier}},
pages = {192},
year = {2017},
isbn = {978-2-7465-1175-0}
}
@article{CFN-dam17,
publisher = {Elsevier Science Publishers},
journal = {Discrete Applied Mathematics},
author = {Bernadette {Charron-Bost} and Matthias F{\"u}gger and {\relax Th}omas Nowak and Manfred Schwarz},
title = {New transience bounds for max-plus linear systems},
volume = {219},
pages = {83-99},
year = {2017},
month = mar,
doi = {10.1016/j.dam.2016.11.003},
pdf = {http://www.lsv.fr/~mfuegger/papers/CFN17_dam.pdf},
url = {https://doi.org/10.1016/j.dam.2016.11.003},
abstract = {Linear max-plus systems describe the behavior of a large variety of complex systems. It is known that these systems show a periodic behavior after an initial transient phase. Assessment of the length of this transient phase provides important information on complexity measures of such systems, and so is crucial in system design. We identify relevant parameters in a graph representation of these systems and propose a modular strategy to derive new upper bounds on the length of the transient phase. By that we are the first to give asymptotically tight and potentially subquadratic transience bounds. We use our bounds to derive new complexity results, in particular in distributed computing.}
}
@article{BM-icomp17,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Berwanger, Dietmar and Mathew, Anup Basil},
title = {Infinite games with finite knowledge gaps},
volume = {254},
pages = {217-237},
year = {2017},
month = jun,
url = {https://doi.org/10.1016/j.ic.2016.10.009},
doi = {10.1016/j.ic.2016.10.009},
abstract = {Infinite games where several players seek to coordinate under imperfect information are deemed to be undecidable, unless the information is hierarchically ordered among the players. We identify a class of games for which joint winning strategies can be constructed effectively without restricting the direction of information flow. Instead, our condition requires that the players attain common knowledge about the actual state of the game over and over again along every play. We show that it is decidable whether a given game satisfies the condition, and prove tight complexity bounds for the strategy synthesis problem under ω-regular winning conditions given by deterministic parity automata.},
pdf = {http://lsv.fr/~dwb/rec.pdf}
}
@article{BMVdB-acta17,
publisher = {Springer},
journal = {Acta Informatica},
author = {Berwanger, Dietmar and Mathew, Anup Basil and {van den Bogaard}, Marie},
title = {Hierarchical information and the synthesis of distributed strategies},
year = {2017},
month = jun,
url = {https://doi.org/10.1007/s00236-017-0306-5},
doi = {10.1007/s00236-017-0306-5},
abstract = {Infinite games with imperfect information are known 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. 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. Finally, we interpret our result in terms of distributed system architectures.},
pdf = {http://lsv.fr/~dwb/hi.pdf}
}
@inproceedings{BR-sr17,
address = {Liverpool, UK},
month = jul,
editor = {{van der Hoek}, Wiebe and Maubert, Bastien and Murano, Aniello and Rubin, Sasha},
acronym = {{SR}'17},
booktitle = {{P}roceedings of the 5th International Workshop on Strategic Reasoning ({SR}'17)},
author = {Dietmar Berwanger and R. Ramanujam},
title = {{Deviator Detection under Imperfect Monitoring}},
year = {2017},
url = {https://arxiv.org/abs/1712.09686},
pdf = {https://arxiv.org/pdf/1712.09686.pdf},
abstract = {Grim-trigger strategies are a fundamental mechanism for sustaining equilibria in iterated games: the players cooperate along an agreed path, and as soon as one player deviates, the others form a coalition to play him down to his minmax level. A precondition to triggering such a strategy is that the identity of the deviating player becomes common knowledge among the other players. This can be difficult or impossible to attain in games where the information structure allows only imperfect monitoring of the played actions or of the global state.
We study the problem of synthesising finite-state strategies for detecting the deviator from an agreed strategy profile in games played on finite graphs with different information structures. We show that the problem is undecidable in the general case where the global state cannot be monitored. On the other hand, we prove that under perfect monitoring of the global state and imperfect monitoring of actions, the problem becomes decidable, and we present an effective synthesis procedure that covers infinitely repeated games with private monitoring.}
}
@article{CCD-ic17,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Vincent Cheval and Hubert Comon{-}Lundh and St{\'e}phanie Delaune},
title = {{A procedure for deciding symbolic equivalence between sets of constraint systems}},
volume = {255},
year = {2017},
pages = {94-125},
doi = {10.1016/j.ic.2017.05.004},
url = {https://www.sciencedirect.com/science/article/pii/S0890540117300949},
abstract = {We consider security properties of cryptographic protocols that can be modelled using trace equivalence, a crucial notion when specifying privacy-type properties, like anonymity, vote-privacy, and unlinkability. Infinite sets of possible traces are symbolically represented using deducibility constraints. We describe an algorithm that decides trace equivalence for protocols that use standard primitives and that can be represented using such constraints. More precisely, we consider symbolic equivalence between sets of constraint systems, and we also consider disequations. Considering sets and disequations is actually crucial to decide trace equivalence for processes that may involve else branches and/or private channels (for a bounded number of sessions). Our algorithm for deciding symbolic equivalence between sets of constraint systems is implemented and performs well in practice. Unfortunately, it does not scale up well for deciding trace equivalence between processes. This is however the first implemented algorithm deciding trace equivalence on such a large class of processes.}
}
@inproceedings{D-PxTP17,
address = {Bras{\'{\i}}lia, Brazil},
month = sep,
year = 2017,
volume = {262},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Catherine Dubois and Bruno {Woltzenlogel Paleo}},
acronym = {{PxTP}'17},
booktitle = {Proceedings of the 5th Workshop on Proof eXchange for Theorem Proving ({PxTP}'17)},
author = {Gilles Dowek},
title = {Analyzing Individual Proofs as the Basis of Interoperability between Proof Systems},
pages = {3-12},
url = {https://arxiv.org/abs/1712.01485v1},
pdf = {https://arxiv.org/pdf/1712.01485v1.pdf},
doi = {10.4204/EPTCS.262.1},
abstract = {We describe the first results of a project of analyzing in which theories formal proofs can be expressed. We use this analysis as the basis of interoperability between proof systems.}
}
@inproceedings{DD-tpnc17,
address = {Prague, Czech Republic},
year = 2017,
volume = 10687,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Carlos Mart{\'{\i}}n{-}Vide and
Roman Neruda and
Miguel A. Vega{-}Rodr{\'{\i}}guez},
acronym = {{TPNC}'17},
booktitle = {Proceedings of the 6th International Conference on Theory and Practice of Natural Computing ({TPNC}'17)},
author = {Alejandro D{\'{\i}}az{-}Caro and Gilles Dowek},
title = {Typing Quantum Superpositions and Measurement},
pages = {281-293},
url = {https://arxiv.org/abs/1601.04294},
doi = {10.1007/978-3-319-71069-3_22},
abstract = {We propose a way to unify two approaches of non-cloning in quantum lambda-calculi. The first approach is to forbid duplicating variables, while the second is to consider all lambda-terms as algebraic-linear functions. We illustrate this idea by defining a quantum extension of first-order simply-typed lambda-calculus, where the type is linear on superposition, while allows cloning base vectors. In addition, we provide an interpretation of the calculus where superposed types are interpreted as vector spaces and non-superposed types as their basis.}
}
@article{D-lmcs17,
journal = {Logical Methods in Computer Science},
author = {Dowek, Gilles},
title = {{Lineal: A linear-algebraic Lambda-calculus}},
volume = {13},
number = {1},
year = {2017},
month = mar,
pages = {1-33},
doi = {10.23638/LMCS-13(1:8)2017},
url = {https://lmcs.episciences.org/3203},
pdf = {https://lmcs.episciences.org/3203/pdf}
}
@article{D-flap17,
publisher = {College Publications},
journal = {IfCoLoG Journal of Logics and their Applications},
author = {Dowek, Gilles},
title = {{Rules and derivations in an elementary logic course}},
volume = {4},
number = {1},
year = {2017},
pages = {21-32},
pdf = {https://hal.inria.fr/hal-01252124/file/ttl.pdf},
note = {Special Issue: Tools for Teaching Logic}
}
@phdthesis{Carlier-phd2017,
author = {Carlier, Pierre},
title = {{Verification of Stochastic Timed Automata}},
school = {{Ecole Normale Sup{\'e}rieure de Cachan (ENS Paris-Saclay) and Universit{\'e} de Mons}},
type = {Th{\`e}se de doctorat},
year = 2017,
month = dec,
url = {https://tel.archives-ouvertes.fr/tel-01696130},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/carlier-phd2017.pdf}
}
This file was generated by bibtex2html 1.98.