@incollection{BFLMOW-hmc18,
author = {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim G.
and Markey, Nicolas and Ouaknine, Jo{\"e}l and
Worrell, James},
title = {Model Checking Real-Time Systems},
booktitle = {Handbook of Model Checking},
editor = {Clarke, Ed and Henzinger, Tom and Veith, Helmut},
publisher = {Springer},
year = 2018,
pages = {1001-1046},
nochapter = {29},
doi = {10.1007/978-3-319-10575-8_29},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLMOW-hmc17.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLMOW-hmc17.pdf},
isbn = {978-3-319-10574-1},
abstract = {This chapter surveys timed automata as a formalism for
model checking real-time systems. We begin with introducing the
model, as an extension of finite-state automata with real-valued
variables for measuring time. We then present the main
model-checking results in this framework, and give a hint about some
recent extensions (namely weighted timed automata and timed
games).}
}
@article{BMRLL-acta16,
publisher = {Springer},
journal = {Acta Informatica},
author = {Bouyer, Patricia and Markey, Nicolas and Randour, Mickael
and Larsen, Kim G. and Laursen, Simon},
title = {Average-energy games},
volume = {55},
number = {2},
year = 2018,
month = jul,
pages = {91-127},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMRLL-acta16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMRLL-acta16.pdf},
doi = {10.1007/s00236-016-0274-1},
abstract = {Two-player quantitative zero-sum games provide a natural
framework to synthesize controllers with performance guarantees for
reactive systems within an uncontrollable environment. Classical
settings include mean-payoff games, where the objective is to
optimize the long-run average gain per action, and energy games,
where the system has to avoid running out of energy. We study
average-energy games, where the goal is to optimize the long-run
average of the accumulated energy. We show that this objective
arises naturally in several applications, and that it yields
interesting connections with previous concepts in the literature. We
prove that deciding the winner in such games is in NP coNP and at
least as hard as solving mean-payoff games, and we establish that
memoryless strategies suffice to win. We also consider the case
where the system has to minimize the average-energy while
maintaining the accumulated energy within predefined bounds at all
times: this corresponds to operating with a finite-capacity storage
for energy. We give results for one-player and two-player games, and
establish complexity bounds and memory requirements.}
}
@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.",
}}
@inproceedings{GBM-stacs18,
address = {Caen, France},
month = feb,
volume = {96},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Niedermeier, Rolf and Vall{\'e}e, Brigitte},
acronym = {{STACS}'18},
booktitle = {{P}roceedings of the 35th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'18)},
author = {Gardy, Patrick and Bouyer, Patricia and Markey, Nicolas},
title = {Dependences in Strategy Logic},
pages = {34:1-34:15},
year = {2018},
doi = {10.4230/LIPIcs.STACS.2018.34},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/8532/pdf/LIPIcs-STACS-2018-34.pdf},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=8532},
abstract = {Strategy Logic (SL) is a very expressive logic for specifying and verifying properties of multi-agent systems: in SL, one can quantify over strategies, assign them to agents, and express properties of the resulting plays. Such a powerful framework has two drawbacks: first, model checking SL has non-elementary complexity; second, the exact semantics of SL is rather intricate, and may not correspond to what is expected. In this paper, we focus on strategy dependences in SL, by tracking how existentially-quantified strategies in a formula may (or may not) depend on other strategies selected in the formula. We study different kinds of dependences, refining the approach of [Mogavero et al., Reasoning about strategies: On the model-checking problem, 2014], and prove that they give rise to different satisfaction relations. In the setting where strategies may only depend on what they have observed, we identify a large fragment of SL for which we prove model checking can be performed in 2-EXPTIME.}
}
@inproceedings{BFG-stacs18,
address = {Caen, France},
month = feb,
volume = {96},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Niedermeier, Rolf and Vall{\'e}e, Brigitte},
acronym = {{STACS}'18},
booktitle = {{P}roceedings of the 35th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'18)},
author = {Bollig, Benedikt and Fortin, Marie and Gastin, Paul},
title = {Communicating Finite-State Machines and Two-Variable Logic},
pages = {17:1-17:14},
year = {2018},
doi = {10.4230/LIPIcs.STACS.2018.17},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/8529/pdf/LIPIcs-STACS-2018-17.pdf},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=8529},
abstract = {Communicating finite-state machines are a fundamental, well-studied model of finite-state processes that communicate via unbounded first-in first-out channels. We show that they are expressively equivalent to existential MSO logic with two first-order variables and the order relation.}
}
@inproceedings{GKLZ-stacs18,
address = {Caen, France},
month = feb,
volume = {96},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Niedermeier, Rolf and Vall{\'e}e, Brigitte},
acronym = {{STACS}'18},
booktitle = {{P}roceedings of the 35th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'18)},
author = {Ganardi, Moses and K{\"o}nig, Daniel and Lohrey, Markus and Zetzsche, Georg},
title = {Knapsack problems for wreath products},
pages = {32:1-32:13},
year = {2018},
doi = {10.4230/LIPIcs.STACS.2018.32},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/8520/pdf/LIPIcs-STACS-2018-32.pdf},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=8520}
}
@article{BFM-ic17,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Blondin, Michael and Finkel, Alain and McKenzie, Pierre},
title = {Handling Infinitely Branching Well-structured Transition Systems},
volume = {258},
year = {2018},
pages = {28--49},
doi = {10.1016/j.ic.2017.11.001}
}
@article{GLL-fmsd17,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Goubault{-}Larrecq, Jean and Lachance, Jean-Philippe},
title = {On the Complexity of Monitoring {O}rchids Signatures, and Recurrence Equations},
volume = {53},
number = {1},
year = {2018},
month = aug,
pages = {6-32},
doi = {10.1007/s10703-017-0303-x},
url = {https://doi.org/10.1007/s10703-017-0303-x},
abstract = {Modern monitoring tools such as our intrusion detection tool Orchids work by firing new monitor instances dynamically. Given an Orchids signature (a.k.a. a rule, a specification), what is the complexity of checking that specification, that signature? In other words, let \(f(n)\) be the maximum number of monitor instances that can be fired on a sequence of \(n\) events: we design an algorithm that decides whether \(f(n)\) is asymptotically exponential or polynomial, and in the latter case returns an exponent \(d\) such that \(f(n)=\Theta(n^d)\). Ultimately, the problem reduces to the following mathematical question, which may have other uses in other domains: given a system of recurrence equations described using the operators \(+\) and \(\max\), and defining integer sequences \(u_n\), what is the asymptotic behavior of \(u_n\) as \(n\) tends to infinity? We show that, under simple assumptions, \(u_n\) is either exponential or polynomial, and that this can be decided, and the exponent computed, using a simple modification of Tarjan's strongly connected components algorithm, in linear time.},
note = {Special issue of RV'16}
}
@article{HM-tcs17,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Haddad, Serge and Monmege, Benjamin},
title = {Interval iteration algorithm for {MDP}s and {IMDP}s},
volume = {735},
year = {2018},
pages = {111-131},
month = jul,
doi = {10.1016/j.tcs.2016.12.003},
url = {http://authors.elsevier.com/sd/article/S0304397516307095},
abstract = {Markov Decision Processes (MDP) are a widely used model including both non-deterministic and probabilistic choices. Minimal and maximal probabilities to reach a target set of states, with respect to a policy resolving non-determinism, may be computed by several methods including value iteration. This algorithm, easy to implement and efficient in terms of space complexity, iteratively computes the probabilities of paths of increasing length. However, it raises three issues: (1) defining a stopping criterion ensuring a bound on the approximation, (2) analysing the rate of convergence, and (3) specifying an additional procedure to obtain the exact values once a sufficient number of iterations has been performed. The first two issues are still open and, for the third one, an upper bound on the number of iterations has been proposed. Based on a graph analysis and transformation of MDPs, we address these problems. First we introduce an interval iteration algorithm, for which the stopping criterion is straightforward. Then we exhibit its convergence rate. Finally we significantly improve the upper bound on the number of iterations required to get the exact values. We extend our approach to also deal with Interval Markov Decision Processes (IMDP) that can be seen as symbolic representations of MDPs.}
}
@article{FHLM-deds17,
publisher = {Springer},
journal = {Discrete Event Dynamic Systems: Theory and Applications},
author = {{\'E}ric Fabre and Lo{\"i}c H{\'e}lou{\"e}t and Engel Lefaucheux and Herv{\'e} Marchand},
title = {Diagnosability of Repairable Faults},
volume = {28},
number = {2},
month = jun,
year = {2018},
pages = {183-213},
doi = {10.1007/s10626-017-0255-8},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FHLM-deds17.pdf},
abstract = {The diagnosis problem for discrete event systems consists in deciding whether some fault event occurred or not in the system, given partial observations on the run of that system. Diagnosability checks whether a correct diagnosis can be issued in bounded time after a fault, for all faulty runs of that system. This problem appeared two decades ago and numerous facets of it have been explored, mostly for permanent faults. It is known for example that diagnosability of a system can be checked in polynomial time, while the construction of a diagnoser is exponential. The present paper examines the case of transient faults, that can appear and be repaired. Diagnosability in this setting means that the occurrence of a fault should always be detected in bounded time, but also before the fault is repaired, in order to prepare for the detection of the next fault or to take corrective measures while they are needed. Checking this notion of diagnosability is proved to be PSPACE-complete. It is also shown that faults can be reliably counted provided the system is diagnosable for faults and for repairs.}
}
@article{BGH-fmsd17,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Bollig, Benedikt and Grindei, Manuela-Lidia and Habermehl, Peter},
title = {Realizability of Concurrent Recursive Programs},
volume = {53},
number = {3},
year = {2018},
pages = {339-362},
doi = {10.1007/s10703-017-0282-y},
abstract = {We study the realizability problem for concurrent recursive programs: Given a distributed system architecture and a sequential specification over words, find a distributed automata implementation that is equivalent to the specification. This problem is well-studied as far as finite-state processes are concerned, and it has a solution in terms of Zielonka's Theorem. We lift Zielonka's Theorem to the case where processes are recursive and modeled as visibly pushdown (or, equivalently, nested-word) automata. However, contrarily to the finite-state case, it is undecidable whether a specification is realizable or not. Therefore, we also consider suitable underapproximation techniques from the literature developed for multi-pushdown systems, and we show that they lead to a realizability framework with effective algorithms.
}
}
@article{ABG-ic17,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Aiswarya, C. and Bollig, Benedikt and Gastin, Paul},
title = {An Automata-Theoretic Approach to the Verification of Distributed Algorithms},
volume = {259},
month = apr,
year = {2018},
pages = {305-327},
doi = {10.1016/j.ic.2017.05.006},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-ic17.pdf},
abstract = {We introduce an automata-theoretic method for the verification of distributed algorithms running on ring networks. In a distributed algorithm, an arbitrary number of processes cooperate to achieve a common goal (e.g., elect a leader). Processes have unique identifiers (pids) from an infinite, totally ordered domain. An algorithm proceeds in synchronous rounds, each round allowing a process to perform a bounded sequence of actions such as send or receive a pid, store it in some register, and compare register contents wrt. the associated total order. An algorithm is supposed to be correct independently of the number of processes. To specify correctness properties, we introduce a logic that can reason about processes and pids. Referring to leader election, it may say that, at the end of an execution, each process stores the maximum pid in some dedicated register.
We show that the verification problem of distributed algorithms can be reduced to satisfiability of a formula from propositional dynamic logic with loop and converse (LCPDL), interpreted over grids over a finite alphabet. This translation is independent of any restriction imposed on the algorithm. However, since the verification problem (and satisfiability for LCPDL) is undecidable, we propose an underapproximation technique, which bounds the number of rounds. This is an appealing approach, as the number of rounds needed by a distributed algorithm to conclude is often exponentially smaller than the number of processes. Using our reduction to LCPDL, we provide an automata-theoretic solution, reducing model checking to emptiness for alternating two-way automata on words. Overall, we show that round-bounded verification of distributed algorithms over rings is PSPACE-complete, provided the number of rounds is given in unary.}
}
@inproceedings{BG-wst18,
address = {Oxford, UK},
month = jul,
editor = {Lucas, Salvador},
acronym = {{WST}'18},
booktitle = {{P}roceedings of the 16th {I}nternational {W}orkshop on {T}ermination
({WST}'18)},
author = {Blanqui, Fr{\'e}d{\'e}ric and Genestier, Guillaume},
title = {Termination of $\lambda \Pi$ modulo rewriting using the size-change principle},
pages = {10--14},
year = 2018,
pdf = {https://hal.inria.fr/hal-01944731/file/main.pdf}
}
@inproceedings{Thire-lfmtp2018,
address = {Oxford, UK},
month = jul,
year = 2018,
publisher = {ACM Press},
editor = {Blanqui, Fr{\'e}d{\'e}ric and Reis, Giselle},
acronym = {{LFMTP}'18},
booktitle = {Proceedings of the 13th {I}nternational {W}orkshop on {L}ogical {F}rameworks and
{M}eta-{L}anguages: {T}heory and {P}ractice ({LFMTP}'18)},
author = {Thir{\'e}, Fran{\c{c}}ois},
title = {{S}haring a {L}ibrary between {P}roof {A}ssistants: {R}eaching out to the {HOL}
{F}amily *},
pages = {57--71},
url = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?LFMTP2018.5},
pdf = {https://hal.inria.fr/hal-01929714/file/sttforall-lfmtp.pdf},
doi = {10.4204/EPTCS.274.4}
}
@inproceedings{Burel-mfcs2018,
address = {Liverpool, UK},
month = aug,
volume = {117},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Potapov, Igor and Spirakis, Paul and Worrell, James},
acronym = {{MFCS}'18},
booktitle = {{P}roceedings of the 42nd
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'18)},
author = {Burel, Guillaume},
title = {Linking Focusing and Resolution with Selection},
pages = {9:1--9:14},
year = {2018},
doi = {10.4230/LIPIcs.MFCS.2018.9},
url = {https://hal.inria.fr/hal-01670476},
pdf = {https://hal.inria.fr/hal-01670476/file/lipics.pdf},
futureannote = {Keywords: logic in computer science, automated deduction,
proof theory, sequent calculus, refinements of resolution, deduction
modulo theory, polarization}
}
@inproceedings{LR-lfmtp2018,
address = {Oxford, UK},
month = jul,
year = 2018,
publisher = {ACM Press},
editor = {Blanqui, Fr{\'e}d{\'e}ric and Reis, Giselle},
acronym = {{LFMTP}'18},
booktitle = {Proceedings of the 13th {I}nternational {W}orkshop on {L}ogical {F}rameworks and
{M}eta-{L}anguages: {T}heory and {P}ractice ({LFMTP}'18)},
author = {Rodolphe Lepigre and Christophe Raffalli},
title = {Abstract Representation of Binders in OCaml using the Bindlib Library},
pages = {42-56},
url = {https://arxiv.org/abs/1807.01872},
pdf = {https://arxiv.org/pdf/1807.01872.pdf},
doi = {10.4204/EPTCS.274.4},
abstract = {The Bindlib library for OCaml provides a set of tools for the manipulation of data structures with variable binding. It is very well suited for the representation of abstract syntax trees, and has already been used for the implementation of half a dozen languages and proof assistants (including a new version of the logical framework Dedukti). Bindlib is optimised for fast substitution, and it supports variable renaming. Since the representation of binders is based on higher-order abstract syntax, variable capture cannot arise during substitution. As a consequence, variable names are not updated at substitution time. They can however be explicitly recomputed to avoid ''visual capture'' (i.e., distinct variables with the same apparent name) when a data structure is displayed.}
}
@article{LR-toplas18,
publisher = {ACM Press},
journal = {ACM Transactions on Programming Languages and Systems},
author = {Rodolphe Lepigre and Christophe Raffalli},
title = {{Practical Subtyping for Curry-Style Languages}},
volume = {41},
number = {1},
year = {2018},
pages = {5:1--5:58},
doi = {10.1145/3285955},
pdf = {https://lepigre.fr/files/publications/LepRaf2018a.pdf},
abstract = {We present a new, syntax-directed framework for Curry-style type systems with subtyping. It supports a rich set of features, and allows for a reasonably simple theory and implementation. The system we consider has sum and product types, universal and existential quantifiers, and inductive and coinductive types. The latter two may carry size invariants that can be used to establish the termination of recursive programs. For example, the termination of quicksort can be derived by showing that partitioning a list does not increase its size. The system deals with complex programs involving mixed induction and coinduction, or even mixed polymorphism and (co-)induction. One of the key ideas is to separate the notion of size from recursion. We do not check the termination of programs directly, but rather show that their (circular) typing proofs are well-founded. Termination is then obtained using a standard (semantic) normalisation proof. To demonstrate the practicality of the system, we provide an implementation accepting all the examples discussed in the article.}
}
@inproceedings{L-types2017,
address = {Budapest, Hungary},
year = 2018,
volume = {104},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Ambrus Kaposi and Tam{\'a}s Kozsik},
acronym = {{TYPES}'17},
booktitle = {{P}roceedings of the 23rd {I}nternational {C}onference on {T}ypes for {P}roofs and {P}rograms
({TYPES}'17},
author = {Rodolphe Lepigre},
title = {{PML\(_2\):} Integrated Program Verification in ML},
pages = {4:1--4:27},
url = {http://drops.dagstuhl.de/opus/volltexte/2018/10052/},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/10052/pdf/LIPIcs-TYPES-2017-4.pdf},
doi = {10.4230/LIPIcs.TYPES.2017.4},
abstract = {We present the PML\(_2\) language, which provides a uniform environment for programming, and for proving properties of programs in an ML-like setting. The language is Curry-style and call-by-value, it provides a control operator (interpreted in terms of classical logic), it supports general recursion and a very general form of (implicit, non-coercive) subtyping. In the system, equational properties of programs are expressed using two new type formers, and they are proved by constructing terminating programs. Although proofs rely heavily on equational reasoning, equalities are exclusively managed by the type-checker. This means that the user only has to choose which equality to use, and not where to use it, as is usually done in mathematical proofs. In the system, writing proofs mostly amounts to applying lemmas (possibly recursive function calls), and to perform case analyses (pattern matchings).}
}
@incollection{SD-EORM18,
author = {Demri, St{\'e}phane},
title = {Reasoning about reversal-bounded counter machines},
editor = {Goli{\'n}ska-Pilarek, Joanna and Zawidzki, Micha\l},
booktitle = {Ewa Orlowska on Relational Methods in Logic and Computer Science},
publisher = {Springer},
series = {Outstanding Contributions to Logic},
volume = {17},
year = {2018},
pages = {441-479},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SD-EORM.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SD-EORM.pdf}
}
@phdthesis{dallon-phd2018,
author = {Dallon, Antoine},
title = {{Verification of indistinguishability properties in cryptographic protocols} -- {Small attacks and efficient decision with SAT-Equiv}},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2018,
month = nov,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/dallon-phd18.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/dallon-phd18.pdf}
}
@phdthesis{duplouy-phd2018,
author = {Duplouy, Yann},
title = {{Applying Formal Methods to Autonomous Vehicle Control}},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2018,
month = nov,
url = {http://www.lsv.fr/~duplouy/defence/}
}
@inproceedings{BGMR-gandalf18,
address = {Saarbr{\"u}cken, Germany},
month = sep,
volume = {277},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Andrea Orlandini and Martin Zimmermann},
acronym = {{GandALF}'18},
booktitle = {{P}roceedings of the 9th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
({GandALF}'18)},
author = {Bouyer, Patricia and Gonz{\'a}lez, Mauricio and Markey, Nicolas and Randour, Mickael},
title = {Multi-weighted Markov Decision Processes with Reachability Objectives},
pages = {250-264},
year = {2018},
doi = {10.4204/EPTCS.277.18},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMR-gandalf18.pdf},
url = {http://arxiv.org/abs/1809.03107},
abstract = {In this paper, we are interested in the synthesis of schedulers in double-weighted Markov decision processes, which satisfy both a percentile constraint over a weighted reachability condition, and a quantitative constraint on the expected value of a random variable defined using a weighted reachability condition. This problem is inspired by the modelization of an electric-vehicle charging problem. We study the cartography of the problem, when one parameter varies, and show how a partial cartography can be obtained via two sequences of opimization problems. We discuss completeness and feasability of the method.}
}
@inproceedings{BJM-rv18,
address = {Limassol, Cyprus},
month = nov,
volume = 11237,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Colombo, Christian and Leucker, Martin},
acronym = {{RV}'18},
booktitle = {{P}roceedings of the 18th {W}orkshop on {R}untime {V}erification ({RV}'18)},
author = {Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas},
title = {Efficient Timed Diagnosis Using Automata with Timed Domains},
pages = {205-221},
year = {2018},
doi = {10.1007/978-3-030-03769-7_12},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BJM-rv18.pdf},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BJM-rv18.pdf},
abstract = {We consider the problems of efficiently diagnosing and predicting what did (or will) happen in a partially-observable one-clock timed automaton. We introduce timed sets as a formalism to keep track of the evolution of the reachable configurations over time, and use our previous work on automata over timed domains to build a candidate diagnoser for our timed automaton. We report on our implementation of this approach compared to the approach of [Tripakis, Fault diagnosis for timed automata, 2002].}
}
@inproceedings{BDH-esorics18,
address = {Barcelona, Spain},
month = sep,
year = 2018,
volume = {11098},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Javier L{\'{o}}pez and
Jianying Zhou and
Miguel Soriano},
acronym = {{ESORICS}'18},
booktitle = {{P}roceedings of the 23rd {E}uropean {S}ymposium on
{R}esearch in {C}omputer {S}ecurity ({ESORICS}'18)},
author = {David Baelde and St{\'e}phanie Delaune and Lucca Hirschi},
title = {{POR} for Security Protocol Equivalences - Beyond Action-Determinism},
pages = {385-405},
url = {https://arxiv.org/abs/1804.03650},
doi = {10.1007/978-3-319-99073-6\_19},
abstract = {Formal methods have proved effective to automatically analyse protocols. Recently, much research has focused on verifying trace equivalence on protocols, which is notably used to model interesting privacy properties such as anonymity or unlinkability. Several tools for checking trace equivalence rely on a naive and expensive exploration of all interleavings of concurrent actions, which calls for partial-order reduction (POR) techniques. In this paper, we present the first POR technique for protocol equivalences that does not rely on an action-determinism assumption: we recast trace equivalence as a reachability problem, to which persistent and sleep set techniques can be applied, and we show how to effectively apply these results in the context of symbolic execution. We report on a prototype implementation, improving the tool DeepSec.}
}
@inproceedings{CDD-esorics18,
address = {Barcelona, Spain},
month = sep,
year = 2018,
volume = {11098},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Javier L{\'{o}}pez and
Jianying Zhou and
Miguel Soriano},
acronym = {{ESORICS}'18},
booktitle = {{P}roceedings of the 23rd {E}uropean {S}ymposium on
{R}esearch in {C}omputer {S}ecurity ({ESORICS}'18)},
author = {V{\'e}ronique Cortier and Antoine Dallon and St{\'e}phanie Delaune},
title = {Efficiently Deciding Equivalence for Standard Primitives and Phases},
pages = {491-511},
url = {https://hal.archives-ouvertes.fr/hal-01819366},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDD-esorics18.pdf},
doi = {10.1007/978-3-319-99073-6\_24},
abstract = {Privacy properties like anonymity or untraceability are now
well identified, desirable goals of many security protocols. Such properties
are typically stated as equivalence properties. However, automatically
checking equivalence of protocols often yields efficiency issues.\par
We propose an efficient algorithm, based on graph planning and SATsolving.
It can decide equivalence for a bounded number of sessions, for
protocols with standard cryptographic primitives and phases (often necessary
to specify privacy properties), provided protocols are well-typed,
that is encrypted messages cannot be confused. The resulting implementation,
SAT-Equiv, demonstrates a significant speed-up w.r.t. other
existing tools that decide equivalence, covering typically more than 100
sessions. Combined with a previous result, SAT-Equiv can now be used to
prove security, for some protocols, for an unbounded number of sessions.}
}
@article{BLMP-jml18,
publisher = {World Scientific},
journal = {Journal of Mathematical Logic},
author = {Brattka, Vasco and Le{~}Roux, St{\'e}phane and Miller, Joseph S. and Pauly, Arno},
title = {{Connected Choice and Brouwer's Fixed Point Theorem}},
year = {2018},
note = {To appear}
}
@inproceedings{D-time18,
address = {Warsaw, Poland},
month = oct,
year = 2018,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Natasha Alechina and Kjetil Norvag and Wojciech Penczek},
acronym = {{TIME}'18},
booktitle = {{P}roceedings of the 25th {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'18)},
author = {Demri, St{\'e}phane},
title = {On temporal and separation logics},
pages = {1:1-1:4},
url = {http://drops.dagstuhl.de/opus/volltexte/2018/9766/pdf/LIPIcs-TIME-2018-1.pdf}
}
@mastersthesis{m2-Hilaire,
author = {Hilaire, Mathieu},
title = {{Complexity of the reachability problem for parametric timed automata}},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2018},
month = sep,
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hilaire-M2-2018.pdf}
}
@techreport{CHKTP-hal18,
author = {Chatain, {\relax Th}omas and Haar, Stefan and Kolc{\'a}k, Juraj and Thakkar, Aalok and Paulev{\'e}, Lo{\"i}c},
institution = {HAL},
month = oct,
note = {33~pages},
number = {hal-01893106},
type = {Research Report},
title = {{Concurrency in Boolean networks}},
year = {2018},
url = {https://hal.inria.fr/hal-01893106},
pdf = {https://hal.inria.fr/hal-01893106/document},
abstract = {Boolean networks (BNs) are widely used to model the qualitative dynamics of biological systems. Besides the logical rules determining the evolution of each component with respect to the state of its regulators, the scheduling of components updates can have a dramatic impact on the predicted behaviours. In this paper, we explore the use of Contextual Petri Nets (CPNs) to study dynamics of BNs with a concurrency theory perspective. After showing bi-directional translations between CPNs and BNs and analogies between results on synchronism sensitivies, we illustrate that usual updating modes for BNs can miss plausible behaviours, i.e., incorrectly conclude on the absence/impossibility of reaching specific configurations. Taking advantage of CPN semantics enabling more behaviour than the generalized asynchronous updating mode, we propose an encoding of BNs ensuring a correct abstraction of any multivalued refinement, as one may expect to achieve when modelling biological systems with no assumption on its time features.}
}
@phdthesis{Lefaucheux-phd2018,
author = {Lefaucheux, Engel},
title = {Controlling Information in Probabilistic Systems},
school = {Universit{\'e} Rennes~1, Rennes, France},
type = {Th{\`e}se de doctorat},
year = 2018,
month = sep,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/lefaucheux-phd18.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/lefaucheux-phd18.pdf}
}
@phdthesis{Grosshans-phd2018,
author = {Grosshans, Nathan},
title = {The limits of {Ne\v{c}iporuk}'s method and the power of programs over monoids taken from small varieties of finite monoids},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2018,
month = sep,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/grosshans-phd18.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/grosshans-phd18.pdf}
}
@inproceedings{LPR-fsttcs18,
address = {Ahmedabad, India},
month = dec,
year = 2018,
volume = {122},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Sumit Ganguly and Paritosh Pandya},
acronym = {{FSTTCS}'18},
booktitle = {{P}roceedings of the 38th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'18)},
author = {Le{~}Roux, Stephane and Pauly, Arno and Randour, Mickael},
title = {Extending finite-memory determinacy to Boolean combinations of winning conditions},
pages = {38:1-38:20},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9937},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9937/pdf/LIPIcs-FSTTCS-2018-38.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2018.38},
abstract = {We study finite-memory (FM) determinacy in games on finite graphs, a central question for applications in controller synthesis, as FM strategies correspond to implementable controllers. We establish general conditions under which FM strategies suffice to play optimally, even in a broad multi-objective setting. We show that our framework encompasses important classes of games from the literature, and permits to go further, using a unified approach. While such an approach cannot match ad-hoc proofs with regard to tightness of memory bounds, it has two advantages: first, it gives a widely-applicable criterion for FM determinacy; second, it helps to understand the cornerstones of FM determinacy, which are often hidden but common in proofs for specific (combinations of) winning conditions.}
}
@inproceedings{M-fsttcs18,
address = {Ahmedabad, India},
month = dec,
year = 2018,
volume = {122},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Sumit Ganguly and Paritosh Pandya},
acronym = {{FSTTCS}'18},
booktitle = {{P}roceedings of the 38th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'18)},
author = {Alessio Mansutti},
title = {Extending propositional separation logic for robustness properties},
pages = {42:1-42:23},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9941},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9941/pdf/LIPIcs-FSTTCS-2018-42.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2018.42},
abstract = {We study an extension of propositional separation logic that can specify robustness properties, such as acyclicity and garbage freedom, for automatic verification of stateful programs with singly-linked lists. We show that its satisfiability problem is PSpace-complete, whereas modest extensions of the logic are shown to be Tower-hard. As separating implication, reachability predicates (under some syntactical restrictions) and a unique quantified variable are allowed, this logic subsumes several PSpace-complete separation logics considered in previous works.}
}
@inproceedings{BHL-fsttcs18,
address = {Ahmedabad, India},
month = dec,
year = 2018,
volume = {122},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Sumit Ganguly and Paritosh Pandya},
acronym = {{FSTTCS}'18},
booktitle = {{P}roceedings of the 38th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'18)},
author = {B{\'e}atrice B{\'e}rard and Stefan Haar and Lo{\"i}c H{\'e}lou{\"e}t},
title = {Hyper Partial Order Logic},
pages = {20:1-20:21},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9919},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9919/pdf/LIPIcs-FSTTCS-2018-20.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2018.20},
abstract = {We define HyPOL, a local hyper logic for partial order models, expressing properties of sets of runs. These properties depict shapes of causal dependencies in sets of partially ordered executions, with similarity relations defined as isomorphisms of past observations. Unsurprisingly, since comparison of projections are included, satisfiability of this logic is undecidable. We then address model checking of HyPOL and show that, already for safe Petri nets, the problem is undecidable. Fortunately, sensible restrictions of observations and nets allow us to bring back model checking of HyPOL to a decidable problem, namely model checking of MSO on graphs of bounded treewidth.}
}
@inproceedings{FLS-fsttcs18,
address = {Ahmedabad, India},
month = dec,
year = 2018,
volume = {122},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Sumit Ganguly and Paritosh Pandya},
acronym = {{FSTTCS}'18},
booktitle = {{P}roceedings of the 38th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'18)},
author = {Alain Finkel and J{\'e}r{\^o}me Leroux and Gr{\'e}goire Sutre},
title = {Reachability for Two-Counter Machines with One Test and One Reset},
pages = {31:1-31:14},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9930},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9930/pdf/LIPIcs-FSTTCS-2018-31.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2018.31},
abstract = {We prove that the reachability relation of two-counter machines with one zero-test and one reset is Presburger-definable and effectively computable. Our proof is based on the introduction of two classes of Presburger-definable relations effectively stable by transitive closure. This approach generalizes and simplifies the existing different proofs and it solves an open problem introduced by Finkel and Sutre in 2000.}
}
@inproceedings{BLS-fsttcs18,
address = {Ahmedabad, India},
month = dec,
year = 2018,
volume = {122},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Sumit Ganguly and Paritosh Pandya},
acronym = {{FSTTCS}'18},
booktitle = {{P}roceedings of the 38th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'18)},
author = {Baelde, David and Lick, Anthony and Schmitz, Sylvain},
title = {A Hypersequent Calculus with Clusters for Tense Logic over Ordinals},
pages = {15:1-15:19},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9914},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9914/pdf/LIPIcs-FSTTCS-2018-15.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2018.15},
abstract = {Prior's tense logic forms the core of linear temporal logic, with both past-and future-looking modalities. We present a sound and complete proof system for tense logic over ordinals. Technically, this is a hypersequent system, enriched with an ordering, clusters, and annotations. The system is designed with proof search algorithms in mind, and yields an optimal coNP complexity for the validity problem. It entails a small model property for tense logic over ordinals: every satisfiable formula has a model of order type at most \(\omega^2\). It also allows to answer the validity problem for ordinals below or exactly equal to a given one.}
}
@techreport{CHP-arxiv18,
author = {Chatain, {\relax Th}omas and Haar, Stefan and Paulev{\'e}, Lo{\"i}c},
institution = {Computing Research Repository},
month = aug,
note = {15~pages},
number = {1808.10240},
type = {Research Report},
title = {Most Permissive Semantics of Boolean Networks},
year = {2018},
url = {https://arxiv.org/abs/1808.10240},
pdf = {https://arxiv.org/pdf/1808.10240v1.pdf},
abstract = {As shown in [3], the usual update modes of
Boolean networks (BNs), including synchronous and (generalized)
asynchronous, fail to capture behaviours introduced by multivalued
refinements. Thus, update modes do not allow a correct abstract
reasoning on dynamics of biological systems, as they may lead to reject
valid BN models.\par
We introduce a new semantics for interpreting BNs which meets with a
correct abstraction of any multivalued refinements, with any update
mode. This semantics subsumes all the usual updating modes, while
enabling new behaviours achievable by more concrete models. Moreover, it
appears that classical dynamical analyses of reachability and
attractors have a simpler computational complexity:
\begin{itemize}
\item reachability can be assessed in a polynomial number of iterations
(instead of being PSPACE-complete with update modes);
\item attractors are hypercubes, and deciding the existence of attractors
with a given upper-bounded dimension is in NP (instead of
PSPACE-complete with update modes).
\end{itemize}
The computation of iterations is in NP in the very general case, and is
linear when local functions are monotonic, or with some usual
representations of functions of BNs (binary decision diagrams, Petri
nets, automata networks, etc.).\par
In brief, the most permissive semantics of BNs enables a correct
abstract reasoning on dynamics of BNs, with a greater tractability than
previously introduced update modes.\par
This technical report lists the main
definitions and properties of the most permissive semantics of BNs, and
draw some remaining open questions.}
}
@inproceedings{JK-ccs18,
address = {Toronto, Canada},
month = oct,
publisher = {ACM Press},
editor = {Backes, Michael and Wang, XiaoFeng},
acronym = {{CCS}'18},
booktitle = {{P}roceedings of the 25th {ACM} {C}onference
on {C}omputer and {C}ommunications {S}ecurity
({CCS}'18)},
author = {Barthe, Gilles and Fan, Xiong and Gancher, Joshua and Gr{\'e}goire, Benjamin and Jacomme, Charlie and Shi, Elaine},
title = {Symbolic Proofs for Lattice-Based Cryptography},
pages = {538-555},
year = {2018},
pdf = {https://eprint.iacr.org/2018/765.pdf},
url = {https://dl.acm.org/citation.cfm?doid=3243734.3243825}
}
@inproceedings{FN-disc18,
address = {New Orleans, USA},
month = oct,
volume = 121,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Ulrich Schmid},
acronym = {{DISC}'18},
booktitle = {{P}roceedings of the 32nd {I}nternational
{S}ymposium on {D}istributed {C}omputing
({DISC}'18)},
author = {F{\"u}gger, Matthias and Nowak, {\relax Th}omas},
title = {Fast Multidimensional Asymptotic and Approximate Consensus},
pages = {27:1-27:15},
year = {2018},
url = {https://arxiv.org/abs/1805.04923}
}
@inproceedings{BLS-atva18,
address = {Los Angeles, California, USA},
month = oct,
year = {2018},
volume = {11138},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Shuvendu Lahiri and Chao Wang},
acronym = {{ATVA}'18},
booktitle = {{P}roceedings of the 16th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'18)},
author = {Benedikt Bollig and Mathieu Lehaut and Nathalie Sznajder},
title = {Round-Bounded Control of Parameterized Systems},
pages = {370-386},
url = {https://hal.archives-ouvertes.fr/hal-01849206},
doi = {10.1007/978-3-030-01090-4_22},
abstract = {We consider systems with unboundedly many processes that communicate through shared memory. In that context, simple verification questions have a high complexity or, in the case of pushdown processes, are even undecidable. Good algorithmic properties are recovered under round-bounded verification, which restricts the system behavior to a bounded number of round-robin schedules. In this paper, we extend this approach to a game-based setting. This allows one to solve synthesis and control problems and constitutes a further step towards a theory of languages over infinite alphabets.}
}
@phdthesis{halfon-phd2018,
author = {Halfon, Simon},
title = {On Effective Representations of Well Quasi-Orderings},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2018,
month = jun,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/halfon-phd18.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/halfon-phd18.pdf}
}
@inproceedings{BBJ-csl18,
address = {Birmingham, UK},
month = sep,
year = 2018,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Ghica, Dan R. and Jung, Achim},
acronym = {{CSL}'18},
booktitle = {{P}roceedings of the 27th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'18)},
author = {B{\'e}rard, B{\'e}atrice and Bouyer, Patricia and Jug{\'e}, Vincent},
title = {Finite bisimulations for dynamical systems with overlapping trajectories},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9693},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9693/pdf/LIPIcs-CSL-2018-26.pdf},
doi = {10.4230/LIPIcs.CSL.2018.26},
abstract = {Having a finite bisimulation is a good feature for a dynamical system, since it can lead to the decidability of the verification of reachability properties. We investigate a new class of o-minimal dynamical systems with very general flows, where the classical restrictions on trajectory intersections are partly lifted. We identify conditions, that we call Finite and Uniform Crossing: When Finite Crossing holds, the time-abstract bisimulation is computable and, under the stronger Uniform Crossing assumption, this bisimulation is finite and definable.}
}
@inproceedings{GMS-concur18,
address = {Beijing, China},
month = sep,
year = 2018,
volume = {118},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Schewe, Sven and Zhang, Lijun},
acronym = {{CONCUR}'18},
booktitle = {{P}roceedings of the 29th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'18)},
author = {Paul Gastin and Sayan Mukherjee and B. Srivathsan},
title = {Reachability in timed automata with diagonal constraints},
pages = {28:1-28:17},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9566},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9566/pdf/LIPIcs-CONCUR-2018-28.pdf},
doi = {10.4230/LIPIcs.CONCUR.2018.28},
abstract = {We consider the reachability problem for timed automata having diagonal constraints (like x - y < 5) as guards in transitions. The best algorithms for timed automata proceed by enumerating reachable sets of its configurations, stored in a data structure called ''zones''. Simulation relations between zones are essential to ensure termination and efficiency. The algorithm employs a simulation test Z <= Z' which ascertains that zone Z does not reach more states than zone Z', and hence further enumeration from Z is not necessary. No effective simulations are known for timed automata containing diagonal constraints as guards. We propose a simulation relation <=_{LU}^d for timed automata with diagonal constraints. On the negative side, we show that deciding Z not <=_{LU}^d Z' is NP-complete. On the positive side, we identify a witness for Z not <=_{LU}^d Z' and propose an algorithm to decide the existence of such a witness using an SMT solver. The shape of the witness reveals that the simulation test is likely to be efficient in practice.}
}
@inproceedings{BFG-concur18,
address = {Beijing, China},
month = sep,
year = 2018,
volume = {118},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Schewe, Sven and Zhang, Lijun},
acronym = {{CONCUR}'18},
booktitle = {{P}roceedings of the 29th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'18)},
author = {Bollig, Benedikt and Fortin, Marie and Gastin, Paul},
title = {It Is Easy to Be Wise After the Event: Communicating Finite-State
Machines Capture First-Order Logic with ''Happened Before''},
pages = {7:1-7:17},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9545},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9545/pdf/LIPIcs-CONCUR-2018-7.pdf},
doi = {10.4230/LIPIcs.CONCUR.2018.7},
abstract = {Message sequence charts (MSCs) naturally arise as executions of communicating finite-state machines (CFMs), in which finite-state processes exchange messages through unbounded FIFO channels. We study the first-order logic of MSCs, featuring Lamport's happened-before relation. We introduce a star-free version of propositional dynamic logic (PDL) with loop and converse. Our main results state that (i) every first-order sentence can be transformed into an equivalent star-free PDL sentence (and conversely), and (ii) every star-free PDL sentence can be translated into an equivalent CFM. This answers an open question and settles the exact relation between CFMs and fragments of monadic second-order logic. As a byproduct, we show that first-order logic over MSCs has the three-variable property.}
}
@article{CFMF-fac18,
publisher = {Springer},
journal = {Formal Aspects of Computing},
author = {Rapha{\"e}l Chane-Yack-Fa and Marc Frappier and Amel Mammar and Alain Finkel},
title = {{Parameterized Verification of Monotone Information Systems}},
volume = {30},
number = {3-4},
year = {2018},
pages = {463-489},
doi = {10.1007/s00165-018-0460-8},
url = {https://link.springer.com/article/10.1007/s00165-018-0460-8},
abstract = {In this paper, we study the information system verification problem as a parameterized verification one. Informations systems are modeled as multi-parameterized systems in a formal language based on the Algebraic State-Transition Diagrams (ASTD) notation. Then, we use the Well Structured Transition Systems (WSTS) theory to solve the coverability problem for an unbounded ASTD state space. Moreover, we define a new framework to prove the effective pred-basis condition of WSTSs, i.e. the computability of a base of predecessors for every states.}
}
@inproceedings{BLS-aiml18,
address = {Bern, Switzerland},
month = aug,
year = 2018,
publisher = {College Publications},
editor = {Guram Bezhanishvili and Giovanna D'Agostino and
George Metcalfe and Thomas Studer},
acronym = {{AiML}'18},
booktitle = {{P}roceedings of the 10th
{C}onference on {A}dvances in {M}odal {L}ogics
({AiML}'18)},
author = {Baelde, David and Lick, Anthony and Schmitz, Sylvain},
title = {A Hypersequent Calculus with Clusters for Linear Frames},
pages = {36-55},
url = {https://hal.inria.fr/hal-01756126},
abstract = {The logic Kt4.3 is the basic modal logic of linear frames. Along with its extensions, it is found at the core of linear-time temporal logics and logics on words. In this paper, we consider the problem of designing proof systems for these logics, in such a way that proof search yields decision procedures for validity with an optimal complexity---coNP in this case. In earlier work, Indrzejczak has proposed an ordered hypersequent calculus that is sound and complete for Kt4.3 but does not yield any decision procedure. We refine his approach, using a hypersequent structure that corresponds to weak rather than strict total orders, and using annotations that reflect the model-theoretic insights given by small models for Kt4.3. We obtain a sound and complete calculus with an associated coNP proof search algorithm. These results extend naturally to the cases of unbounded and dense frames, and to the complexity of the two-variable fragment of first-order logic over total orders.}
}
@inproceedings{DF-aiml18,
address = {Bern, Switzerland},
month = aug,
year = 2018,
publisher = {College Publications},
editor = {Guram Bezhanishvili and Giovanna D'Agostino and
George Metcalfe and Thomas Studer},
acronym = {{AiML}'18},
booktitle = {{P}roceedings of the 10th
{C}onference on {A}dvances in {M}odal {L}ogics
({AiML}'18)},
author = {Demri, St{\'e}phane and Fervari, Raul},
title = {On the complexity of modal separation logics},
pages = {179-198},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DF-aiml18.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DF-aiml18.pdf}
}
@phdthesis{Gilbert-phd2018,
author = {Gilbert, Fr{\'e}d{\'e}ric},
title = {{Extending higher-order logic with predicate subtyping}},
school = {Universit{\'e} Paris~7, Paris, France},
type = {Th{\`e}se de doctorat},
year = 2018,
month = apr,
pdf = {https://hal.inria.fr/hal-01673518/file/dissertation.pdf}
}
@techreport{Burel-hal18,
author = {Burel, Guillaume},
institution = {HAL Research Report},
number = {hal-01670476},
type = {Research Report},
title = {{Linking Focusing and Resolution with Selection}},
year = {2018},
month = apr,
url = {https://hal.inria.fr/hal-01670476},
pdf = {https://hal.inria.fr/hal-01670476/file/lipics.pdf},
abstract = {Focusing and selection are techniques that shrink the proof search space for respectively sequent calculi and resolution. To bring out a link between them, we generalize them both: we introduce a sequent calculus where each occurrence of an atom can have a positive or a negative polarity; and a resolution method where each literal, whatever its sign, can be selected in input clauses. We prove the equivalence between cut-free proofs in this sequent calculus and derivations of the empty clause in that resolution method. Such a generalization is not semi-complete in general, which allows us to consider complete instances that correspond to theories of any logical strength. We present three complete instances: first, our framework allows us to show that ordinary focusing corresponds to hyperresolution and semantic resolution; the second instance is deduction modulo theory and the related framework called superdeduction; and a new setting, not captured by any existing framework, extends deduction modulo theory with rewriting rules having several left-hand sides, which restricts even more the proof search space.}
}
@inproceedings{FNS-podc18,
address = {Egham, UK},
month = jul,
publisher = {ACM Press},
editor = {Keidar, Idit},
acronym = {{PODC}'18},
booktitle = {Proceedings of the {ACM} Symposium on Principles of Distributed Computing ({PODC}'18)},
author = {F{\"u}gger, Matthias and Nowak, {\relax Th}omas and Schwarz, Manfred},
title = {Tight Bounds for Asymptotic and Approximate Consensus},
pages = {325-334},
year = {2018},
doi = {10.1145/3212734.3212762},
url = {https://arxiv.org/abs/1705.02898},
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.
\par
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{Z-icomp18,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Zetzsche, Georg},
title = {The Emptiness Problem for Valence Automata over Graph Monoids},
year = {2018},
note = {To appear}
}
@article{LZ-tocs18,
publisher = {Springer},
journal = {Theory of Computing Systems},
author = {Lohrey, Markus and Zetzsche, Georg},
title = {Knapsack in Graph Groups},
volume = {62},
number = {1},
year = {2018},
month = jan,
pages = {192-246},
doi = {10.1007/s00224-017-9808-3}
}
@inproceedings{SGF-hscc18,
address = {Porto, Portugal},
month = apr,
publisher = {ACM Press},
editor = {Prandini, Maria and Deshmukh, Jyotirmoy V.},
acronym = {{HSCC}'18},
booktitle = {{P}roceedings of the 21st {ACM} {I}nternational {C}onference
on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
({HSCC}'18)},
author = {Saoud, Adnane and Girard, Antoine and Fribourg, Laurent},
title = {Contract based Design of Symbolic Controllers for Vehicle Platooning},
pages = {277-278},
year = {2018},
doi = {10.1145/3178126.3187001},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SGF-hscc18.pdf},
abstract = {In this work, we present an application of symbolic control and contract
based design techniques to vehicle platooning. We use a compositional approach based on continuous-time assume-guarantee contracts. Each vehicle in the platoon is assigned an assumeguarantee contract; and a controller is synthesized using symbolic control to enforce the satisfaction of this contract. The assumeguarantee framework makes it possible to deal with different types of vehicles and asynchronous controllers (i.e controllers with different
sampling periods). Numerical results illustrate the effectiveness of the approach.},
note = {Poster}
}
@article{B-jfp18,
publisher = {Cambridge University Press},
journal = {Journal of Functional Programming},
author = {Blanqui, Fr{\'e}d{\'e}ric},
title = {Size-based termination of higher-order rewriting},
volume = {28},
year = {2018},
month = apr,
doi = {10.1017/S0956796818000072},
pdf = {https://hal.inria.fr/hal-01424921/file/main.pdf},
url = {https://www.cambridge.org/core/journals/journal-of-functional-programming/article/sizebased-termination-of-higherorder-rewriting/2134D9160988448FA62DD693D337892D},
abstract = {We provide a general and modular criterion for the termination of simply typed \(\lambda\)-calculus extended with function symbols defined by user-defined rewrite rules. Following a work of Hughes, Pareto and Sabry for functions defined with a fixpoint operator and pattern matching, several criteria use typing rules for bounding the height of arguments in function calls. In this paper, we extend this approach to rewriting-based function definitions and more general user-defined notions of size.}
}
@article{AGK-lmcs18,
journal = {Logical Methods in Computer Science},
author = {Akshay, S. and Gastin, Paul and Krishna, Shankara Narayanan},
title = {Analyzing Timed Systems Using Tree Automata},
volume = {14},
number = {2},
pages = {1-35},
year = {2018},
month = may,
doi = {10.23638/LMCS-14(2:8)2018},
pdf = {https://lmcs.episciences.org/4489/pdf},
url = {https://lmcs.episciences.org/4489},
abstract = {Timed systems, such as timed automata, are usually analyzed using their operational semantics on timed words. The classical region abstraction for timed automata reduces them to (untimed) finite state automata with the same time-abstract properties, such as state reachability. We propose a new technique to analyze such timed systems using finite tree automata instead of finite word automata. The main idea is to consider timed behaviors as graphs with matching edges capturing timing constraints. When a family of graphs has bounded tree-width, they can be interpreted in trees and MSO-definable properties of such graphs can be checked using tree automata. The technique is quite general and applies to many timed systems. In this paper, as an example, we develop the technique on timed pushdown systems, which have recently received considerable attention. Further, we also demonstrate how we can use it on timed automata and timed multi-stack pushdown systems (with boundedness restrictions).}
}
@inproceedings{BBFLMR-fm18,
address = {Oxford, UK},
month = jul,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Roscoe, {Bill W.} and Peleska, Jan},
acronym = {{FM}'18},
booktitle = {{P}roceedings of the 22nd {I}nternational {S}ymposium on {F}ormal
{M}ethods ({FM}'18)},
author = {Bacci, Giovanni and Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim G. and Markey, Nicolas and Reynier, Pierre-Alain},
title = {Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty},
pages = {203-221},
year = {2018},
doi = {10.1007/978-3-319-95582-7_12},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBFLMR-fm18.pdf},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBFLMR-fm18.pdf},
note = {Best paper award},
abstract = {In this paper, we propose a novel framework for the synthesis of robust and optimal energy-aware controllers. The framework is based on energy timed automata, allowing for easy expression of timing-constraints and variable energy-rates. We prove decidability of the energy-constrained infinite-run problem in settings with both certainty and uncertainty of the energy-rates. We also consider the optimization problem of identifying the minimal upper bound that will permit existence of energy-constrained infinite runs. Our algorithms are based on quantifier elimination for linear real arithmetic. Using Mathematica and Mjollnir, we illustrate our framework through a real industrial example of a hydraulic oil pump. Compared with previous approaches our method is completely automated and provides improved results.}
}
@article{BBBC-jlamp18,
publisher = {Elsevier Science Publishers},
journal = {Journal of Logic and Algebraic Methods in Programming},
author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye, Thomas and Carlier, Pierre},
title = {When are Stochastic Transition Systems Tameable?},
volume = {99},
pages = {41-96},
year = {2018},
month = oct,
doi = {10.1016/j.jlamp.2018.03.004},
pdf = {https://arxiv.org/pdf/1703.04806.pdf},
url = {https://doi.org/10.1016/j.jlamp.2018.03.004},
abstract = {A decade ago, Abdulla, Ben Henda and Mayr introduced the elegant concept of decisiveness for denumerable Markov chains [1]. Roughly speaking, decisiveness allows one to lift most good properties from finite Markov chains to denumerable ones, and therefore to adapt existing verification algorithms to infinite-state models. Decisive Markov chains however do not encompass stochastic real-time systems, and general stochastic transition systems (STSs for short) are needed. In this article, we provide a framework to perform both the qualitative and the quantitative analysis of STSs. First, we define various notions of decisiveness (inherited from [1]), notions of fairness and of attractors for STSs, and make explicit the relationships between them. Then, we define a notion of abstraction, together with natural concepts of soundness and completeness, and we give general transfer properties, which will be central to several verification algorithms on STSs. We further design a generic construction which will be useful for the analysis of ω-regular properties, when a finite attractor exists, either in the system (if it is denumerable), or in a sound denumerable abstraction of the system. We next provide algorithms for qualitative model-checking, and generic approximation procedures for quantitative model-checking. Finally, we instantiate our framework with stochastic timed automata (STA), generalized semi-Markov processes (GSMPs) and stochastic time Petri nets (STPNs), three models combining dense-time and probabilities. This allows us to derive decidability and approximability results for the verification of these models. Some of these results were known from the literature, but our generic approach permits to view them in a unified framework, and to obtain them with less effort. We also derive interesting new approximability results for STA, GSMPs and STPNs.}
}
@inproceedings{JKS-eurosp17,
address = {Paris, France},
month = apr,
publisher = {{IEEE} Press},
editor = {Andrei Sabelfeld and Matthew Smith},
acronym = {{EuroS\&P}'17},
booktitle = {{P}roceedings of the 2nd IEEE European Symposium on
Security and Privacy ({EuroS\&P}'17)},
author = {Jacomme, Charlie and Kremer, Steve and Scerri, Guillaume},
title = {Symbolic Models for Isolated Execution Environments},
pages = {530-545},
year = {2018},
doi = {10.1109/EuroSP.2017.16},
url = {https://ieeexplore.ieee.org/document/7962001/},
abstract = {Isolated Execution Environments (IEEs), such as ARM
TrustZone and Intel SGX, offer the possibility to
execute sensitive code in isolation from other
malicious programs, running on the same machine, or
a potentially corrupted OS. A key feature of IEEs is
the ability to produce reports binding
cryptographically a message to the program that
produced it, typically ensuring that this message is
the result of the given program running on an
IEE. We present a symbolic model for specifying and
verifying applications that make use of such
features. For this we introduce the S{\(\ell\)}APIC
process calculus, that allows to reason about
reports issued at given locations. We also provide
tool support, extending the SAPIC/TAMARIN toolchain
and demonstrate the applicability of our framework
on several examples implementing secure outsourced
computation (SOC), a secure licensing protocol and a
one-time password protocol that all rely on such
IEEs.}
}
@inproceedings{JK-csf18,
address = {Oxford, UK},
month = jul,
publisher = {{IEEE} Computer Society Press},
editor = {Chong, Steve and Delaune, St{\'e}phanie},
acronym = {{CSF}'18},
booktitle = {{P}roceedings of the
31st {IEEE} {C}omputer {S}ecurity {F}oundations
{S}ymposium ({CSF}'18)},
author = {Jacomme, Charlie and Kremer, Steve},
title = {An extensive formal analysis of multi-factor authentication protocols},
pages = {1-15},
year = {2018},
doi = {10.1109/CSF.2018.00008},
pdf = {https://easychair.org/publications/preprint/m89p},
url = {https://ieeexplore.ieee.org/document/8429292/},
abstract = {Passwords are still the most widespread means for authenticating users, even though they have been shown to create huge security problems. This motivated the use of additional authentication mechanisms used in so-called multi-factor authentication protocols. In this paper we define a detailed threat model for this kind of protocols: while in classical protocol analysis attackers control the communication network, we take into account that many communications are performed over TLS channels, that computers may be infected by different kinds of malwares, that attackers could perform phishing, and that humans may omit some actions. We formalize this model in the applied pi calculus and perform an extensive analysis and comparison of several widely used protocols - variants of Google 2-step and FIDO's U2F. The analysis is completely automated, generating systematically all combinations of threat scenarios for each of the protocols and using the ProVerif tool for automated protocol analysis. Our analysis highlights weaknesses and strengths of the different protocols, and allows us to suggest several small modifications of the existing protocols which are easy to implement, yet improve their security in several threat scenarios.}
}
@inproceedings{FMNNS-date18,
address = {Dresden, Germany},
month = mar,
publisher = {{IEEE} Computer Society Press},
acronym = {{DATE}'18},
booktitle = {{P}roceedings of the {C}onference on {D}esign, {A}utomation and {T}est in
{E}urope (DATE'18)},
author = {Matthias F{\"u}gger and
J{\"u}rgen Maier and
Robert Najvirt and
{\relax Th}omas Nowak and
Ulrich Schmid},
title = {A Faithful Binary Circuit Model with Adversarial Noise},
pages = {1327-1332},
year = {2018},
doi = {10.23919/DATE.2018.8342219},
pdf = {http://www.lsv.fr/~mfuegger/papers/FMNNS18_date.pdf},
url = {https://doi.org/10.23919/DATE.2018.8342219},
abstract = {Accurate delay models are important for static and dynamic timing analysis of digital circuits, and mandatory for formal verification. However, F{\"u}gger et al. [IEEE TC 2016] proved that pure and inertial delays, which are employed for dynamic timing analysis in state-of-the-art tools like ModelSim, NC-Sim and VCS, do not yield faithful digital circuit models. Involution delays, which are based on delay functions that are mathematical involutions depending on the previous-output-to- input time offset, were introduced by F{\"u}gger et al. [DATE'15] as a faithful alternative (that can easily be used with existing tools). Although involution delays were shown to predict real signal traces reasonably accurately, any model with a deterministic delay function is naturally limited in its modeling power.
\par
In this paper, we thus extend the involution model, by adding non-deterministic delay variations (random or even adversarial), and prove analytically that faithfulness is not impaired by this generalization. Albeit the amount of non-determinism must be considerably restricted to ensure this property, the result is surprising: the involution model differs from non-faithful models mainly in handling fast glitch trains, where small delay shifts have large effects. This originally suggested that adding even small variations should break the faithfulness of the model, which turned out not to be the case. Moreover, the results of our simulations also confirm that this generalized involution model has larger modeling power and, hence, applicability.}
}
@article{FFL-toc18,
publisher = {{IEEE} Computer Society Press},
journal = {IEEE Transactions on Computers},
author = {Stephan Friedrichs and Matthias F{\"u}gger and Christoph Lenzen},
title = {Metastability-Containing Circuits},
volume = {67},
number = {8},
pages = {1167-1183},
year = {2018},
month = aug,
doi = {10.1109/TC.2018.2808185},
url = {https://ieeexplore.ieee.org/document/8314764/},
abstract = {In digital circuits, metastability can cause deteriorated signals that neither are logical 0 nor logical 1, breaking the abstraction of Boolean logic. Synchronizers, the only traditional countermeasure, exponentially decrease the odds of maintained metastability over time. We propose a fundamentally different approach: It is possible to deterministically contain metastability by fine-grained logical masking so that it cannot infect the entire circuit. At the heart of our approach lies a time- and value-discrete model for metastability in synchronous clocked digital circuits, in which metastability is propagated in a worst-case fashion. The proposed model permits positive results and passes the test of reproducing Marino's impossibility results. We fully classify which functions can be computed by circuits with standard registers. Regarding masking registers, we show that more functions become computable with each clock cycle, and that masking registers permit exponentially smaller circuits for some tasks. Demonstrating the applicability of our approach, we present the first fault-tolerant distributed clock synchronization algorithm that deterministically guarantees correct behavior in the presence of metastability. As a consequence, clock domains can be synchronized without using synchronizers, enabling metastability-free communication between them.}
}
@inproceedings{FKLW-async18,
address = {Vienna, Austria},
month = may,
publisher = {{IEEE} Computer Society},
editor = {Krstic, Milos and Jones, {Ian W.}},
acronym = {{ASYNC}'18},
booktitle = {{P}roceedings of the 24th {IEEE} {I}nternational {S}ymposium on {A}synchronous {C}ircuits and {S}ystems ({ASYNC}'18)},
author = {Matthias F{\"u}gger and Attila Kinali and Christoph Lenzen and Ben Wiederhake},
title = {Fast All-Digital Clock Frequency Adaptation Circuit for Voltage Droop Tolerance},
pages = {68-77},
year = {2018},
doi = {10.1109/ASYNC.2018.00025},
url = {https://hal.inria.fr/hal-01936403},
abstract = {Naive handling of supply voltage droops in synchronous circuits results in conservative bounds on clock speeds, resulting in poor performance even if droops are rare. Adaptive strategies detect such potentially hazardous events and either initiate a rollback to a previous state or proactively reduce clock speed in order to prevent timing violations. The performance of such solutions critically depends on a very fast response to droops. However, state-of-the-art solutions incur synchronization delay to avoid that the clock signal is affected by metastability. Addressing the challenges discussed by Keith Bowman in his ASYNC 2017 keynote talk, we present an all-digital circuit that can respond to droops within a fraction of a clock cycle. This is achieved by delaying clock signals based on measurement values while they undergo synchronization simultaneously. We verify our solution by formally proving correctness, complemented by VHDL and Spice simulations of a 65 nm ASIC design confirming the theoretically obtained results.}
}
@article{BVdB-ijfcs18,
publisher = {World Scientific},
journal = {International Journal of Foundations of Computer Science},
author = {Berwanger, Dietmar and {van den Bogaard}, Marie},
title = {Consensus Game Acceptors and Iterated Transductions},
volume = {29},
number = {02},
pages = {165-185},
year = {2018},
month = feb,
doi = {10.1142/S0129054118400026},
url = {https://www.worldscientific.com/doi/abs/10.1142/S0129054118400026},
abstract = {We study a game for recognising formal languages, in which two players with imperfect information should coordinate on a common decision, given private input words correlated by a finite graph. The players have a common objective to avoid an inadmissible decision, in spite of the uncertainty induced by the input.
We show that the acceptor model based on consensus games characterises context-sensitive languages. Further, we describe the expressiveness of these games in terms of iterated synchronous transductions and identify a subclass that characterises context-free languages.},
pdf = {http://www.lsv.fr/~dwb/consensus.pdf}
}
@inproceedings{DGK-lics18,
address = {Oxford, UK},
publisher = {ACM Press},
editor = {Hofmann, Martin and Dawar, Anuj and Gr{\"a}del, Erich},
acronym = {{LICS}'18},
booktitle = {{P}roceedings of the 33rd {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'18)},
author = {Dave, Vrunda and Gastin, Paul and Krishna, Shankara Narayanan},
month = jul,
title = {{Regular Transducer Expressions for Regular Transformations}},
year = {2018},
url = {https://arxiv.org/abs/1802.02094},
pdf = {https://arxiv.org/pdf/1802.02094.pdf},
pages = {315-324},
doi = {10.1145/3209108.3209182},
abstract = {Functional MSO transductions, deterministic two-way transducers, as well as streaming string transducers are all equivalent models for regular functions. In this paper, we show that every regular function, either on finite words or on infinite words, captured by a deterministic two-way transducer, can be described with a regular transducer expression (RTE). For infinite words, the transducer uses Muller acceptance and \(\omega\)-regular look-ahead. RTEs are constructed from constant functions using the combinators if-then-else (deterministic choice), Hadamard product, and unambiguous versions of the Cauchy product, the 2-chained Kleene-iteration and the 2-chained omega-iteration. Our proof works for transformations of both finite and infinite words, extending the result on finite words of Alur et al. in LICS'14. In order to construct an RTE associated with a deterministic two-way Muller transducer with look-ahead, we introduce the notion of transition monoid for such two-way transducers where the look-ahead is captured by some backward deterministic Büchi automaton. Then, we use an unambiguous version of Imre Simon's famous forest factorization theorem in order to derive a ''good'' (\(\omega\)-)regular expression for the domain of the two-way transducer. ''Good'' expressions are unambiguous and Kleene-plus as well as \(\omega\)-iterations are only used on subexpressions corresponding to idempotent elements of the transition monoid. The combinator expressions are finally constructed by structural induction on the ''Good'' (\(\omega\)-)regular expression describing the domain of the transducer.}
}
@inproceedings{JMS-wodes18,
address = {Sorrento Coast, Italy},
month = may # {-} # jun,
year = 2018,
volume = {51(7)},
series = {IFAC-PapersOnLine},
publisher = {Elsevier Science Publishers},
editor = {Chris Hadjicostis and Jan Komenda},
acronym = {{WODES}'18},
booktitle = {{P}roceedings of the 14th {W}orkshop on {D}iscrete {E}vent {S}ystems
({WODES}'18)},
author = {Lo{\"i}g Jezequel and Agnes Madalinski and Stefan Schwoon},
title = {{Distributed computation of vector clocks in Petri nets unfolding for test selection}},
pages = {106-111},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JMS-wodes18.pdf},
abstract = {It has been shown that annotating Petri net unfoldings with time stamps allows for
building distributed testers for distributed systems. However, the construction of the annotated
unfolding of a distributed system currently remains a centralized task. In this paper we extend
a distributed unfolding technique in order to annotate the resulting unfolding with time stamps.
This allows for distributed construction of distributed testers for distributed systems.}
}
@article{BHSS-fi18,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {B{\'e}atrice B{\'e}rard and Stefan Haar and Sylvain Schmitz and Stefan Schwoon},
title = {{The Complexity of Diagnosability and Opacity Verification for Petri Nets}},
volume = 161,
number = 4,
year = 2018,
pages = {317-349},
doi = {10.3233/FI-2018-1706},
url = {https://hal.inria.fr/hal-01852119},
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.
\par
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.
\par
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 convergent 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.}
}
@inproceedings{CGR-automata18,
address = {Ghent, Belgium},
month = jun,
year = 2018,
volume = 10875,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Jan Baetens and Martin Kutrib},
acronym = {{AUTOMATA}'18},
booktitle = {{P}roceedings of the 24th Annual International Workshop on Cellular Automata and Discrete Complex Systems ({AUTOMATA}'18)},
author = {Carton, Olivier and Guillon, Bruno and Reiter, Fabian},
title = {{Counter Machines and Distributed Automata}},
pages = {13-28},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CGR-automata18.pdf},
doi = {10.1007/978-3-319-92675-9\_2},
abstract = {We prove the equivalence of two classes of counter machines and one class of distributed automata. Our counter machines operate on finite words, which they read from left to right while incrementing or decrementing a fixed number of counters. The two classes differ in the extra features they offer: one allows to copy counter values, whereas the other allows to compute copyless sums of counters. Our distributed automata, on the other hand, operate on directed path graphs that represent words. All nodes of a path synchronously execute the same finite-state machine, whose state diagram must be acyclic except for self-loops, and each node receives as input the state of its direct predecessor. These devices form a subclass of linear-time one-way cellular automata.}
}
@inproceedings{CHP-automata18,
address = {Ghent, Belgium},
month = jun,
year = 2018,
volume = 10875,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Jan Baetens and Martin Kutrib},
acronym = {{AUTOMATA}'18},
booktitle = {{P}roceedings of the 24th Annual International Workshop on Cellular Automata and Discrete Complex Systems ({AUTOMATA}'18)},
author = {Chatain, {\relax Th}omas and Haar, Stefan and Paulev{\'e}, Lo{\"i}c},
title = {{Boolean Networks: Beyond Generalized Asynchronicity}},
pages = {29-42},
url = {https://hal.inria.fr/hal-01768359v2},
doi = {10.1007/978-3-319-92675-9\_3},
abstract = {Boolean networks are commonly used in systems biology to model dynamics of biochemical networks by abstracting away many (and often unknown) parameters related to speed and species activity thresholds. It is then expected that Boolean networks produce an over-approximation of behaviours (reachable configurations), and that subsequent refinements would only prune some impossible transitions. However, we show that even generalized asynchronous updating of Boolean networks, which subsumes the usual updating modes including synchronous and fully asynchronous, does not capture all transitions doable in a multi-valued or timed refinement. We define a structural model transformation which takes a Boolean network as input and outputs a new Boolean network whose asynchronous updating simulates both synchronous and asynchronous updating of the original network, and exhibits even more behaviours than the generalized asynchronous updating. We argue that these new behaviours should not be ignored when analyzing Boolean networks, unless some knowledge about the characteristics of the system explicitly allows one to restrict its behaviour.}
}
@inproceedings{LGS-atpn18,
address = {Bratislava, Slovakia},
month = jun,
year = 2018,
volume = {10877},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Victor Khomenko and {Olivier H.} Roux},
acronym = {{PETRI~NETS}'18},
booktitle = {{P}roceedings of the 39th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'18)},
author = {Engel Lefaucheux and Alessandro Giua and Carla Seatzu},
title = {{Basis Coverability Graph for Partially Observable Petri Nets with Application to Diagnosability Analysis}},
pages = {164-183},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LGS-atpn18.pdf},
abstract = {Petri nets have been proposed as a fundamental model for
discrete-event systems in a wide variety of applications and have been
an asset to reduce the computational complexity involved in solving a
series of problems, such as control, state estimation, fault diagnosis, etc.
Many of those problems require an analysis of the reachability graph
of the Petri net. The basis reachability graph is a condensed version of
the reachability graph that was introduced to efficiently solve problems
linked to partial observation. It was in particular used for diagnosis which
consists in deciding whether some fault events occurred or not in the
system, given partial observations on the run of the system. However
this method is, with very specific exceptions, limited to bounded Petri
nets. In this paper, we introduce the notion of basis coverability graph
to remove this requirement. We then establish the relationship between
the coverability graph and the basis coverability graph. Finally, we focus
on the diagnosability problem: we show how the basis coverability graph
can be used to get an efficient algorithm.}
}
@inproceedings{BBDH-atpn18,
address = {Bratislava, Slovakia},
month = jun,
year = 2018,
volume = {10877},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Victor Khomenko and {Olivier H.} Roux},
acronym = {{PETRI~NETS}'18},
booktitle = {{P}roceedings of the 39th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'18)},
author = {Barbot, Beno{\^i}t and B{\'e}rard, B{\'e}atrice and Duplouy, Yann and Haddad, Serge},
title = {{Integrating Simulink Models into the Model Checker Cosmos}},
pages = {363-373},
url = {https://hal.archives-ouvertes.fr/hal-01725835/},
pdf = {https://hal.archives-ouvertes.fr/hal-01725835/document},
doi = {10.1007/978-3-319-91268-4_19},
abstract = {We present an implementation for Simulink model executions in the statistical model-checker Cosmos. We take profit of this implementation for an hybrid modeling combining Petri nets and Simulink models.}
}
@techreport{BBFHP-hal18,
author = {Barbot, Beno{\^i}t and Beccuti, Marco and Franceschinis, Giuliana and Haddad, Serge and Picaronny, Claudine},
institution = {HAL-Inria},
month = mar,
number = {hal-01726011},
type = {Research Report},
title = {Bounds Computation for Symmetric Nets},
year = {2018},
url = {https://hal.inria.fr/hal-01726011},
pdf = {https://hal.inria.fr/hal-01726011/file/main.pdf},
abstract = {Monotonicity in Markov chains is the starting point for quantitative abstraction of complex probabilistic systems leading to (upper or lower) bounds for probabilities and mean values relevant to their analysis. While numerous case studies exist in the literature, there is no generic model for which monotonicity is directly derived from its structure. Here we propose such a model and formalize it as a subclass of Stochastic Symmetric (Petri) Nets (SSNs) called Stochastic Monotonic SNs (SMSNs). On this subclass the monotonicity is proven by coupling arguments that can be applied on an abstract description of the state (symbolic marking). Our class includes both process synchronizations and resource sharings and can be extended to model open or cyclic closed systems. Automatic methods for transforming a non monotonic system into a monotonic one matching the MSN pattern, or for transforming a monotonic system with large state space into one with reduced state space are presented. We illustrate the interest of the proposed method by expressing standard monotonic models and modelling a flexible manufacturing system case study.}
}
@article{GM-softc18,
publisher = {Springer},
journal = {Soft Computing},
author = {Gastin, Paul and Monmege, Benjamin},
title = {{A unifying survey on weighted logics and weighted automata}},
volume = {22},
number = {4},
year = {2018},
month = feb,
pages = {1047-1065},
doi = {10.1007/s00500-015-1952-6},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/softc2016-GM.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/softc2016-GM.pdf},
abstract = {Logical formalisms equivalent to weighted automata have been the topic of numerous research papers in the recent years. It started with the seminal result by Droste and Gastin on weighted logics over semirings for words. It has been extended in two dimensions by many authors. First, the weight domain has been extended to valuation monoids, valuation structures, etc. to capture more quantitative properties. Along another dimension, different structures such as ranked or unranked trees, nested words, Mazurkiewicz traces, etc. have been considered. The long and involved proofs of equivalences in all these papers are implicitly based on the same core arguments. This article provides a meta-theorem which unifies these different approaches. Towards this, we first revisit weighted automata by defining a new semantics for them in two phases---an abstract semantics based on multisets of weight structures (independent of particular weight domains) followed by a concrete semantics. Then, we introduce a core weighted logic with a minimal number of features and a simplified syntax, and lift the new semantics to this logic. We show at the level of the abstract semantics that weighted automata and core weighted logic have the same expressive power. Finally, we show how previous results can be recovered from our result by logical reasoning. In this paper, we prove the meta-theorem for words, ranked and unranked trees, showing the robustness of our approach.}
}
@inproceedings{LFV-adhs18,
address = {Oxford, UK},
month = jul,
year = 2018,
number = 16,
volume = 51,
series = {IFAC-PapersOnLine},
publisher = {Elsevier Science Publishers},
editor = {Alessandro Abate and Antoine Girard and Maurice Heemels},
acronym = {{ADHS}'18},
booktitle = {{P}roceedings of the 6th {IFAC} {C}onference on {A}nalysis and
{D}esign of {H}ybrid {S}ystems ({ADHS}'18)},
author = {Adrien Le{ }Co{\"e}nt and Laurent Fribourg and Jonathan Vacher},
title = {Control Synthesis for Stochastic Switched Systems using the Tamed Euler Method},
pages = {259-264},
url = {https://doi.org/10.1016/j.ifacol.2018.08.044},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LFV-adhs18.pdf},
doi = {10.1016/j.ifacol.2018.08.044},
abstract = {In this paper, we explain how, under the one-sided Lipschitz (OSL) hypothesis, one can find an error bound for a variant of the Euler-Maruyama approximation method for stochastic switched systems. We then explain how this bound can be used to control stochastic switched switched system in order to stabilize them in a given region. The method is illustrated on several examples of the literature.}
}
@inproceedings{SGF-ecc18,
address = {Limassol, Cyprus},
month = jun,
year = 2018,
publisher = {{IEEE} Press},
editor = {Thomas Parisini},
acronym = {{ECC}'18},
booktitle = {{P}roceedings of the European Control Conference ({ECC}'18)},
author = {Adnane Saoud and Antoine Girard and Laurent Fribourg},
title = {On the Composition of Discrete and Continuous-time Assume-Guarantee Contracts for Invariance},
pages = {435-440},
url = {https://ieeexplore.ieee.org/document/8550622},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SGF-ecc18.pdf},
doi = {10.23919/ECC.2018.8550622},
abstract = {Many techniques for verifying invariance prop- erties are limited to systems of moderate size. In this paper, we propose an approach based on assume-guarantee contracts and compositional reasoning for verifying invariance properties of a broad class of discrete-time and continuous-time systems consisting of interconnected components. The notion of assume- guarantee contracts makes it possible to divide responsibil- ities among the system components: a contract specifies an invariance property that a component must fulfill under some assumptions on the behavior of its environment (i.e. of the other components). We define weak and strong semantics of assume- guarantee contracts for both discrete-time and continuous-time systems. We then establish a certain number of results for compositional reasoning, which allow us to show that a global invariance property of the whole system is satisfied when all components satisfy their own contract. Interestingly, we show that the weak satisfaction of the contract is sufficient to deal with cascade compositions, while strong satisfaction is needed to reason about feedback composition. Specific results for systems described by differential inclusions are then developed. Throughout the paper, the main results are illustrated using simple examples.}
}
@article{LFMDC-tcs18,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Adrien Le{ }Co{\"e}nt and
Laurent Fribourg and
Nicolas Markey and
Florian De{ }Vuyst and
Ludovic Chamoin},
title = {Compositional synthesis of state-dependent switching control},
volume = {750},
year = {2018},
pages = {53-68},
doi = {10.1016/j.tcs.2018.01.021},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LFMDC-tcs18.pdf},
url = {https://doi.org/10.1016/j.tcs.2018.01.021},
abstract = {We present a correct-by-design method of state-dependent control synthesis for sampled switching systems. Given a target region R of the state space, our method builds a capture set S and a control that steers any element of S into R. The method works by iterated backward reachability from R. The method is also used to synthesize a recurrence control that makes any state of R return to R infinitely often. We explain how the synthesis method can be performed in a compositional manner, and apply it to the synthesis of a compositional control of a concrete floor-heating system with 11 rooms and up to 2^11=2048 toswitching modes.}
}
@article{LACF-fmsd18,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Adrien Le{ }Co{\"{e}}nt and
Julien {Alexandre dit Sandretto} and
Alexandre Chapoutot and
Laurent Fribourg},
title = {An improved algorithm for the control synthesis of nonlinear sampled switched systems},
volume = {53},
number = {3},
year = {2018},
pages = {363-383},
doi = {10.1007/s10703-017-0305-8},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LACF-fmsd18.pdf},
url = {https://link.springer.com/article/10.1007/s10703-017-0305-8},
abstract = {A novel algorithm for the control synthesis for nonlinear switched systems is presented in this paper. Based on an existing procedure of state-space bisection and made available for nonlinear systems with the help of guaranteed integration, the algorithm has been improved to be able to consider longer patterns of modes with a better pruning approach. Moreover, the use of guaranteed integration also permits to take bounded perturbations and varying parameters into account. It is particularly interesting for safety critical applications, such as in aeronautical, military or medical fields. The whole approach is entirely guaranteed and the induced controllers are correct-by-design. Some experimentations are performed to show the important gain of the new algorithm.}
}
@article{ABDL-tcs18,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Alechina, Natasha and Bulling, Nils and Demri,
St{\'e}phane and Logan, Brian},
title = {On the Complexity of Resource-Bounded Logics},
volume = {750},
year = {2018},
pages = {69--100},
doi = {10.1016/j.tcs.2018.01.019},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABDL-tcs18.pdf}
}
@article{HGJX-lmcs18,
journal = {Logical Methods in Computer Science},
author = {Ho, Weng Kin and Goubault-Larrecq, Jean and Jung, Achim and Xi, Xiaoyong},
title = {{The Ho-Zhao Problem}},
volume = {14},
number = {1},
year = {2018},
month = jan,
pages = {1-19},
doi = {10.23638/LMCS-14(1:7)2018},
url = {https://lmcs.episciences.org/4218},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HGJX-lmcs18.pdf}
}
@article{H-ipl18,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Haddad, Serge},
title = {{Memoryless determinacy of finite parity games: Another simple proof}},
volume = {132},
pages = {19-21},
month = apr,
year = {2018},
pdf = {https://hal.inria.fr/hal-01541508/document},
doi = {10.1016/j.ipl.2017.11.012},
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ö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 Grädel [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].}
}
@inproceedings{CCDJR-lata18,
address = {Bar-Ilan, Israel},
month = apr,
year = 2018,
volume = {10792},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Mart{\'\i}n-Vide, Carlos},
acronym = {{LATA}'18},
booktitle = {{P}roceedings of the 12th {I}nternational {C}onference on {L}anguage
and {A}utomata {T}heory and {A}pplications ({LATA}'18)},
author = {Chatain, {\relax Th}omas and Comlan, Maurice and Delfieu, David and Jezequel, Lo{\"i}g and Roux, Olivier H.},
title = {Pomsets and Unfolding of Reset Petri Nets},
pages = {258-270},
url = {https://doi.org/10.1007/978-3-319-77313-1_20},
doi = {10.1007/978-3-319-77313-1_20},
abstract = {Reset Petri nets are a particular class of Petri nets where transition firings can remove all tokens from a place without checking if this place actually holds tokens or not. In this paper we look at partial order semantics of such nets. In particular, we propose a pomset bisimulation for comparing their concurrent behaviours. Building on this pomset bisimulation we then propose a generalization of the standard finite complete prefixes of unfolding to the class of safe reset Petri nets.}
}
@inproceedings{DLM-fossacs18,
address = {Thessaloniki, Greece},
month = apr,
year = 2018,
volume = {10803},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baier, Christel and {Dal Lago}, Ugo},
acronym = {{FoSSaCS}'18},
booktitle = {{P}roceedings of the 21st {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'18)},
author = {St{\'e}phane Demri and {\'E}tienne Lozes and Alessio Mansutti},
title = {The Effects of Adding Reachability Predicates in Propositional Separation Logic},
pages = {476-493},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DLM-fossacs18.pdf}
}
@inproceedings{B-fossacs18,
address = {Thessaloniki, Greece},
month = apr,
year = 2018,
volume = {10803},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baier, Christel and {Dal Lago}, Ugo},
acronym = {{FoSSaCS}'18},
booktitle = {{P}roceedings of the 21st {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'18)},
author = {Bouyer, Patricia},
title = {Games on graphs with a public signal monitoring},
pages = {530-547},
url = {https://arxiv.org/abs/1710.07163},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/B-fossacs18.pdf},
doi = {10.1007/978-3-319-89366-2_29},
abstract = {We study Nash equilibria in games on graphs with an imperfect monitoring based on a public signal. In such games, deviations and players responsible for those deviations can be hard to detect and track. We propose a generic epistemic game abstraction, which conveniently allows to represent the knowledge of the players about these deviations, and give a characterization of Nash equilibria in terms of winning strategies in the abstraction. We then use the abstraction to develop algorithms for some payoff functions.}
}
This file was generated by bibtex2html 1.98.