@inproceedings{FFLRS-fsfma14,
address = {Singapore},
month = may,
year = 2014,
volume = 156,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Lin, Shang{-}Wei and Petrucci, Laure},
acronym = {{FSFMA}'14},
booktitle = {{P}roceedings of the 2nd {F}rench-{S}ingaporean {W}orkshop
on {F}ormal {M}ethods and {A}pplications ({FSFMA}'14)},
author = {Feld, Gilles and Fribourg, Laurent and Labrousse, Denis and
Revol, Bertrand and Soulat, Romain},
title = {Correct-by-design Control Synthesis for Multilevel
Converters using State Space Decomposition},
pages = {5-16},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FFLRS-fsfma14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FFLRS-fsfma14.pdf},
doi = {10.4204/EPTCS.156.5},
abstract = {High-power converters based on elementary switching cells are
more and more used in the industry of power electronics owing to various
advantages such as lower voltage stress and reduced power loss. However,
the complexity of controlling such converters is a major challenge that
the power manufacturing industry has to face with. The synthesis of
industrial switching controllers relies today on heuristic rules and
empiric simulation. The state of the system is not guaranteed to stay
within the limits that are admissible for its correct electrical behavior.
We show here how to apply a formal method in order to synthesize a
correct-by-design control that guarantees that the power converter will
always stay within a predefined safe zone of variations for its input
parameters. The method is applied in order to synthesize a
correct-by-design control for 5-level and 7-level power converters with a
flying capacitor topology. We check the validity of our approach by
numerical simulations for 5 and 7 levels. We also perform physical
experimentations using a prototype built by SATIE laboratory for 5
levels}
}
@misc{cassting-D24,
author = {Markey, Nicolas and Chaturvedi, Namit and Geeraerts, Gilles
and Srba, Ji{\v{r}}{\'\i}},
title = {Efficient strategy synthesis for complex objectives},
howpublished = {Cassting deliverable~D2.4 (FP7-ICT-601148)},
month = oct,
year = {2014},
note = {20~pages},
type = {Contract Report},
url = {http://www.cassting-project.eu/wp-content/uploads/2014/10/deliv-24.pdf},
pdf = {http://www.cassting-project.eu/wp-content/uploads/2014/10/deliv-24.pdf}
}
@inproceedings{JLMX-mfps30,
address = {Ithaca, New~York, USA},
month = jun,
year = 2014,
volume = 308,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Jacobs, Bart and Silva, Alexandra and Staton, Sam},
acronym = {{MFPS}'14},
booktitle = {{P}roceedings of the 30th {C}onference on
{M}athematical {F}oundations of {P}rogramming
{S}emantics ({MFPS}'14)},
author = {Jaziri, Samy and Larsen, Kim G. and Mardare, Radu and Xue, Bingtian},
title = {Adequacy and Complete Axiomatization for Timed Modal Logic},
pages = {183-210},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/JLMX-mfps14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JLMX-mfps14.pdf},
doi = {10.1016/j.entcs.2014.10.011},
abstract = {In this paper we develop the metatheory for Timed Modal
Logic~(TML), which is the modal logic used for the analysis of timed
transition systems~(TTSs). We solve a series of long-standing open
problems related to~TML. Firstly, we prove that TML enjoys the
Hennessy-Milner property and solve one of the open questions in the field.
Secondly, we prove that the set of validities are not recursively
enumerable. Nevertheless, we develop a strongly-complete proof system
for~TML. Since the logic is not compact, the proof system contains
infinitary rules, but only with countable sets of instances. Thus, we~can
involve topological results regarding Stone spaces, such as the
Rasiowa-Sikorski lemma, to complete the proofs.}
}
@article{CDGH-ic15,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Chatterjee, Krishnendu and Doyen, Laurent and Gimbert, Hugo
and Henzinger, Thomas A.},
title = {Randomness for free},
volume = {245},
month = dec,
year = 2015,
pages = {3-16},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDGH-ic15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDGH-ic15.pdf},
doi = {10.1016/j.ic.2015.06.003},
abstract = {We consider two-player zero-sum games on finite-state graphs.
These games can be classified on the basis of the information of the
players and on the mode of interaction between them. On the basis of
information the classification is as follows: (a)~partial-observation
(both players have partial view of the game); (b)~one-sided
complete-observation (one player has complete observation); and
(c)~complete-observation (both players have complete view of the game).
On~the basis of mode of interaction we have the following classification:
(a)~concurrent (players interact simultaneously); and (b)~turn-based
(players interact in turn). The~two sources of randomness in these games
are randomness in the transition function and randomness in the
strategies. In general, randomized strategies are more powerful than
deterministic strategies, and probabilistic transitions give more general
classes of games. We present a complete characterization for the classes
of games where randomness is not helpful~in: (a)~the transition function
(probabilistic transitions can be simulated by deterministic transitions);
and (b)~strategies (pure strategies are as powerful as randomized
strategies). As~a consequence of our characterization we obtain new
undecidability results for these games.}
}
@article{LM-ic14,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas},
title = {Augmenting {ATL} with strategy contexts},
volume = {245},
month = dec,
year = 2015,
pages = {98-123},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2014-05.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2014-05.pdf},
doi = {10.1016/j.ic.2014.12.020},
abstract = {We study the extension of the alternating-time temporal logic
(ATL) with strategy contexts: contrary to the original semantics, in this
semantics the strategy quantifiers do not reset the previously selected
strategies.\par
We show that our extension ATLsc is very expressive, but that its decision
problems are quite hard: model checking is \(k\)-EXPTIME-complete when the
formula has k nested strategy quantifiers; satisfiability is undecidable,
but we prove that it is decidable when restricting to turn-based games.
Our algorithms are obtained through a very convenient translation to QCTL
(the~computation-tree logic CTL extended with atomic quantification),
which we show also applies to Strategy Logic, as well as when strategy
quantification ranges over memoryless strategies.}
}
@inproceedings{DJLMS-fsttcs14,
address = {New~Dehli, India},
month = dec,
year = 2014,
volume = {29},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Raman, Venkatesh and Suresh, S.~P.},
acronym = {{FSTTCS}'14},
booktitle = {{P}roceedings of the 34th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'14)},
author = {Doyen, Laurent and Juhl, Line and Larsen, Kim G. and
Markey, Nicolas and Shirmohammadi, Mahsa},
title = {Synchronizing words for weighted and timed automata},
pages = {121-132},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DJLMS-fsttcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DJLMS-fsttcs14.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2014.121},
abstract = {The problem of synchronizing automata is concerned with the
existence of a word that sends all states of the automaton to one and the
same state. This problem has classically been studied for complete
deterministic finite automata, with the existence problem being
NLOGSPACE-complete.\par
In this paper we consider synchronizing-word problems for weighted and
timed automata. We consider the synchronization problem in several
variants and combinations of these, including deterministic and
non-deterministic timed and weighted automata, synchronization to unique
location with possibly different clock valuations or accumulated weights,
as well as synchronization with a safety condition forbidding the
automaton to visit states outside a safety-set during synchronization
(e.g. energy constraints). For deterministic weighted automata, the
synchronization problem is proven PSPACE-complete under energy
constraints, and in 3-EXPSPACE under general safety constraints. For timed
automata the synchronization problems are shown to be PSPACE-complete in
the deterministic case, and undecidable in the non-deterministic case.}
}
@inproceedings{BMS-fsttcs14,
address = {New~Dehli, India},
month = dec,
year = 2014,
volume = {29},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Raman, Venkatesh and Suresh, S.~P.},
acronym = {{FSTTCS}'14},
booktitle = {{P}roceedings of the 34th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'14)},
author = {Bouyer, Patricia and Markey, Nicolas and Stan, Daniel},
title = {Mixed {N}ash Equilibria in Concurrent Games},
pages = {351-363},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-fsttcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-fsttcs14.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2014.351},
abstract = {We study mixed-strategy Nash equilibria in multiplayer
deterministic concurrent games played on graphs, with terminal-reward
payoffs (that is, absorbing states with a value for each player). We show
undecidability of the existence of a constrained Nash equilibrium (the
constraint requiring that one player should have maximal payoff), with
only three players and 0/1-rewards (i.e., reachability objectives). This
has to be compared with the undecidability result by Ummels and Wojtczak
for turn-based games which requires 14 players and general rewards. Our
proof has various interesting consequences: (i)~the~undecidability of the
existence of a Nash equilibrium with a constraint on the social welfare;
(ii)~the~undecidability of the existence of an (unconstrained) Nash
equilibrium in concurrent games with terminal-reward payoffs.}
}
@article{BBBMBGJ-lmcs14,
journal = {Logical Methods in Computer Science},
author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye,
{\relax Th}omas and Menet, Quentin and Baier, Christel and
Gr{\"o}{\ss}er, Marcus and Jurdzi{\'n}ski, Marcin},
title = {Stochastic Timed Automata},
volume = 10,
number = {4:6},
nopages = {},
month = dec,
year = 2014,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBMBGJ-mfcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBMBGJ-mfcs14.pdf},
doi = {10.2168/LMCS-10(4:6)2014},
abstract = {A~stochastic timed automaton is a purely stochastic process
defined on a timed automaton, in which both delays and discrete choices
are made randomly. We study the almost-sure model-checking problem for
this model, that is, given a stochastic timed automaton~\(\mathcal{A}\)
and a property~\(\varphi\), we want to decide whether \(\mathcal{A}\)
satisfies~\(\varphi\) with probability~\(1\). In this paper, we identify
several classes of automata and of properties for which this can be
decided. The proof relies on the construction of a finite abstraction,
called the thick graph, that we interpret as a finite Markov chain, and
for which we can decide the almost-sure model-checking problem.
Correctness of the abstraction holds when automata are almost-surely fair,
which we show, is the case for two large classes of systems, single-clock
automata and so-called weak-reactive automata. Techniques employed in this
article gather tools from real-time verification and probabilistic
verification, as well as topological games played on timed automata.}
}
@article{BMS-tcs14,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan},
title = {Robust Reachability in Timed Automata and Games: A~Game-based Approach},
volume = 563,
year = {2015},
month = jan,
pages = {43-74},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-tcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-tcs14.pdf},
doi = {10.1016/j.tcs.2014.08.014 },
abstract = {Reachability checking is one of the most basic problems in
verification. By solving this problem in a game, one can synthesize a
strategy that dictates the actions to be performed for ensuring that the
target location is reached. In this work, we are interested in
synthesizing {"}robust{"} strategies for ensuring reachability of a location
in timed automata. By robust, we mean that it must still ensure
reachability even when the delays are perturbed by the environment. We
model this perturbed semantics as a game between the controller and its
environment, and solve the parameterized robust reachability problem: we
show that the existence of an upper bound on the perturbations under which
there is a strategy reaching a target location is EXPTIME-complete. We
also extend our algorithm, with the same complexity, to turn-based timed
games, where the successor state is entirely determined by the environment
in some locations.}
}
@article{FKS-fmsd14,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Fribourg, Laurent and K{\"u}hne, Ulrich and Soulat, Romain},
title = {Finite Controlled Invariants for Sampled Switched Systems},
year = 2014,
month = dec,
volume = 45,
number = 3,
pages = {303-329},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FKS-fmsd14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FKS-fmsd14.pdf},
doi = {10.1007/s10703-014-0211-2},
abstract = {We consider in this paper switched systems, a class of hybrid
systems recently used with success in various domains such as automotive
industry and power electronics. We propose a state-dependent control
strategy which makes the trajectories of the analyzed system converge to
finite cyclic sequences of points. Our method relies on a technique of
decomposition of the state space into local regions where the control is
uniform. We have implemented the procedure using zonotopes, and applied it
successfully to several examples of the literature and industrial case
studies in power electronics.}
}
@inproceedings{SLAF-syncop14,
address = {Grenoble, France},
volume = 145,
series = {Electronic Proceedings in Theoretical Computer Science},
month = apr,
year = 2014,
editor = {Andr{\'e}, {\'E}tienne and Frehse, Goran},
acronym = {{SYNCOP}'14},
booktitle = {{P}roceedings of the 1st {I}nternational {W}orkshop on {S}ynthesis
of {C}ontinuous {P}arameters ({SYNCOP}'14)},
author = {Sun, Youcheng and Lipari, Giuseppe and
Andr{\'e}, {\'E}tienne and Fribourg, Laurent},
title = {Toward Parametric Timed Interfaces for Real-Time Components},
pages = {49-64},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SLAF-syncop14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SLAF-syncop14.pdf},
doi = {10.4204/EPTCS.145.6},
abstract = {We propose here a framework to model real-time components
consisting of concurrent real-time tasks running on a single processor,
using parametric timed automata. Our framework is generic and modular, so
as to be easily adapted to different schedulers and more complex task
models. We first perform a parametric schedulability analysis of the
components using the inverse method. We show that the method unfortunately
does not provide satisfactory results when the task periods are considered
as parameters. After identifying and explaining the problem, we present a
solution adapting the model by making use of the worst-case scenario in
schedulability analysis. We show that the analysis with the inverse method
always converges on the modified model when the system load is strictly
less than~\(100\%\). Finally, we show how to use our parametric analysis for
the generation of timed interfaces in compositional system design.}
}
@inproceedings{BGM-atva14,
address = {Sydney, Australia},
month = nov,
year = {2014},
volume = 8837,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cassez, Franck and Raskin, Jean-Fran{\c{c}}ois},
acronym = {{ATVA}'14},
booktitle = {{P}roceedings of the 12th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'14)},
author = {Bouyer, Patricia and Gardy, Patrick and Markey, Nicolas},
title = {Quantitative verification of weighted {K}ripke structures},
pages = {64-80},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-atva14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-atva14.pdf},
doi = {10.1007/978-3-319-11936-6_6},
abstract = {Extending formal verification techniques to handle quantitative
aspects, both for the models and for the properties to be checked, has
become a central research topic over the last twenty years. Following
several recent works, we study model checking for (one-dimensional)
weighted Kripke structures with positive and negative weights, and
temporal logics constraining the total and/or average weight. We prove
decidability when only accumulated weight is constrained, while allowing
average-weight constraints alone already is undecidable.}
}
@inproceedings{MV-atva14,
address = {Sydney, Australia},
month = nov,
year = {2014},
volume = 8837,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cassez, Franck and Raskin, Jean-Fran{\c{c}}ois},
acronym = {{ATVA}'14},
booktitle = {{P}roceedings of the 12th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'14)},
author = {Markey, Nicolas and Vester, Steen},
title = {Symmetry Reduction in Infinite Games with Finite Branching},
pages = {281-296},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/MV-atva14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/MV-atva14.pdf},
doi = {10.1007/978-3-319-11936-6_21},
abstract = {Symmetry reductions have been applied extensively for the
verification of finite-state concurrent systems and hardware designs using
model-checking of temporal logics such as LTL, CTL and
CTL\textsuperscript{*}, as well as real-time and probabilistic-system
model-checking. In this paper we extend the technique to handle
infinite-state games on graphs with finite branching where the objectives
of the players can be very general. As particular applications, it is
shown that the technique can be applied to reduce the state space in
parity games as well as when doing model-checking of the temporal logic
ATL\textsuperscript{*}.}
}
@inproceedings{DMS-concur14,
address = {Rome, Italy},
month = sep,
year = 2014,
volume = 8704,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baldan, Paolo and Gorla, Daniele},
acronym = {{CONCUR}'14},
booktitle = {{P}roceedings of the 25th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'14)},
author = {Doyen, Laurent and Massart, {\relax Th}ierry and Shirmohammadi, Mahsa},
title = {Robust Synchronization in {M}arkov Decision Processes},
pages = {234-248},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DMS-concur14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DMS-concur14.pdf},
doi = {10.1007/978-3-662-44584-6_17},
abstract = {We consider synchronizing properties of Markov decision
processes (MDP), viewed as generators of sequences of probability
distributions over states. A~probability distribution is \(p\)-synchronizing
if the probability mass is at least~\(p\) in some state, and a sequence of
probability distributions is weakly \(p\)-synchronizing, or strongly
\(p\)-synchronizing if respectively infinitely many, or all but finitely many
distributions in the sequence are \(p\)-synchronizing.\par
For each synchronizing mode, an MDP can be \textit{(i)}~sure winning if
there is a strategy that produces a \(1\)-synchronizing sequence;
\textit{(ii)}~almost-sure winning if there is a strategy that produces a
sequence that is, for all \(\epsilon>0\), a \((1-\epsilon)\)-synchronizing
sequence; \textit{(iii)}~limit-sure winning if for all \(\epsilon>0\),
there is a strategy that produces a \((1-\epsilon)\)-synchronizing
sequence.\par
For each synchronizing and winning mode, we consider the problem of
deciding whether an MDP is winning, and we establish matching upper and
lower complexity bounds of the problems, as well as the optimal memory
requirement for winning strategies: \textit{(a)}~for all winning modes, we
show that the problems are PSPACE-complete for weakly synchronizing, and
PTIME-complete for strongly synchronizing; \textit{(b)}~we~show that for
weakly synchronizing, exponential memory is sufficient and may be
necessary for sure winning, and infinite memory is necessary for
almost-sure winning; for strongly synchronizing, linear-size memory is
sufficient and may be necessary in all modes; \textit{(c)}~we~show a
robustness result that the almost-sure and limit-sure winning modes
coincide for both weakly and strongly synchronizing.}
}
@inproceedings{BMM-concur14,
address = {Rome, Italy},
month = sep,
year = 2014,
volume = 8704,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baldan, Paolo and Gorla, Daniele},
acronym = {{CONCUR}'14},
booktitle = {{P}roceedings of the 25th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'14)},
author = {Bouyer, Patricia and Markey, Nicolas and Matteplackel,
Raj~Mohan},
title = {Averaging in~{LTL}},
pages = {266-280},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMM-concur14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMM-concur14.pdf},
doi = {10.1007/978-3-662-44584-6_19},
abstract = {For the accurate analysis of computerized systems, powerful
quantitative formalisms have been designed, together with efficient
verification algorithms. However, verification has mostly remained
boolean---either a property is~true, or it~is false. We~believe that this
is too crude in a context where quantitative information and constraints
are crucial: correctness should be quantified!\par In a recent line of
works, several authors have proposed quantitative semantics for temporal
logics, using e.g. \emph{discounting} modalities (which give less
importance to distant events). In~the present paper, we define and study a
quantitative semantics of~LTL with \emph{averaging} modalities, either on
the long run or within an until modality. This, in a way, relaxes the
classical Boolean semantics of~LTL, and provides a measure of certain
properties of a model. We~prove that computing and even approximating the
value of a formula in this logic is undecidable.}
}
@article{BBMU-lmcs14,
journal = {Logical Methods in Computer Science},
author = {Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas
and Ummels, Michael},
title = {Pure {N}ash Equilibria in Concurrent Games},
volume = {11},
number = {2:9},
nopages = {},
month = jun,
year = 2015,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBMU-lmcs15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBMU-lmcs15.pdf},
doi = {10.2168/LMCS-11(2:9)2015},
abstract = {We study pure-strategy Nash equilibria in multiplayer concurrent
games, for a variety of omega-regular objectives. For simple objectives
(e.g. reachability, B{\"u}chi objectives), we transform the problem of
deciding the existence of a Nash equilibrium in a given concurrent game
into that of deciding the existence of a winning strategy in a turn-based
two-player game (with a refined objective). We use that transformation to
design algorithms for computing Nash equilibria, which in most cases have
optimal worst-case complexity. For automata-defined objectives, we extend
the above algorithms using a simulation relation which allows us to
consider the product of the game with the automata defining the
objectives. Building on previous algorithms for simple qualitative
objectives, we define and study a semi-quantitative framework, where all
players have several boolean objectives equipped with a preorder; a player
may for instance want to satisfy all her objectives, or to maximise the
number of objectives that she achieves. In most cases, we prove that the
algorithms we obtain match the complexity of the problem they address.}
}
@article{LM-lmcs14,
journal = {Logical Methods in Computer Science},
author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas},
title = {Quantified {CTL}: Expressiveness and Complexity},
volume = 10,
number = {4:17},
nopages = {},
month = dec,
year = 2014,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LM-lmcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LM-lmcs14.pdf},
doi = {10.2168/LMCS-10(4:17)2014},
abstract = {While it was defined long ago, the extension of CTL with
quantification over atomic propositions has never been studied
extensively. Considering two different semantics (depending whether
propositional quantification refers to the Kripke structure or to its
unwinding tree), we~study its expressiveness (showing in particular that
QCTL coincides with Monadic Second-Order Logic for both semantics) and
characterise the complexity of its model-checking and satisfiability
problems, depending on the number of nested propositional quantifiers
(showing that the structure semantics populates the polynomial hierarchy
while the tree semantics populates the exponential hierarchy).}
}
@phdthesis{mahsa-phd2014,
author = {Shirmohammadi, Mahsa},
title = {Qualitative Analysis of Synchronizing Probabilistic Systems},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France and Universit\'e Libre de Bruxelles, Belgium},
type = {Th{\`e}se de doctorat},
year = 2014,
month = dec,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/mahsa-phd14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/mahsa-phd14.pdf}
}
@misc{cassting-D13,
author = {Markey, Nicolas and Doyen, Laurent and Berwanger, Dietmar},
title = {Models for large-scale systems},
howpublished = {Cassting deliverable~D1.3 (FP7-ICT-601148)},
month = sep,
year = {2015},
note = {17~pages},
type = {Contract Report},
url = {http://www.cassting-project.eu/wp-content/uploads/deliv-13.pdf},
pdf = {http://www.cassting-project.eu/wp-content/uploads/deliv-13.pdf}
}
@misc{cassting-D21,
author = {Geeraerts, Gilles and Dehouck, Samuel and Markey, Nicolas and Larsen, Kim G.},
title = {Efficient algorithms for multi-player games with quantitative aspects},
howpublished = {Cassting deliverable~D2.1 (FP7-ICT-601148)},
month = mar,
year = {2015},
note = {22~pages},
type = {Contract Report},
url = {http://www.cassting-project.eu/wp-content/uploads/deliv-21.pdf},
pdf = {http://www.cassting-project.eu/wp-content/uploads/deliv-21.pdf}
}
@misc{cassting-D63,
author = {Markey, Nicolas and Delaborde, Arthur},
title = {Annual report for Year~2},
howpublished = {Cassting deliverable~D6.3 (FP7-ICT-601148)},
month = may,
year = {2015},
note = {34~pages},
type = {Contract Report},
nourlnote = {confidentiel}
}
@article{BGM-ipl15,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Bouyer, Patricia and Gardy, Patrick and Markey, Nicolas},
title = {On~the semantics of Strategy Logic},
volume = {116},
number = {2},
pages = {75-79},
month = feb,
year = {2016},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-ipl15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-ipl15.pdf},
doi = {10.1016/j.ipl.2015.10.004},
abstract = {We define and study a slight variation on the semantics of
Strategy Logic: while in the classical semantics, all strategies are
shifted during the evaluation of temporal modalities, we propose to only
shift the strategies that have been assigned to a player, thus matching
the intuition that we can assign the very same strategy to the players at
different points in time. We prove that surprisingly, this renders the
model-checking problem undecidable.}
}
@inproceedings{BV-fsttcs15,
address = {Bangalore, India},
month = dec,
year = 2015,
volume = {45},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Harsha, Prahladh and Ramalingam, G.},
acronym = {{FSTTCS}'15},
booktitle = {{P}roceedings of the 35th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'15)},
author = {Berwanger, Dietmar and Van{ }den{ }Bogaard, Marie},
title = {Games with Delays. A~{F}rankenstein Approach},
pages = {307-319},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BV-fsttcs15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BV-fsttcs15.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2015.307},
abstract = {We investigate infinite games on finite graphs where the
information flow is perturbed by non-deterministic signalling delays. It
is known that such perturbations make synthesis problems virtually
unsolvable, in the general case. On the classical model where signals are
attached to states, tractable cases are rare and difficult to identify. In
this paper, we propose a model where signals are detached from control
states, and we identify a subclass on which equilibrium outcomes can be
preserved, even if signals are delivered with a delay that is finitely
bounded. To offset the perturbation, our solution procedure combines
responses from a collection of virtual plays following an equilibrium
strategy in the instant-signalling game to synthesise, in a
Dr.~Frankenstein manner, an equivalent equilibrium strategy for the
delayed-signalling game.}
}
@inproceedings{BGM-fsttcs15,
address = {Bangalore, India},
month = dec,
year = 2015,
volume = {45},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Harsha, Prahladh and Ramalingam, G.},
acronym = {{FSTTCS}'15},
booktitle = {{P}roceedings of the 35th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'15)},
author = {Bouyer, Patricia and Gardy, Patrick and Markey, Nicolas},
title = {Weighted strategy logic with boolean goals over one-counter games},
pages = {69-83},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-fsttcs15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-fsttcs15.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2015.69},
abstract = {Strategy Logic is a powerful specification language for
expressing non-zero-sum properties of multi-player games. SL conveniently
extends the logic ATL with explicit quantification and assignment of
strategies. In this paper, we consider games over one-counter automata,
and a quantitative extension 1cSL of SL with assertions over the value of
the counter. We prove two results: we first show that, if decidable, model
checking the so-called Boolean-goal fragment of 1cSL has non-elementary
complexity; we actually prove the result for the Boolean-goal fragment of
SL over finite-state games, which was an open question in (Mogavero
\emph{et~al.} Reasoning about strategies: On the model-checking problem.
2014). As a first step towards proving decidability, we then show that the
Boolean-goal fragment of 1cSL over one-counter games enjoys a nice
periodicity property.}
}
@inproceedings{ncma2015-bou,
address = {Porto, Portugal},
month = aug,
year = 2015,
volume = 318,
series = {books@ocg.at},
publisher = {Austrian Computer Society},
editor = {Freund, Rudolf and Holzer, Markus and Moreira, Nelma and Reis, Rog{\'e}rio},
acronym = {{NCMA}'15},
booktitle = {{P}roceedings of the 7th {W}orkshop on {N}on-{C}lassical {M}odels
of {A}utomata and {A}pplications ({NCMA}'15)},
author = {Bouyer, Patricia},
title = {On the optimal reachability problem in weighted timed automata and
games},
pages = {11-36},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ncma15-bou.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ncma15-bou.pdf},
abstract = {In these notes, we survey works made on the models of weighted
timed automata and games, and more specifically on the optimal
reachability problem.}
}
@phdthesis{reichert-phd15,
author = {Reichert, Julien},
title = {D{\'e}cidabilit{\'e} et complexit{\'e} de jeux
d'accessibilit{\'e} sur des syst{\`e}mes {\`a} compteurs},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2015,
month = jul,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/reichert-phd15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/reichert-phd15.pdf}
}
@inproceedings{FGMMP-rp15,
address = {Warsaw, Poland},
month = sep,
year = 2015,
volume = {9328},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Boja{\'n}czyk, Miko{\l}aj and Lasota, S{\l}awomir and Potapov, Igor},
acronym = {{RP}'15},
booktitle = {{P}roceedings of the 9th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'15)},
author = {Fribourg, Laurent and Goubault, {\'E}ric and Mohamed, Sameh
and Mrozek, Marian and Putot, Sylvie},
title = {A~Topological Method for Finding Invariants of
Continuous Systems},
pages = {63-75},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FGMMP-rp15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FGMMP-rp15.pdf},
doi = {10.1007/978-3-319-24537-9_7},
abstract = {A~usual way to find positive invariant sets of ordinary
differential equations is to restrict the search to predefined finitely
generated shapes, such as linear templates, or ellipsoids as in classical
quadratic Lyapunov function based approaches. One then looks for
generators or parameters for which the corresponding shape has the
property that the flow of the ODE goes inwards on its border. But for
non-linear systems, where the structure of invariant sets may be very
complicated, such simple predefined shapes are generally not well suited.
The present work proposes a more general approach based on a topological
property, namely Wa\.{z}ewski's property. Even for complicated non-linear
dynamics, it is possible to successfully restrict the search for isolating
blocks of simple shapes, that are bound to contain non-empty invariant
sets. This approach generalizes the Lyapunov-like approaches, by allowing
for inwards and outwards flow on the boundary of these shapes, with extra
topological conditions. We developed and implemented an algorithm based on
Wa\.{z}ewski's property, SOS optimization and some extra combinatorial and
algebraic properties, that shows very nice results on a number of
classical polynomial dynamical systems.}
}
@inproceedings{BFM-avocs15,
address = {Edinburgh, UK},
month = sep,
year = {2015},
volume = 72,
series = {Electronic Communications of the EASST},
publisher = {European Association of Software Science and Technology},
editor = {Grov, Gudmund and Ireland, Andrew},
acronym = {{AVoCS}'15},
booktitle = {{P}roceedings of the 15th {I}nternational
{W}orkshop on {A}utomated {V}erification
of {C}ritical {S}ystems
({AVoCS}'15)},
author = {Bouyer, Patricia and Fang, Erwin and Markey, Nicolas},
title = {Permissive strategies in timed automata and games},
nopages = {263-277},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFM-avocs15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFM-avocs15.pdf},
doi = {10.14279/tuj.eceasst.72.1015},
abstract = {Timed automata are a convenient framework for modelling and
reasoning about real-time systems. While these models are now very
well-understood, they do not offer a convenient way of taking timing
imprecisions into account. Several solutions (e.g. parametric guard
enlargement) have recently been proposed over the last ten years to take
such imprecisions into account. In this paper, we propose a new approach
for handling robust reachability, based on permissive strategies. While
classical strategies propose to play an action at an exact point in time,
permissive strategies return an interval of possible dates when to play
the selected action. With such a permissive strategy, we associate a
penalty, which is the inverse of the length of the proposed interval, and
accumulates along the run. We show that in that setting, optimal
strategies can be computed in polynomial time for one-clock timed
automata.}
}
@inproceedings{BMRLL-gandalf15,
address = {Genova, Italy},
month = sep,
year = 2015,
volume = {193},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Esparza, Javier and Tronci, Enrico},
acronym = {{GandALF}'15},
booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
({GandALF}'15)},
author = {Bouyer, Patricia and Markey, Nicolas and Randour, Mickael
and Larsen, Kim G. and Laursen, Simon},
title = {Average-energy games},
pages = {1-15},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMRLL-gandalf15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMRLL-gandalf15.pdf},
doi = {10.4204/EPTCS.193.1},
abstract = {Two-player quantitative zero-sum games provide a natural
framework to synthesize controllers with performance guarantees for
reactive systems within an uncontrollable environment. Classical settings
include mean-payoff games, where the objective is to optimize the long-run
average gain per action, and energy games, where the system has to avoid
running out of energy.\par
We study \emph{average-energy} games, where the goal is to optimize the
long-run average of the accumulated energy. We show that this objective
arises naturally in several applications, and that it yields interesting
connections with previous concepts in the literature. We prove that
deciding the winner in such games is in
\textsf{NP}{{\(\cap\)}}\textsf{coNP} and at least as hard as solving
mean-payoff games, and we establish that memoryless strategies suffice to
win. We also consider the case where the system has to minimize the
average-energy while maintaining the accumulated energy within predefined
bounds at all times: this corresponds to operating with a finite-capacity
storage for energy. We give results for one-player and two-player games,
and establish complexity bounds and memory requirements.}
}
@inproceedings{LMS-gandalf15,
address = {Genova, Italy},
month = sep,
year = 2015,
volume = {193},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Esparza, Javier and Tronci, Enrico},
acronym = {{GandALF}'15},
booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
({GandALF}'15)},
author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and
Sangnier, Arnaud},
title = {{{\(\textsf{ATL}_{\textsf{sc}}\)}} with partial observation},
pages = {43-57},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LMS-gandalf15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LMS-gandalf15.pdf},
doi = {10.4204/EPTCS.193.4},
abstract = {Alternating-time temporal logic with strategy contexts
({{\(\textsf{ATL}_{\textsf{sc}}\)}}) is a powerful formalism for
expressing properties of multi-agent systems: it~extends \textsf{CTL} with
\emph{strategy quantifiers}, offering a convenient way of expressing both
collaboration and antagonism between several agents. Incomplete
observation of the state space is a desirable feature in such a framework,
but it quickly leads to undecidable verification problems. In this paper,
we prove that \emph{uniform} incomplete observation (where all players
have the same observation) preserves decidability of the model checking
problem, even for very expressive logics such as
{{\(\textsf{ATL}_{\textsf{sc}}\)}}.}
}
@inproceedings{BV-dlt15,
address = {Liverpool, UK},
month = jul,
year = 2015,
volume = {9168},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Potapov, Igor},
acronym = {{DLT}'15},
booktitle = {{P}roceedings of the 19th {I}nternational
{C}onference on {D}evelopments in {L}anguage {T}heory
({DLT}'15)},
author = {Berwanger, Dietmar and Van{ }den{ }Bogaard, Marie},
title = {Consensus Game Acceptors},
pages = {108-119},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BV-dlt15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BV-dlt15.pdf},
doi = {10.1007/978-3-319-21500-6_8},
abstract = {We study a game for recognising formal languages, in which two
players with imperfect information need to coordinate on a common
decision, given private input strings correlated by a finite graph. The
players have a joint objective to avoid an inadmissible decision, in spite
of the uncertainty induced by the input.\par
We show that the acceptor model based on consensus games characterises
context-sensitive languages, and conversely, that winning strategies in
such games can be described by context-sensitive languages. We also
discuss consensus game acceptors with a restricted observation pattern
that describe nondeterministic linear-time languages.}
}
@inproceedings{BMV-atva15,
address = {Shanghai, China},
month = oct,
year = {2015},
volume = {9364},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Finkbeiner, Bernd and Pu, Geguang and Zhang, Lijun},
acronym = {{ATVA}'15},
booktitle = {{P}roceedings of the 13th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'15)},
author = {Berwanger, Dietmar and Mathew, Anup Basil and
Van{ }den{ }Bogaard, Marie},
title = {Hierarchical Information Patterns and Distributed Strategy Synthesis},
pages = {378-393},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-atva15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-atva15.pdf},
doi = {10.1007/978-3-319-24953-7_28},
abstract = {Infinite games with imperfect information tend to be
undecidable unless the information flow is severely restricted. One
fundamental decidable case occurs when there is a total ordering among
players, such that each player has access to all the information that the
following ones receive.\par
In this paper we consider variations of this hierarchy principle for
synchronous games with perfect recall, and identify new decidable classes
for which the distributed synthesis problem is solvable with finite-state
strategies. In particular, we show that decidability is maintained when
the information hierarchy may change along the play, or when transient
phases without hierarchical information are allowed.}
}
@article{CLMT-dagstuhl15,
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
journal = {Dagstuhl Reports},
editor = {Chatterjee, Krishnendu and Lafortune, St{\'e}phane and
Markey, Nicolas and Thomas, Wolfgang},
author = {Chatterjee, Krishnendu and Lafortune, St{\'e}phane and
Markey, Nicolas and Thomas, Wolfgang},
title = {Non-Zero-Sum-Games and Control ({D}agstuhl Seminar~15061)},
pages = {1-25},
year = {2015},
volume = {5},
number = {2},
month = jun,
url = {http://drops.dagstuhl.de/opus/volltexte/2015/5042},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CLMT-dagstuhl15.pdf},
doi = {10.4230/DagRep.5.2.1},
abstract = {In this report, the program, research issues, and results of
Dagstuhl Seminar 15061 {"}Non-Zero-Sum-Games and Control{"} are described.
The area of non-zero-sum games is addressed in a wide range of topics:
multi-player games, partial-observation games, quantitative game models,
and---as~a special focus---connections with control engineering
(supervisory control).}
}
@inproceedings{BMPS-formats15,
address = {Madrid, Spain},
month = sep,
year = 2015,
volume = {9268},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Sankaranarayanan, Sriram and Vicario, Enrico},
acronym = {{FORMATS}'15},
booktitle = {{P}roceedings of the 13th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'15)},
author = {Bouyer, Patricia and Markey, Nicolas and Perrin, Nicolas
and Schlehuber, Philipp},
title = {Timed automata abstraction of switched dynamical systems
using control funnels},
pages = {60-75},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMPS-formats15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMPS-formats15.pdf},
doi = {10.1007/978-3-319-22975-1_5},
abstract = {The~development of formal methods for control design is an
important challenge with potential applications in a wide range of
safety-critical cyber-physical systems. Focusing on switched dynamical
systems, we~propose a new abstraction, based on time-varying regions of
invariance (the~\emph{control funnels}), that models behaviors of systems as
timed automata. The main advantage of this method is that it allows
automated verification of formal specifications and reactive controller
synthesis without discretizing the evolution of the state of the system.
Efficient constructions are possible in the case of linear dynamics.
We~demonstrate the potential of our approach with two examples.}
}
@inproceedings{AM-formats15,
address = {Madrid, Spain},
month = sep,
year = 2015,
volume = {9268},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Sankaranarayanan, Sriram and Vicario, Enrico},
acronym = {{FORMATS}'15},
booktitle = {{P}roceedings of the 13th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'15)},
author = {Andr{\'e}, {\'E}tienne and Markey, Nicolas},
title = {Language Preservation Problems in Parametric Timed Automata},
pages = {27-43},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AM-formats15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AM-formats15.pdf},
doi = {10.1007/978-3-319-22975-1_3},
abstract = {Parametric timed automata (PTA) are a powerful formalism to
model and reason about concurrent systems with some unknown timing delays.
In this paper, we address the (untimed) language- and trace-preservation
problems: given a reference parameter valuation, does there exist another
parameter valuation with the same untimed language (or trace)? We show
that these problems are undecidable both for general PTA, and even for the
restricted class of L/U-PTA. On the other hand, we exhibit decidable
subclasses: 1-clock PTA, and 1-parameter deterministic L-PTA and U-PTA.}
}
@inproceedings{BJM-concur15,
address = {Madrid, Spain},
month = sep,
year = 2015,
volume = {42},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Aceto, Luca and de Frutos-Escrig, David},
acronym = {{CONCUR}'15},
booktitle = {{P}roceedings of the 26th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'15)},
author = {Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas},
title = {On~the Value Problem in Weighted Timed Games},
pages = {311-324},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BJM-concur15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BJM-concur15.pdf},
doi = {10.4230/LIPIcs.CONCUR.2015.311},
abstract = {A~weighted timed game is a timed game with extra quantitative
information representing e.g. energy consumption. Optimizing the cost for
reaching a target is a natural question, which has been investigated for
ten years. Existence of optimal strategies is known to be undecidable in
general, and only very restricted classes of games have been described for
which optimal cost and almost-optimal strategies can be computed.\par
In this paper, we show that the value problem is undecidable in general
weighted timed games. The undecidability proof relies on that for the
existence of optimal strategies and on a diagonalization construction
recently designed in the context of quantitative temporal logics. We then
provide an algorithm to compute arbitrary approximations of the value in a
game, and almost-optimal strategies. The algorithm applies in a large
subclass of weighted timed games, and is the first approximation scheme
which is designed in the current context.}
}
@inproceedings{CDV-icalp15,
address = {Kyoto, Japan},
month = jul,
year = 2015,
volume = {9135},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Halld{\'o}rsson, Magnus M. and Iwama, Kazuo and Kobayashi,
Naoki and Speckmann, Bettina},
acronym = {{ICALP}'15},
booktitle = {{P}roceedings of the 42nd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'15)~-- {P}art~{II}},
author = {Chatterjee, Krishnendu and Doyen, Laurent and Vardi, Moshe},
title = {The Complexity of Synthesis from Probabilistic Components},
pages = {108-120},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDV-icalp15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDV-icalp15.pdf},
doi = {10.1007/978-3-662-47666-6_9},
abstract = {The synthesis problem asks for the automatic construction of a
system from its specification. In the traditional setting, the system is
{"}constructed from scratch{"} rather than composed from reusable
components. However, this is rare in practice, and almost every
non-trivial software system relies heavily on the use of libraries of
reusable components. Recently, Lustig and Vardi introduced dataflow and
controlflow synthesis from libraries of reusable components. They proved
that dataflow synthesis is undecidable, while controlflow synthesis is
decidable. The problem of controlflow synthesis from libraries of
probabilistic components was considered by Nain, Lustig and Vardi, and was
shown to be decidable for qualitative analysis (that asks that the
specification be satisfied with probability~1). Our main contribution for
controlflow synthesis from probabilistic components is to establish better
complexity bounds for the qualitative analysis problem, and to show that
the more general quantitative problem is undecidable. For the qualitative
analysis, we show that the problem (i)~is EXPTIME-complete when the
specification is given as a deterministic parity word automaton, improving
the previously known 2EXPTIME upper bound; and (ii)~belongs to
UP\(\cap\)coUP and is parity-games hard, when the specification is given
directly as a parity condition on the components, improving the previously
known EXPTIME upper bound.}
}
@article{BFRR-ic15,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Bruy{\`e}re, V{\'e}ronique and Filiot, Emmanuel and
Randour, Mickael and Raskin, Jean-Fran{\c{c}}ois},
title = {Meet Your Expectations With Guarantees: Beyond Worst-Case
Synthesis in Quantitative Games},
volume = {254},
number = {2},
month = jun,
year = 2017,
pages = {259-295},
note = {To appear},
doi = {10.1016/j.ic.2016.10.011},
abstract = {Classical analysis of two-player quantitative games involves an adversary (modeling the environment of the system) which is purely antagonistic and asks for strict guarantees while Markov decision processes model systems facing a purely randomized environment: the aim is then to optimize the expected payoff, with no guarantee on individual outcomes. We introduce the beyond worst-case synthesis problem, which is to construct strategies that guarantee some quantitative requirement in the worst-case while providing a higher expected value against a particular stochastic model of the environment given as input.
We study the beyond worst-case synthesis problem for two important quantitative settings: the mean-payoff and the shortest path. In both cases, we show how to decide the existence of finite-memory strategies satisfying the problem and how to synthesize one if one exists. We establish algorithms and we study complexity bounds and memory requirements.}
}
@inproceedings{RRS-cav15,
address = {San Francisco, CA, USA},
month = jul,
year = 2015,
volume = 9206,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Kroening, Daniel and Pasareanu, Corina},
acronym = {{CAV}'15},
booktitle = {{P}roceedings of the 27th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'15)~-- Part~{I}},
author = {Randour, Mickael and Raskin, Jean-Fran{\c{c}}ois and Sankur, Ocan},
title = {Percentile Queries in Multi-Dimensional {M}arkov Decision Processes},
pages = {123-139},
url = {http://arxiv.org/abs/1410.4801},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RRS-arxiv14.pdf},
doi = {10.1007/978-3-319-21690-4_8},
abstract = {Multi-dimensional weighted Markov decision processes (MDPs) are
useful to analyze systems with multiple objectives that are potentially
conflicting and make necessary the analysis of trade-offs. In this paper,
we study the complexity of percentile queries in such MDPs and provide
algorithms to synthesize strategies that enforce such constraints. Given a
multi-dimensional weighted MDP and a quantitative payoff function~\(f\),
quantitative thresholds~\(v_i\) (one per dimension), and probability
thresholds~\(\alpha_{i}\), we show how to compute a single strategy that
enforces that for all dimension~\(i\), the probability that an
outcome~\(\rho\) satisfies \(f_{i}(\rho) \geq v_{i}\) is at
least~\(\alpha_{i}\). We study this problem for the classical quantitative
payoffs studied in the literature (sup, inf, lim sup, lim inf,
mean-payoff, truncated sum, discounted sum). So our work can be seen as an
extension to the quantitative case of the multi-objective model checking
problem on MDPs studied by Etessami et al. in unweighted MDPs.}
}
@inproceedings{FKM-syncop15,
address = {London, UK},
volume = 44,
series = {Open Access Series in Informatics},
month = apr,
year = 2015,
editor = {Andr{\'e}, {\'E}tienne and Frehse, Goran},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
acronym = {{SYNCOP}'15},
booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {S}ynthesis
of {C}ontinuous {P}arameters ({SYNCOP}'15)},
author = {Fribourg, Laurent and K{\"u}hne, Ulrich and Markey, Nicolas},
title = {Game-based Synthesis of Distributed Controllers for Sampled Switched Systems},
pages = {47-61},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FKM-syncop15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FKM-syncop15.pdf},
doi = {10.4230/OASIcs.SynCoP.2015.47},
abstract = {Switched systems are a convenient formalism for modeling
physical processes interacting with a digital controller. Unfortunately,
the formalism does not capture the distributed nature encountered e.g. in
cyber-physical systems, which are organized as networks of elements
interacting with each other and with local controllers. Most current
methods for control synthesis can only produce a centralized controller,
which is assumed to have complete knowledge of all the component states
and can interact with all of them. In~this paper, we~consider a controller
synthesis method based on state space decomposition, and propose a
game-based approach in order to extend it within a distributed framework.}
}
@inproceedings{LDRCF-syncop15,
address = {London, UK},
volume = 44,
series = {Open Access Series in Informatics},
month = apr,
year = 2015,
editor = {Andr{\'e}, {\'E}tienne and Frehse, Goran},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
acronym = {{SYNCOP}'15},
booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {S}ynthesis
of {C}ontinuous {P}arameters ({SYNCOP}'15)},
author = {Le{~}Co{\"e}nt, Adrien and De{~}Vuyst, Florian and Rey,
{\relax Ch}ristian and Chamoin, Ludovic and Fribourg, Laurent},
title = {Guaranteed control of switched control systems
using model order reduction and state-space bisection},
pages = {32-46},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LDCRF-syncop15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LDCRF-syncop15.pdf},
doi = {10.4230/OASIcs.SynCoP.2015.32},
abstract = {This paper considers discrete-time linear systems controlled by
a quantized law, i.e., a piecewise constant time function taking a finite
set of values. We show how to generate the control by, first, applying
model reduction to the original system, then using a {"}state-space
bisection{"} method for synthesizing a control at the reduced-order
level, and finally computing an upper bound to the deviations between the
controlled output trajectories of the reduced-order model and those of the
original model. The effectiveness of our approach is illustrated on
several examples of the literature.}
}
@article{AFG-sif15,
publisher = {SIF},
journal = {1024~-- Bulletin de la soci{\'e}t{\'e} informatique de France},
author = {Abiteboul, Serge and Fribourg, Laurent and
Goubault{-}Larrecq, Jean},
title = {{G}{\'e}rard {B}erry~: un~informaticien m{\'e}daille d'or du {CNRS}~2014},
volume = 4,
pages = {139-142},
month = oct,
year = 2014,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AFG-sif15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AFG-sif15.pdf},
abstract = {C'est un chercheur en informatique qui vient de recevoir la
m{\'e}daille d'or du CNRS, la plus haute distinction scientifique fran{\c
c}aise toutes disciplines confondues. Les informaticiens sont rares {\`a}
avoir {\'e}t{\'e} ainsi honor{\'e}s : ce n'est que la seconde fois
apr{\`e}s Jacques Stern en~2006.}
}
@inproceedings{RRS-vmcai15,
address = {Mumbai, India},
month = jan,
year = 2015,
volume = 8931,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {D'Souza, Deepak and Lal, Akash and Larsen, Kim Guldstrand},
acronym = {{VMCAI}'15},
booktitle = {{P}roceedings of the 16th {I}nternational {C}onference on
{V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation
({VMCAI}'15)},
author = {Randour, Mickael and Raskin, Jean-Fran{\c{c}}ois and
Sankur, Ocan},
title = {Variations on the Stochastic Shortest Path Problem},
pages = {1-18},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/RRS-vmcai15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RRS-vmcai15.pdf},
doi = {10.1007/978-3-662-46081-8_1},
abstract = {In this invited contribution, we revisit the stochastic shortest
path problem, and show how recent results allow one to improve over the
classical solutions: we present algorithms to synthesize strategies with
multiple guarantees on the distribution of the length of paths reaching a
given target, rather than simply minimizing its expected value. The
concepts and algorithms that we propose here are applications of more
general results that have been obtained recently for Markov decision
processes and that are described in a series of recent papers.}
}
@article{VCDHRR-icomp15,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Velner, Yaron and Chatterjee, Krishnendu and Doyen, Laurent
and Henzinger, Thomas A. and Rabinovich, Alexander Moshe and
Raskin, Jean-Fran{\c{c}}ois},
title = {The complexity of multi-mean-payoff and multi-energy games},
year = 2015,
month = apr,
volume = 241,
pages = {177-196},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDRR-icomp15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDRR-icomp15.pdf},
doi = {10.1016/j.ic.2015.03.001},
abstract = {In mean-payoff games, the objective of the protagonist is to
ensure that the limit average of an infinite sequence of numeric weights
is nonnegative. In energy games, the objective is to ensure that the
running sum of weights is always nonnegative. Multi-mean-payoff and
multi-energy games replace individual weights by tuples, and the limit
average (resp., running sum) of each coordinate must be (resp.,~remain)
nonnegative. We prove finite-memory determinacy of multi-energy games and
show inter-reducibility of multi-mean-payoff and multi-energy games for
finite-memory strategies. We improve the computational complexity for
solving both classes with finite-memory strategies: we prove
coNP-completeness improving the previous known \textsf{EXPSPACE} bound.
For memoryless strategies, we show that deciding the existence of a
winning strategy for the protagonist is NP-complete. We present the first
solution of multi-mean-payoff games with infinite-memory strategies: we
show that mean-payoff-sup objectives can be decided in
\textsf{NP}{{\(\cap\)}}\textsf{coNP}, whereas mean-payoff-inf objectives
are coNP-complete.}
}
@article{CDRR-icomp15,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Chatterjee, Krishnendu and Doyen, Laurent and Randour, Mickael and
Raskin, Jean-Fran{\c{c}}ois},
title = {Looking at Mean-Payoff and Total-Payoff through Windows},
year = 2015,
month = jun,
volume = 242,
pages = {25-52},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDRR-icomp15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDRR-icomp15.pdf},
doi = {10.1016/j.ic.2015.03.010},
abstract = {We consider two-player games played on weighted directed graphs
with mean-payoff and total-payoff objectives, two classical quantitative
objectives. While for single-dimensional games the complexity and memory
bounds for both objectives coincide, we show that in contrast to
multi-dimensional mean-payoff games that are known to be coNP-complete,
multi-dimensional total-payoff games are undecidable. We introduce
conservative approximations of these objectives, where the payoff is
considered over a local finite window sliding along a play, instead of the
whole play. For single dimension, we show that (i)~if the window size is
polynomial, deciding the winner takes polynomial time, and (ii)~the
existence of a bounded window can be decided in
\(\textsf{NP}\cap\textsf{coNP}\), and is at least as hard as solving
mean-payoff games. For multiple dimensions, we show that (i)~the problem
with fixed window size is EXPTIME-complete, and (ii)~there is no
primitive-recursive algorithm to decide the existence of a bounded
window.}
}
@inproceedings{BJ-fossacs17,
address = {Uppsala, Sweden},
month = apr,
year = 2017,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Esparza, Javier and Murawski, Andrzej},
acronym = {{FoSSaCS}'17},
booktitle = {{P}roceedings of the 20th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'17)},
author = {Bouyer, Patricia and Jug{\'e}, Vincent},
title = {Dynamic Complexity of the {D}yck Reachability},
pages = {265-280},
url = {https://arxiv.org/abs/1610.07499},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BJ-fossacs17.pdf},
doi = {10.1007/978-3-662-54458-7_16},
abstract = {Dynamic complexity is concerned with updating the output of a problem when the input is slightly changed. We study the dynamic complexity of Dyck reachability problems in directed and undirected graphs, where updates may add or delete edges. We show a strong dichotomy between such problems, based on the size of the Dyck alphabet. Some of them are P-complete (under a strong notion of reduction) while the others lie either in DynFO or in NL.}
}
@inproceedings{BHMRZ-fossacs17,
address = {Uppsala, Sweden},
month = apr,
year = 2017,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Esparza, Javier and Murawski, Andrzej},
acronym = {{FoSSaCS}'17},
booktitle = {{P}roceedings of the 20th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'17)},
author = {Bouyer, Patricia and Hofman, Piotr and Markey, Nicolas and Randour, Mickael and Zimmermann, Martin},
title = {Bounding Average-energy Games},
pages = {179-195},
url = {https://arxiv.org/abs/1610.07858},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHMRZ-fossacs17.pdf},
doi = {10.1007/978-3-662-54458-7_11},
abstract = {We consider average-energy games, where the goal is to minimize the long-run average of the accumulated energy. Decidability of average-energy games with a lower-bound constraint on the energy level (but no upper bound) is an open problem; in particular, there is no known upper bound on the memory that is required for winning strategies.
By reducing average-energy games with lower-bounded energy to infinite-state mean-payoff games and analyzing the frequency of low-energy configurations, we show an almost tight doubly-exponential upper bound on the necessary memory, and that the winner of average-energy games with lower-bounded energy can be determined in doubly-exponential time. We also prove EXPSPACE-hardness of this problem.
Finally, we consider multi-dimensional extensions of all types of average-energy games: without bounds, with only a lower bound, and with both a lower and an upper bound on the energy. We show that the fully-bounded version is the only case to remain decidable in multiple dimensions.}
}
@article{J-ijac16,
publisher = {World Scientific},
journal = {International Journal of Algebra and Computation},
author = {Jug{\'e}, Vincent},
title = {The Relaxation Normal Form of Braids is Regular},
volume = {27},
number = {1},
year = {2017},
pages = {61-106},
month = feb,
url = {https://arxiv.org/abs/1507.03248},
doi = {10.1142/S0218196717500059},
abstract = {Braids can be represented geometrically as laminations of punctured disks. The geometric complexity of a braid is the minimal complexity of a lamination that represents it, and tight laminations are representatives of minimal complexity. These laminations give rise to a normal form of braids, via a relaxation algorithm. We study here this relaxation algorithm and the associated normal form. We prove that this normal form is regular and prefix-closed. We provide an effective construction of a deterministic automaton that recognizes this normal form.}
}
@phdthesis{mvdb-phd2016,
author = {Van{ }den{ }Bogaard, Marie},
title = {Motifs de Flot d'Information dans les Jeux {\`a} Information Imparfaite},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2016,
month = nov,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/mvdb-phd16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/mvdb-phd16.pdf}
}
@article{BMPS-rts16,
publisher = {Kluwer Academic Publishers},
journal = {Real-Time Systems},
author = {Bouyer, Patricia and Markey, Nicolas and Perrin,
Nicolas and Schlehuber{-}Caissier, Philipp},
title = {Timed automata abstraction of switched dynamical
systems using control funnels},
volume = {53},
number = {3},
year = {2017},
pages = {327-353},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMPS-rts16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMPS-rts16.pdf},
doi = {10.1007/s11241-016-9262-3},
abstract = {The development of formal methods for control design
is an important challenge with potential
applications in a wide range of safety-critical
cyber-physical systems. Focusing on switched
dynamical systems, we propose a new abstraction,
based on time-varying regions of invariance (control
funnels), that models behaviors of systems as timed
automata. The~main advantage of this method is that
it allows for the automated verification and
reactive controller synthesis without discretizing
the evolution of the state of the system. Efficient
and analytic constructions are possible in the case
of linear dynamics whereas bounding funnels with
conjectured properties based on numerical
simulations can be used for general nonlinear
dynamics. We~demonstrate the potential of our
approach with three examples.}
}
@phdthesis{mohamed-PhD16,
author = {Mohamed, Sameh},
title = {Une m{\'e}thode topologique pour la recherche d'ensembles invariants de syst{\`e}mes
continus et {\`a} commutation},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = {2016},
month = oct,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/mohamed-phd16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/mohamed-phd16.pdf}
}
@proceedings{FM-formats16,
title = {{P}roceedings of the 14th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'16)},
booktitle = {{P}roceedings of the 14th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'16)},
acronym = {{FORMATS}'16},
editor = {Fr{\"a}nzle, Martin and Markey, Nicolas},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {9884},
doi = {10.1007/978-3-319-44878-7},
url = {http://link.springer.com/book/10.1007/978-3-319-44878-7},
year = 2016,
month = aug,
address = {Qu\'ebec City, Canada}
}
@proceedings{BDJMS-casstingsyncop16,
title = {{P}roceedings of the {C}assting Workshop on
{G}ames for the {S}ynthesis of {C}omplex {S}ystems ({C}assting'16)
and of the 3rd {I}nternational {W}orkshop on
{S}ynthesis of {C}omplex {P}arameters ({S}yn{C}o{P}'16)},
booktitle = {{P}roceedings of the {C}assting Workshop on
{G}ames for the {S}ynthesis of {C}omplex {S}ystems ({C}assting'16)
and of the 3rd {I}nternational {W}orkshop on
{S}ynthesis of {C}omplex {P}arameters ({S}yn{C}o{P}'16)},
acronym = {{C}assting{{\slash}}{S}yn{C}o{P}'16},
editor = {Brihaye, {\relax Th}omas and Delahaye, Beno{\^\i}t and Jezequel,
Lo{\"\i}g and Markey, Nicolas and Srba, Ji{\v{r}}{\'i}},
doi = {10.4204/EPTCS.220},
url = {http://eptcs.web.cse.unsw.edu.au/content.cgi?CASSTINGSynCoP2016},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = 220,
year = 2016,
month = jul,
address = {Eindhoven, The~Netherlands}
}
@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).}
}
@inproceedings{BMS-gandalf16,
address = {Catania, Italy},
month = sep,
year = 2016,
volume = {226},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Cantone, Domenico and Delzanno, Giorgio},
acronym = {{GandALF}'16},
booktitle = {{P}roceedings of the 7th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
({GandALF}'16)},
author = {Bouyer, Patricia and Markey, Nicolas and Stan, Daniel},
title = {Stochastic Equilibria under Imprecise Deviations in
Terminal-Reward Concurrent Games},
pages = {61-75},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-gandalf16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-gandalf16.pdf},
doi = {10.4204/EPTCS.226.5},
abstract = {We study the existence of mixed-strategy equilibria in
concurrent games played on graphs. While existence is guaranteed
with safety objectives for each player, Nash equilibria need not
exist when players are given arbitrary terminal-reward objectives,
and their existence is undecidable with qualitative reachability
objectives (and~only three players). However, these results rely on
the fact that the players can enforce infinite plays while trying to
improve their payoffs. In this paper, we introduce a relaxed notion
of equilibria, where deviations are imprecise. We prove that
contrary to Nash equilibria, such (stationary) equilibria always
exist, and we develop a PSPACE algorithm to compute one.}
}
@inproceedings{LFS-rp16,
address = {Aalborg, Denmark},
month = sep,
year = 2016,
volume = {9899},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Larsen, Kim G. and Srba, Ji{\v{r}}{\'\i}},
acronym = {{RP}'16},
booktitle = {{P}roceedings of the 10th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'16)},
author = {Le{~}Co{\"e}nt, Adrien and Fribourg, Laurent and
Soulat, Romain},
title = {Compositional analysis of Boolean networks using local fixed-point
iterations},
pages = {134-147},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LFS-rp16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LFS-rp16.pdf},
doi = {10.1007/978-3-319-45994-3_10},
abstract = {We present a compositional method which allows to
over-approximate the set of attractors and under-approximate the set
of basins of attraction of a Boolean network~(BN). This merely
consists in replacing a global fixed-point computation by a
composition of local fixed-point computations. Once these
approximations have been computed, it~becomes much more tractable to
generate the exact sets of attractors and basins of attraction. We
illustrate the interest of our approach on several examples, among
which is a BN modeling a railway interlocking system with 50 nodes
and millions of attractors.}
}
@inproceedings{LFMDC-rp16,
address = {Aalborg, Denmark},
month = sep,
year = 2016,
volume = {9899},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Larsen, Kim G. and Srba, Ji{\v{r}}{\'\i}},
acronym = {{RP}'16},
booktitle = {{P}roceedings of the 10th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'16)},
author = {Le{~}Co{\"e}nt, Adrien and Fribourg, Laurent and
Markey, Nicolas and De{~}Vuyst, Florian and Chamoin, Ludovic},
title = {Distributed Synthesis of State-Dependent Switching Control},
pages = {119-133},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LFMDC-rp16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LFMDC-rp16.pdf},
doi = {10.1007/978-3-319-45994-3_9},
abstract = {We present a correct-by-design method of state-dependent
control synthesis for linear discrete-time switching systems. Given
an objective region~\(R\) of the state space, the method builds a
capture set~\(S\) and a control which steers any element of~\(S\)
into~\(R\). The method works by iterated backward reachability
from~\(R\). More precisely, \(S\)~is given as a parametric extension
of~\(R\), and the maximum value of the parameter is solved by linear
programming. The method can also be used to synthesize a stability
control which maintains indefinitely within~\(R\) all the states
starting at~\(R\). We~explain how the synthesis method can be
performed in a distributed manner. The method has been implemented
and successfully applied to the synthesis of a distributed control
of a concrete floor heating system with 11 rooms and \(2^11 = 2048\)
switching modes.}
}
@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.}
}
@inproceedings{Bouyer-mfcs16,
address = {Krakow, Poland},
month = aug,
year = 2016,
volume = {58},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
acronym = {{MFCS}'16},
booktitle = {{P}roceedings of the 41st
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'16)},
author = {Bouyer, Patricia},
title = {Optimal Reachability in Weighted Timed Automata and Games},
pages = {3:1-3:3},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/bouyer-mfcs16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bouyer-mfcs16.pdf},
doi = {10.4230/LIPIcs.MFCS.2016.3},
abstract = {This is an overview of the invited talk delivered at the 41st International Symposium on Math- ematical Foundations of Computer Science (MFCS-2016).}
}
@inproceedings{ABKMT-mfcs16,
address = {Krakow, Poland},
month = aug,
year = 2016,
volume = {58},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
acronym = {{MFCS}'16},
booktitle = {{P}roceedings of the 41st
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'16)},
author = {Akshay, S. and Bouyer, Patricia and Krishna, Shankara Narayanan and
Manasa, Lakshmi and Trivedi, Ashutosh },
title = {Stochastic Timed Games Revisited},
pages = {8:1-8:14},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABKMT-mfcs16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABKMT-mfcs16.pdf},
doi = {10.4230/LIPIcs.MFCS.2016.8},
abstract = {Stochastic timed games (STGs), introduced by Bouyer and Forejt,
naturally generalize both continuous-time Markov chains and timed automata
by providing a partition of the locations between those controlled by two
players (Player Box and Player Diamond) with competing objectives and
those governed by stochastic laws. Depending on the number of
players---2,~1, or~0---subclasses of stochastic timed games are often
classified as \(2\frac{1}{2}\)-player, \(1\frac{1}{2}\)-player, and
\(\frac{1}{2}\)-player games where the \(\frac{1}{2}\) symbolizes the
presence of the stochastic {"}nature{"} player. For STGs with reachability
objectives it is known that \(1\frac{1}{2}\)-player one-clock STGs are
decidable for qualitative objectives, and that \(2\frac{1}{2}\)-player
three-clock STGs are undecidable for quantitative reachability objectives.
This paper further refines the gap in this decidability spectrum. We show
that quantitative reachability objectives are already undecidable for
\(1\frac{1}{2}\)-player four-clock STGs, and even under the time-bounded
restriction for \(2\frac{1}{2}\)-player five-clock~STGs. We~also obtain a
class of \(1\frac{1}{2}\), \(2\frac{1}{2}\)-player STGs for which the
quantitative reachability problem is decidable.}
}
@inproceedings{NPR-mfcs16,
address = {Krakow, Poland},
month = aug,
year = 2016,
volume = {58},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
acronym = {{MFCS}'16},
booktitle = {{P}roceedings of the 41st
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'16)},
author = {Reino Niskanen and Igor Potapov and Julien Reichert},
title = {Undecidability of Two-dimensional Robot Games},
pages = {73:1-73:13},
url = {http://arxiv.org/abs/1604.08779},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/NPR-mfcs16.pdf},
doi = {10.4230/LIPIcs.MFCS.2016.73},
abstract = {Robot game is a two-player vector addition game played on the integer lattice \(\mathbb{Z}^n\). Both players have sets of vectors and in each turn the vector chosen by a player is added to the current configuration vector of the game. One of the players, called Eve, tries to play the game from the initial configuration to the origin while the other player, Adam, tries to avoid the origin. The problem is to decide whether or not Eve has a winning strategy. In this paper we prove undecidability of the robot game in dimension two answering the question formulated by Doyen and Rabinovich in 2011 and closing the gap between undecidable and decidable cases.}
}
@inproceedings{DLM-concur16,
address = {Qu{\'e}bec City, Canada},
month = aug,
year = 2016,
volume = {59},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Desharnais, Jos{\'e}e and Jagadeesan, Radha},
acronym = {{CONCUR}'16},
booktitle = {{P}roceedings of the 27th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'16)},
author = {David, Am{\'e}lie and Laroussinie, Fran{\c{c}}ois and
Markey, Nicolas},
title = {On~the expressiveness of~{QCTL}},
pages = {28:1-28:15},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DLM-concur16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DLM-concur16.pdf},
doi = {10.4230/LIPIcs.CONCUR.2016.28},
abstract = {QCTL extends the temporal logic CTL with quantification
over atomic propositions. While the algorithmic questions for QCTL
and its fragments with limited quantification depth are
well-understood (e.g. satisfiability of QCTL\textsuperscript{\(k\)},
with at most \(k\) nested blocks of quantifiers, is
\(k+1\)-EXPTIME-complete), very few results are known about the
expressiveness of this logic. We~address such expressiveness
questions in this paper. We first consider the \emph{distinguishing
power} of these logics (i.e.,~their ability to separate models),
their relationship with behavioural equivalences, and their ability
to capture the behaviours of finite Kripke structures with so-called
characteristic formulas. We then consider their \emph{expressive
power} (i.e.,~their ability to express a property), showing that in
terms of expressiveness the hierarchy QCTL\textsuperscript{\(k\)}
collapses at level~2 (in~other terms, any~QCTL formula can be
expressed using at most two nested blocks of quantifiers).}
}
@article{LDRCF-ijdc16,
publisher = {Springer},
journal = {International Journal of Dynamics and Control},
author = {Le{~}Co{\"e}nt, Adrien and De{~}Vuyst, Florian and Rey,
Christian and Chamoin, Ludovic and Fribourg, Laurent},
title = {Control of mechanical systems using set-based methods},
pages = {1-17},
year = 2016,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LDRCF-ijdc16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LDRCF-ijdc16.pdf},
doi = {10.1007/s40435-016-0245-y},
abstract = {This paper considers large discrete-time linear systems obtained
from discretized partial differential equations, and controlled by a
\emph{quantized} law, i.e., a piecewise constant time function taking a
finite set of values. We show how to generate the control by, first,
applying \emph{model reduction} to the original system, then using a
{"}state-space bisection{"} method for synthesizing a control at the
reduced-order level, and finally computing an upper bound on the
deviations between the controlled output trajectories of the reduced-order
model and those of the original model. The effectiveness of our approach
is illustrated on several examples of the literature.}
}
@inproceedings{LACF-snr16,
address = {Vienna, Austria},
month = apr,
year = 2016,
publisher = {{IEEE} Computer Society Press},
acronym = {{SNR}'16},
booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop
on {S}ymbolic and {N}umerical {M}ethods for
{R}eachability {A}nalysis ({SNR}'16)},
author = {Le{~}Co{\"e}nt, Adrien and Alexandre{ }dit{ }Sandretto,
Julien and Chapoutot, Alexandre and Fribourg,
Laurent},
title = {Control of Nonlinear Switched Systems Based on
Validated Simulation},
pages = {1-6},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LACF-snr16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LACF-snr16.pdf},
abstract = {We present an algorithm of control synthesis for nonlinear
switched systems, based on an existing procedure of state-space
bisection and made available for nonlinear systems with the help of
validated simulation. The use of validated simulation also permits
to take bounded perturbations and varying parameters into account.
The whole approach is entirely guaranteed and the induced
controllers are correct-by-design.}
}
@inproceedings{BBCM-csr16,
address = {St~Petersburg, Russia},
month = jun,
year = 2016,
volume = {9691},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gerhard J. Woeginger},
acronym = {{CSR}'16},
booktitle = {{P}roceedings of the 11th {I}nternational {C}omputer {S}cience
{S}ymposium in {R}ussia ({CSR}'16)},
author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and Carlier,
Pierre
and Menet, Quentin},
title = {Compositional Design of Stochastic Timed Automata},
pages = {117-130},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBCM-csr16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBCM-csr16.pdf},
doi = {10.1007/978-3-319-34171-2_9},
abstract = {In this paper, we study the model of stochastic timed automata
and we target the definition of adequate composition operators that will
allow a compositional approach to the design of stochastic systems with
hard real-time constraints. This paper achieves the first step towards
that goal. Firstly, we define a parallel composition operator that
(we~prove) corresponds to the interleaving semantics for that model; we
give conditions over probability distributions, which ensure that the
operator is well-defined; and we exhibit problematic behaviours when this
condition is not satisfied. We furthermore identify a large and natural
subclass which is closed under parallel composition. Secondly, we define
a bisimulation notion which naturally extends that for continuous-time
Markov chains. Finally, we importantly show that the defined bisimulation
is a congruence w.r.t. the parallel composition, which is an expected
property for a proper modular approach to system design.}
}
@inproceedings{BBBC-icalp16,
address = {Rome, Italy},
month = jul,
year = 2016,
volume = {55},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chatzigiannakis, Ioannis and Mitzenmacher,
Michael and Rabani, Yuval and Sangiorgi, Davide},
acronym = {{ICALP}'16},
booktitle = {{P}roceedings of the 43rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'16)},
author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye,
{\relax Th}omas
and Carlier, Pierre},
title = {Analysing Decisive Stochastic Processes},
pages = {101:1-101:14},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBC-icalp16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBC-icalp16.pdf},
doi = {10.4230/LIPIcs.ICALP.2016.101},
abstract = {In~2007, Abdulla \textit{et~al.} introduced the elegant concept
of decisive Markov chain. Intuitively, decisiveness allows one to lift the
good properties of finite Markov chains to infinite Markov chains. For
instance, the approximate quantitative reachability problem can be solved
for decisive Markov chains (enjoying reasonable effectiveness assumptions)
including probabilistic lossy channel systems and probabilistic vector
addition systems with states. In this paper, we extend the concept of
decisiveness to more general stochastic processes. This extension is non
trivial as we consider stochastic processes with a potentially continuous
set of states and uncountable branching (common features of real-time
stochastic processes). This allows us to obtain decidability results for
both qualitative and quantitative verification problems on some classes of
real-time stochastic processes, including generalized semi-Markov
processes and stochastic timed automata.}
}
@inproceedings{CD-icalp16,
address = {Rome, Italy},
month = jul,
year = 2016,
volume = {55},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chatzigiannakis, Ioannis and Mitzenmacher,
Michael and Rabani, Yuval and Sangiorgi, Davide},
acronym = {{ICALP}'16},
booktitle = {{P}roceedings of the 43rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'16)},
author = {Chatterjee, Krishnendu and Doyen, Laurent},
title = {Computation Tree Logic for Synchronization Properties},
pages = {98:1-98:14},
url = {http://arxiv.org/abs/1604.06384},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-icalp16.pdf},
doi = {10.4230/LIPIcs.ICALP.2016.98},
abstract = {We present a logic that extends CTL (Computation Tree Logic)
with operators that express synchronization properties. A property is
synchronized in a system if it holds in all paths of a certain length. The
new logic is obtained by using the same path quantifiers and temporal
operators as in CTL, but allowing a different order of the quantifiers.
This small syntactic variation induces a logic that can express
non-regular properties for which known extensions of MSO with equality of
path length are undecidable. We show that our variant of CTL is decidable
and that the model-checking problem is in \(\Delta_3^P = P^{NP^NP}\), and
is DP-hard. We analogously consider quantifier exchange in extensions of
CTL, and we present operators defined using basic operators of CTL* that
express the occurrence of infinitely many synchronization points. We show
that the model-checking problem remains in \(\Delta_3^P\). The
distinguishing power of CTL and of our new logic coincide if the Next
operator is allowed in the logics, thus the classical bisimulation
quotient can be used for state-space reduction before model checking.}
}
@article{BMV-ic16,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Bouyer, Patricia and Markey, Nicolas and Vester, Steen},
title = {{N}ash Equilibria in Symmetric Graph Games with Partial Observation},
volume = {254},
number = {2},
month = jun,
year = 2017,
pages = {238-258},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-ic16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-ic16.pdf},
doi = {10.1016/j.ic.2016.10.010},
abstract = {We investigate a model for representing large multiplayer games,
which satisfy strong symmetry properties. This model is made of multiple
copies of an arena; each player plays in his own arena, and can partially
observe what the other players do. Therefore, this game has partial
information and symmetry constraints, which make the computation of Nash
equilibria difficult. We show several undecidability results, and for
bounded-memory strategies, we precisely characterize the complexity of
computing pure Nash equilibria (for qualitative objectives) in this game
model.}
}
@inproceedings{BCM-cav16,
address = {Toronto, Canada},
month = jul,
year = 2016,
volume = 9779,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Chaudhuri, Swarat and Farzan, Azadeh},
acronym = {{CAV}'16},
booktitle = {{P}roceedings of the 28th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'16)~-- {P}art~{I}},
author = {Bouyer, Patricia and Colange, Maximilien and Markey, Nicolas},
title = {Symbolic Optimal Reachability in Weighted Timed Automata},
pages = {513-530},
url = {http://arxiv.org/abs/1602.00481},
doi = {10.1007/978-3-319-41528-4_28},
abstract = {Weighted timed automata have been defined in the early 2000's
for modelling resource-consumption or -allocation problems in real-time
systems. Optimal reachability is decidable in weighted timed automata, and
a symbolic forward algorithm has been developed to solve that problem. This
algorithm uses so-called priced zones, an extension of standard zones with
cost functions. In order to ensure termination, the algorithm requires
clocks to be bounded. For unpriced timed automata, much work has been done
to develop sound abstractions adapted to the forward exploration of timed
automata, ensuring termination of the model-checking algorithm without
bounding the clocks. In this paper, we take advantage of recent
developments on abstractions for timed automata, and propose an algorithm
allowing for symbolic analysis of all weighted timed automata, without
requiring bounded clocks.}
}
@inproceedings{BMRSS-icalp16,
address = {Rome, Italy},
month = jul,
year = 2016,
volume = {55},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chatzigiannakis, Ioannis and Mitzenmacher,
Michael and Rabani, Yuval and Sangiorgi, Davide},
acronym = {{ICALP}'16},
booktitle = {{P}roceedings of the 43rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'16)},
author = {Bouyer, Patricia and Markey, Nicolas and Randour,
Mickael and Sangnier, Arnaud and Stan, Daniel},
title = {Reachability in Networks of Register Protocols under
Stochastic Schedulers},
pages = {106:1-106:14},
url = {http://arxiv.org/abs/1602.05928},
doi = {10.4230/LIPIcs.ICALP.2016.106},
abstract = {We study the almost-sure reachability problem in a distributed
system obtained as the asynchronous composition of~\(N\) copies (called
\emph{processes}) of the same automaton (called \emph{protocol}), that can
communicate via a shared register with finite domain. The automaton has
two types of transitions: write-transitions update the value of the
register, while read-transitions move to a new state depending on the
content of the register. Non-determinism is resolved by a stochastic
scheduler. Given a protocol, we focus on almost-sure reachability of a
target state by one of the processes. The answer to this problem naturally
depends on the number~\(N\) of processes. However, we prove that our
setting has a cut-off property : the answer to the almost-sure
reachability problem is constant when \(N\) is large enough; we~then
develop an EXPSPACE algorithm deciding whether this constant answer is
positive or negative.}
}
@inproceedings{CD-lics16,
address = {New York City, USA},
month = jul,
year = 2016,
publisher = {ACM Press},
editor = {Grohe, Martin and Koskinen, Eric and Shankar, Natarajan},
acronym = {{LICS}'16},
booktitle = {{P}roceedings of the 31st {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'16)},
author = {Chatterjee, Krishnendu and Doyen, Laurent},
title = {Perfect-information Stochastic Games with
Generalized Mean-Payoff Objectives},
pages = {247-256},
url = {http://arxiv.org/abs/1604.06376},
doi = {10.1145/2933575.2934513},
abstract = {Graph games provide the foundation for modeling and synthesizing reactive processes. In the synthesis of stochastic reactive processes, the traditional model is perfect-information stochastic games, where some transitions of the game graph are controlled by two adversarial players, and the other transitions are executed probabilistically. We consider such games where the objective is the conjunction of several quantitative objectives (specified as mean-payoff conditions), which we refer to as generalized mean-payoff objectives. The basic decision problem asks for the existence of a finite-memory strategy for a player that ensures the generalized mean-payoff objective be satisfied with a desired probability against all strategies of the opponent. A special case of the decision problem is the almost-sure problem where the desired probability is~1. Previous results presented a semi-decision procedure for epsilon-approximations of the almost-sure problem. In this work, we show that both the almost-sure problem as well as the general basic decision problem are coNP-complete, significantly improving the previous results. Moreover, we show that in the case of 1-player stochastic games, randomized memoryless strategies are sufficient and the problem can be solved in polynomial time. In contrast, in two-player stochastic games, we show that even with randomized strategies exponential memory is required in general, and present a matching exponential upper bound. We also study the basic decision problem with infinite-memory strategies and present computational complexity results for the problem. Our results are relevant in the synthesis of stochastic reactive systems with multiple quantitative 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{FGMP-hscc16,
address = {Vienna, Austria},
month = apr,
year = 2016,
publisher = {ACM Press},
editor = {Abate, Alessandro and Fainekos, Georgios},
acronym = {{HSCC}'16},
booktitle = {{P}roceedings of the 19th {ACM} {I}nternational {C}onference
on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
({HSCC}'16)},
author = {Fribourg, Laurent and Goubault, {\'E}ric and Mohamed, Sameh
and Putot, Sylvie},
title = {A~Topological Method for Finding Invariant Sets of Switched Systems},
pages = {61-70},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FGMP-hscc16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FGMP-hscc16.pdf},
doi = {10.1145/2883817.2883822},
abstract = {We~revisit the problem of finding controlled invariants sets
(viability), for a class of differential inclusions, using topological
methods based on Wazewski property. In~many ways, this generalizes the
Viability Theorem approach, which is itself a generalization of the
Lyapunov function approach for systems described by ordinary differential
equations. We give a computable criterion based on SoS methods for a class
of differential inclusions to have a non-empty viability kernel within
some given region. We use this method to prove the existence of
(controlled) invariant sets of switched systems inside a region described
by a polynomial template, both with time-dependent switching and with
state-based switching through a finite set of hypersurfaces. A~Matlab
implementation allows us to demonstrate its use.}
}
@techreport{BJM-arxiv16,
author = {Bouyer, Patricia and Markey, Nicolas and Jug{\'e}, Vincent},
title = {Dynamic Complexity of Parity Games with Bounded Tree-Width},
institution = {Computing Research Repository},
number = {1610.00571},
year = {2016},
url = {https://arxiv.org/abs/1610.00571},
pdf = {https://arxiv.org/abs/1610.00571},
month = oct,
type = {Research Report},
note = {33~pages}
}
@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.}
}
@incollection{CDH-kimfest17,
author = {Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, {\relax Th}omas~A.},
title = {The Cost of Exactness in Quantitative Reachability},
editor = {Aceto, Luca and Bacci, Giorgio and Bacci, Giovani
and Ing{\'o}lfsd{\'o}ttir, Anna and Legay, Axel and
Mardare, Radu},
booktitle = {Models, Algorithms, Logics and Tools: Essays
Dedicated to Kim Guldstrand Larsen on the Occasion
of His 60th Birthday},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {10460},
year = {2017},
pages = {367-381},
month = aug,
doi = {10.1007/978-3-319-63121-9_18},
abstract = {In the analysis of reactive systems a quantitative objective assigns a real value to every trace of the system. The value decision problem for a quantitative objective requires a trace whose value is at least a given threshold, and the exact value decision problem requires a trace whose value is exactly the threshold. We compare the compu- tational complexity of the value and exact value decision problems for classical quantitative objectives, such as sum, discounted sum, energy, and mean-payoff for two standard models of reactive systems, namely, graphs and graph games.},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDH-2017.pdf}
}
@article{CDFR-ic17,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Krishnendu Chatterjee and Laurent Doyen and Emmanuel Filiot and Jean{-}Fran{\c{c}}ois Raskin},
title = {Doomsday equilibria for omega-regular games},
volume = {254},
year = {2017},
pages = {296-315},
doi = {10.1016/j.ic.2016.10.012},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDFR-ic2017.pdf},
abstract = {Two-player games on graphs provide the theoretical framework for many important problems such as reactive synthesis. While the traditional study of two-player zero-sum games has been extended to multi-player games with several notions of equilibria, they are decidable only for perfect-information games, whereas several applications require imperfect-information games.\par
In this paper we propose a new notion of equilibria, called doomsday equilibria, which is a strategy profile such that all players satisfy their own objective, and if any coalition of players deviates and violates even one of the players objective, then the objective of every player is violated.\par
We present algorithms and complexity results for deciding the existence of doomsday equilibria for various classes of ?-regular objectives, both for imperfect-information games, and for perfect-information games. We provide optimal complexity bounds for imperfect-information games, and in most cases for perfect- information games.}
}
@inproceedings{D-rp17,
address = {London, UK},
month = sep,
year = 2017,
volume = {10506},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Matthew Hague and Igor Potapov},
acronym = {{RP}'17},
booktitle = {{P}roceedings of the 11th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'17)},
author = {Doyen, Laurent},
title = {The Multiple Dimensions of Mean-Payoff Games},
pages = {1-8},
url = {https://doi.org/10.1007/978-3-319-67089-8_1},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Doyen-rp2017.pdf},
doi = {10.1007/978-3-319-67089-8_1},
abstract = {We consider quantitative game models for the design of reactive systems working in resource-constrained environment. The game is played on a finite weighted graph where some resource (e.g., battery) can be consumed or recharged along the edges of the graph.}
}
@phdthesis{gardy-phd2017,
author = {Gardy, Patrick},
title = {Semantics of {S}trategy {L}ogic},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2017,
month = jun,
url = {https://tel.archives-ouvertes.fr/tel-01561802},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/gardy-phd17.pdf}
}
@inproceedings{GBBLM-gretsi17,
address = {Juan-les-Pins, France},
month = sep,
year = 2017,
publisher = {},
editor = {},
acronym = {{GRETSI}'17},
booktitle = {Actes du XXVI$^{\text{\`eme}}$ colloque GRETSI},
author = {Mauricio Gonz{\'a}lez and Olivier Beaude and
Patricia Bouyer and Samson Lasaulce and Nicolas
Markey},
title = {Strat{\'e}gies d'ordonnancement de consommation
d'{\'e}nergie en pr{\'e}sence d'information
imparfaite de pr{\'e}vision},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GBBLM-gretsi17.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GBBLM-gretsi17.pdf}
}
@techreport{BJM-arxiv17,
author = {Bouyer, Patricia and Markey, Nicolas and
Jug{\'e}, Vincent},
institution = {Computing Research Repository},
month = feb,
note = {14~pages},
number = {1702.05183},
type = {Research Report},
title = {Courcelle's Theorem Made Dynamic},
year = {2017},
url = {https://arxiv.org/abs/1702.05183},
pdf = {https://arxiv.org/abs/1702.05183}
}
@inproceedings{BHJ-concur17,
address = {Berlin, Germany},
month = sep,
year = 2017,
volume = {85},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Meyer, Roland and Nestmann, Uwe},
acronym = {{CONCUR}'17},
booktitle = {{P}roceedings of the 28th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'17)},
author = {Bouyer, Patricia and Haddad, Serge and Jug{\'e}, Vincent},
title = {Unbounded product-form {P}etri nets},
pages = {31:1--31:16},
url = {http://drops.dagstuhl.de/opus/volltexte/2017/7795},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7795/pdf/LIPIcs-CONCUR-2017-31.pdf},
doi = {10.4230/LIPIcs.CONCUR.2017.31},
abstract = {Computing steady-state distributions in infinite-state stochastic systems is in general a very difficult task. Product-form Petri nets are those Petri nets for which the steady-state distribution can be described as a natural product corresponding, up to a normalising constant, to an exponentiation of the markings. However, even though some classes of nets are known to have a product-form distribution, computing the normalising constant can be hard. The class of (closed) \(\Pi^3\)-nets has been proposed in an earlier work, for which it is shown that one can compute the steady-state distribution efficiently. However these nets are bounded. In this paper, we generalise queuing Markovian networks and closed \(\Pi^3\)-nets to obtain the class of open \(\Pi^3\)-nets, that generate infinite-state systems. We show interesting properties of these nets: (1) we prove that liveness can be decided in polynomial time, and that reachability in live \(\Pi^3\)-nets can be decided in polynomial time; (2) we show that we can decide ergodicity of such nets in polynomial time as well; (3) we provide a pseudo-polynomial time algorithm to compute the normalising constant.}
}
@inproceedings{AGKS-concur17,
address = {Berlin, Germany},
month = sep,
year = 2017,
volume = {85},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Meyer, Roland and Nestmann, Uwe},
acronym = {{CONCUR}'17},
booktitle = {{P}roceedings of the 28th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'17)},
author = {Akshay, S. and Gastin, Paul and Krishna, Shankara Narayanan and Sarkar, Ilias},
title = {Towards an Efficient Tree Automata based technique for Timed Systems},
pages = {39:1--39:15},
url = {http://drops.dagstuhl.de/opus/volltexte/2017/7801},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7801/pdf/LIPIcs-CONCUR-2017-39.pdf},
doi = {10.4230/LIPIcs.CONCUR.2017.39},
abstract = {The focus of this paper is the analysis of real-time systems with recursion, through the development of good theoretical techniques which are implementable. Time is modeled using clock variables, and recursion using stacks. Our technique consists of modeling the behaviours of the timed system as graphs, and interpreting these graphs on tree terms by showing a bound on their tree-width. We then build a tree automaton that accepts exactly those tree terms that describe realizable runs of the timed system. The emptiness of the timed system thus boils down to emptiness of a finite tree automaton that accepts these tree terms. This approach helps us in obtaining an optimal complexity, not just in theory (as done in earlier work e.g.[concur16]), but also in going towards an efficient implementation of our technique. To do this, we make several improvements in the theory and exploit these to build a first prototype tool that can analyze timed systems with recursion.}
}
@inproceedings{BQS-concur17,
address = {Berlin, Germany},
month = sep,
year = 2017,
volume = {85},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Meyer, Roland and Nestmann, Uwe},
acronym = {{CONCUR}'17},
booktitle = {{P}roceedings of the 28th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'17)},
author = {Bollig, Benedikt and Quaas, Karin and Sangnier, Arnaud},
title = {The Complexity of Flat Freeze LTL},
pages = {33:1--33:16},
url = {http://drops.dagstuhl.de/opus/volltexte/2017/7799},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7799/pdf/LIPIcs-CONCUR-2017-33.pdf},
doi = {10.4230/LIPIcs.CONCUR.2017.33},
abstract = {We consider the model-checking problem for freeze LTL on one-counter automata (OCAs). Freeze LTL extends LTL with the freeze quantifier, which allows one to store different counter values of a run in registers so that they can be compared with one another. As the model-checking problem is undecidable in general, we focus on the flat fragment of freeze LTL, in which the usage of the freeze quantifier is restricted. Recently, Lechner et al. showed that model checking for flat freeze LTL on OCAs with binary encoding of counter updates is decidable and in 2NEXPTIME. In this paper, we prove that the problem is, in fact, NEXPTIME-complete no matter whether counter updates are encoded in unary or binary. Like Lechner et al., we rely on a reduction to the reachability problem in OCAs with parameterized tests (OCAPs). The new aspect is that we simulate OCAPs by alternating two-way automata over words. This implies an exponential upper bound on the parameter values that we exploit towards an NP algorithm for reachability in OCAPs with unary updates. We obtain our main result as a corollary.}
}
@inproceedings{BJM-formats17,
address = {Berlin, Germany},
month = sep,
year = 2017,
volume = {10419},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abate, Alessandro and Geeraerts, Gilles},
acronym = {{FORMATS}'17},
booktitle = {{P}roceedings of the 15th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'17)},
author = {Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas},
title = {On the Determinization of Timed Systems},
pages = {25-41},
url = {https://hal.archives-ouvertes.fr/hal-01566436/},
doi = {10.1007/978-3-319-65765-3_2},
abstract = {We introduce a new formalism called automata over a timed domain which provides an adequate framework for the determinization of timed systems. In this formalism, determinization w.r.t. timed language is always possible at the cost of changing the timed domain. We give a condition for determinizability of automata over a timed domain without changing the timed domain, which allows us to recover several known determinizable classes of timed systems, such as strongly-non-zeno timed automata, integer-reset timed automata, perturbed timed automata, etc. Moreover in the case of timed automata this condition encompasses most determinizability conditions from the literature.}
}
@phdthesis{stan-phd2017,
author = {Stan, Daniel},
title = {Randomized Strategies in Concurrent Games},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2017,
month = mar,
url = {https://hal.archives-ouvertes.fr/tel-01519354},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/stan-phd17.pdf}
}
@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{FMW-cav17,
address = {Heidelberg, Germany},
month = jul,
volume = {10427},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Kuncak, Viktor and Majumdar, Rupak},
acronym = {{CAV}'17},
booktitle = {{P}roceedings of the 29th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'17)},
author = {Fortin, Marie and Muscholl, Anca and Walukiewicz, Igor},
title = {Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems},
pages = {155-175},
year = {2017},
doi = {10.1007/978-3-319-63390-9_9},
url = {https://arxiv.org/abs/1606.08707},
abstract = {}
}
@article{ABH-ijfcs17,
publisher = {World Scientific},
journal = {International Journal of Foundations of Computer Science},
author = {Atig, Mohamed Faouzi and Bollig, Benedikt and Habermehl, Peter},
title = {Emptiness of ordered multi-pushdown automata is {2ETIME}-complete},
volume = {28},
number = {8},
year = {2017},
pages = {945-975},
doi = {10.1142/S0129054117500332},
url = {http://www.worldscientific.com/doi/abs/10.1142/S0129054117500332},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABH-ijfcs17.pdf},
abstract = {We consider ordered multi-pushdown automata, a multi-stack extension
of pushdown automata that comes with a constraint on stack operations: a pop
can only be performed on the first non-empty stack (which implies that we
assume a linear ordering on the collection of stacks). We show that the
emptiness problem for multi-pushdown automata is 2ETIME-complete.
Containment in 2ETIME is shown by translating an automaton
into a grammar for which we can check if the generated language is empty.
The lower bound is established by simulating the behavior of an alternating
Turing machine working in exponential space. We also compare ordered
multi-pushdown automata with the model of bounded-phase (visibly)
multi-stack pushdown automata, which do not impose an ordering on stacks,
but restrict the number of alternations of pop operations on different
stacks.}
}
@incollection{BLMOW-kimfest17,
author = {Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois and
Markey, Nicolas and Ouaknine, Jo{\"e}l and Worrell,
James},
title = {Timed temporal logics},
editor = {Aceto, Luca and Bacci, Giorgio and Bacci, Giovani
and Ing{\'o}lfsd{\'o}ttir, Anna and Legay, Axel and
Mardare, Radu},
booktitle = {Models, Algorithms, Logics and Tools: Essays
Dedicated to Kim Guldstrand Larsen on the Occasion
of His 60th Birthday},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {10460},
year = {2017},
pages = {211-230},
month = aug,
doi = {10.1007/978-3-319-65764-6_11},
abstract = {Since the early 1990's, classical temporal logics
have been extended with timing constraints. While
temporal logics only express contraints on the order
of events, their timed extensions can add
quantitative constraints on delays between those
events. We survey expressiveness and algorithmic
results on those logics, and discuss semantic
choices that may look unimportant but do have an
impact on the questions we consider.},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLMOW-kimfest17.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLMOW-kimfest17.pdf}
}
@inproceedings{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].}
}
@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{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{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.}
}
@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.}
}
@mastersthesis{m2-Gonzalez,
author = {Gonz{\'a}lez, Mauricio},
title = {{Constructions d'Information Parfaite pour certains Jeux {\`a} Information Imparfaite. Quelques Algorithmes.}},
school = {Universit{\'e} Pierre et Marie Curie, Paris, France},
type = {Rapport de {M}aster},
year = {2015},
month = dec
}
@mastersthesis{m2-Fang,
author = {Fang, Erwin},
title = {{Permissive multi-strategies in timed games}},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2013},
month = aug
}
@mastersthesis{m2-Fortin,
author = {Fortin, Marie},
title = {{Verification of distributed systems with parameterized network topology}},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2015},
month = sep
}
@mastersthesis{m2-Jaziri,
author = {Jaziri, Samy},
title = {{Robustness issues in priced timed automata}},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2014},
month = sep
}
@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.}
}
@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}
}
@article{BM-icomp17,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Berwanger, Dietmar and Mathew, Anup Basil},
title = {Infinite games with finite knowledge gaps},
volume = {254},
pages = {217-237},
year = {2017},
month = jun,
url = {https://doi.org/10.1016/j.ic.2016.10.009},
doi = {10.1016/j.ic.2016.10.009},
abstract = {Infinite games where several players seek to coordinate under imperfect information are deemed to be undecidable, unless the information is hierarchically ordered among the players. We identify a class of games for which joint winning strategies can be constructed effectively without restricting the direction of information flow. Instead, our condition requires that the players attain common knowledge about the actual state of the game over and over again along every play. We show that it is decidable whether a given game satisfies the condition, and prove tight complexity bounds for the strategy synthesis problem under ω-regular winning conditions given by deterministic parity automata.},
pdf = {http://lsv.fr/~dwb/rec.pdf}
}
@article{BMVdB-acta17,
publisher = {Springer},
journal = {Acta Informatica},
author = {Berwanger, Dietmar and Mathew, Anup Basil and {van den Bogaard}, Marie},
title = {Hierarchical information and the synthesis of distributed strategies},
year = {2017},
month = jun,
url = {https://doi.org/10.1007/s00236-017-0306-5},
doi = {10.1007/s00236-017-0306-5},
abstract = {Infinite games with imperfect information are known to be undecidable unless the information flow is severely restricted. One fundamental decidable case occurs when there is a total ordering among players, such that each player has access to all the information that the following ones receive. In this paper we consider variations of this hierarchy principle for synchronous games with perfect recall, and identify new decidable classes for which the distributed synthesis problem is solvable with finite-state strategies. In particular, we show that decidability is maintained when the information hierarchy may change along the play, or when transient phases without hierarchical information are allowed. Finally, we interpret our result in terms of distributed system architectures.},
pdf = {http://lsv.fr/~dwb/hi.pdf}
}
@inproceedings{BR-sr17,
address = {Liverpool, UK},
month = jul,
editor = {{van der Hoek}, Wiebe and Maubert, Bastien and Murano, Aniello and Rubin, Sasha},
acronym = {{SR}'17},
booktitle = {{P}roceedings of the 5th International Workshop on Strategic Reasoning ({SR}'17)},
author = {Dietmar Berwanger and R. Ramanujam},
title = {{Deviator Detection under Imperfect Monitoring}},
year = {2017},
url = {https://arxiv.org/abs/1712.09686},
pdf = {https://arxiv.org/pdf/1712.09686.pdf},
abstract = {Grim-trigger strategies are a fundamental mechanism for sustaining equilibria in iterated games: the players cooperate along an agreed path, and as soon as one player deviates, the others form a coalition to play him down to his minmax level. A precondition to triggering such a strategy is that the identity of the deviating player becomes common knowledge among the other players. This can be difficult or impossible to attain in games where the information structure allows only imperfect monitoring of the played actions or of the global state.
We study the problem of synthesising finite-state strategies for detecting the deviator from an agreed strategy profile in games played on finite graphs with different information structures. We show that the problem is undecidable in the general case where the global state cannot be monitored. On the other hand, we prove that under perfect monitoring of the global state and imperfect monitoring of actions, the problem becomes decidable, and we present an effective synthesis procedure that covers infinitely repeated games with private monitoring.}
}
@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{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.}
}
@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.}
}
@phdthesis{Carlier-phd2017,
author = {Carlier, Pierre},
title = {{Verification of Stochastic Timed Automata}},
school = {{Ecole Normale Sup{\'e}rieure de Cachan (ENS Paris-Saclay) and Universit{\'e} de Mons}},
type = {Th{\`e}se de doctorat},
year = 2017,
month = dec,
url = {https://tel.archives-ouvertes.fr/tel-01696130},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/carlier-phd2017.pdf}
}
@inproceedings{DLM-pnse16,
address = {Torun, Poland},
month = jun,
year = 2016,
volume = 1591,
series = {CEUR Workshop Proceedings},
publisher = {CEUR-WS.org},
editor = {Lawrence Cabac and Lars Michael Kristensen and Heiko R{\"o}lke:},
acronym = {{PNSE}'16},
booktitle = {{P}roceedings of the 10th {I}nternational {W}orkshop on {P}etri
{N}ets and {S}oftware {E}ngineering ({PNSE}'16)},
author = {Alban Linard and
Beno{\^{\i}}t Barbot and
Didier Buchs and
Maximilien Colange and
Cl{\'{e}}ment D{\'{e}}moulins and
Lom{-}Messan Hillah and
Alexis Martin},
title = {Layered Data: {A} Modular Formal Definition without Formalisms},
pages = {287-306},
url = {http://ceur-ws.org/Vol-1591/},
pdf = {http://ceur-ws.org/Vol-1591/paper19.pdf},
abstract = {Defining formalisms and models in a modular way is a painful task. Metamodeling tools and languages have usually not been created with this goal in mind. This article proposes a data structure, called layered data, that allows defining easily modular abstract syntax for for- malisms and models. It also shows its use through an exhaustive example. As a side effect, this article discusses the notion of formalism, and asserts that they do not exist as standalone objects, but rather as relations between models.}
}
@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.}
}
@inproceedings{BBM-fsttcs19,
address = {Bombay, India},
month = dec,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Arkadev Chattopadhyay and Paul Gastin},
acronym = {{FSTTCS}'19},
booktitle = {{P}roceedings of the 39th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'19)},
author = {Nathalie Bertrand and Patricia Bouyer and Anirban Majumdar},
title = {Concurrent parameterized games},
pages = {31:1-31:15},
year = 2019,
doi = {10.4230/LIPIcs.FSTTCS.2019.31},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2019/11593/pdf/LIPIcs-FSTTCS-2019-31.pdf},
url = {https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11593},
abstract = {Traditional concurrent games on graphs involve a fixed number of players, who take decisions simultaneously, determining the next state of the game. In this paper, we introduce a parameterized variant of concurrent games on graphs, where the parameter is precisely the number of players. Parameterized concurrent games are described by finite graphs, in which the transitions bear regular languages to describe the possible move combinations that lead from one vertex to another. We consider the problem of determining whether the first player, say Eve, has a strategy to ensure a reachability objective against any strategy profile of her opponents as a coalition. In particular Eve's strategy should be independent of the number of opponents she actually has. Technically, this paper focuses on an a priori simpler setting where the languages labeling transitions only constrain the number of opponents (but not their precise action choices). These constraints are described as semilinear sets, finite unions of intervals, or intervals. We establish the precise complexities of the parameterized reachability game problem, ranging from PTIME-complete to PSPACE-complete, in a variety of situations depending on the contraints (semilinear predicates, unions of intervals, or intervals) and on the presence or not of non-determinism.}
}
@article{BQS-lmcs19,
journal = {Logical Methods in Computer Science},
author = {Bollig, Benedikt and Quaas, Karin and Sangnier, Arnaud},
title = {The Complexity of Flat Freeze LTL},
volume = {15},
number = {3},
pages = {32:1-32:26},
year = 2019,
doi = {10.23638/LMCS-15(3:32)2019},
pdf = {https://lmcs.episciences.org/5795/pdf},
url = {https://arxiv.org/abs/1609.06124},
abstract = {We consider the model-checking problem for freeze LTL on one-counter automata (OCA). Freeze LTL extends LTL with the freeze quantifier, which allows one to store different counter values of a run in registers so that they can be compared with one another. As the model-checking problem is undecidable in general, we focus on the flat fragment of freeze LTL, in which the usage of the freeze quantifier is restricted. In a previous work, Lechner et al. showed that model checking for flat freeze LTL on OCA with binary encoding of counter updates is decidable and in 2NEXPTIME. In this paper, we prove that the problem is, in fact, NEXPTIME-complete no matter whether counter updates are encoded in unary or binary. Like Lechner et al., we rely on a reduction to the reachability problem in OCA with parameterized tests (OCA(P)). The new aspect is that we simulate OCA(P) by alternating two-way automata over words. This implies an exponential upper bound on the parameter values that we exploit towards an NP algorithm for reachability in OCA(P) with unary updates. We obtain our main result as a corollary. As another application, relying on a reduction by Bundala and Ouaknine, one obtains an alternative proof of the known fact that reachability in closed parametric timed automata with one parametric clock is in NEXPTIME.}
}
@inproceedings{GMG-dlt19,
address = {Warsaw, Poland},
month = aug,
volume = {11647},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Piotrek Hofman and Micha\l Skrzypczak},
acronym = {{DLT}'19},
booktitle = {{P}roceedings of the 23th {I}nternational
{C}onference on {D}evelopments in {L}anguage {T}heory
({DLT}'19)},
author = {Paul Gastin and Amaldev Manuel and R. Govind},
title = {Logics for Reversible Regular Languages and Semigroups with Involution},
pages = {182-191},
doi = {10.1007/978-3-030-24886-4_13},
year = 2019,
pdf = {https://arxiv.org/pdf/1907.01214.pdf},
url = {https://arxiv.org/abs/1907.01214},
abstract = {We present MSO and FO logics with predicates ``between'' and
``neighbour'' that characterise various fragments of the class of regular
languages that are closed under the reverse operation. The standard
connections that exist between MSO and FO logics and varieties of finite
semigroups extend to this setting with semigroups extended with an
involution. The case is different for FO with neighbour relation where
we show that one needs additional equations to characterise the class.}
}
@inproceedings{Gastin-cai19,
address = {Ni{\u s}, Serbia},
month = jun,
volume = 11545,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Miroslav {\'C}iri{\'c} and Manfred Droste and Jean-{\'E}ric Pin},
acronym = {{CAI}'19},
booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on
{A}lgebraic {I}nformatics ({CAI}'19)},
author = {Gastin, Paul},
title = {Modular Descriptions of Regular Functions},
pages = {3-9},
note = {Invited talk},
year = 2019,
pdf = {https://arxiv.org/abs/1908.01137},
doi = {10.1007/978-3-030-21363-3_1},
abstract = {We discuss various formalisms to describe string-to-string
transformations. Many are based on automata and can be seen as operational
descriptions, allowing direct implementations when the input scanner is
deterministic. Alternatively, one may use more human friendly descriptions
based on some simple basic transformations (e.g., copy, duplicate, erase,
reverse) and various combinators such as function com- position or extensions
of regular operations.}
}
@inproceedings{GMS-cav19,
address = {New York, USA},
month = jul,
volume = {11561},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Isil Dillig and Serdar Tasiran},
acronym = {{CAV}'19},
booktitle = {{P}roceedings of the 31st
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'19)},
author = {Paul Gastin and Sayan Mukherjee and B. Srivathsan},
title = {Fast algorithms for handling diagonal constraints in timed automata},
pages = {41-59},
year = 2019,
doi = {10.1007/978-3-030-25540-4_3},
pdf = {https://arxiv.org/pdf/1904.08590.pdf},
url = {https://arxiv.org/abs/1904.08590}
}
@inproceedings{BBM-mfcs19,
address = {Aachen, Germany},
month = aug,
volume = {138},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Pinar Heggernes and Joost-Pieter Katoen and Peter Rossmanith},
acronym = {{MFCS}'19},
booktitle = {{P}roceedings of the 42nd
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'19)},
author = {Manfred Droste and Paul Gastin},
title = {Aperiodic Weighted Automata and Weighted First-Order Logic},
pages = {76:1-76:15},
year = 2019,
doi = {10.4230/LIPIcs.MFCS.2019.76},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/11020/pdf/LIPIcs-MFCS-2019-76.pdf},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11020}
}
@inproceedings{BT-mfcs19,
address = {Aachen, Germany},
month = aug,
volume = {138},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Pinar Heggernes and Joost-Pieter Katoen and Peter Rossmanith},
acronym = {{MFCS}'19},
booktitle = {{P}roceedings of the 42nd
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'19)},
author = {Patricia Bouyer and Nathan Thomasset},
title = {Nash equilibria in games over graphs equipped with a communication mechanism},
pages = {9:1-9:14},
year = 2019,
doi = {10.4230/LIPIcs.MFCS.2019.9},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/10953/pdf/LIPIcs-MFCS-2019-9.pdf},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=10953}
}
@inproceedings{BBM-concur19,
address = {Amsterdam, The Netherlands},
month = aug,
volume = {140},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Wan Fokkink and Rob {van Glabbeek}},
acronym = {{CONCUR}'19},
booktitle = {{P}roceedings of the 30th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'19)},
author = {Nathalie Bertrand and Patricia Bouyer and Anirban Majumdar},
title = {Reconfiguration and message losses in parameterized broadcast networks},
pages = {32:1-32:15},
year = 2019,
doi = {10.4230/LIPIcs.CONCUR.2019.32},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/10934/pdf/LIPIcs-CONCUR-2019-32.pdf},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=10934}
}
@article{GBM-tocsys19,
publisher = {Springer},
journal = {Theory of Computing Systems},
author = {Gardy, Patrick and Bouyer, Patricia and Markey, Nicolas},
title = {Dependences in Strategy Logic},
volume = {64},
number = {3},
year = 2020,
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GBM-tocsys19.pdf},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GBM-tocsys19.pdf}
}
@inproceedings{BKMMMP-ijcai19,
futureaddress = {},
month = jul,
publisher = {IJCAI organization},
editor = {Kraus, Sarit},
acronym = {{IJCAI}'19},
booktitle = {{P}roceedings of the 28th {I}nternational {J}oint
{C}onference on {A}rtificial {I}ntelligence
({IJCAI}'19)},
author = {Bouyer, Patricia and Kupferman, Orna and Markey, Nicolas and Maubert, Bastien and Murano, Aniello and Perelli, Giuseppe},
title = {Reasoning about Quality and Fuzziness of Strategic Behaviours},
pages = {1588-1594},
year = 2019,
doi = {10.24963/ijcai.2019/220},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKMMMP-ijcai19.pdf},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKMMMP-ijcai19.pdf}
}
@inproceedings{Fortin-icalp19,
address = {Patras, Greece},
month = jul,
volume = {132},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chatzigiannakis, Ioannis and Merelli, Emanuela},
acronym = {{ICALP}'19},
booktitle = {{P}roceedings of the 46th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'19)},
author = {Fortin, Marie},
title = {FO = FO3 for linear orders with monotone binary relations},
year = 2019,
pages = {116:1-116:13},
doi = {10.4230/LIPIcs.ICALP.2019.116},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/10692/pdf/LIPIcs-ICALP-2019-116.pdf},
url = {http://drops.dagstuhl.de/opus/volltexte/2019/10692/},
abstract = {We show that over the class of linear orders with additional
binary relations satisfying some monotonicity conditions, monadic first-order
logic has the three-variable property. This generalizes (and gives a new proof
of) several known results, including the fact that monadic first-order logic
has the three-variable property over linear orders, as well as over
(R, <, +1), and answers some open questions mentioned in a paper from
Antonopoulos, Hunter, Raza and Worrell [FoSSaCS 2015]. Our proof is based on
a translation of monadic first-order logic formulas into formulas of a star-free
variant of Propositional Dynamic Logic, which are in turn easily expressible in
monadic first-order logic with three variables.}
}
@inproceedings{AGJK-lics19,
address = {Vancouver, Canada},
month = jun,
publisher = {{IEEE} Press},
editor = {Bouyer, Patricia},
acronym = {{LICS}'19},
booktitle = {{P}roceedings of the 34th {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'19)},
author = {Akshay, S. and Gastin, Paul and Jug{\'e}, Vincent and Krishna, Shankara Narayanan},
title = {Timed systems through the lens of logic},
pages = {1-13},
year = 2019,
doi = {10.1109/LICS.2019.8785684},
pdf = {https://arxiv.org/pdf/1903.03773.pdf},
url = {https://arxiv.org/abs/1903.03773},
abstract = {In this paper, we analyze timed systems with data structures, using a rich interplay of logic and properties of graphs. We start by describing behaviors of timed systems using graphs with timing constraints. Such a graph is called realizable if we can assign time-stamps to nodes or events so that they are consistent with the timing constraints. The logical definability of several graph properties has been a challenging problem, and we show, using a highly non-trivial argument, that the realizability property for collections of graphs with strict timing constraints is logically definable in a class of propositional dynamic logic (EQ-ICPDL), which is strictly contained in MSO. Using this result, we propose a novel, algorithmically efficient and uniform proof technique for the analysis of timed systems enriched with auxiliary data structures, like stacks and queues. Our technique unravels new results (for emptiness checking as well as model checking) for timed systems with richer features than considered so far, while also recovering existing results.}
}
@inproceedings{CD-lics19,
address = {Vancouver, Canada},
month = jun,
publisher = {{IEEE} Press},
editor = {Bouyer, Patricia},
acronym = {{LICS}'19},
booktitle = {{P}roceedings of the 34th {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'19)},
author = {Chatterjee, Krishnendu and Doyen, Laurent},
title = {Graph Planning with Expected Finite Horizon},
pages = {1-13},
year = 2019,
doi = {10.1109/LICS.2019.8785706},
abstract = {Graph planning gives rise to fundamental algorithmic questions such as shortest path, traveling salesman problem, etc. A classical problem in discrete planning is to consider a weighted graph and construct a path that maximizes the sum of weights for a given time horizon T. However, in many scenarios, the time horizon is not fixed, but the stopping time is chosen according to some distribution such that the expected stopping time is T. If the stopping time distribution is not known, then to ensure robustness, the distribution is chosen by an adversary, to represent the worst-case scenario. A stationary plan for every vertex always chooses the same outgoing edge. For fixed horizon or fixed stopping-time distribution, stationary plans are not sufficient for optimality. Quite surprisingly we show that when an adversary chooses the stopping-time distribution with expected stopping time T, then stationary plans are sufficient. While computing optimal stationary plans for fixed horizon is NP-complete, we show that computing optimal stationary plans under adversarial stopping-time distribution can be achieved in polynomial time. Consequently, our polynomial-time algorithm for adversarial stopping time also computes an optimal plan among all possible plans.}
}
@inproceedings{BBR-fossacs19,
address = {Prague, Czech Republic},
month = apr,
year = 2019,
volume = {11425},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Boja{\'n}czyk, Mikolaj and Simpson, Alex},
acronym = {{FoSSaCS}'19},
booktitle = {{P}roceedings of the 22nd {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'19)},
author = {Benedikt Bollig and Patricia Bouyer and Fabian Reiter},
title = {Identifiers in Registers - Describing Network Algorithms with Logic},
pages = {115-132},
url = {https://arxiv.org/abs/1811.08197},
pdf = {https://arxiv.org/pdf/1811.08197.pdf},
doi = {10.1007/978-3-030-17127-8},
abstract = {We propose a formal model of distributed computing based on register automata
that captures a broad class of synchronous network algorithms. The local memory
of each process is represented by a finite-state controller and a fixed number
of registers, each of which can store the unique identifier of some process in
the network. To underline the naturalness of our model, we show that it has the
same expressive power as a certain extension of first-order logic on graphs
whose nodes are equipped with a total order. Said extension lets us define new
functions on the set of nodes by means of a so-called partial fixpoint
operator. In spirit, our result bears close resemblance to a classical theorem
of descriptive complexity theory that characterizes the complexity class PSPACE
in terms of partial fixpoint logic (a proper superclass of the logic we
consider here).}
}
@inproceedings{BKMMMP-ecai20,
address = {Santiago de Compostela, Spain},
month = sep,
optvolume = {??},
optseries = {Frontiers in Artificial Intelligence and Applications},
publisher = {{IOS} Press},
editor = {Lang, J{\'e}r{\^o}me and De Giacomo, Giuseppe and Barro and Sen{\'e}n Barro and O'Sullivan, Barry},
acronym = {{ECAI}'20},
booktitle = {{P}roceedings of the 24th {E}uropean {C}onference on
{A}rtificial {I}ntelligence ({ECAI}'20)},
author = {Patricia Bouyer and Orna Kupferman and Nicolas Markey and Bastien Maubert and Aniello Murano and Giuseppe Perelli},
title = {{Reasoning About Quality and Fuzziness of Strategic Behaviours}},
pages = {2887-2888},
year = 2020,
pdf = {https://ebooks.iospress.nl/publication/55232},
url = {https://ebooks.iospress.nl/publication/55232},
doi = {10.3233/FAIA200437}
}
@techreport{JFA-arxiv20,
author = {Jawher Jerray and
Laurent Fribourg and
{\'E}tienne Andr{\'e}},
institution = {Computing Research Repository},
month = june,
number = {2006.09993},
type = {Research Report},
title = {{Guaranteed phase synchronization of hybrid oscillators using symbolic Euler's method: The Brusselator and biped examples}},
year = {2020},
url = {https://arxiv.org/abs/2006.09993},
pdf = {https://arxiv.org/abs/2006.09993}
}
@techreport{JFA-arxiv20bis,
author = {Jawher Jerray and
Laurent Fribourg and
{\'E}tienne Andr{\'e}},
institution = {Computing Research Repository},
month = july,
number = {2007.13644},
type = {Research Report},
title = {{Robust optimal control using dynamic programming and guaranteed Euler's method}},
year = {2020},
url = {https://arxiv.org/abs/2007.13644},
pdf = {https://arxiv.org/abs/2007.13644}
}
@techreport{JF-arxiv20,
author = {Jawher Jerray and Laurent Fribourg},
institution = {Computing Research Repository},
month = december,
number = {2012.09310},
type = {Research Report},
title = {{Generation of bounded invariants via stroboscopic set-valued maps: Application to the stability analysis of parametric time-periodic systems}},
year = {2020},
url = {https://arxiv.org/abs/2012.09310},
pdf = {https://arxiv.org/abs/2012.09310}
}
@inproceedings{LeRoux-cie2020,
address = {Fisciano, Italy},
month = june,
year = 2020,
volume = 12098,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Marcella Anselmo and Gianluca Della Vedova and Florin Manea and Arno Pauly },
acronym = {{CiE}'20},
booktitle = {{P}roceedings of the 16th {C}onference on {C}omputability in {E}urope ({CiE 2020})},
author = {Le Roux, St{\'e}phane},
title = {{Time-Aware Uniformization of Winning Strategies}},
pages = {193-204},
url = {https://link.springer.com/chapter/10.1007%2F978-3-030-51466-2_17},
pdf = {https://link.springer.com/chapter/10.1007%2F978-3-030-51466-2_17},
doi = {https://doi.org/10.1007/978-3-030-51466-2_17}
}
@article{BLRPR-ic21,
author = {Bruy{\`e}re, V{\'e}ronique and Le Roux, St{\'e}phane and Pauly, Arno
and Raskin, Jean{-}Fran{\c{c}}ois},
title = {On the existence of weak subgame perfect equilibria},
volume = {276},
year = 2021,
doi = {https://doi.org/10.1016/j.ic.2020.104553},
url = {https://www.sciencedirect.com/science/article/pii/S0890540120300419?via%3Dihub}
}
@article{BBFLMR-fac21,
publisher = {Springer},
journal = {Formal Aspects of Computing},
author = {Bacci, Giovanni and
Bouyer, Patricia and
Fahrenberg, Uli and
Larsen, Kim and
Markey, Nicolas and
Reynier, Pierre{-}Alain},
title = {Optimal and robust controller synthesis using energy timed automata
with uncertainty},
volume = {33},
pages = {3--25},
year = 2021,
doi = {10.1007/s00165-020-00521-4},
url = {https://link.springer.com/article/10.1007/s00165-020-00521-4}
}
@phdthesis{fortin-phd2020,
author = {Fortin, Marie},
title = {{Expressivity of first-order logic, star-free propositional dynamic logic and communicating automata}},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2020,
month = nov,
url = {https://tel.archives-ouvertes.fr/tel-03079438},
pdf = {https://tel.archives-ouvertes.fr/tel-03079438/document}
}
@inproceedings{BRS-csl21,
address = {Ljubljana, Slovenia},
month = jan,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Baier, Christel and Goubault{-}Larrecq, Jean},
acronym = {{CSL}'21},
booktitle = {{P}roceedings of the 29th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'21)},
author = {Benedikt Bollig and Fedor Ryabinin and Arnaud Sangnier},
title = {Reachability in Distributed Memory Automata},
pages = {13:1-13:16},
year = {2021},
doi = {10.4230/LIPIcs.CSL.2021.13},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2021/13447/},
url = {https://drops.dagstuhl.de/opus/volltexte/2021/13447/}
}
@inproceedings{BBM-fsttcs20,
address = {Goa, India},
month = dec,
volume = {182},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Nitin Saxena and Sunil Simon},
acronym = {{FSTTCS}'20},
booktitle = {{P}roceedings of the 40th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'20)},
author = {Nathalie Bertrand and Patricia Bouyer and Anirban Majumdar},
title = {Synthesizing safe coalition strategies},
pages = {39:1--39:17},
year = {2020},
doi = {https://doi.org/10.4230/LIPIcs.FSTTCS.2020.39},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2020/13280/pdf/LIPIcs-FSTTCS-2020-39.pdf},
url = {https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=13280}
}
@inproceedings{BBRRV-fsttcs20,
address = {Goa, India},
month = dec,
volume = {182},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Nitin Saxena and Sunil Simon},
acronym = {{FSTTCS}'20},
booktitle = {{P}roceedings of the 40th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'20)},
author = {Paul Gastin and Sayan Mukherjee and B Srivathsan},
title = {Reachability for updatable timed automata made faster and more effective},
pages = {47:1--47:17},
year = {2020},
doi = {https://doi.org/10.4230/LIPIcs.FSTTCS.2020.47},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2020/13288/pdf/LIPIcs-FSTTCS-2020-47.pdf},
url = {https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=13288}
}
@inproceedings{AG-fsttcs20,
address = {Goa, India},
month = dec,
volume = {182},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Nitin Saxena and Sunil Simon},
acronym = {{FSTTCS}'20},
booktitle = {{P}roceedings of the 40th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'20)},
author = {C. Aiswarya and Paul Gastin},
title = {Weighted Tiling Systems for Graphs: Evaluation Complexity},
year = {2020},
doi = {https://doi.org/10.4230/LIPIcs.FSTTCS.2020.34},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2020/13275/pdf/LIPIcs-FSTTCS-2020-34.pdf},
url = {https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=13275}
}
@inproceedings{BBRRV-gandalf20,
address = {Brussels, Belgium},
month = sep,
volume = {326},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Bresolin, Davide and Raskin, Jean-Fran\c{c}ois},
acronym = {{GandALF}'20},
booktitle = {{P}roceedings of the 11th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
({GandALF}'20)},
author = {Bouyer, Patricia and Brihaye, Thomas and Randour, Mickael and Rivi{\`e}re, C{\'e}dric and Vandenhove, Pierre},
title = {Decisiveness of Stochastic Systems and its Application to Hybrid Models},
pages = {149?165},
year = {2020},
doi = {10.4204/EPTCS.326.10},
pdf = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?GANDALF2020.10.pdf},
url = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?GANDALF2020.10}
}
@inproceedings{BBBFS-gandalf20,
address = {Brussels, Belgium},
month = sep,
volume = {326},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Bresolin, Davide and Raskin, Jean-Fran\c{c}ois},
acronym = {{GandALF}'20},
booktitle = {{P}roceedings of the 11th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
({GandALF}'20)},
author = {B{\'e}atrice B{\'e}rard and
Benedikt Bollig and
Patricia Bouyer and
Matthias F{\"u}gger and
Nathalie Sznajder},
title = {Synthesis in Presence of Dynamic Links},
pages = {33?49},
year = {2020},
doi = {10.4204/EPTCS.326.3},
pdf = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?GANDALF2020.3.pdf},
url = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?GANDALF2020.3}
}
@inproceedings{DFG-mfcs20,
address = {Prague, Czech Republic},
month = aug,
volume = {170},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Javier Esparza and Dan Kr{\'a}l},
acronym = {{MFCS}'20},
booktitle = {{P}roceedings of the 43rd
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'20)},
author = {Dou{\'e}neau-Tabot, Ga{\"e}tan and Filiot, Emmanuel and Gastin, Paul},
title = {Register transducers are marble transducers},
pages = {29:1--29:14},
year = 2020,
doi = {https://doi.org/10.4230/LIPIcs.MFCS.2020.29},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2020/12697/pdf/LIPIcs-MFCS-2020-29.pdf},
url = {https://drops.dagstuhl.de/opus/volltexte/2020/12697/}
}
@inproceedings{BLORV-concur20,
address = {Vienna, Austria},
month = sep,
volume = {171},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Igor Konnov and Laura Kovacs},
acronym = {{CONCUR}'20},
booktitle = {{P}roceedings of the 31st
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'20)},
author = {Bouyer, Patricia and Le Roux, St{\'e}phane and Oualhadj, Youssouf and Randour, Mickael and Vandenhove, Pierre},
title = {Games Where You Can Play Optimally with Arena-Independent Finite Memory},
pages = {24:1--24:22},
year = 2020,
doi = {10.4230/LIPIcs.CONCUR.2020.24},
url = {https://drops.dagstuhl.de/opus/volltexte/2020/12836}
}
@inproceedings{AGSW-concur20,
address = {Vienna, Austria},
month = sep,
volume = {171},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Igor Konnov and Laura Kovacs},
acronym = {{CONCUR}'20},
booktitle = {{P}roceedings of the 31st
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'20)},
author = {Bharat Adsul and Paul Gastin and Saptarshi Sarkar and Pascal Weil},
title = {Wreath/cascade products and related decomposition results for the concurrent setting of {M}azurkiewicz traces},
pages = {19:1--19:17},
year = 2020,
doi = {10.4230/LIPIcs.CONCUR.2020.19},
url = {https://drops.dagstuhl.de/opus/volltexte/2020/12831}
}
@mastersthesis{m2-Doueneau,
author = {Ga{\"e}tan Dou{\'e}neau-Tabot},
title = {{Register Models for Pebble Transducers and Applications to Optimization}},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2019},
month = sep
}
@phdthesis{jaziri-phd2019,
author = {Samy Jaziri},
title = {{Automata on Timed Structures}},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2019,
month = sep,
url = {https://tel.archives-ouvertes.fr/tel-02384274},
pdf = {https://tel.archives-ouvertes.fr/tel-02384274/document}
}
@phdthesis{saoud-phd2019,
author = {Adnane Saoud},
title = {{Compositional and Efficient Controller Synthesis for Cyber-Physical Systems}},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2019,
month = oct,
url = {https://tel.archives-ouvertes.fr/tel-02317723},
pdf = {https://tel.archives-ouvertes.fr/tel-02317723/document}
}
@phdthesis{gonzalez-phd2019,
author = {Gonz{\'a}lez, Mauricio},
title = {{Stochastic Games on Graphs with Applications to Smart-Grids Optimization}},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2019,
month = nov,
url = {http://www.theses.fr/2019SACLN064},
pdf = {http://www.lsv.fr/~gonzalez/phd/Thesis_Gonzalez_V2_2.pdf}
}
@article{LRP-dga20,
publisher = {Springer},
journal = {Dynamic Games and Applications},
author = {Le Roux, St{\'e}phane and Pauly, Arno},
title = {A Semi-Potential for Finite and Infinite Games in Extensive Form},
volume = {10},
number = {1},
pages = {120-144},
year = 2020,
doi = {10.1007/s13235-019-00301-7},
url = {https://doi.org/10.1007/s13235-019-00301-7}
}
@inproceedings{AVLRM-sac20,
address = {Brno, Czech Republic},
month = mar,
publisher = {ACM Press},
editor = {Chih{-}Cheng Hung and Tom{\'{a}}s Cern{\'{y}} and Dongwan Shin and Alessio Bechini},
acronym = {{SAC}'20},
booktitle = {{P}roceedings of the 35th {ACM/SIGAPP} {S}ymposium on {A}pplied {C}omputing ({SAC}'20)},
author = {Nikolaos Alexopoulos and Emmanouil Vasilomanolakis and St{\'e}phane {Le Roux} and Steven Rowe and Max M{\"u}hlh{\"a}user},
title = {{TRIDEnT}: Towards a Decentralized Threat Indicator Marketplace},
pages = {332-341},
year = {2020},
doi = {10.1145/3341105.3374020},
url = {https://doi.org/10.1145/3341105.3374020}
}
@inproceedings{ZSGF-ecc19,
address = {Naples, Italy},
month = jun,
publisher = {{IEEE} Press},
acronym = {{ECC}'19},
booktitle = {{P}roceedings of the 18th {E}uropean {C}ontrol {C}onference ({ECC}'19)},
author = {Daniele Zonetti and Adnane Saoud and Antoine Girard and Laurent Fribourg},
title = {A symbolic approach to voltage stability and power sharing in time-varying{DC} microgrids},
pages = {903-909},
year = {2019},
doi = {10.23919/ECC.2019.8796095},
url = {https://doi.org/10.23919/ECC.2019.8796095}
}
@inproceedings{CF-cyphy19,
address = {New York City, NY, USA},
month = oct,
editor = {Roger D. Chamberlain and Martin Grimheden and Walid Taha},
volume = {11971},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
noeditor = {},
acronym = {{CyPhy/WESE}'19},
booktitle = {9th International Workshop on Cyber Physical Systems ({CyPhy}'19) and 15th International Workshop on Model-Based Design ({WESE}'19), Revised Selected Papers},
author = {Adrien {Le Co{\"{e}}nt} and Laurent Fribourg},
title = {Guaranteed Optimal Reachability Control of Reaction-Diffusion Equations Using One-Sided Lipschitz Constants and Model Reduction},
pages = {181-202},
year = {2019},
doi = {10.1007/978-3-030-41131-2_9},
url = {https://doi.org/10.1007/978-3-030-41131-2_9}
}
@inproceedings{DFKN-dsd19,
address = {Kallithea, Greece},
month = aug,
publisher = {{IEEE} Press},
noeditor = {},
acronym = {{DSD}'19},
booktitle = {{P}roceedings of the 22nd {E}uromicro {C}onference on {D}igital {S}ystem {D}esign ({DSD}'19)},
author = {Jean{-}Luc Danger and Laurent Fribourg and Ulrich K{\"u}hne and Maha Naceur},
title = {LAOCO{\"O}N: {A} Run-Time Monitoring and Verification Approach for Hardware Trojan Detection},
pages = {269-276},
year = {2019},
doi = {10.1109/DSD.2019.00047},
url = {https://doi.org/10.1109/DSD.2019.00047}
}
@inproceedings{CF-cdc19,
address = {Nice, France},
month = dec,
publisher = {{IEEE} Control System Society},
noeditor = {},
acronym = {{CDC}'19},
booktitle = {{P}roceedings of the 58th {IEEE} {C}onference on
{D}ecision and {C}ontrol ({CDC}'19)},
author = {Adrien {Le Co{\"e}nt} and Laurent Fribourg},
title = {Guaranteed Control of Sampled Switched Systems using Semi-Lagrangian Schemes and One-Sided Lipschitz Constants},
pages = {599-604},
year = {2019},
doi = {10.1109/CDC40024.2019.9029376},
pdf = {https://arxiv.org/pdf/1903.05882.pdf},
url = {https://doi.org/10.1109/CDC40024.2019.9029376}
}
@inproceedings{ACFJL-acsd19,
address = {Aachen, Germany},
month = jun,
publisher = {{IEEE} Computer Society Press},
editor = {J{\"o}rg Keller and Wojciech Penczek},
acronym = {{ACSD}'19},
booktitle = {{P}roceedings of the 19th {I}nternational
{C}onference on {A}pplication of {C}oncurrency
to {S}ystem {D}esign
({ACSD}'19)},
author = {{\'E}tienne Andr{\'e} and Emmanuel Coquard and Laurent Fribourg and Jawher Jerray and David Lesens},
title = {Parametric Schedulability Analysis of a Launcher Flight Control System Under Reactivity Constraints},
pages = {13-22},
year = {2019},
doi = {10.1109/ACSD.2019.00006},
url = {https://doi.org/10.1109/ACSD.2019.00006}
}
@proceedings{CG-fsttcs2019,
address = {Bombay, India},
month = dec,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Arkadev Chattopadhyay and Paul Gastin},
acronym = {{FSTTCS}'19},
booktitle = {{P}roceedings of the 39th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'19)},
title = {{P}roceedings of the 39th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'19)},
author = {Arkadev Chattopadhyay and Paul Gastin},
year = {2019},
url = {http://www.dagstuhl.de/dagpub/978-3-95977-131-3}
}
@inproceedings{B-atva19,
address = {Taipei, Taiwan},
month = oct,
volume = {11781},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Yu{-}Fang Chen and Chih{-}Hong Cheng and Javier Esparza},
acronym = {{ATVA}'19},
booktitle = {{P}roceedings of the 17th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'19)},
author = {Patricia Bouyer},
title = {{A Note on Game Theory and Verification (Invited Talk)}},
pages = {3-22},
doi = {10.1007/978-3-030-31784-3_1},
year = 2019
}
@inproceedings{B-time19,
address = {M{\'{a}}laga, Spain},
month = oct,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Johann Gamper and Sophie Pinchinat and Guido Sciavicco},
acronym = {{TIME}'19},
booktitle = {{P}roceedings of the 26th {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'19)},
author = {Patricia Bouyer},
title = {{On the Computation of Nash Equilibria in Games on Graphs (Invited Talk)}},
pages = {3:1-3:3},
doi = {10.4230/LIPIcs.TIME.2019.3},
year = 2019
}
@article{LRP-ic20,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Le Roux, St{\'e}phane and Pauly, Arno},
title = {Equilibria in multi-player multi-outcome infinite sequential games},
volume = {276},
year = 2021,
doi = {https://doi.org/10.1016/j.ic.2020.104557},
url = {https://www.sciencedirect.com/science/article/pii/S0890540120300456?via%3Dihub}
}
@article{BGHLR-ic20,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Brihaye, Thomas and Geeraerts, Gilles and Hallet, Marion and Le Roux, St{\'e}phane},
title = {On the termination of dynamics in sequential games},
volume = {272},
year = 2020,
doi = {10.1016/j.ic.2019.104505}
}
@inproceedings{AGKR-tacas2020,
address = {Dublin, Ireland},
month = apr,
volume = {12078},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Armin Biere and David Parker},
acronym = {{TACAS}'20},
booktitle = {{P}roceedings of the 26th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'20)},
author = {Akshay, S. and Gastin, Paul and Krishna, Shankara Narayanan and Roychoudhary, Sparsa},
title = {Revisiting Underapproximate Reachability for Multipushdown Systems},
pages = {387--404},
doi = {10.1007/978-3-030-45190-5_21},
year = 2020,
pdf = {https://arxiv.org/pdf/2002.05950.pdf},
url = {https://link.springer.com/chapter/10.1007/978-3-030-45190-5_21},
longurl = {https://arxiv.org/abs/2002.05950}
}
@inproceedings{BBLS-fossacs2020,
address = {Dublin, Ireland},
month = apr,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Barbara K{\"o}nig and Jean Goubault-Larrecq},
acronym = {{FoSSaCS}'20},
booktitle = {{P}roceedings of the 23rd {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'20)},
author = {B{\'e}atrice B{\'e}rard and Benedikt Bollig and Mathieu Lehaut and Nathalie Sznajder},
title = {Parameterized Synthesis for Fragments of First-Order Logic over Data Words},
pages = {97--118},
doi = {10.1007/978-3-030-45231-5_6},
year = 2020
}
@inproceedings{BD-stacs2020,
address = {Montpellier, France},
month = mar,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Bl{\"a}ser, Markus and Paul, Christophe},
acronym = {{STACS}'20},
booktitle = {{P}roceedings of the 37th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'20)},
author = {Berwanger, Dietmar and Doyen, Laurent},
title = {Observation and Distinction. Representing Information in Infinite Games},
pages = {48:1--48:17},
doi = {10.4230/LIPIcs.STACS.2020.48},
year = 2020
}
This file was generated by bibtex2html 1.98.