In formal verification, runtime monitoring consists
of observing the execution of a system in order to
decide as quickly as possible whether or not it
satisfies a given property. We consider monitoring
in a distributed setting, for properties given as
reachability timed automata. In such a setting,
the system is made of several components, each
equipped with its own local clock and monitor.
The monitors observe events occurring on their
associated component, and receive timestamped events
from other monitors through FIFO channels. Since
clocks are local, they cannot be perfectly
synchronized, resulting in imprecise timestamps.
Consequently, they must be seen as intervals,
leading monitors to consider possible reorderings of
events. In this context, each monitor aims to
provide, as early as possible, a verdict on the
property it is monitoring, based on its potentially
incomplete and imprecise knowledge of the current
execution. In this paper, we propose an on-line
monitoring algorithm for timed properties, robust to
time imprecision and partial information from
distant components. We first identify the date at
which a monitor can safely compute a verdict based
on received events. We then propose a monitoring
algorithm that updates this date when new
information arrives, maintains the current set of
states in which the property can reside, and updates
its verdict accordingly.
@inproceedings{rv2024-HJMR,
author = {Henry, L{\'e}o and J{\'e}ron, Thierry and Markey,
Nicolas and Roussanaly, Victor},
title = {Distributed Monitoring of Timed Properties},
editor = {{\'A}brah{\'a}m, Erikz and Abbas, Houssam},
booktitle = {{P}roceedings of the 24th {I}nternational {W}orkshop
on {R}untime {V}erification ({RV}'24)},
acronym = {{RV}'24},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {15191},
pages = {243-261},
year = {2024},
month = oct,
doi = {10.1007/978-3-031-74234-7_16},
abstract = {In formal verification, runtime monitoring consists
of observing the execution of a system in order to
decide as quickly as possible whether or not it
satisfies a given property. We consider monitoring
in a distributed setting, for properties given as
reachability timed automata. In~such a setting,
the~system is made of several components, each
equipped with its own local clock and monitor.
The~monitors observe events occurring on their
associated component, and receive timestamped events
from other monitors through FIFO channels. Since
clocks are local, they cannot be perfectly
synchronized, resulting in imprecise timestamps.
Consequently, they must be seen as intervals,
leading monitors to consider possible reorderings of
events. In this context, each monitor aims to
provide, as early as possible, a verdict on the
property it is monitoring, based on its potentially
incomplete and imprecise knowledge of the current
execution. In~this~paper, we~propose an on-line
monitoring algorithm for timed properties, robust to
time imprecision and partial information from
distant components. We~first identify the date at
which a monitor can safely compute a verdict based
on received events. We~then propose a monitoring
algorithm that updates this date when new
information arrives, maintains the current set of
states in which the property can reside, and updates
its verdict accordingly.},
}
We introduce a new class of automata (which we coin
EU-automata) running on infininte trees of
arbitrary (finite) arity. We develop and study
several algorithms to perform classical operations
(union, intersection, complement, projection,
alternation removal) for those automata, and
precisely characterise their complexities. We also
develop algorithms for solving membership and
emptiness for the languages of trees accepted by
EU-automata.
We then use EU-automata to obtain
several algorithmic and expressiveness results for
the temporal logic QCTL (which extends
CTL with quantification over atomic
propositions) and for MSO. On the one hand,
we obtain decision procedures with optimal
complexity for QCTL satisfiability and
model checking; on the other hand, we obtain an
algorithm for translating any QCTL formula
with k quantifier alternations to formulas with
at most one quantifier alternation, at the expense
of a (k+1)-exponential blow-up in the size of
the formulas. Using the same techniques, we prove
that any MSO formula can be translated into
a formula with at most four quantifier alternations
(and only two second-order-quantifier alternations),
again with a (k+1)-exponential blow-up in the
size of the formula.
@techreport{arxiv2410.18799-LM,
author = {Laroussinie, Fran{\c c}ois and Markey, Nicolas},
title = {Arbitrary-arity Tree Automata and QCTL},
number = {2410.18799},
year = {2024},
month = oct,
doi = {10.48550/arXiv.2410.18799},
institution = {arXiv},
abstract = {We~introduce a new class of automata (which we coin
\emph{EU-automata}) running on infininte trees of
arbitrary (finite) arity. We~develop and study
several algorithms to perform classical operations
(union, intersection, complement, projection,
alternation removal) for those automata, and
precisely characterise their complexities. We~also
develop algorithms for solving membership and
emptiness for the languages of trees accepted by
EU-automata. \par We~then use EU-automata to obtain
several algorithmic and expressiveness results for
the temporal logic \textsf{QCTL} (which extends
\textsf{CTL} with quantification over atomic
propositions) and for \textsf{MSO}. On the one hand,
we obtain decision procedures with optimal
complexity for \textsf{QCTL} satisfiability and
model checking; on the other hand, we obtain an
algorithm for translating any \textsf{QCTL} formula
with \(k\) quantifier alternations to formulas with
at most one quantifier alternation, at~the~expense
of a \((k+1)\)-exponential blow-up in the size of
the formulas. Using the same techniques, we~prove
that any \textsf{MSO} formula can be translated into
a formula with at most four quantifier alternations
(and only two second-order-quantifier alternations),
again with a \((k+1)\)-exponential blow-up in the
size of the formula.},
}
[Pra24]
AdityaPrakash.
Checking History-Determinism is NP-hard for Parity
Automata.
In FoSSaCS'24,
Lecture Notes in Computer Science 14574, pages 212-233. Springer-Verlag, April 2024.
We consider the automatic online synthesis of
black-box test cases from functional requirements
specified as automata for reactive implementations.
The goal of the tester is to reach some given state,
so as to satisfy a coverage criterion, while
monitoring the violation of the requirements. We
develop an approach based on Monte Carlo Tree
Search, which is a classical technique in
reinforcement learning for efficiently selecting
promising inputs. Seeing the automata requirements
as a game between the implementation and the tester,
we develop a heuristic by biasing the search towards
inputs that are promising in this game.
We experimentally show that our heuristic
accelerates the convergence of the Monte Carlo Tree
Search algorithm, thus improving the performance of
testing.
@techreport{2407.18994-SJMMN,
author = {Sankur, Ocan and J{\'e}ron, Thierry and Markey,
Nicolas and Mentr{\'e}, David and Noguchi, Reiya},
title = {Online Test Synthesis From Requirements: Enhancing
Reinforcement Learning with Game Theory},
number = {2407-18994},
year = {2024},
month = jul,
doi = {10.48550/arXiv.2407-18994},
institution = {arXiv},
abstract = {We consider the automatic online synthesis of
black-box test cases from functional requirements
specified as automata for reactive implementations.
The goal of the tester is to reach some given state,
so as to satisfy a coverage criterion, while
monitoring the violation of the requirements. We
develop an approach based on Monte~Carlo Tree
Search, which is a classical technique in
reinforcement learning for efficiently selecting
promising inputs. Seeing the automata requirements
as a game between the implementation and the tester,
we develop a heuristic by biasing the search towards
inputs that are promising in this game.
We~experimentally show that our heuristic
accelerates the convergence of the Monte~Carlo Tree
Search algorithm, thus improving the performance of
testing.},
}
Synchronizing a (deterministic, finite-state)
automaton is the problem of finding a sequence of
actions to be played in the automaton in order to
end up in the same state independently of the
starting state. We consider synchronization
with LTL constraints on the executions
leading to synchronization, extending the results
of [Petra Wolf. Synchronization under dynamic
constraints. FSTTCS'20] by showing that the problem
is PSPACE-complete for LTL as well
as for restricted fragments (involving only
modality F or G), while it is
NP-complete for constraints expressed using
only modality X.
@article{ipl182()-BFM,
author = {Bertrand, Nathalie and Francon, Hugo and Markey,
Nicolas},
title = {Synchronizing words under {LTL} constraints},
publisher = {Elsevier},
journal = {Information Processing Letters},
volume = {182},
year = {2023},
month = aug,
doi = {10.1016/j.ipl.2023.106392},
abstract = {Synchronizing a (deterministic, finite-state)
automaton is the problem of finding a sequence of
actions to be played in the automaton in order to
end up in the same state independently of the
starting state. We~consider synchronization
with~\textsf{LTL} constraints on the executions
leading to synchronization, extending the results
of~[Petra~Wolf. Synchronization under dynamic
constraints. FSTTCS'20] by~showing that the problem
is \textsf{PSPACE}-complete for~\textsf{LTL} as well
as for restricted fragments (involving only
modality~\textsf{F} or~\textsf{G}), while it is
\textsf{NP}-complete for constraints expressed using
only modality~\textsf{X}.},
}
Temporal logics are extensively used for the
specification of on-going behaviors of computer
systems. Two significant developments in this area
are the extension of traditional temporal logics
with modalities that enable the specification of
on-going strategic behaviors in multi-agent systems,
and the transition of temporal logics to a
quantitative setting, where different satisfaction
values enable the specifier to formalize concepts
such as certainty or quality. In the first class,
SL (Strategy Logic) is one of the most natural and
expressive logics describing strategic behaviors. In
the second class, a notable logic is
LTL[F], which extends
LTL with quality operators.
In this
work we introduce and study
SL[F], which enables the
specification of quantitative strategic behaviors.
The satisfaction value of an
SL[F] formula is a real value
in [0,1], reflecting "how much" or
"how well" the strategic on-going objectives of
the underlying agents are satisfied. We demonstrate
the applications of SL[F] in
quantitative reasoning about multi-agent systems,
showing how it can express and measure concepts like
stability in multi-agent systems, and how it
generalizes some fuzzy temporal logics. We also
provide a model-checking algorithm for
SL[F], based on a
quantitative extension of
Quantified CTL*. Our algorithm
provides the first decidability result for a
quantitative extension of Strategy Logic. In
addition, it can be used for synthesizing strategies
that maximize the quality of the systems' behavior
@article{tocl24(3)-BKMMMP,
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},
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
volume = {24},
number = {3},
pages = {21:1-21:38},
year = {2023},
month = jul,
doi = {10.1145/3582498},
abstract = {Temporal logics are extensively used for the
specification of on-going behaviors of computer
systems. Two significant developments in this area
are the extension of traditional temporal logics
with modalities that enable the specification of
on-going strategic behaviors in multi-agent systems,
and the transition of temporal logics to a
quantitative setting, where different satisfaction
values enable the specifier to formalize concepts
such as certainty or quality. In~the first class,
SL~(Strategy~Logic)~is one of the most natural and
expressive logics describing strategic behaviors. In
the second class, a notable logic is
\(\textsf{LTL}[\mathcal{F}]\), which extends
\textsf{LTL} with quality operators. \par In~this
work we introduce and study
\(\textsf{SL}[\mathcal{F}]\), which enables the
specification of quantitative strategic behaviors.
The satisfaction value of an
\(\textsf{SL}[\mathcal{F}]\) formula is a real value
in \([0,1]\), reflecting {"}how~much{"} or
{"}how~well{"} the strategic on-going objectives of
the underlying agents are satisfied. We demonstrate
the applications of \(\textsf{SL}[\mathcal{F}]\) in
quantitative reasoning about multi-agent systems,
showing how it can express and measure concepts like
stability in multi-agent systems, and how it
generalizes some fuzzy temporal logics. We also
provide a model-checking algorithm for
\(\textsf{SL}[\mathcal{F}]\), based on a
quantitative extension of
Quantified~\(\textsf{CTL}^*\). Our~algorithm
provides the first decidability result for a
quantitative extension of Strategy Logic. In
addition, it can be used for synthesizing strategies
that maximize the quality of the systems' behavior},
}
Network congestion games are a simple model for
reasoning about routing problems in a network. They
are a very popular topic in algorithmic game theory,
and a huge amount of results about existence and
(in)efficiency of equilibrium strategy profiles in
those games have been obtained over the last
20 years.
In particular, the price of anarchy
has been defined as an important notion for
measuring the inefficiency of Nash equilibria.
Generic bounds have been obtained for the price of
anarchy over various classes of networks, but little
attention has been put on the effective computation
of this value for a given network. This talk
presents recent results on this problem in different
settings.
@inproceedings{formats2023-Mar,
author = {Markey, Nicolas},
title = {Computing the price of anarchy in atomic network
congestion games (invited~talk)},
editor = {Petrucci, Laure and Sproston, Jeremy},
booktitle = {{P}roceedings of the 21st {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'23)},
acronym = {{FORMATS}'23},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {14138},
pages = {3-12},
year = {2023},
month = sep,
doi = {10.1007/978-3-031-42626-1_1},
abstract = {Network congestion games are a simple model for
reasoning about routing problems in a network. They
are a very popular topic in algorithmic game theory,
and a huge amount of results about existence and
(in)efficiency of equilibrium strategy profiles in
those games have been obtained over the last
20~years. \par In~particular, the price of anarchy
has been defined as an important notion for
measuring the inefficiency of Nash equilibria.
Generic bounds have been obtained for the price of
anarchy over various classes of networks, but little
attention has been put on the effective computation
of this value for a given network. This talk
presents recent results on this problem in different
settings.},
}
@patent{EP4064057B1,
author = {Noguchi, Reiya and J{\'e}ron, Thierry and Markey,
Nicolas and Sankur, Ocan},
title = {Method and system for correcting the operation of a
target computer system by using timed requirements},
number = {EP 4 064 057 B1},
year = {2023},
month = jul,
}
[AAB23]
ShaullAlmagor,
DanielAssa, and
UdiBoker.
Synchronized CTL over One-Counter Automata.
In FSTTCS'23,
Leibniz International Proceedings in Informatics 284, pages 19:1-19:22. Leibniz-Zentrum für Informatik, December 2023.
@inproceedings{fsttcs2023-AAB,
author = {Almagor, Shaull and Assa, Daniel and Boker, Udi},
title = {Synchronized {CTL} over One-Counter Automata},
editor = {Bouyer, Patricia and Srinivasan, Srikanth},
booktitle = {{P}roceedings of the 43rd {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'23)},
acronym = {{FSTTCS}'23},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {284},
pages = {19:1-19:22},
year = {2023},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2023.19},
}
@article{siglog-news35()-BL,
author = {Boker, Udi and Lehtinen, Karoliina},
title = {When a Little Nondeterminism Goes a Long Way: an
Introduction to History-Determinism},
publisher = {ACM Press},
journal = {SIGLOG News},
volume = {35},
pages = {24-51},
year = {2023},
month = jan,
}
@article{mathprog-CDS,
author = {Cominetti, Roberto and Dose, Valerio and Scarsini,
Marco},
title = {The~price of anarchy in routing games as a function
of the demand},
journal = {Mathematical Programming},
year = {2023},
doi = {10.1007/s10107-021-01701-7},
note = {To~appear},
}
@techreport{GoG-fij23,
author = {Fijalkow, Nathana{\"e}l and Bertrand, Nathalie and
Bouyer, Patricia and Brenguier, Romain and Carayol,
Arnaud and Fearnley, John and Gimbert, Hugo an Horn,
Florian and Ibsen{-}Jensen, Rasmus and Markey,
Nicolas and Monmege, Benjamin and Novotn{\'y}, Petr
and Randour, Mickael and Sankur, Ocan and Schmitz,
Sylvain and Serre, Olivier and Skomra, Mateusz},
title = {Games on graphs},
number = {2305.10546},
year = {2023},
month = may,
doi = {10.48550/arXiv.2305.10546},
institution = {arXiv},
}
@phdthesis{phd-ganguly,
author = {Ganguly, Ritam},
title = {Runtime verification of distributed systems},
year = {2023},
school = {Michigan State University, USA},
type = {{PhD} thesis},
}
[HK23]
ÉmileHazard and
DenisKuperberg.
Explorable automata.
In CSL'23,
Leibniz International Proceedings in Informatics 252, pages 24:1-24:18. Leibniz-Zentrum für Informatik, February 2023.
@article{mathprog199(1)-WMRX,
author = {Wu, Zijun and M{\"o}hring, Rolf H. and Ren, Chunying
and Xu, Dachaun},
title = {A~convergence analysis of the price of anarchy in
atomic congestion games},
journal = {Mathematical Programming},
volume = {199},
number = {1},
pages = {937-993},
year = {2023},
month = may,
doi = {10.1007/s10107-022-01853-0},
}
Partial observability and controllability are two
well-known issues in test-case synthesis for
reactive systems. We address the problem of partial
control in the synthesis of test cases from
timed-automata specifications. We extend a previous
approach to this problem from the untimed to the
timed setting. This extension requires a deep
reworking of the models, game interpretation and
test-synthesis algorithms. We exhibit strategies of
a game that try to minimize both cooperations of the
system and distance to the satisfaction of a test
purpose or to the next cooperation, and prove they
are winning under some fairness assumptions. This
entails that when turning those strategies into test
cases, we get properties such as soundness and
exhaustiveness of the test synthesis method. We
finally propose a symbolic algorithm to compute
those strategies.
@article{fmsd60(2)-HJM,
author = {Henry, L{\'e}o and J{\'e}ron, Thierry and Markey,
Nicolas},
title = {Control strategies for off-line testing of timed
systems},
publisher = {Springer-Verlag},
journal = {Formal Methods in System Design},
volume = {60},
number = {2},
pages = {147-194},
year = {2022},
month = apr,
doi = {10.1007/s10703-022-00403-w},
abstract = {Partial observability and controllability are two
well-known issues in test-case synthesis for
reactive systems. We address the problem of partial
control in the synthesis of test cases from
timed-automata specifications. We extend a previous
approach to this problem from the untimed to the
timed setting. This extension requires a deep
reworking of the models, game interpretation and
test-synthesis algorithms. We exhibit strategies of
a game that try to minimize both cooperations of the
system and distance to the satisfaction of a test
purpose or to the next cooperation, and prove they
are winning under some fairness assumptions. This
entails that when turning those strategies into test
cases, we get properties such as soundness and
exhaustiveness of the test synthesis method. We
finally propose a symbolic algorithm to compute
those strategies.},
}
We study games with reachability objectives under
energy constraints. We first prove that under strict
energy constraints (either only lower-bound
constraint or interval constraint), those games are
LOGSPACE-equivalent to energy games with the same
energy constraints but without reachability
objective (i.e., for infinite runs). We then
consider two relaxations of the upper-bound
constraints (while keeping the lower-bound
constraint strict): in the first one, called weak
upper bound, the upper bound is absorbing, i.e.,
when the upper bound is reached, the extra energy is
not stored; in the second one, we allow for
temporary violations of the upper bound, imposing
limits on the number or on the amount of violations.
We prove that when considering weak upper
bound, reachability objectives require memory, but
can still be solved in polynomial-time for
one-player arenas; we prove that they are in NP in
the two-player setting. Allowing for bounded
violations makes the problem PSPACE-complete for
one-player arenas and EXPTIME-complete for two
players. We then address the problem of existence of
bounds for a given arena. We show that with
reachability objectives, existence can be a simpler
problem than the game itself, and conversely that
with infinite games, existence can be harder.
@article{icomp2022-HMR,
author = {H{\'e}lou{\"e}t, Lo{\"\i}c and Markey, Nicolas and
Raha, Ritam},
title = {Reachability games with relaxed energy constraints},
publisher = {Elsevier},
journal = {Information and Computation},
volume = {285~(Part~B)},
year = {2022},
month = may,
doi = {10.1016/j.ic.2021.104806},
abstract = {We study games with reachability objectives under
energy constraints. We first prove that under strict
energy constraints (either only lower-bound
constraint or interval constraint), those games are
LOGSPACE-equivalent to energy games with the same
energy constraints but without reachability
objective (i.e., for infinite runs). We then
consider two relaxations of the upper-bound
constraints (while keeping the lower-bound
constraint strict): in the first one, called weak
upper bound, the upper bound is absorbing, i.e.,
when the upper bound is reached, the extra energy is
not stored; in the second one, we allow for
temporary violations of the upper bound, imposing
limits on the number or on the amount of violations.
\par We prove that when considering weak upper
bound, reachability objectives require memory, but
can still be solved in polynomial-time for
one-player arenas; we prove that they are in NP in
the two-player setting. Allowing for bounded
violations makes the problem PSPACE-complete for
one-player arenas and EXPTIME-complete for two
players. We then address the problem of existence of
bounds for a given arena. We show that with
reachability objectives, existence can be a simpler
problem than the game itself, and conversely that
with infinite games, existence can be harder.},
}
We consider atomic congestion games on
series-parallel networks, and study the structure of
the sets of Nash equilibria and social local optima
on a given network when the number of players
varies. We establish that these sets are definable
in Presburger arithmetic and that they admit
semilinear representations whose all period vectors
have a common direction. As an application, we prove
that the prices of anarchy and stability converge
to 1 as the number of players goes to infinity, and
show how to exploit these semilinear representations
to compute these ratios precisely for a given
network and number of players.
@inproceedings{fsttcs2022-BMSS,
author = {Bertrand, Nathalie and Markey, Nicolas and
Sadhukhan, Suman and Sankur, Ocan},
title = {Semilinear Representations for Series-Parallel
Atomic Congestion Games},
editor = {Dawar, Anuj and Guruswami, Venkatesan},
booktitle = {{P}roceedings of the 42nd {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'22)},
acronym = {{FSTTCS}'22},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {250},
pages = {32:1-32:20},
year = {2022},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2022.32},
abstract = {We~consider atomic congestion games on
series-parallel networks, and study the structure of
the sets of Nash equilibria and social local optima
on a given network when the number of players
varies. We establish that these sets are definable
in Presburger arithmetic and that they admit
semilinear representations whose all period vectors
have a common direction. As~an~application, we~prove
that the prices of anarchy and stability converge
to~1 as the number of players goes to infinity, and
show how to exploit these semilinear representations
to compute these ratios precisely for a given
network and number of players.},
}
We consider the parameterized verification problem
for distributed algorithms where the goal is to
develop techniques to prove the correctness of a
given algorithm regardless of the number of
participating processes. Motivated by an
asynchronous binary consensus algorithm of
[J. Aspnes; Fast deterministic consensus in a noisy
environment; J. Algorithms, 2002], we consider
round-based distributed algorithms communicating
with shared memory. A particular challenge in these
systems is that 1) the number of processes is
unbounded, and, more importantly, 2) there is a
fresh set of registers at each round. A verification
algorithm thus needs to manage both sources of
infinity. In this setting, we prove that the safety
verification problem, which consists in deciding
whether all possible executions avoid a given error
state, is PSPACE-complete. For negative instances of
the safety verification problem, we also provide
exponential lower and upper bounds on the minimal
number of processes needed for an error execution
and on the minimal round on which the error state
can be covered.
@inproceedings{icalp2022-BMSW,
author = {Bertrand, Nathalie and Markey, Nicolas and Sankur,
Ocan and Waldburger, Nicolas},
title = {Parameterized safety verification of round-based
shared-memory systems},
editor = {Woodruff, David and Boja{\'n}czyk, Miko{\l}aj},
booktitle = {{P}roceedings of the 49th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'22)},
acronym = {{ICALP}'22},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
pages = {113:1-113:20},
year = {2022},
month = jul,
doi = {10.4230/LIPIcs.ICALP.2022.113},
abstract = {We consider the parameterized verification problem
for distributed algorithms where the goal is to
develop techniques to prove the correctness of a
given algorithm regardless of the number of
participating processes. Motivated by an
asynchronous binary consensus algorithm~of
[J.~Aspnes; Fast deterministic consensus in a noisy
environment; J.~Algorithms,~2002], we~consider
round-based distributed algorithms communicating
with shared memory. A~particular challenge in these
systems is that 1)~the~number of processes is
unbounded, and, more importantly, 2)~there is a
fresh set of registers at each round. A~verification
algorithm thus needs to manage both sources of
infinity. In~this setting, we~prove that the safety
verification problem, which consists in deciding
whether all possible executions avoid a given error
state, is PSPACE-complete. For~negative instances of
the safety verification problem, we~also provide
exponential lower and upper bounds on the minimal
number of processes needed for an error execution
and on the minimal round on which the error state
can be covered.},
}
A chronicle is a temporal model introduced by
Dousson et al. for situation recognition.
In short, a chronicle consists of a set of events
and a set of real-valued temporal constraints on the
delays between pairs of events. This work
investigates the relationship between chronicles and
classical temporal model formalisms, namely
TPTL and MTL. More specifically,
we answer the following question: is it possible to
find an equivalent formula in such formalisms for
any chronicle? This question arises from the
observation that a single chronicle captures complex
temporal behaviours that do not order the events in
time.
In this article, we introduce the subclass
of linear chronicles, which defines a temporal order
of occurrence of the event to be recognized in a
temporal sequence. Our first result is that any
chronicle can be expressed as a disjunction of
linear chronicles. Our second result is that any
linear chronicle has an equivalent TPTL
formula. Using existing expressiveness results
between TPTL and MTL, we show that
some chronicles have no equivalent in MTL.
This confirms that the model of chronicle has
interesting properties for situation recognition.
@inproceedings{time2022-GM,
author = {Guyet, {\relax Th}omas and Markey, Nicolas},
title = {Logical forms of chronicles},
editor = {Artikis, Alexander and Posenato, Roberto and
Tonetta, Stefano},
booktitle = {{P}roceedings of the 29th {I}nternational
{S}ymposium on {T}emporal {R}epresentation and
{R}easoning ({TIME}'22)},
acronym = {{TIME}'22},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
pages = {7:1-7:15},
year = {2022},
month = nov,
doi = {10.4230/LIPIcs.TIME.2022.7},
abstract = {A~chronicle is a temporal model introduced by
Dousson~\textit{et~al.} for situation recognition.
In~short, a chronicle consists of a set of events
and a set of real-valued temporal constraints on the
delays between pairs of events. This~work
investigates the relationship between chronicles and
classical temporal model formalisms, namely
\textsf{TPTL} and~\textsf{MTL}. More~specifically,
we~answer the following question: is~it possible to
find an equivalent formula in such formalisms for
any chronicle? This~question arises from the
observation that a single chronicle captures complex
temporal behaviours that do not order the events in
time.\par In~this article, we~introduce the subclass
of linear chronicles, which defines a temporal order
of occurrence of the event to be recognized in a
temporal sequence. Our~first result is that any
chronicle can be expressed as a disjunction of
linear chronicles. Our~second result is that any
linear chronicle has an equivalent \textsf{TPTL}
formula. Using existing expressiveness results
between \textsf{TPTL} and~\textsf{MTL}, we~show that
some chronicles have no equivalent in~\textsf{MTL}.
This confirms that the model of chronicle has
interesting properties for situation recognition.},
}
Network congestion games are a convenient model for
reasoning about routing problems in a network:
agents have to move from a source to a target vertex
while avoiding congestion, measured as a cost
depending on the number of players using the same
link. Network congestion games have been extensively
studied over the last 40 years, while their
extension with timing constraints were considered
more recently.
Most of the results on network
congestion games consider blind strategies: they are
static, and do not adapt to the strategies selected
by the other players. We extend the recent results
of [Bertrand et al., Dynamic network
congestion games. FSTTCS'20] to timed network
congestion games, in which the availability of the
edges depend on (discrete) time. We prove that
computing Nash equilibria satisfying some constraint
on the total cost (and in particular, computing the
best and worst Nash equilibria), and computing the
social optimum, can be achieved in exponential
space. The social optimum can be computed in
polynomial space if all players have the same source
and target.
@inproceedings{formats2022-GMS,
author = {Goeminne, Aline and Markey, Nicolas and Sankur,
Ocan},
title = {Non-Blind Strategies in Timed Network Congestion
Games},
editor = {Bogomolov, Sergiy and Parker, David},
booktitle = {{P}roceedings of the 20th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'22)},
acronym = {{FORMATS}'22},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {13465},
pages = {183-199},
year = {2022},
month = sep,
doi = {10.1007/978-3-031-15839-1_11},
abstract = {Network congestion games are a convenient model for
reasoning about routing problems in a network:
agents have to move from a source to a target vertex
while avoiding congestion, measured as a cost
depending on the number of players using the same
link. Network congestion games have been extensively
studied over the last 40 years, while their
extension with timing constraints were considered
more recently. \par Most of the results on network
congestion games consider blind strategies: they are
static, and do not adapt to the strategies selected
by the other players. We extend the recent results
of [Bertrand~\textit{et~al.}, Dynamic network
congestion games. FSTTCS'20] to timed network
congestion games, in which the availability of the
edges depend on (discrete) time. We prove that
computing Nash equilibria satisfying some constraint
on the total cost (and in particular, computing the
best and worst Nash equilibria), and computing the
social optimum, can be achieved in exponential
space. The social optimum can be computed in
polynomial space if all players have the same source
and target.},
}
We consider the problem of repairing inconsistent
real-time requirements with respect to two
consistency notions: non-vacuity, which means that
each requirement can be realized without violating
other ones, and rt-consistency, which means that
inevitable violations are detected immediately.
We provide an iterative algorithm, based on solving
SMT queries, to replace designated parameters of
real-time requirements with new Boolean expressions
and time constraints, so that the resulting set of
requirements becomes consistent.
@inproceedings{atva2022-NSJMM,
author = {Noguchi, Reiya and Sankur, Ocan and J{\'e}ron,
Thierry and Markey, Nicolas and Mentr{\'e}, David},
title = {Repairing Real-Time Requirements},
editor = {Bouajjani, Ahmed and Hol{\'\i}k, Luk{\'a}{\v s} and
Wu, Zhilin},
booktitle = {{P}roceedings of the 20th {I}nternational
{S}ymposium on {A}utomated {T}echnology for
{V}erification and {A}nalysis ({ATVA}'22)},
acronym = {{ATVA}'22},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {13505},
pages = {371-387},
year = {2022},
month = oct,
doi = {10.1007/978-3-031-19992-9_24},
abstract = {We~consider the problem of repairing inconsistent
real-time requirements with respect to two
consistency notions: non-vacuity, which means that
each requirement can be realized without violating
other ones, and rt-consistency, which means that
inevitable violations are detected immediately.
We~provide an iterative algorithm, based on solving
SMT queries, to replace designated parameters of
real-time requirements with new Boolean expressions
and time constraints, so that the resulting set of
requirements becomes consistent.},
}
@patent{EP3907615B1,
author = {Noguchi, Reiya and J{\'e}ron, Thierry and Markey,
Nicolas and Sankur, Ocan},
title = {Method and system for testing the operation of a
target computer system by using timed requirements},
number = {EP 3 907 615 B1},
year = {2022},
month = nov,
}
[BHL+22]
SougataBose,
Thomas A.Henzinger,
KaroliinaLehtinen,
SvenSchewe, and
PatrickTotzke.
History-deterministic timed automata are not
determinizable.
In RP'22,
Lecture Notes in Computer Science 13608, pages 67-76. Springer-Verlag, October 2022.
@inproceedings{rp2022-BHLST,
author = {Bose, Sougata and Henzinger, Thomas A. and Lehtinen,
Karoliina and Schewe, Sven and Totzke, Patrick},
title = {History-deterministic timed automata are not
determinizable},
editor = {Lin, Anthony W. and Zetzsche, Georg and Potapov,
Igor},
booktitle = {{P}roceedings of the 16th {W}orkshop on
{R}eachability {P}roblems in {C}omputational
{M}odels ({RP}'22)},
acronym = {{RP}'22},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {13608},
pages = {67-76},
year = {2022},
month = oct,
doi = {10.1007/978-3-031-19135-0_5},
}
@inproceedings{fossacs2022-BL,
author = {Boker, Udi and Lehtinen, Karoliina},
title = {Token Games and History-Deterministic Quantitative
Automata},
editor = {Bouyer, Patricia and Schr{\"o}der, Lutz},
booktitle = {{P}roceedings of the 25th {I}nternational
{C}onference on {F}oundations of {S}oftware
{S}cience and {C}omputation {S}tructure
({FoSSaCS}'22)},
acronym = {{FoSSaCS}'22},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {13242},
pages = {120-139},
year = {2022},
month = apr,
doi = {10.1007/978-3-030-99253-8_7},
}
@inproceedings{fossacs2022-BLS,
author = {Boker, Udi and Lehtinen, Karoliina and Sickert,
Salomon},
title = {On the Translation of Automata to Linear Temporal
Logic},
editor = {Bouyer, Patricia and Schr{\"o}der, Lutz},
booktitle = {{P}roceedings of the 25th {I}nternational
{C}onference on {F}oundations of {S}oftware
{S}cience and {C}omputation {S}tructure
({FoSSaCS}'22)},
acronym = {{FoSSaCS}'22},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {13242},
pages = {140-160},
year = {2022},
month = apr,
doi = {10.1007/978-3-030-99253-8_8},
}
[HLT22]
Thomas A.Henzinger,
KaroliinaLehtinen, and
PatrickTotzke.
History-deterministic timed automata.
In CONCUR'22,
Leibniz International Proceedings in Informatics 243, pages 14:1-14:21. Leibniz-Zentrum für Informatik, September 2022.
@inproceedings{concur2022-HLT,
author = {Henzinger, Thomas A. and Lehtinen, Karoliina and
Totzke, Patrick},
title = {History-deterministic timed automata},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl,
Anca},
booktitle = {{P}roceedings of the 33rd {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'22)},
acronym = {{CONCUR}'22},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {243},
pages = {14:1-14:21},
year = {2022},
month = sep,
doi = {10.4230/LIPIcs.CONCUR.2022.14},
}
@inproceedings{wine2022-HM,
author = {Hao, Bainian and Michini, Carla},
title = {Inefficiency of Pure Nash Equilibria in
Series-Parallel Network Congestion Games},
editor = {Hansen, Kristoffer Arnsfelt and Liu, Tracy Xiao and
Malekian, Azarakhsh},
booktitle = {{P}roceedings of the 18th {I}nternational
{C}onference on {W}eb and {I}nternet {E}conomics
({WINE}'22)},
acronym = {{WINE}'22},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {13778},
pages = {3-20},
year = {2022},
month = jul,
doi = {10.1007/978-3-031-22832-2_1},
}
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{fac2020-BBFLMR,
author = {Bacci, Giovanni and Bouyer, Patricia and Fahrenberg,
Uli and Larsen, Kim Guldstrand and Markey, Nicolas
and Reynier, Pierre-Alain},
title = {Optimal and Robust Controller Synthesis Using Energy
Timed Automata with Uncertainty},
publisher = {Springer-Verlag},
journal = {Formal Aspects of Computing},
volume = {33},
number = {1},
pages = {3-25},
year = {2021},
month = jan,
doi = {10.1007/s00165-020-00521-4},
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.},
}
We consider the problems of efficiently diagnosing
(and predicting) what did (and will) happen after a
given sequence of observations of the execution of a
partially-observable one-clock timed automaton. This
is made difficult by the facts that timed automata
are infinite-state systems, and that they can in
general not be determinized.
We introduce timed
markings as a formalism to keep track of the
evolution of the set of reachable configurations
over time. We show how timed markings can be used to
efficiently represent the closure under silent
transitions of such automata. We report on our
implementation of this approach compared to the
approach of [Tripakis, Fault diagnosis for timed
automata, 2002], and provide some insight to a
generalization of our approach to n-clock
timed automata.
@article{sttt23(2)-BHJJM,
author = {Bouyer, Patricia and Henry, L{\'e}o and Jaziri, Samy
and J{\'e}ron, Thierry and Markey, Nicolas},
title = {Diagnosing timed automata using timed markings},
publisher = {Springer-Verlag},
journal = {International Journal on Software Tools for
Technology Transfer},
volume = {23},
number = {2},
pages = {229-253},
year = {2021},
month = apr,
doi = {10.1007/s10009-021-00606-2},
abstract = {We~consider the problems of efficiently diagnosing
(and~predicting) what did (and~will) happen after a
given sequence of observations of the execution of a
partially-observable one-clock timed automaton. This
is made difficult by the facts that timed automata
are infinite-state systems, and that they can in
general not be determinized. \par We~introduce timed
markings as a formalism to keep track of the
evolution of the set of reachable configurations
over time. We show how timed markings can be used to
efficiently represent the closure under silent
transitions of such automata. We report on our
implementation of this approach compared to the
approach of [Tripakis, Fault diagnosis for timed
automata,~2002], and provide some insight to a
generalization of our approach to {{\(n\)}}-clock
timed automata.},
}
[AZZ+21]
JieAn,
BohuaZhan,
NaijunZhan, and
MiaomiaoZhang.
Learning nondeterministic real-time automata.
ACM Transactions on Embedded Computing Systems 20(5s):99:1-99:26. ACM Press, October 2021.
@article{tocl22(1)-BFFGMMPPRS,
author = {Berthon, Rapha{\"e}l and Fijalkow, Nathana{\"e}l and
Filiot, Emmanuel and Guha, Shibashis and Maubert,
Bastien and Murano, Aniello and Pinault, Laureline
and Pinchinat, Sophie and Rubin, Sasha and Serre,
Olivier},
title = {Alternating Tree Automata with Qualitative
Semantics},
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
volume = {22},
number = {1},
pages = {7:1-7:24},
year = {2021},
month = jan,
doi = {10.1145/3431860},
}
@inproceedings{fsttcs2021-BK,
author = {Boker, Udi and Lehtinen, Karoliina},
title = {History Determinism vs.~Good for Gameness in
Quantitative Automata},
editor = {Boja{\'n}czyk, Miko{\l}aj and Chekuri, Chandra},
booktitle = {{P}roceedings of the 41st {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'21)},
acronym = {{FSTTCS}'21},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {213},
pages = {38:1-38:20},
year = {2021},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2021.38},
}
[Lod21]
ChristofLöding.
Automata on infinite trees.
In Jean-ÉricPin (eds.),
Handbook of automata theory.
EMS Press, 2021.
@incollection{hat-ch8,
author = {L{\"o}ding, Christof},
title = {Automata on infinite trees},
editor = {Pin, Jean-{\'E}ric},
booktitle = {Handbook of automata theory},
publisher = {EMS~Press},
volume = {1},
pages = {265-302},
chapter = {8},
year = {2021},
doi = {10.4171/AUTOMATA-1/8},
}
[MPS+21]
BastienMaubert,
SophiePinchinat,
FrançoisSchwarzentruber, and
SilviaStranieri.
Concurrent Games in Dynamic Epistemic Logic.
In IJCAI'20,
pages 1877-1883.
IJCAI organization, January 2021.
@inproceedings{ijcai2020-MPSS,
author = {Maubert, Bastien and Pinchinat, Sophie and
Schwarzentruber, Fran{\c c}ois and Stranieri,
Silvia},
title = {Concurrent Games in Dynamic Epistemic Logic},
editor = {Bessiere, Christian},
booktitle = {{P}roceedings of the 29th {I}nternational {J}oint
{C}onference on {A}rtificial {I}ntelligence
({IJCAI}'20)},
acronym = {{IJCAI}'20},
publisher = {IJCAI organization},
pages = {1877-1883},
year = {2021},
month = jan,
doi = {10.24963/ijcai.2020/260},
}
[Pin21]
Jean-ÉricPin.
Handbook of automata theory.
EMS Press, 2021.
@inproceedings{sbmf2021-SK,
author = {Saeedloei, Neda and Klu{\'z}niak, Feliks},
title = {Minimization of the Number of Clocks for Timed
Scenarios},
editor = {Campos, S{\'e}rgio Vale Aguiar and Minea, Marius},
booktitle = {{P}roceedings of the24th {B}razilian {S}ymposium on
{F}ormal {M}ethods ({SBMF}'21)},
acronym = {{SBMF}'21},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {13130},
pages = {122-139},
year = {2021},
confmonth = {12},
doi = {10.1007/978-3-030-92137-8_8},
}
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 with the same set of traces? We show that these
problems are undecidable both for general PTA and
for the restricted class of L/U-PTA, even for
integer-valued parameters, or over bounded time.
On the other hand, we exhibit decidable subclasses:
1-clock PTA, and 1-parameter deterministic L-PTA and
U-PTA. We also consider robust versions of these
problems, where we additionally require that the
language be preserved for all valuations between the
reference valuation and the new valuation.
@article{lmcs16(1)-ALM,
author = {Andr{\'e}, {\'E}tienne and Lime, Didier and Markey,
Nicolas},
title = {Language-preservation problems in parametric timed
automata},
journal = {Logical Methods in Computer Science},
volume = {16},
number = {1},
year = {2020},
month = jan,
doi = {10.23638/LMCS-16(1:5)2020},
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 with the same set of traces? We~show that these
problems are undecidable both for general PTA and
for the restricted class of L{\slash}U-PTA, even for
integer-valued parameters, or over bounded time.
On~the other~hand, we~exhibit decidable subclasses:
1-clock PTA, and 1-parameter deterministic L-PTA and
U-PTA. We~also consider robust versions of these
problems, where we additionally require that the
language be preserved for all valuations between the
reference valuation and the new valuation.},
}
Strategy Logic (SL) is a very expressive
temporal logic for specifying and verifying
properties of multi-agent systems: in SL,
one can quantify over strategies, assign them to
agents, and express LTL 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, revisiting the approach of [Mogavero
et al., Reasoning about strategies: On the
model-checking problem, 2014]. We explain why
elementary dependences, as defined by
Mogavero et al., do not exactly capture the
intended concept of behavioral strategies.
We address this discrepancy by introducing
timeline dependences, and exhibit a large
fragment of SL for which model checking can
be performed in 2EXPTIME under this new
semantics.
@article{tocsys64(3)-GBM,
author = {Gardy, Patrick and Bouyer, Patricia and Markey,
Nicolas},
title = {Dependences in Strategy Logic},
publisher = {Springer-Verlag},
journal = {Theory of Computing Systems},
volume = {64},
number = {3},
pages = {467-507},
year = {2020},
month = apr,
doi = {10.1007/s00224-019-09926-y},
abstract = {Strategy Logic~(\textsf{SL}) is a very expressive
temporal logic for specifying and verifying
properties of multi-agent systems: in~\textsf{SL},
one can quantify over strategies, assign them to
agents, and express \textsf{LTL} properties of the
resulting plays. Such a powerful framework has two
drawbacks: first, model checking \textsf{SL} has
non-elementary complexity; second, the exact
semantics of \textsf{SL} is rather intricate, and
may not correspond to what is expected. In~this
paper, we~focus on \emph{strategy dependences}
in~\textsf{SL}, by tracking how
existentially-quantified strategies in a formula may
(or~may~not) depend on other strategies selected in
the formula, revisiting the approach of~[Mogavero
\emph{et~al.}, Reasoning about strategies: On~the
model-checking problem,~2014]. We~explain why
\emph{elementary} dependences, as defined by
Mogavero~\emph{et~al.}, do not exactly capture the
intended concept of behavioral strategies.
We~address this discrepancy by introducing
\emph{timeline} dependences, and exhibit a large
fragment of \textsf{SL} for which model checking can
be performed in \textsf{2EXPTIME} under this new
semantics.},
}
Congestion games are a classical type of games
studied in game theory, in which n players choose a
resource, and their individual cost increases with
the number of other players choosing the same
resource. In network congestion games (NCGs), the
resources correspond to simple paths in a graph,
e.g. representing routing options from a source to a
target. In this paper, we introduce a variant
of NCGs, referred to as dynamic NCGs: in this
setting, players take transitions synchronously,
they select their next transitions dynamically, and
they are charged a cost that depends on the number
of players simultaneously using the same transition.
We study, from a complexity perspective,
standard concepts of game theory in dynamic NCGs:
social optima, Nash equilibria, and subgame perfect
equilibria. Our contributions are the following: the
existence of a strategy profile with social cost
bounded by a constant is in PSPACE and NP-hard.
(Pure) Nash equilibria always exist in dynamic NCGs;
the existence of a Nash equilibrium with bounded
cost can be decided in EXPSPACE, and computing a
witnessing strategy profile can be done in
doubly-exponential time. The existence of a subgame
perfect equilibrium with bounded cost can be decided
in 2EXPSPACE, and a witnessing strategy profile can
be computed in triply-exponential time.
@inproceedings{fsttcs2020-BMSS,
author = {Bertrand, Nathalie and Markey, Nicolas and
Sadhukhan, Suman and Sankur, Ocan},
title = {Dynamic network congestion games},
editor = {Saxena, Nitin and Simon, Sunil},
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)},
acronym = {{FSTTCS}'20},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {182},
pages = {40:1-40:16},
year = {2020},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2020.40},
abstract = {Congestion games are a classical type of games
studied in game theory, in which n players choose a
resource, and their individual cost increases with
the number of other players choosing the same
resource. In network congestion games~(NCGs), the
resources correspond to simple paths in a graph,
e.g.~representing routing options from a source to a
target. In this paper, we introduce a variant
of~NCGs, referred to as dynamic~NCGs: in~this
setting, players take transitions synchronously,
they select their next transitions dynamically, and
they are charged a cost that depends on the number
of players simultaneously using the same transition.
\par We~study, from a complexity perspective,
standard concepts of game theory in dynamic NCGs:
social optima, Nash equilibria, and subgame perfect
equilibria. Our contributions are the following: the
existence of a strategy profile with social cost
bounded by a constant is in PSPACE and NP-hard.
(Pure)~Nash equilibria always exist in dynamic~NCGs;
the existence of a Nash equilibrium with bounded
cost can be decided in EXPSPACE, and computing a
witnessing strategy profile can be done in
doubly-exponential time. The~existence of a subgame
perfect equilibrium with bounded cost can be decided
in 2EXPSPACE, and a witnessing strategy profile can
be computed in triply-exponential~time.},
}
Timed automata are a convenient mathematical model
for modelling and reasoning about real-time systems.
While they provide a powerful way of representing
timing aspects of such systems, timed automata
assume arbitrary precision and zero-delay actions;
in particular, a state might be declared reachable
in a timed automaton, but impossible to reach in the
physical system it models.
In this paper, we
consider permissive strategies as a way to overcome
this problem: such strategies propose intervals of
delays instead of single delays, and aim at reaching
a target state whichever delay actually takes place.
We develop an algorithm for computing the optimal
permissiveness (and an associated
maximally-permissive strategy) in acyclic timed
automata and games.
@inproceedings{formats2020-CJMM,
author = {Clement, Emily and J{\'e}ron, Thierry and Markey,
Nicolas and Mentr{\'e}, David},
title = {Computing maximally-permissive strategies in acyclic
timed automata},
editor = {Bertrand, Nathalie and Jansen, Nils},
booktitle = {{P}roceedings of the 18th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'20)},
acronym = {{FORMATS}'20},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {12288},
pages = {111-126},
year = {2020},
month = sep,
doi = {10.1007/978-3-030-57628-8_7},
abstract = {Timed automata are a convenient mathematical model
for modelling and reasoning about real-time systems.
While they provide a powerful way of representing
timing aspects of such systems, timed automata
assume arbitrary precision and zero-delay actions;
in~particular, a~state might be declared reachable
in a timed automaton, but impossible to reach in the
physical system it models. \par In this paper, we
consider permissive strategies as a way to overcome
this problem: such strategies propose intervals of
delays instead of single delays, and aim at reaching
a target state whichever delay actually takes place.
We develop an algorithm for computing the optimal
permissiveness (and~an associated
maximally-permissive strategy) in acyclic timed
automata and games.},
}
Active learning of timed languages is concerned with
the inference of timed automata by observing some of
the timed words in their languages. The learner can
query for the membership of words in the language,
or propose a candidate model and ask if it is
equivalent to the target. The major difficulty of
this framework is the inference of clock resets,
which are central to the dynamics of timed automata
but not directly observable.
Interesting first
steps have already been made by restricting to the
subclass of event-recording automata, where clock
resets are tied to observations. In order to advance
towards learning of general timed automata, we
generalize this method to a new class, called
reset-free event-recording automata, where some
transitions may reset no clocks.
Central to our
contribution is the notion of invalidity, and the
algorithm and data structures to deal with it,
allowing on-the-fly detection and pruning of reset
hypotheses that contradict observations. This notion
is a key to any efficient active-learning procedure
for generic timed automata.
@inproceedings{formats2020-HJM,
author = {Henry, L{\'e}o and J{\'e}ron, Thierry and Markey,
Nicolas},
title = {Active learning of timed automata with unobservable
resets},
editor = {Bertrand, Nathalie and Jansen, Nils},
booktitle = {{P}roceedings of the 18th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'20)},
acronym = {{FORMATS}'20},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {12288},
pages = {144-160},
year = {2020},
month = sep,
doi = {10.1007/978-3-030-57628-8_9},
abstract = {Active learning of timed languages is concerned with
the inference of timed automata by observing some of
the timed words in their languages. The learner can
query for the membership of words in the language,
or propose a candidate model and ask if it is
equivalent to the target. The major difficulty of
this framework is the inference of clock resets,
which are central to the dynamics of timed automata
but not directly observable. \par Interesting first
steps have already been made by restricting to the
subclass of event-recording automata, where clock
resets are tied to observations. In order to advance
towards learning of general timed automata, we
generalize this method to a new class, called
reset-free event-recording automata, where some
transitions may reset no clocks. \par Central to our
contribution is the notion of invalidity, and the
algorithm and data structures to deal with it,
allowing on-the-fly detection and pruning of reset
hypotheses that contradict observations. This notion
is a key to any efficient active-learning procedure
for generic timed automata.},
}
Requirements engineering is a key phase in the
development process. Ensuring that requirements are
consistent is essential so that they do not conflict
and admit implementations. We consider the formal
verification of rt-consistency, which imposes that
the inevitability of definitive errors of a
requirement should be anticipated, and that of
partial consistency, which was recently introduced
as a more effective check. We generalize and
formalize both notions for discrete-time timed
automata, develop three incremental algorithms, and
present experimental results.
@inproceedings{formats2020-JMMNS,
author = {J{\'e}ron, Thierry and Markey, Nicolas and
Mentr{\'e}, David and Noguchi, Reiya and Sankur,
Ocan},
title = {Incremental methods for checking real-time
consistency},
editor = {Bertrand, Nathalie and Jansen, Nils},
booktitle = {{P}roceedings of the 18th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'20)},
acronym = {{FORMATS}'20},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {12288},
pages = {249-264},
year = {2020},
month = sep,
doi = {10.1007/978-3-030-57628-8_15},
abstract = {Requirements engineering is a key phase in the
development process. Ensuring that requirements are
consistent is essential so that they do not conflict
and admit implementations. We~consider the formal
verification of rt-consistency, which imposes that
the inevitability of definitive errors of a
requirement should be anticipated, and that of
partial consistency, which was recently introduced
as a more effective check. We~generalize and
formalize both notions for discrete-time timed
automata, develop three incremental algorithms, and
present experimental results.},
}
[ACZ+20]
JieAn,
MingshuaiChen,
BohuaZhan,
NaijunZhan, and
MiaomiaoZhang.
Learning One-Clock Timed Automata.
In TACAS'20 (Part I),
Lecture Notes in Computer Science 12078, pages 444-462. Springer-Verlag, April 2020.
@inproceedings{tacas2020-ACZZZ,
author = {An, Jie and Chen, Mingshuai and Zhan, Bohua and
Zhan, Naijun and Zhang, Miaomiao},
title = {Learning One-Clock Timed Automata},
editor = {Biere, Armin and Parker, David},
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)~-- {P}art~{I}},
acronym = {{TACAS}'20 (Part~{I})},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {12078},
pages = {444-462},
year = {2020},
month = apr,
doi = {10.1007/978-3-030-45190-5_25},
}
[AHK20]
GuyAvni,
Thomas A.Henzinger, and
OrnaKupferman.
Dynamic Resource Allocation Games.
Theoretical Computer Science 807:42-55. Elsevier, February 2020.
@article{tcs807()-AHK,
author = {Avni, Guy and Henzinger, Thomas A. and Kupferman,
Orna},
title = {Dynamic Resource Allocation Games},
publisher = {Elsevier},
journal = {Theoretical Computer Science},
volume = {807},
pages = {42-55},
year = {2020},
month = feb,
doi = {10.1016/j.tcs.2019.06.031},
}
[AMP+20]
GalAmram,
ShaharMaoz,
OrPistiner, and
Jan OliverRingert.
Energy μ-Calculus: Symbolic Fixed-Point
Algorithms for ω-Regular Energy Games.
Technical Report 2005.00641, arXiv, May 2020.
@techreport{arxiv-AMPR,
author = {Amram, Gal and Maoz, Shahar and Pistiner, Or and
Ringert, Jan Oliver},
title = {Energy {{\(\mu\)}}-Calculus: Symbolic Fixed-Point
Algorithms for {{\(\omega\)}}-Regular Energy Games},
number = {2005.00641},
year = {2020},
month = may,
institution = {arXiv},
}
[BFF+20]
RaphaëlBerthon,
NathanaëlFijalkow,
EmmanuelFiliot,
ShibashisGuha,
BastienMaubert,
AnielloMurano,
LaurelinePinault,
SophiePinchinat,
SashaRubin, and
OlivierSerre.
Alternating Tree Automata with Qualitative
Semantics.
Technical Report 2002-03664, arXiv, February 2020.
@techreport{arxiv2002.03664-BFFGMMPPRS,
author = {Berthon, Rapha{\"e}l and Fijalkow, Nathana{\"e}l and
Filiot, Emmanuel and Guha, Shibashis and Maubert,
Bastien and Murano, Aniello and Pinault, Laureline
and Pinchinat, Sophie and Rubin, Sasha and Serre,
Olivier},
title = {Alternating Tree Automata with Qualitative
Semantics},
number = {2002-03664},
year = {2020},
month = feb,
institution = {arXiv},
}
@inproceedings{fsttcs2020-BKLS,
author = {Boker, Udi and Kuperberg, Denis and Lehtinen,
Karoliina and Skrzypczak, Michal},
title = {On succinctness and recognisability of alternating
good-for-games automata},
editor = {Saxena, Nitin and Simon, Sunil},
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)},
acronym = {{FSTTCS}'20},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {182},
pages = {41:1-41:13},
year = {2020},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2020.41},
}
@article{or68(2)-CCMS,
author = {Colini{-}Baldeschi, Riccardo and Cominetti, Roberto
and Mertikopoulos, Panayotis and Scarsini, Marco},
title = {When is selfish routing bad? {T}he~price of anarchy
in light and heavy traffic},
publisher = {Informs},
journal = {Operations Research},
volume = {68},
number = {2},
pages = {411-434},
year = {2020},
month = apr,
doi = {10.1287/opre.2019.1894},
}
@book{Had20-IEDES,
author = {Hadjicostis, Christoforos N.},
title = {Estimation and Inference in Discrete Event
Systems~-- A~model-based approach with finite
automata},
publisher = {Springer-Verlag},
series = {Communications and Control Engineering},
year = {2020},
}
@inproceedings{lics2020-LZ,
author = {Lehtinen, Karoliina and Zimmermann, Martin},
title = {Good-for-games {\(\omega\)}-pushdown automata},
editor = {Hermanns, Holger and Zhang, Lijun and Kobayashi,
Naoki and Miller, Dale},
booktitle = {{P}roceedings of the 35th {A}nnual {S}ymposium on
{L}ogic in {C}omputer {S}cience ({LICS}'20)},
acronym = {{LICS}'20},
publisher = {IEEE Comp. Soc. Press},
pages = {689-702},
year = {2020},
month = jul,
doi = {10.1145/3373718.3394737},
}
[MMP+20]
BastienMaubert,
AnielloMurano,
SophiePinchinat,
FrançoisSchwarzentruber, and
SilviaStranieri.
Dynamic Epistemic Logic Games with Epistemic
Temporal Goals.
Technical Report 2001-07141, arXiv, January 2020.
@techreport{arxiv2001.07141-MMPSS,
author = {Maubert, Bastien and Murano, Aniello and Pinchinat,
Sophie and Schwarzentruber, Fran{\c c}ois and
Stranieri, Silvia},
title = {Dynamic Epistemic Logic Games with Epistemic
Temporal Goals},
number = {2001-07141},
year = {2020},
month = jan,
institution = {arXiv},
}
@phdthesis{phd-roussanaly,
author = {Roussanaly, Victor},
title = {Efficient verification of real-time systems},
year = {2020},
month = nov,
school = {Universit{\'e} Rennes~1, France},
type = {Th\`ese de doctorat},
}
[Wol20]
PetraWolf.
Synchronization under Dynamic Constraints.
In FSTTCS'20,
Leibniz International Proceedings in Informatics 182, pages 58:1-58:14. Leibniz-Zentrum für Informatik, December 2020.
We introduce and study
SL[F]—a quantitative
extension of SL (Strategy Logic),
one of the most natural and expressive logics
describing strategic behaviours. The satisfaction
value of an SL[F] formula
is a real value in [0,1], reflecting "how
much" or "how well" the strategic on-going
objectives of the underlying agents are satisfied.
We demonstrate the applications of
SL[F] in quantitative
reasoning about multi-agent systems, by showing how
it can express concepts of stability in multi-agent
systems, and how it generalises some fuzzy temporal
logics. We also provide a model-checking algorithm
for our logic, based on a quantitative extension of
Quantified CTL.
@inproceedings{ijcai2019-BKMMMP,
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},
editor = {Kraus, Sarit},
booktitle = {{P}roceedings of the 28th {I}nternational {J}oint
{C}onference on {A}rtificial {I}ntelligence
({IJCAI}'19)},
acronym = {{IJCAI}'19},
publisher = {IJCAI organization},
pages = {1588-1594},
year = {2019},
month = aug,
doi = {10.24963/ijcai.2019/220},
abstract = {We~introduce and study
{\(\textsf{SL}[\mathcal{F}]\)}---a~quantitative
extension of {\(\textsf{SL}\)} (Strategy Logic),
one~of the most natural and expressive logics
describing strategic behaviours. The satisfaction
value of an {\(\textsf{SL}[\mathcal{F}]\)} formula
is a real value in~{\([0,1]\)}, reflecting {"}how
much{"} or {"}how well{"} the strategic on-going
objectives of the underlying agents are satisfied.
We~demonstrate the applications of
{\(\textsf{SL}[\mathcal{F}]\)} in quantitative
reasoning about multi-agent systems, by showing how
it can express concepts of stability in multi-agent
systems, and how it generalises some fuzzy temporal
logics. We~also provide a model-checking algorithm
for our logic, based on a quantitative extension of
Quantified~\textsf{CTL}.},
}
We study games with reachability objectives under
energy constraints. We first prove that under strict
energy constraints (either only lower-bound
constraint or interval constraint), those games are
LOGSPACE-equivalent to energy games with
the same energy constraints but without reachability
objective (i.e., for infinite runs). We then
consider two kinds of relaxations of the upper-bound
constraints (while keeping the lower-bound
constraint strict): in the first one, called
weak upper bound, the upper bound is
absorbing, in the sense that it allows
receiving more energy when the upper bound is
already reached, but the extra energy will not be
stored; in the second one, we allow for
temporary violations of the upper bound,
imposing limits on the number or on the amount of
violations.
We prove that when considering weak
upper bound, reachability objectives require memory,
but can still be solved in polynomial-time for
one-player arenas; we prove that they are in
coNP in the two-player setting. Allowing
for bounded violations makes the problem
PSPACE-complete for one-player arenas and
EXPTIME-complete for two players.
@inproceedings{gandalf2019-HMR,
author = {H{\'e}lou{\"e}t, Lo{\"\i}c and Markey, Nicolas and
Raha, Ritam},
title = {Reachability games with relaxed energy constraints},
editor = {Leroux, J{\'e}r{\^o}me and Raskin, Jean-Fran{\c
c}ois},
booktitle = {{P}roceedings of the 10th {I}nternational
{S}ymposium on {G}ames, {A}utomata, {L}ogics and
{F}ormal {V}erification ({GandALF}'19)},
acronym = {{GandALF}'19},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {305},
pages = {17-33},
year = {2019},
month = sep,
doi = {10.4204/EPTCS.305.2},
abstract = {We study games with reachability objectives under
energy constraints. We first prove that under strict
energy constraints (either only lower-bound
constraint or interval constraint), those games are
\textsf{LOGSPACE}-equivalent to energy games with
the same energy constraints but without reachability
objective (i.e., for infinite runs). We then
consider two kinds of relaxations of the upper-bound
constraints (while keeping the lower-bound
constraint strict): in the first one, called
\emph{weak upper bound}, the upper bound is
\emph{absorbing}, in the sense that it allows
receiving more energy when the upper bound is
already reached, but the extra energy will not be
stored; in~the second~one, we~allow for
\emph{temporary violations} of the upper bound,
imposing limits on the number or on the amount of
violations.\par We prove that when considering weak
upper bound, reachability objectives require memory,
but can still be solved in polynomial-time for
one-player arenas; we prove that they are in
\textsf{coNP} in the two-player setting. Allowing
for bounded violations makes the problem
\textsf{PSPACE}-complete for one-player arenas and
\textsf{EXPTIME}-complete for two players.},
}
We present abstraction-refinement algorithms for
model checking safety properties of timed automata.
The abstraction domain we consider abstracts away
zones by restricting the set of clock constraints
that can be used to define them, while the
refinement procedure computes the set of constraints
that must be taken into consideration in the
abstraction so as to exclude a given spurious
counterexample. We implement this idea in two ways:
an enumerative algorithm where a lazy abstraction
approach is adopted, meaning that possibly different
abstract domains are assigned to each exploration
node; and a symbolic algorithm where the abstract
transition system is encoded with Boolean formulas.
@inproceedings{cav2019-RSM,
author = {Roussanaly, Victor and Sankur, Ocan and Markey,
Nicolas},
title = {Abstraction Refinement Algorithms for Timed
Automata},
editor = {Dillig, I{\c s}il and Ta{\c s}iran, Serdar},
booktitle = {{P}roceedings of the 31st {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'19)},
acronym = {{CAV}'19},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {11561},
pages = {22-40},
year = {2019},
month = jul,
doi = {10.1007/978-3-030-25540-4_2},
abstract = {We~present abstraction-refinement algorithms for
model checking safety properties of timed automata.
The~abstraction domain we consider abstracts away
zones by restricting the set of clock constraints
that can be used to define them, while the
refinement procedure computes the set of constraints
that must be taken into consideration in the
abstraction so as to exclude a given spurious
counterexample. We~implement this idea in two~ways:
an~enumerative algorithm where a lazy abstraction
approach is adopted, meaning that possibly different
abstract domains are assigned to each exploration
node; and a symbolic algorithm where the abstract
transition system is encoded with Boolean formulas.},
}
[BBG+19]
ThomasBrihaye,
VéroniqueBruyère,
AlineGoeminne,
Jean-FrançoisRaskin, and
MarieVan den Bogaard.
The Complexity of Subgame Perfect Equilibria in
Quantitative Reachability Games.
In CONCUR'19,
Leibniz International Proceedings in Informatics 140, pages 13:1-13:16. Leibniz-Zentrum für Informatik, August 2019.
@inproceedings{concur2019-BBGRB,
author = {Brihaye, {\relax Th}omas and Bruy{\`e}re,
V{\'e}ronique and Goeminne, Aline and Raskin,
Jean-Fran{\c c}ois and Van{~}den{ }Bogaard, Marie},
title = {The~Complexity of Subgame Perfect Equilibria in
Quantitative Reachability Games},
editor = {Fokkink, Wan J. and van Glabbeek, Rob},
booktitle = {{P}roceedings of the 30th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'19)},
acronym = {{CONCUR}'19},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {140},
pages = {13:1-13:16},
year = {2019},
month = aug,
doi = {10.4230/LIPIcs.CONCUR.2019.13},
}
[BGM+19]
DamienBusatto-Gaston,
BenjaminMonmege,
Pierre-AlainReynier, and
OcanSankur.
Robust Controller Synthesis in Timed Büchi
Automata: A Symbolic Approach.
In CAV'19,
Lecture Notes in Computer Science 11561, pages 572-590. Springer-Verlag, July 2019.
@inproceedings{concur2019-BL,
author = {Boker, Udi and Lehtinen, Karoliina},
title = {Good-for-game Automata: from Non-determinism to
Alternation},
editor = {Fokkink, Wan J. and van Glabbeek, Rob},
booktitle = {{P}roceedings of the 30th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'19)},
acronym = {{CONCUR}'19},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {140},
pages = {19:1-19:16},
year = {2019},
month = aug,
doi = {10.4230/LIPIcs.CONCUR.2019.19},
}
@article{moor44(4)-CJKU,
author = {Correa, Jos{\'e} R. and de~Jong, Jasper and
de~Keizer, Bart and Uetz, Marc},
title = {The inefficiency of {N}ash and subgame-perfect
equilibria for network routing},
publisher = {Informs},
journal = {Mathematics of Operations Research},
volume = {44},
number = {4},
pages = {1286-1303},
year = {2019},
month = nov,
doi = {10.1287/moor.2018.0968},
}
@article{jcss100()-DMS,
author = {Doyen, Laurent and Massart, {\relax Th}ierry and
Shirmohammadi, Mahsa},
title = {The complexity of synchronizing {M}arkov decision
processes},
publisher = {Elsevier},
journal = {Journal of Computer and System Sciences},
volume = {100},
pages = {96-129},
year = {2019},
month = mar,
doi = {10.1016/j.jcss.2018.09.004},
}
[FGH+19]
HenningFernau,
Vladimir V.Gusev,
StefanHoffmann,
MarkusHolzer,
Mikhail V.Volkov, and
PetraWolf.
Computational Complexity of Synchronization under
Regular Constraints.
In MFCS'19,
Leibniz International Proceedings in Informatics 138, pages 63:1-63:14. Leibniz-Zentrum für Informatik, August 2019.
@inproceedings{mfcs2019-FGHHVW,
author = {Fernau, Henning and Gusev, Vladimir V. and Hoffmann,
Stefan and Holzer, Markus and Volkov, Mikhail V. and
Wolf, Petra},
title = {Computational Complexity of Synchronization under
Regular Constraints},
editor = {Rossmanith, Peter and Heggernes, Pinar and Katoen,
Joost-Pieter},
booktitle = {{P}roceedings of the 44th {I}nternational
{S}ymposium on {M}athematical {F}oundations of
{C}omputer {S}cience ({MFCS}'19)},
acronym = {{MFCS}'19},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {138},
pages = {63:1-63:14},
year = {2019},
month = aug,
doi = {10.4230/LIPIcs.MFCS.2019.63},
}
This article focuses on the existence and synthesis
of strategies in double-weighted Markov decision
processes, which satisfy both a probability
constraint over a weighted reachability condition,
and a quantitative constraint on the expected value
of a random variable defined using another
reachability condition. This work generalizes a
scheduling problem for energy consumption (typically
the problem of charging electric vehicles). We study
the set of values of a parameter (a threshold) for
which the problem has a solution, and show how a
partial characterization of this set can be obtained
via two sequences of optimization problems. We also
discuss the completeness and feasibility of the
resulting approach.
@inproceedings{gretsi2019-GBLM,
author = {Gonz{\'a}lez, Mauricio and Bouyer, Patricia and
Lasaulce, Samson and Markey, Nicolas},
title = {Optimisation en pr\'esence de contraintes en
probabilit\'es et processus markoviens
contr\^ol\'es},
booktitle = {{A}ctes du 27{\`e}me {C}olloque du {G}roupe
d'{\'E}tudes du {T}raitement du {S}ignal et des
{I}mages ({GRETSI}'19)},
acronym = {{GRETSI}'19},
year = {2019},
month = aug,
abstract = {This article focuses on the existence and synthesis
of strategies in double-weighted Markov decision
processes, which satisfy both a probability
constraint over a weighted reachability condition,
and a quantitative constraint on the expected value
of a random variable defined using another
reachability condition. This work generalizes a
scheduling problem for energy consumption (typically
the problem of charging electric vehicles). We~study
the set of values of a parameter (a~threshold) for
which the problem has a solution, and show how a
partial characterization of this set can be obtained
via two sequences of optimization problems. We~also
discuss the completeness and feasibility of the
resulting approach.},
}
@phdthesis{phd-jaziri,
author = {Jaziri, Samy},
title = {Automata on timed structures},
year = {2019},
month = sep,
school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France},
}
[KMS19]
SophiaKnight,
BastienMaubert, and
FrançoisSchwarzentruber.
Reasoning about knowledge and messages in
asynchronous multi-agent systems.
Mathematical Structures in Computer Science 29(1):127-168. January 2019.
@article{mscs29(1)-KMS,
author = {Knight, Sophia and Maubert, Bastien and
Schwarzentruber, Fran{\c c}ois},
title = {Reasoning about knowledge and messages in
asynchronous multi-agent systems},
journal = {Mathematical Structures in Computer Science},
volume = {29},
number = {1},
pages = {127-168},
year = {2019},
month = jan,
doi = {10.1017/S0960129517000214},
}
[LDW+19]
VincentLangenfeld,
DanielDietsch,
BerndWestphal,
JochenHoenicke, and
AmalindaPost.
Scalable Analysis of Real-Time Requirements.
In RE'19,
pages 234-244.
IEEE Comp. Soc. Press, September 2019.
@inproceedings{re2019-LDWHP,
author = {Langenfeld, Vincent and Dietsch, Daniel and
Westphal, Bernd and Hoenicke, Jochen and Post,
Amalinda},
title = {Scalable Analysis of Real-Time Requirements},
editor = {Damian, Daniela E. and Perini, Anna and Lee,
Seok-Won},
booktitle = {{P}roceedings of the 27th {I}nternaitonal
{R}equirements Engineering {C}onference ({RE}'19)},
acronym = {{RE}'19},
publisher = {IEEE Comp. Soc. Press},
pages = {234-244},
year = {2019},
month = sep,
doi = {10.1109/RE.2019.00033},
}
[MPS19]
BastienMaubert,
SophiePinchinat, and
FrançoisSchwarzentruber.
Reachability Games in Dynamic Epistemic Logic.
In IJCAI'19,
pages 499-505.
IJCAI organization, August 2019.
@article{jalc24(2-4)-Nic,
author = {Nicaud, Cyril},
title = {The {{\v{C}}}ern{\'y} conjecture holds with high
probability},
journal = {Journal of Automata, Languages and Combinatorics},
volume = {24},
number = {2-4},
pages = {343-365},
year = {2019},
doi = {10.25596/jalc-2019-343},
}
@article{tocl20(2)-QS,
author = {Quaas, Karin and Shirmohammadi, Mahsa},
title = {Synchronizing Data Words for Register Automata},
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
volume = {20},
number = {2},
pages = {11:1-11:27},
year = {2019},
month = apr,
doi = {10.1145/3309760},
}
@article{jalc24(2-4)-Shi,
author = {Shitov, Yaroslav},
title = {An Improvement to a Recent Upper Bound for
Synchronizing Words of Finite Automata},
journal = {Journal of Automata, Languages and Combinatorics},
volume = {24},
number = {2-4},
pages = {367-373},
year = {2019},
doi = {10.25596/jalc-2019-367},
}
@phdthesis{phd-sickert,
author = {Sickert, Salomon},
title = {A~unified translation of Linear Temporal Logic to
{\(\omega\)}-automata},
year = {2019},
month = jul,
school = {Technischen Universit{\"a}t M{\"u}nchen, Germany},
}
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.
@article{acta55(2)-BMRLL,
author = {Bouyer, Patricia and Markey, Nicolas and Randour,
Mickael and Larsen, Kim Guldstrand and Laursen,
Simon},
title = {Average-energy games},
publisher = {Springer-Verlag},
journal = {Acta Informatica},
volume = {55},
number = {2},
pages = {91-127},
year = {2018},
month = mar,
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
\(\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.},
}
We present a correct-by-design method of
state-dependent control synthesis for sampled
switching systems. Given a target region R of
the state space, our method builds a capture
set S and a control that steers any element
of S into R. The method works by iterated
backward reachability from R. It is also used to
synthesize a recurrence control that makes any state
of R return to R infinitely often.
We explain how the synthesis method can be performed
in a compositional manner, and apply it to the
synthesis of a compositional control for a concrete
floor-heating system with 11 rooms and up to
211=2048 switching modes.
@article{tcs750()-LFMDC,
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},
publisher = {Elsevier},
journal = {Theoretical Computer Science},
volume = {750},
pages = {53-68},
year = {2018},
month = nov,
doi = {10.1016/j.tcs.2018.01.021},
abstract = {We present a correct-by-design method of
state-dependent control synthesis for sampled
switching systems. Given a target region~\(R\) of
the state space, our~method builds a capture
set~\(S\) and a~control that steers any element
of~\(S\) into~\(R\). The~method works by iterated
backward reachability from~\(R\). It~is also used to
synthesize a recurrence control that makes any state
of~\(R\) return to~\(R\) infinitely often.
We~explain how the synthesis method can be performed
in a compositional manner, and apply it to the
synthesis of a compositional control for a concrete
floor-heating system with 11~rooms and up to
\(2^{11}=2048\) switching modes.},
}
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.
@inproceedings{fm2018-BBFLMR,
author = {Bacci, Giovanni and Bouyer, Patricia and Fahrenberg,
Uli and Larsen, Kim Guldstrand and Markey, Nicolas
and Reynier, Pierre-Alain},
title = {Optimal and Robust Controller Synthesis Using Energy
Timed Automata with Uncertainty},
editor = {Havelund, Klaus and Peleska, Jan and Roscoe, Bill W.
and de Vink, Erik},
booktitle = {{P}roceedings of the 22nd {I}nternational
{S}ymposium on {F}ormal {M}ethods ({FM}'18)},
acronym = {{FM}'18},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {10951},
pages = {203-221},
year = {2018},
month = jul,
doi = {10.1007/978-3-319-95582-7_12},
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.},
}
Reconfigurable broadcast networks provide a
convenient formalism for modelling and reasoning
about networks of mobile agents broadcasting
messages to other agents following some (evolving)
communication topology. The parameterized
verification of such models aims at checking whether
a given property holds irrespective of the initial
configuration (number of agents, initial states and
initial communication topology). We focus here on
the synchronization property, asking whether
all agents converge to a set of target states after
some execution. This problem is known to be
decidable in polynomial time when no constraints are
imposed on the evolution of the communication
topology (while it is undecidable for static
broadcast networks).
In this paper we
investigate how various constraints on
reconfigurations affect the decidability and
complexity of the synchronization problem.
In particular, we show that when bounding the number
of reconfigured links between two communications
steps by a constant, synchronization becomes
undecidable; on the other hand, synchronization
remains decidable in PTIME when the bound grows with
the number of agents.
@inproceedings{tacas2018-2-BBM,
author = {Balasubramanian, A. R. and Bertrand, Nathalie and
Markey, Nicolas},
title = {Parameterized verification of synchronization in
constrained reconfigurable broadcast networks},
editor = {Beyer, Dirk and Huisman, Marieke},
booktitle = {{P}roceedings of the 24th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'18)~-- {P}art~{II}},
acronym = {{TACAS}'18 (Part~{II})},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {10806},
pages = {38-54},
year = {2018},
month = apr,
doi = {10.1007/978-3-319-89963-3_3},
abstract = {Reconfigurable broadcast networks provide a
convenient formalism for modelling and reasoning
about networks of mobile agents broadcasting
messages to other agents following some (evolving)
communication topology. The parameterized
verification of such models aims at checking whether
a given property holds irrespective of the initial
configuration (number of agents, initial states and
initial communication topology). We~focus here on
the \emph{synchronization property}, asking whether
all agents converge to a set of target states after
some execution. This~problem is known to be
decidable in polynomial time when no constraints are
imposed on the evolution of the communication
topology (while~it~is undecidable for static
broadcast networks).\par In this paper we
investigate how various constraints on
reconfigurations affect the decidability and
complexity of the synchronization problem.
In~particular, we show that when bounding the number
of reconfigured links between two communications
steps by a constant, synchronization becomes
undecidable; on~the other hand, synchronization
remains decidable in PTIME when the bound grows with
the number of agents.},
}
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{gandalf2018-BGMR,
author = {Bouyer, Patricia and Gonz{\'a}lez, Mauricio and
Markey, Nicolas and Randour, Mickael},
title = {Multi-weighted Markov Decision Processes with
Reachability Objectives},
editor = {Orlandini, Andrea and Zimmermann, Martin},
booktitle = {{P}roceedings of the 9th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics and {F}ormal
{V}erification ({GandALF}'18)},
acronym = {{GandALF}'18},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {277},
pages = {250-264},
year = {2018},
month = sep,
doi = {10.4204/EPTCS.277.18},
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.},
}
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
autmata, 2002].
@inproceedings{rv2018-BJM,
author = {Bouyer, Patricia and Jaziri, Samy and Markey,
Nicolas},
title = {Efficient timed diagnosis using automata with timed
domains},
editor = {Colombo, Christian and Leucker, Martin},
booktitle = {{P}roceedings of the 18th {I}nternational {W}orkshop
on {R}untime {V}erification ({RV}'18)},
acronym = {{RV}'18},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {11237},
pages = {205-221},
year = {2018},
month = nov,
doi = {10.1007/978-3-030-03769-7_12},
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
autmata,~2002].},
}
Strategy Logic (SL) is a very expressive
temporal logic for specifying and verifying
properties of multi-agent systems: in SL,
one can quantify over strategies, assign them to
agents, and express LTL 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, revisiting the approach of [Mogavero
et al., Reasoning about strategies: On the
model-checking problem, 2014]. We explain why
elementary dependences, as defined by
Mogavero et al., do not exactly capture the
intended concept of behavioral strategies.
We address this discrepancy by introducing
timeline dependences, and exhibit a large
fragment of SL for which model checking can
be performed in 2EXPTIME under this new
semantics.
@inproceedings{stacs2018-GBM,
author = {Gardy, Patrick and Bouyer, Patricia and Markey,
Nicolas},
title = {Dependences in Strategy Logic},
editor = {Niedermeier, Rolf and Vall{\'e}e, Brigitte},
booktitle = {{P}roceedings of the 35th {S}ymposium on
{T}heoretical {A}spects of {C}omputer {S}cience
({STACS}'18)},
acronym = {{STACS}'18},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {96},
pages = {34:1-34:14},
year = {2018},
month = feb,
doi = {10.4230/LIPIcs.STACS.2018.34},
abstract = {Strategy Logic~(\textsf{SL}) is a very expressive
temporal logic for specifying and verifying
properties of multi-agent systems: in~\textsf{SL},
one can quantify over strategies, assign them to
agents, and express \textsf{LTL} properties of the
resulting plays. Such a powerful framework has two
drawbacks: first, model checking \textsf{SL} has
non-elementary complexity; second, the exact
semantics of \textsf{SL} is rather intricate, and
may not correspond to what is expected. In~this
paper, we~focus on \emph{strategy dependences}
in~\textsf{SL}, by tracking how
existentially-quantified strategies in a formula may
(or~may~not) depend on other strategies selected in
the formula, revisiting the approach of~[Mogavero
\emph{et~al.}, Reasoning about strategies: On~the
model-checking problem,~2014]. We~explain why
\emph{elementary} dependences, as defined by
Mogavero~\emph{et~al.}, do not exactly capture the
intended concept of behavioral strategies.
We~address this discrepancy by introducing
\emph{timeline} dependences, and exhibit a large
fragment of \textsf{SL} for which model checking can
be performed in \textsf{2EXPTIME} under this new
semantics.},
}
Partial observability and controllability are two
well-known issues in test-case synthesis for
interactive systems. We address the problem of
partial control in the synthesis of test cases from
timed-automata specifications. Building on the tioco
timed testing framework, we extend a previous game
interpretation of the test-synthesis problem from
the untimed to the timed setting. This extension
requires a deep reworking of the models, game
interpretation and test-synthesis algorithms.
We exhibit strategies of a game that tries to
minimize both control losses and distance to the
satisfaction of a test purpose, and prove they are
winning under some fairness assumptions. This
entails that when turning those strategies into test
cases, we get properties such as soundness and
exhaustiveness of the test synthesis method.
@inproceedings{spin2018-HJM,
author = {Henry, L{\'e}o and J{\'e}ron, Thierry and Markey,
Nicolas},
title = {Control strategies for off-line testing of timed
systems},
editor = {Gallardo, Mar{\'\i}a-del-Mar and Merino, Pedro},
booktitle = {{P}roceedings of the 25th {I}nternational
{S}ymposium on {M}odel-{C}herking {S}oftware
({SPIN}'18)},
acronym = {{SPIN}'18},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {10869},
pages = {171-189},
year = {2018},
month = jun,
doi = {10.1007/978-3-319-94111-0_10},
abstract = {Partial observability and controllability are two
well-known issues in test-case synthesis for
interactive systems. We~address the problem of
partial control in the synthesis of test cases from
timed-automata specifications. Building on the tioco
timed testing framework, we~extend a previous game
interpretation of the test-synthesis problem from
the untimed to the timed setting. This extension
requires a deep reworking of the models, game
interpretation and test-synthesis algorithms.
We~exhibit strategies of a game that tries to
minimize both control losses and distance to the
satisfaction of a test purpose, and prove they are
winning under some fairness assumptions. This
entails that when turning those strategies into test
cases, we get properties such as soundness and
exhaustiveness of the test synthesis method.},
}
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).
@incollection{hmc2018-BFLMOW,
author = {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim
Guldstrand and Markey, Nicolas and Ouaknine,
Jo{\"e}l and Worrell, James},
title = {Model Checking Real-Time Systems},
editor = {Clarke, Edmund M. and Henzinger, Thomas A. and
Veith, Helmut and Bloem, Roderick},
booktitle = {Handbook of Model Checking},
publisher = {Springer-Verlag},
pages = {1001-1046},
chapter = {29},
year = {2018},
month = may,
doi = {10.1007/978-3-319-10575-8_29},
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).},
}
[AGK18]
GuyAvni,
ShibashisGuha, and
OrnaKupferman.
Timed Network Games with Clocks.
In MFCS'18,
Leibniz International Proceedings in Informatics 117, pages 23:1-23:18. Leibniz-Zentrum für Informatik, August 2018.
@inproceedings{mfcs2018-AGK,
author = {Avni, Guy and Guha, Shibashis and Kupferman, Orna},
title = {Timed Network Games with Clocks},
editor = {Potapov, Igor and Spirakis, Paul G. and Worrell,
James},
booktitle = {{P}roceedings of the 43rd {I}nternational
{S}ymposium on {M}athematical {F}oundations of
{C}omputer {S}cience ({MFCS}'18)},
acronym = {{MFCS}'18},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {117},
pages = {23:1-23:18},
year = {2018},
month = aug,
doi = {10.4230/LIPIcs.MFCS.2018.23},
}
[AKP18]
ShaullAlmagor,
OrnaKupferman, and
GiuseppePerelli.
Synthesis of Controllable Nash Equilibria in
Quantitative Objective Games.
In IJCAI'18,
pages 35-41.
IJCAI organization, July 2018.
@inproceedings{ijcai2018-AKP,
author = {Almagor, Shaull and Kupferman, Orna and Perelli,
Giuseppe},
title = {Synthesis of Controllable {N}ash Equilibria in
Quantitative Objective Games},
editor = {Lang, J{\'e}r{\^o}me},
booktitle = {{P}roceedings of the 27th {I}nternational {J}oint
{C}onference on {A}rtificial {I}ntelligence
({IJCAI}'18)},
acronym = {{IJCAI}'18},
publisher = {IJCAI organization},
pages = {35-41},
year = {2018},
month = jul,
doi = {10.24963/ijcai.2018/5},
}
[AMM+18]
BenjaminAminof,
VadimMalvone,
AnielloMurano, and
SashaRubin.
Graded modalities in Strategy Logic.
Information and Computation 261(4):634-649. Elsevier, August 2018.
@article{icomp261(4)-AMMR,
author = {Aminof, Benjamin and Malvone, Vadim and Murano,
Aniello and Rubin, Sasha},
title = {Graded modalities in Strategy Logic},
publisher = {Elsevier},
journal = {Information and Computation},
volume = {261},
number = {4},
pages = {634-649},
year = {2018},
month = aug,
doi = {10.1016/j.ic.2018.02.021},
}
[BEK18]
MichaelBlondin,
JavierEsparza, and
AntonínKučera.
Automatic Analysis of Expected Termination Time for
Population Protocols.
In CONCUR'18,
Leibniz International Proceedings in Informatics 118, pages 33:1-33:16. Leibniz-Zentrum für Informatik, September 2018.
@inproceedings{concur2018-BEK,
author = {Blondin, Michael and Esparza, Javier and Ku{\v
c}era, Anton{\'\i}n},
title = {Automatic Analysis of Expected Termination Time for
Population Protocols},
editor = {Schewe, Sven and Zhang, Lijun},
booktitle = {{P}roceedings of the 29th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'18)},
acronym = {{CONCUR}'18},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {118},
pages = {33:1-33:16},
year = {2018},
month = sep,
doi = {10.4230/LIPIcs.CONCUR.2018.33},
}
[BF18]
EzioBartocci and
YlièsFalcone.
Lectures on Runtime Verification.
Lecture Notes in Computer Science 10457.
Springer-Verlag, 2018.
@book{lectRV-BF18,
title = {Lectures on Runtime Verification},
editor = {Bartocci, Ezio and Falcone, Yli{\`e}s},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {10457},
year = {2018},
doi = {10.1007/978-3-319-75632-5},
}
@inproceedings{fsttcs2018-BMR,
author = {Busatto-Gaston, Damien and Monmege, Benjamin and
Reynier, Pierre-Alain},
title = {Symbolic Approximation of Weighted Timed Games},
editor = {Ganguli, Sumit and Pandya, Paritosh K.},
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)},
acronym = {{FSTTCS}'18},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {122},
pages = {28:1-28:16},
year = {2018},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2018.28},
}
@inproceedings{fsttcs2018-BK,
author = {Bagnol, Marc and Kuperberg, Denis},
title = {B{\"u}chi Good-for-game Automata are Efficiently
Recognizable},
editor = {Ganguli, Sumit and Pandya, Paritosh K.},
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)},
acronym = {{FSTTCS}'18},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {122},
pages = {16:1-16:14},
year = {2018},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2018.16},
}
[Bok18]
UdiBoker.
Why these automata types?.
In LPAR'18,
EPiC Series in Computing 57, pages 143-163. EasyChair, November 2018.
@book{hbmc18-CHVB,
author = {Clarke, Edmund M. and Henzinger, Thomas A. and
Veith, Helmut and Bloem, Roderick},
title = {Handbook of Model Checking},
publisher = {Springer-Verlag},
year = {2018},
month = apr,
doi = {10.1007/978-3-319-10575-8},
}
[DM18]
DarioDella Monica and
AnielloMurano.
Parity-energy ATL for Qualitative and Quantitative
Reasoning in MAS.
In AAMAS'18,
pages 1441-1449.
International Foundation for Autonomous Agents and
Multiagent Systems, July 2018.
@inproceedings{aamas2018-DM,
author = {Della{ }Monica, Dario and Murano, Aniello},
title = {Parity-energy {ATL} for Qualitative and Quantitative
Reasoning in~{MAS}},
editor = {Andr{\'e}, Elisabeth and Koenig, Sven and Dastani,
Mehdi and Sukthankar, Gita},
booktitle = {{P}roceedings of the 17th {I}nternational
{C}onference on {A}utonomous {A}gents and
{M}ultiagent {S}ystems ({AAMAS}'18)},
acronym = {{AAMAS}'18},
publisher = {International Foundation for Autonomous Agents and
Multiagent Systems},
pages = {1441-1449},
year = {2018},
month = jul,
}
[DMP18]
CătălinDima,
BastienMaubert, and
SophiePinchinat.
Relating Paths in Transition Systems: The Fall of
the Modal Mu-Calculus.
ACM Transactions on Computational Logic 19(3):23:1-23:33. ACM Press, September 2018.
@article{tocl19(3)-DMS,
author = {Dima, C{\u a}t{\u a}lin and Maubert, Bastien and
Pinchinat, Sophie},
title = {Relating Paths in Transition Systems: The~Fall of
the Modal Mu-Calculus},
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
volume = {19},
number = {3},
pages = {23:1-23:33},
year = {2018},
month = sep,
doi = {10.1145/3231596},
}
[FMM+18]
NathanaëlFijalkow,
BastienMaubert,
AnielloMurano, and
SashaRubin.
Quantifying Bounds in Strategy Logic.
In CSL'18,
Leibniz International Proceedings in Informatics 119, pages 23:1-23:23. Leibniz-Zentrum für Informatik, September 2018.
@inproceedings{csl2018-FMMR,
author = {Fijalkow, Nathana{\"e}l and Maubert, Bastien and
Murano, Aniello and Rubin, Sasha},
title = {Quantifying Bounds in Strategy Logic},
editor = {Ghica, Dan R. and Jung, Achim},
booktitle = {{P}roceedings of the 27th {EACSL} {A}nnual
{C}onference on {C}omputer {S}cience {L}ogic
({CSL}'18)},
acronym = {{CSL}'18},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {119},
pages = {23:1-23:23},
year = {2018},
month = sep,
doi = {10.4230/LIPIcs.CSL.2018.23},
}
@inproceedings{acsd2018-HMM,
author = {H{\'e}lou{\"e}t, Lo{\"\i}c and Marchand, Herv{\'e}
and Mullins, John},
title = {Concurrent secrets with quantified suspicion},
editor = {Chatain, {\relax Th}omas and Grosu, Radu and
Juh{\'a}s, Gabriel},
booktitle = {{P}roceedings of the 18th {I}nternational
{C}onference on {A}pplication of {C}oncurrency to
{S}ystem {D}esign ({ACSD}'18)},
acronym = {{ACSD}'18},
publisher = {IEEE Comp. Soc. Press},
pages = {75-84},
year = {2018},
month = jun,
doi = {10.1109/ACSD.2018.00011},
}
@inproceedings{cdc2018-JW,
author = {Jacquot, Paulin and Wan, Cheng},
title = {Routing game on parallel networks: the~convergence
of atomic to nonatomic},
booktitle = {{P}roceedings of the 57th {IEEE} {C}onference on
{D}ecision and {C}ontrol ({CDC}'18)},
acronym = {{CDC}'18},
publisher = {IEEE Comp. Soc. Press},
pages = {6951-6956},
year = {2018},
month = dec,
doi = {10.1109/CDC.2018.8619369},
}
@article{aric45()-LLH,
author = {Lafortune, St{\'e}phane and Lin, Feng and
Hadjicostis, Christoforos N.},
title = {On~the history of diagnosability and opacity in
discrete event systems},
publisher = {Elsevier},
journal = {Annual Reviews in Control},
volume = {45},
pages = {257-266},
year = {2018},
doi = {10.1016/j.arcontrol.2018.04.002},
}
@inproceedings{stacs2018-Szy,
author = {Szyku{\l}a, Marek},
title = {Improving the Upper Bound on the Length of the
Shortest Reset Word},
editor = {Niedermeier, Rolf and Vall{\'e}e, Brigitte},
booktitle = {{P}roceedings of the 35th {S}ymposium on
{T}heoretical {A}spects of {C}omputer {S}cience
({STACS}'18)},
acronym = {{STACS}'18},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {96},
pages = {56:1-56:13},
year = {2018},
month = feb,
doi = {10.4230/LIPIcs.STACS.2018.56},
}
The development of formal methods for control design
is an important challenge with potential
applications in a wide range of safety-critical
cyber-physical systems. Focusing on switched
dynamical systems, we propose a new abstraction,
based on time-varying regions of invariance (control
funnels), that models behaviors of systems as timed
automata. The main advantage of this method is that
it allows for the automated verification and
reactive controller synthesis without discretizing
the evolution of the state of the system. Efficient
and analytic constructions are possible in the case
of linear dynamics whereas bounding funnels with
conjectured properties based on numerical
simulations can be used for general nonlinear
dynamics. We demonstrate the potential of our
approach with three examples.
@article{rts53(3)-BMPS,
author = {Bouyer, Patricia and Markey, Nicolas and Perrin,
Nicolas and Schlehuber{-}Caissier, Philipp},
title = {Timed automata abstraction of switched dynamical
systems using control funnels},
publisher = {Kluwer Academic},
journal = {Real-Time Systems},
volume = {53},
number = {3},
pages = {327-353},
year = {2017},
month = may,
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.},
}
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.
@article{icomp254()-BMV,
author = {Bouyer, Patricia and Markey, Nicolas and Vester,
Steen},
title = {{N}ash Equilibria in Symmetric Graph Games with
Partial Observation},
publisher = {Elsevier},
journal = {Information and Computation},
volume = {254},
number = {2},
pages = {238-258},
year = {2017},
month = jun,
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.},
}
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.
@inproceedings{fossacs2017-BHMRZ,
author = {Bouyer, Patricia and Hofman, Piotr and Markey,
Nicolas and Randour, Mickael and Zimmermann, Martin},
title = {Bounding Average-energy Games},
editor = {Esparza, Javier and Murawski, Andrzej},
booktitle = {{P}roceedings of the 20th {I}nternational
{C}onference on {F}oundations of {S}oftware
{S}cience and {C}omputation {S}tructure
({FoSSaCS}'17)},
acronym = {{FoSSaCS}'17},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {10203},
pages = {179-195},
year = {2017},
month = apr,
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.\par 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.\par
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.},
}
We introduce a new formalism called automata
over a timed domain which provides an adequate
framework for the determinization of timed systems.
In this formalism, determinization w.r.t. timed
language is always possible at the cost of changing
the timed domain. We give a condition for
determinizability of automata over a timed domain
without changing the timed domain, which allows us
to recover several known determinizable classes of
timed systems, such as strongly-non-zeno timed
automata, integer-reset timed automata, perturbed
timed automata, etc. Moreover in the case of timed
automata this condition encompasses most
determinizability conditions from the literature.
@inproceedings{formats2017-BJM,
author = {Bouyer, Patricia and Jaziri, Samy and Markey,
Nicolas},
title = {On the determinization of timed systems},
editor = {Abate, Alessandro and Geeraerts, Gilles},
booktitle = {{P}roceedings of the 15th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'17)},
acronym = {{FORMATS}'17},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {10419},
pages = {25-41},
year = {2017},
month = sep,
doi = {10.1007/978-3-319-65765-3_2},
abstract = {We introduce a new formalism called \emph{automata
over a timed domain} which provides an adequate
framework for the determinization of timed systems.
In~this formalism, determinization w.r.t. timed
language is always possible at the cost of changing
the timed domain. We~give a condition for
determinizability of automata over a timed domain
without changing the timed domain, which allows us
to recover several known determinizable classes of
timed systems, such as strongly-non-zeno timed
automata, integer-reset timed automata, perturbed
timed automata, etc. Moreover in the case of timed
automata this condition encompasses most
determinizability conditions from the literature.},
}
@inproceedings{mfcs2017-Mar,
author = {Markey, Nicolas},
title = {Temporal logics for multi-agent systems
(invited~talk)},
editor = {Larsen, Kim Guldstrand and Bodlaender, Hans L. and
Raskin, Jean-Fran{\c c}ois},
booktitle = {{P}roceedings of the 42nd {I}nternational
{S}ymposium on {M}athematical {F}oundations of
{C}omputer {S}cience ({MFCS}'17)},
acronym = {{MFCS}'17},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {84},
pages = {84:1-84:3},
year = {2017},
month = aug,
doi = {10.4230/LIPIcs.MFCS.2017.84},
}
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.
@incollection{kimfest2017-BLMOW,
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, Giovanni
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-Verlag},
series = {Lecture Notes in Computer Science},
volume = {10460},
pages = {211-230},
year = {2017},
month = aug,
doi = {10.1007/978-3-319-63121-9_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.},
}
[ABD+17]
ErnstAlthaus,
BjörnBeber,
WernerDamm,
StefanDisch,
WillemHagemann,
AstridRakow,
ChristophScholl,
UweWaldmann, and
BorisWirtz.
Verification of linear hybrid systems with large
discrete state spaces using counterexample-guided
abstraction refinement.
Science of Computer Programming 148:123-160. Elsevier, November 2017.
@article{scp148()-ABDDHRSWW,
author = {Althaus, Ernst and Beber, Bj{\"o}rn and Damm, Werner
and Disch, Stefan and Hagemann, Willem and Rakow,
Astrid and Scholl, Christoph and Waldmann, Uwe and
Wirtz, Boris},
title = {Verification of linear hybrid systems with large
discrete state spaces using counterexample-guided
abstraction refinement},
publisher = {Elsevier},
journal = {Science of Computer Programming},
volume = {148},
pages = {123-160},
year = {2017},
month = nov,
doi = {10.1016/j.scico.2017.04.010},
}
[AGK17]
GuyAvni,
ShibashisGuha, and
OrnaKupferman.
Timed Network Games.
In MFCS'17,
Leibniz International Proceedings in Informatics 84, pages 37:1-37:16. Leibniz-Zentrum für Informatik, August 2017.
@inproceedings{mfcs2017-AGK,
author = {Avni, Guy and Guha, Shibashis and Kupferman, Orna},
title = {Timed Network Games},
editor = {Larsen, Kim Guldstrand and Bodlaender, Hans L. and
Raskin, Jean-Fran{\c c}ois},
booktitle = {{P}roceedings of the 42nd {I}nternational
{S}ymposium on {M}athematical {F}oundations of
{C}omputer {S}cience ({MFCS}'17)},
acronym = {{MFCS}'17},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {84},
pages = {37:1-37:16},
year = {2017},
month = aug,
doi = {10.4230/LIPIcs.MFCS.2017.37},
}
@inproceedings{concur2017-AGKS,
author = {Akshay, S. and Gastin, Paul and Krishna, Shankara
Narayanan and Sarkar, Ilias},
title = {Towards an Efficient Tree Automata Based Technique
for Timed Systems},
editor = {Meyer, Roland and Nestmann, Uwe},
booktitle = {{P}roceedings of the 28th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'17)},
acronym = {{CONCUR}'17},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {85},
pages = {39:1-39:15},
year = {2017},
month = sep,
doi = {10.4230/LIPIcs.CONCUR.2017.39},
}
[AKR+17]
ShaullAlmagor,
OrnaKupferman,
Jan OliverRingert, and
YaronVelner.
Quantitative Assume Guarantee Synthesis.
In CAV'17,
Lecture Notes in Computer Science 10427, pages 353-374. Springer-Verlag, July 2017.
@inproceedings{cav2017-AKRV,
author = {Almagor, Shaull and Kupferman, Orna and Ringert, Jan
Oliver and Velner, Yaron},
title = {Quantitative Assume Guarantee Synthesis},
editor = {Majumdar, Rupak and Kuncak, Viktor},
booktitle = {{P}roceedings of the 29th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'17)},
acronym = {{CAV}'17},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {10427},
pages = {353-374},
year = {2017},
month = jul,
doi = {10.1007/978-3-319-63390-9_19},
}
@article{sigact-news48(1)-AT,
author = {Alur, Rajeev and Tripakis, Stavros},
title = {Automatic Synthesis of Distributed Protocols},
publisher = {ACM Press},
journal = {SIGACT News},
volume = {48},
number = {1},
pages = {55-90},
year = {2017},
month = mar,
doi = {10.1145/3061640.3061652},
}
[BDG+17]
NathalieBertrand,
MiheerDewaskar,
BlaiseGenest, and
HugoGimbert.
Controlling a population.
In CONCUR'17,
Leibniz International Proceedings in Informatics 85, pages 12:1-12:16. Leibniz-Zentrum für Informatik, September 2017.
@inproceedings{concur2017-BDGG,
author = {Bertrand, Nathalie and Dewaskar, Miheer and Genest,
Blaise and Gimbert, Hugo},
title = {Controlling a population},
editor = {Meyer, Roland and Nestmann, Uwe},
booktitle = {{P}roceedings of the 28th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'17)},
acronym = {{CONCUR}'17},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {85},
pages = {12:1-12:16},
year = {2017},
month = sep,
doi = {10.4230/LIPIcs.CONCUR.2017.12},
}
[BGG17]
NathalieBertrand,
BlaiseGenest, and
HugoGimbert.
Qualitative Determinacy and Decidability of
Stochastic Games with Signals.
Journal of the ACM 64(5):33:1-33:48. ACM Press, October 2017.
@article{jacm64(5)-BGG,
author = {Bertrand, Nathalie and Genest, Blaise and Gimbert,
Hugo},
title = {Qualitative Determinacy and Decidability of
Stochastic Games with Signals},
publisher = {ACM Press},
journal = {Journal of the~ACM},
volume = {64},
number = {5},
pages = {33:1-33:48},
year = {2017},
month = oct,
doi = {10.1145/3107926},
}
[BGH+17]
ThomasBrihaye,
GillesGeeraerts,
AxelHaddad, and
BenjaminMonmege.
Pseudopolynomial iterative algorithm to solve
total-payoff games and min-cost reachability game.
Acta Informatica 54(1):85-125. Springer-Verlag, February 2017.
@article{acta54(1)-BGHM,
author = {Brihaye, {\relax Th}omas and Geeraerts, Gilles and
Haddad, Axel and Monmege, Benjamin},
title = {Pseudopolynomial iterative algorithm to solve
total-payoff games and min-cost reachability game},
publisher = {Springer-Verlag},
journal = {Acta Informatica},
volume = {54},
number = {1},
pages = {85-125},
year = {2017},
month = feb,
doi = {10.1007/s00236-016-0276-z},
}
[BHM17]
BéatriceBérard,
LoïcHélouët, and
JohnMullins.
Non-interference in partial order models.
ACM Transactions on Embedded Computing Systems.
ACM Press, 2017. To appear.
@article{tecs-BHM,
author = {B{\'e}rard, B{\'e}atrice and H{\'e}lou{\"e}t,
Lo{\"\i}c and Mullins, John},
title = {Non-interference in partial order models},
publisher = {ACM Press},
journal = {ACM Transactions on Embedded Computing Systems},
year = {2017},
note = {To~appear},
}
Dynamic complexity is concerned with updating the
output of a problem when the input is slightly
changed. We study the dynamic complexity of model
checking a fixed monadic second-order formula over
evolving subgraphs of a fixed maximal graph having
bounded tree-width; here the subgraph evolves by
losing or gaining edges (from the maximal graph).
We show that this problem is in DynFO (with LOGSPACE
precomputation), via a reduction to a Dyck
reachability problem on an acyclic automaton.
@techreport{arxiv1702.05183-BJM,
author = {Bouyer, Patricia and Jug{\'e}, Vincent and Markey,
Nicolas},
title = {{C}ourcelle's Theorem Made Dynamic},
number = {1702.05183},
year = {2017},
month = feb,
institution = {arXiv},
abstract = {Dynamic complexity is concerned with updating the
output of a problem when the input is slightly
changed. We study the dynamic complexity of model
checking a fixed monadic second-order formula over
evolving subgraphs of a fixed maximal graph having
bounded tree-width; here the subgraph evolves by
losing or gaining edges (from the maximal graph).
We~show that this problem is in DynFO (with LOGSPACE
precomputation), via a reduction to a Dyck
reachability problem on an acyclic automaton.},
}
[BMM17]
RaphaëlBerthon,
BastienMaubert, and
AnielloMurano.
Decidability Results for ATL*
with Imperfect Information and Perfect Recall.
In AAMAS'17,
pages 1250-1258.
International Foundation for Autonomous Agents and
Multiagent Systems, May 2017.
@inproceedings{aamas2017-BMM,
author = {Berthon, Rapha{\"e}l and Maubert, Bastien and
Murano, Aniello},
title = {Decidability Results for {ATL\textsuperscript{*}}
with Imperfect Information and Perfect Recall},
editor = {Das, Sanmay and Durfee, Ed and Larson, Kate and
Winikoff, Michael},
booktitle = {{P}roceedings of the 16th {I}nternational
{C}onference on {A}utonomous {A}gents and
{M}ultiagent {S}ystems ({AAMAS}'17)},
acronym = {{AAMAS}'17},
publisher = {International Foundation for Autonomous Agents and
Multiagent Systems},
pages = {1250-1258},
year = {2017},
month = may,
}
[BMM+17]
RaphaëlBerthon,
BastienMaubert,
AnielloMurano,
SashaRubin, and
Moshe Y.Vardi.
Strategy Logic with Imperfect Information.
In LICS'17,
pages 1-12.
IEEE Comp. Soc. Press, June 2017.
@article{acta54(1)-BRS,
author = {Brenguier, Romain and Raskin, Jean-Fran{\c c}ois and
Sankur, Ocan},
title = {Assume-admissible synthesis},
publisher = {Springer-Verlag},
journal = {Acta Informatica},
volume = {54},
number = {1},
pages = {41-83},
year = {2017},
month = feb,
doi = {10.1007/s00236-016-0273-2},
}
[BW17]
Julian C.Bradfield and
IgorWalukiewicz.
The mu-calculus and model-checking.
In Edmund M.Clarke,
Thomas A.Henzinger, and
HelmutVeith (eds.),
Handbook of Model Checking.
Springer-Verlag, 2017. To appear.
@incollection{HMC-BW,
author = {Bradfield, Julian C. and Walukiewicz, Igor},
title = {The mu-calculus and model-checking},
editor = {Clarke, Edmund M. and Henzinger, Thomas A. and
Veith, Helmut},
booktitle = {Handbook of Model Checking},
publisher = {Springer-Verlag},
year = {2017},
note = {To~appear},
}
[CDH17]
KrishnenduChatterjee,
LaurentDoyen, and
Thomas A.Henzinger.
The Cost of Exactness in Quantitative Reachability.
In Models, Algorithms, Logics and Tools: Essays
Dedicated to Kim Guldstrand Larsen on the Occasion
of His 60th Birthday,
Lecture Notes in Computer Science 10460, pages 367-381. Springer-Verlag, August 2017.
@inproceedings{kimfest2017-CDH,
author = {Chatterjee, Krishnendu and Doyen, Laurent and
Henzinger, Thomas A.},
title = {The Cost of Exactness in Quantitative Reachability},
editor = {Aceto, Luca and Bacci, Giorgio and Bacci, Giovanni
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-Verlag},
series = {Lecture Notes in Computer Science},
volume = {10460},
pages = {367-381},
year = {2017},
month = aug,
doi = {10.1007/978-3-319-63121-9_18},
}
[DKR+17]
ManfredDroste,
TemurKutsia,
GeorgeRahonis, and
WolfgangSchreiner.
MK-fuzzy Automata and MSO Logics.
In GandALF'17,
Electronic Proceedings in Theoretical Computer
Science 256, pages 106-120. September 2017.
@inproceedings{gandalf2017-DKRS,
author = {Droste, Manfred and Kutsia, Temur and Rahonis,
George and Schreiner, Wolfgang},
title = {{MK}-fuzzy Automata and {MSO} Logics},
editor = {Bouyer, Patricia and Orlandini, Andrea and
San{~}Pietro, Pierluigi},
booktitle = {{P}roceedings of the 8th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics and {F}ormal
{V}erification ({GandALF}'17)},
acronym = {{GandALF}'17},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {256},
pages = {106-120},
year = {2017},
month = sep,
doi = {10.4204/EPTCS.256.8},
}
[EGL+17]
JavierEsparza,
PierreGanty,
JérômeLeroux, and
RupakMajumdar.
Verification of Population Protocols.
Acta Informatica 54(2):191-215. Springer-Verlag, March 2017.
@article{atca54(2)-EGLM,
author = {Esparza, Javier and Ganty, Pierre and Leroux,
J{\'e}r{\^o}me and Majumdar, Rupak},
title = {Verification of Population Protocols},
publisher = {Springer-Verlag},
journal = {Acta Informatica},
volume = {54},
number = {2},
pages = {191-215},
year = {2017},
month = mar,
doi = {10.1007/s00236-016-0272-3},
}
Energy consumption problems (e.g., electric vehicles
charging) are very related to communication
problems. The "water-filling" algorithm can be used,
but it is not robust w.r.t. the noise of the
"non-flexible", i.e. not-controllable, energy
consumption forecasting. We propose a robust
algorithm using the probabilistic model-checker
PRISM, to exploit the idea of discretizing the
consumption action (as for a modulation to small
constellation) and the dynamic structure of the
problem in a Markov-decision-process model.
@inproceedings{gretsi2017-GBBLM,
author = {Gonz{\'a}lez, Mauricio and Beaude, Olivier and
Bouyer, Patricia and Lasaulce, Samson and Markey,
Nicolas},
title = {Strat{\'e}gies d'ordonnancement de consommation
d'{\'e}nergie en pr{\'e}sence d'information
imparfaite de pr{\'e}vision},
booktitle = {{A}ctes du 26{\`e}me {C}olloque du {G}roupe
d'{\'E}tudes du {T}raitement du {S}ignal et des
{I}mages ({GRETSI}'17)},
acronym = {{GRETSI}'17},
year = {2017},
month = sep,
abstract = {Energy consumption problems (e.g., electric vehicles
charging) are very related to communication
problems. The "water-filling" algorithm can be used,
but it is not robust w.r.t. the noise of the
"non-flexible", i.e. not-controllable, energy
consumption forecasting. We~propose a robust
algorithm using the probabilistic model-checker
PRISM, to exploit the idea of discretizing the
consumption action (as~for a modulation to small
constellation) and the dynamic structure of the
problem in a Markov-decision-process model.},
}
[GHP+17]
JulianGutierrez,
PaulHarrenstein,
GiuseppePerelli, and
MichaelWooldridge.
Nash Equilibrium and Bisimulation Invariance.
In CONCUR'17,
Leibniz International Proceedings in Informatics 85, pages 17:1-17:16. Leibniz-Zentrum für Informatik, September 2017.
@inproceedings{concur2017-GHPW,
author = {Gutierrez, Julian and Harrenstein, Paul and Perelli,
Giuseppe and Wooldridge, Michael},
title = {{N}ash Equilibrium and Bisimulation Invariance},
editor = {Meyer, Roland and Nestmann, Uwe},
booktitle = {{P}roceedings of the 28th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'17)},
acronym = {{CONCUR}'17},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {85},
pages = {17:1-17:16},
year = {2017},
month = sep,
doi = {10.4230/LIPIcs.CONCUR.2017.17},
}
[JBB+17]
SwenJacobs,
RoderickBloem,
RomainBrenguier,
RüdigerEhlers,
TimotheusHell,
RobertKönighofer,
Guillermo A.Pérez,
Jean-FrançoisRaskin,
LeonidRyzhyk,
OcanSankur,
MartinSeidl,
LeanderTentrup, and
AdamWalker.
The first reactive synthesis competition
(SYNTCOMP 2014).
International Journal on Software Tools for
Technology Transfer 19(3):367-390. Springer-Verlag, June 2017.
@article{sttt19(3)-JBBEHKPRRSSTW,
author = {Jacobs, Swen and Bloem, Roderick and Brenguier,
Romain and Ehlers, R{\"u}diger and Hell, Timotheus
and K{\"o}nighofer, Robert and P{\'e}rez, Guillermo
A. and Raskin, Jean-Fran{\c c}ois and Ryzhyk, Leonid
and Sankur, Ocan and Seidl, Martin and Tentrup,
Leander and Walker, Adam},
title = {The first reactive synthesis competition
({SYNTCOMP}~2014)},
publisher = {Springer-Verlag},
journal = {International Journal on Software Tools for
Technology Transfer},
volume = {19},
number = {3},
pages = {367-390},
year = {2017},
month = jun,
doi = {10.1007/s10009-016-0416-3},
}
@article{lmcs13(1)-MMPV,
author = {Mogavero, Fabio and Murano, Aniello and Perelli,
Giuseppe and Vardi, Moshe Y.},
title = {Reasoning About Strategies: On~the~Satisfiability
Problem},
journal = {Logical Methods in Computer Science},
volume = {13},
number = {1},
year = {2017},
month = mar,
doi = {10.23638/LMCS-13(1:9)2017},
}
@inproceedings{hscc2017-RPV,
author = {Roohi, Nima and Prabhakar, Pavithra and Viswanathan,
Mahesh},
title = {Robust model checking of timed automata under clock
drifts},
editor = {Frehse, Goran and Mitra, Sayan},
booktitle = {{P}roceedings of the 20th {I}nternational {W}orkshop
on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
({HSCC}'14)},
acronym = {{HSCC}'17},
publisher = {ACM Press},
pages = {153-162},
year = {2017},
month = apr,
doi = {10.1145/3049797.3049821},
}
[ST17]
OcanSankur and
Jean-PierreTalpin.
An Abstraction Technique For Parameterized Model
Checking of Leader Election Protocols: Application
to FTSP.
In TACAS'17,
Lecture Notes in Computer Science 10205.
Springer-Verlag, April 2017.
@inproceedings{tacas2017-ST,
author = {Sankur, Ocan and Talpin, Jean-Pierre},
title = {An~Abstraction Technique For Parameterized Model
Checking of Leader Election Protocols: Application
to~{FTSP}},
editor = {Legay, Axel and Margaria, Tiziana},
booktitle = {{P}roceedings of the 23rd {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'17)~-- {P}art~{I}},
acronym = {{TACAS}'17},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {10205},
year = {2017},
month = apr,
doi = {10.1007/978-3-662-54577-5_2},
}
@phdthesis{phd-stan,
author = {Stan, Daniel},
title = {Randomized strategies in concurrent games},
year = {2017},
month = mar,
school = {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
France},
type = {Th\`ese de doctorat},
}
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.
@article{ipl116(2)-BGM,
author = {Bouyer, Patricia and Gardy, Patrick and Markey,
Nicolas},
title = {On the semantics of Strategy Logic},
publisher = {Elsevier},
journal = {Information Processing Letters},
volume = {116},
number = {2},
pages = {75-79},
year = {2016},
month = feb,
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.},
}
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{cav2016-BCM,
author = {Bouyer, Patricia and Colange, Maximilien and Markey,
Nicolas},
title = {Symbolic Optimal Reachability in Weighted Timed
Automata},
editor = {Chaudhuri, Swarat and Farzan, Azadeh},
booktitle = {{P}roceedings of the 28th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'16)},
acronym = {{CAV}'16},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9779},
pages = {513-530},
year = {2016},
month = jul,
doi = {10.1007/978-3-319-41528-4_28},
url = {http://arxiv.org/abs/1602.00481},
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.},
}
We study the almost-sure reachability problem in a
distributed system obtained as the asynchronous
composition of N copies (called
processes) of the same automaton (called
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{icalp2016-BMRSS,
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},
editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael
and Rabani, Yuval and Sangiorgi, Davide},
booktitle = {{P}roceedings of the 43rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'16)~-- Part~{II}},
acronym = {{ICALP}'16},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {55},
pages = {106:1-106:14},
year = {2016},
month = jul,
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.},
}
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{gandalf2016-BMS,
author = {Bouyer, Patricia and Markey, Nicolas and Stan,
Daniel},
title = {Stochastic Equilibria under Imprecise Deviations in
Terminal-Reward Concurrent Games},
editor = {Cantone, Domenico and Delzanno, Giorgio},
booktitle = {{P}roceedings of the 7th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics and {F}ormal
{V}erification ({GandALF}'16)},
acronym = {{GandALF}'16},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {226},
pages = {61-75},
year = {2016},
month = sep,
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.},
}
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
QCTLk, 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 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 expressive power (i.e., their
ability to express a property), showing that in
terms of expressiveness the hierarchy
QCTLk collapses at level 2
(in other terms, any QCTL formula can be expressed
using at most two nested blocks of quantifiers).
@inproceedings{concur2016-DLM,
author = {David, Am{\'e}lie and Laroussinie, Fran{\c c}ois and
Markey, Nicolas},
title = {On~the expressiveness of~{QCTL}},
editor = {Desharnais, Jules and Jagadeesan, Radha},
booktitle = {{P}roceedings of the 27th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'16)},
acronym = {{CONCUR}'16},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {59},
pages = {28:1-28:15},
year = {2016},
month = aug,
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).},
}
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{syncop2015-FKM,
author = {Fribourg, Laurent and K{\"u}hne, Ulrich and Markey,
Nicolas},
title = {Game-based Synthesis of Distributed Controllers for
Sampled Switched Systems},
editor = {Andr{\'e}, {\'E}tienne and Frehse, Goran},
booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop
on {S}ynthesis of {C}omplex {P}arameters
({S}yn{C}o{P}'15)},
acronym = {{S}yn{C}o{P}'15},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {OpenAccess Series in Informatics},
volume = {44},
pages = {47-61},
year = {2016},
month = apr,
doi = {10.4230/OASIcs.SynCoP.2015.48},
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.},
}
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
211 = 2048 switching modes.
@inproceedings{rp2016-LFMDC,
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},
editor = {Larsen, Kim Guldstrand and Srba, Ji{\v r}{\'\i}},
booktitle = {{P}roceedings of the 10th {W}orkshop on
{R}eachability {P}roblems in {C}omputational
{M}odels ({RP}'16)},
acronym = {{RP}'16},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9899},
pages = {119-133},
year = {2016},
month = sep,
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.},
}
@proceedings{cassting-syncop2016-DJMS,
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)},
editor = {Brihaye, {\relax Th}omas and Delahaye, Beno{\^\i}t
and Jezequel, Lo{\"\i}g and Markey, Nicolas and
Srba, Ji{\v r}{\'\i}},
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},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {220},
year = {2016},
month = jul,
confyear = {2016},
confmonth = {4},
doi = {10.4204/EPTCS.220},
url = {http://eptcs.web.cse.unsw.edu.au/
content.cgi?CASSTINGSynCoP2016},
}
@proceedings{formats2016-FM,
title = {{P}roceedings of the 14th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'16)},
editor = {Fr{\"a}nzle, Martin and Markey, Nicolas},
booktitle = {{P}roceedings of the 14th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'16)},
acronym = {{FORMATS}'16},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9884},
year = {2016},
month = aug,
doi = {10.1007/978-3-319-44878-7},
url = {http://link.springer.com/book/10.1007/978-3-319-44878-7},
}
[ABB+16]
José BacelarAlmeida,
ManuelBarbosa,
GillesBarthe,
FrançoisDupressoir, and
MichaelEmmi.
Verifying Constant-Time Implementations.
In USENIX Security'16,
pages 53-70.
Usenix Association, August 2016.
@article{jacm63(3)-ABK,
author = {Almagor, Shaull and Boker, Udi and Kupferman, Orna},
title = {Formally Reasoning about Quality},
publisher = {ACM Press},
journal = {Journal of the~ACM},
volume = {63},
number = {3},
pages = {24:1-24:56},
year = {2016},
month = sep,
doi = {10.1145/2875421},
}
[AGK16]
S.Akshay,
PaulGastin, and
Shankara NarayananKrishna.
Analyzing Timed Systems Using Tree Automata.
In CONCUR'16,
Leibniz International Proceedings in Informatics 59, pages 27:1-27:14. Leibniz-Zentrum für Informatik, August 2016.
@inproceedings{concur2016-AGK,
author = {Akshay, S. and Gastin, Paul and Krishna, Shankara
Narayanan},
title = {Analyzing Timed Systems Using Tree Automata},
editor = {Desharnais, Jules and Jagadeesan, Radha},
booktitle = {{P}roceedings of the 27th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'16)},
acronym = {{CONCUR}'16},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {59},
pages = {27:1-27:14},
year = {2016},
month = aug,
doi = {10.4230/LIPIcs.CONCUR.2016.27},
}
[AHK16]
GuyAvni,
Thomas A.Henzinger, and
OrnaKupferman.
Dynamic Resource Allocation Games.
In SAGT'16,
Lecture Notes in Computer Science 9928, pages 153-166. Springer-Verlag, September 2016.
@inproceedings{sagt2016-AHK,
author = {Avni, Guy and Henzinger, Thomas A. and Kupferman,
Orna},
title = {Dynamic Resource Allocation Games},
booktitle = {{P}roceedings of the 9th {I}nternational {S}ymposium
on {A}lgorithmic {G}ame {T}heory ({SAGT}'16)},
acronym = {{SAGT}'16},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9928},
pages = {153-166},
year = {2016},
month = sep,
doi = {10.1007/978-3-662-53354-3_13},
}
[AJK16]
SimonAußerlechner,
SwenJacobs, and
AyratKhalimov.
Tight Cutoffs for Guarded Protocols with Fairness.
In VMCAI'16,
Lecture Notes in Computer Science 9583, pages 476-494. Springer-Verlag, January 2016.
@inproceedings{vmcai2016-AJK,
author = {Au{\ss}erlechner, Simon and Jacobs, Swen and
Khalimov, Ayrat},
title = {Tight Cutoffs for Guarded Protocols with Fairness},
editor = {Jobstmann, Barbara and Leino, K. Rustan M.},
booktitle = {{P}roceedings of the 17th {I}nternational {W}orkshop
on {V}erification, {M}odel {C}hecking, and
{A}bstract {I}nterpretation ({VMCAI}'16)},
acronym = {{VMCAI}'16},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9583},
pages = {476-494},
year = {2016},
month = jan,
doi = {10.1007/978-3-662-49122-5_23},
}
[AK16]
ShaullAlmagor and
OrnaKupferman.
High-Quality Synthesis Against Stochastic
Environments.
In CSL'16,
Leibniz International Proceedings in Informatics 62, pages 28:1-28:17. Leibniz-Zentrum für Informatik, September 2016.
@inproceedings{aamas2016-AMMR,
author = {Aminof, Benjamin and Malvone, Vadim and Murano,
Aniello and Rubin, Sasha},
title = {Graded Strategy Logic: Reasoning about Uniqueness of
Nash Equilibria},
editor = {Jonker, Catholijn M. and Marsella, Stacy and
Thangarajah, John and Tuyls, Karl},
booktitle = {{P}roceedings of the 15th {I}nternational
{C}onference on {A}utonomous {A}gents and
{M}ultiagent {S}ystems ({AAMAS}'16)},
acronym = {{AAMAS}'16},
publisher = {International Foundation for Autonomous Agents and
Multiagent Systems},
pages = {698-706},
year = {2016},
month = may,
}
@book{BO16-CSAPP,
author = {Bryant, Randal E. and O'Hallaron, David R.},
title = {Computer Systems~-- A~programmer's perspective},
publisher = {Pearson},
year = {2016},
}
[BPR+16]
RomainBrenguier,
Guillermo A.Pérez,
Jean-FrançoisRaskin, and
MathieuSassolas.
Admissibility in Quantitative Graph Games.
In FSTTCS'16,
Leibniz International Proceedings in Informatics, pages 42:1-42:14. Leibniz-Zentrum für Informatik, December 2016.
@inproceedings{fsttcs2016-BPRS,
author = {Brenguier, Romain and P{\'e}rez, Guillermo A. and
Raskin, Jean-Fran{\c c}ois and Sassolas, Mathieu},
title = {Admissibility in Quantitative Graph Games},
editor = {Akshay, S. and Lal, Akash and Saurabh, Saket and
Sen, Sandeep},
booktitle = {{P}roceedings of the 36th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'16)},
acronym = {{FSTTCS}'16},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
pages = {42:1-42:14},
year = {2016},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2016.42},
}
@inproceedings{icalp2016-CD,
author = {Chatterjee, Krishnendu and Doyen, Laurent},
title = {Computation Tree Logic for Synchronization
Properties},
editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael
and Rabani, Yuval and Sangiorgi, Davide},
booktitle = {{P}roceedings of the 43rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'16)~-- Part~{II}},
acronym = {{ICALP}'16},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {55},
pages = {98:1-98:14},
year = {2016},
month = jul,
doi = {10.4230/LIPIcs.ICALP.2016.98},
}
[CFG+16]
RodicaCondurache,
EmmanuelFiliot,
RaffaellaGentilini, and
Jean-FrançoisRaskin.
The Complexity of Rational Synthesis.
In ICALP'16,
Leibniz International Proceedings in Informatics 55, pages 121:1-121:15. Leibniz-Zentrum für Informatik, July 2016.
@inproceedings{icalp2016-CFGR,
author = {Condurache, Rodica and Filiot, Emmanuel and
Gentilini, Raffaella and Raskin, Jean-Fran{\c c}ois},
title = {The Complexity of Rational Synthesis},
editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael
and Rabani, Yuval and Sangiorgi, Davide},
booktitle = {{P}roceedings of the 43rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'16)~-- Part~{II}},
acronym = {{ICALP}'16},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {55},
pages = {121:1-121:15},
year = {2016},
month = jul,
doi = {10.4230/LIPIcs.ICALP.2016.121},
}
[DLF+16]
AlexandreDuret-Lutz,
AlexandreLewkowicz,
AmauryFauchille,
ThibaultMichaud,
ÉtienneRenault, and
LaurentXu.
Spot 2.0 – A Framework for LTL and
ω-Automata Manipulation.
In ATVA'16,
Lecture Notes in Computer Science 9938, pages 122-129. Springer-Verlag, October 2016.
@inproceedings{atva2016-DLFMRX,
author = {Duret{-}Lutz, Alexandre and Lewkowicz, Alexandre and
Fauchille, Amaury and Michaud, Thibault and Renault,
{\'E}tienne and Xu, Laurent},
title = {Spot~2.0~-- {A}~Framework for {LTL} and
{{\(\omega\)}}-Automata Manipulation},
editor = {Artho, Cyrille and Legay, Axel and Peled, Doron A.},
booktitle = {{P}roceedings of the 14th {I}nternational
{S}ymposium on {A}utomated {T}echnology for
{V}erification and {A}nalysis ({ATVA}'16)},
acronym = {{ATVA}'16},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9938},
pages = {122-129},
year = {2016},
month = oct,
doi = {10.1007/978-3-319-46520-3_8},
}
[EGL+16]
JavierEsparza,
PierreGanty,
JérômeLeroux, and
RupakMajumdar.
Model checking Population Protocols.
In FSTTCS'16,
Leibniz International Proceedings in Informatics, pages 27:1-27:14. Leibniz-Zentrum für Informatik, December 2016.
@inproceedings{fsttcs2016-EGLM,
author = {Esparza, Javier and Ganty, Pierre and Leroux,
J{\'e}r{\^o}me and Majumdar, Rupak},
title = {Model checking Population Protocols},
editor = {Akshay, S. and Lal, Akash and Saurabh, Saket and
Sen, Sandeep},
booktitle = {{P}roceedings of the 36th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'16)},
acronym = {{FSTTCS}'16},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
pages = {27:1-27:14},
year = {2016},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2016.27},
}
[FJM+16]
YlièsFalcone,
ThierryJéron,
HervéMarchand, and
SrinivasPinisetty.
Runtime enforcement of regular timed properties by
suppressing and delaying events.
Science of Computer Programming 123:2-41. Elsevier, July 2016.
@article{scp123()-FJMP,
author = {Falcone, Yli{\`e}s and J{\'e}ron, Thierry and
Marchand, Herv{\'e} and Pinisetty, Srinivas},
title = {Runtime enforcement of regular timed properties by
suppressing and delaying events},
publisher = {Elsevier},
journal = {Science of Computer Programming},
volume = {123},
pages = {2-41},
year = {2016},
month = jul,
doi = {10.1016/j.scico.2016.02.008},
}
[HK16]
LoïcHélouët and
KarimKecir.
Realizability of Schedules by Stochastic Time
Petri Nets with Blocking Semantics.
In PETRI NETS'16,
Lecture Notes in Computer Science 9698, pages 155-175. Springer-Verlag, June 2016.
@inproceedings{pn2016-HK,
author = {H{\'e}lou{\"e}t, Lo{\"\i}c and Kecir, Karim},
title = {Realizability of Schedules by Stochastic Time
{P}etri Nets with Blocking Semantics},
editor = {Kordon, Fabrice and Moldt, Daniel},
booktitle = {{P}roceedings of the 37th {I}nternational
{C}onference on {A}pplications and {T}heory of
{P}etri Nets and {C}oncurrency ({PETRI NETS}'16)},
acronym = {{PETRI~NETS}'16},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9698},
pages = {155-175},
year = {2016},
month = jun,
doi = {10.1007/978-3-319-39086-4_11},
}
@inproceedings{fsttcs2016-HSTW,
author = {Herbreteau, Fr{\'e}d{\'e}ric and Srivathsan, B. and
Tran, Thanh-Tung and Walukiewicz, Igor},
title = {Why liveness for timed automata is hard, and what we
can do about~it},
editor = {Akshay, S. and Lal, Akash and Saurabh, Saket and
Sen, Sandeep},
booktitle = {{P}roceedings of the 36th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'16)},
acronym = {{FSTTCS}'16},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
pages = {48:1-48:14},
year = {2016},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2016.48},
}
@article{icomp251()-HSW,
author = {Herbreteau, Fr{\'e}d{\'e}ric and Srivathsan, B. and
Walukiewicz, Igor},
title = {Efficient emptiness check for timed {B}{\"u}chi
automata},
publisher = {Elsevier},
journal = {Information and Computation},
volume = {251},
pages = {67-90},
year = {2016},
month = dec,
doi = {10.1016/j.ic.2016.07.004},
}
[JKP16]
WojciechJamroga,
BeataKonikowska, and
WojciechPenczek.
Multi-Valued Verification of Strategic Ability.
In AAMAS'16,
pages 1180-1189.
International Foundation for Autonomous Agents and
Multiagent Systems, May 2016.
@inproceedings{aamas2016-JKP,
author = {Jamroga, Wojciech and Konikowska, Beata and Penczek,
Wojciech},
title = {Multi-Valued Verification of Strategic Ability},
editor = {Jonker, Catholijn M. and Marsella, Stacy and
Thangarajah, John and Tuyls, Karl},
booktitle = {{P}roceedings of the 15th {I}nternational
{C}onference on {A}utonomous {A}gents and
{M}ultiagent {S}ystems ({AAMAS}'16)},
acronym = {{AAMAS}'16},
publisher = {International Foundation for Autonomous Agents and
Multiagent Systems},
pages = {1180-1189},
year = {2016},
month = may,
}
[KMP16]
Shankara NarayananKrishna,
KhushrajMadnani, and
Paritosh K.Pandya.
Metric Temporal Logic with Counting.
In FoSSaCS'16,
Lecture Notes in Computer Science 9634, pages 335-352. Springer-Verlag, April 2016.
@inproceedings{fossacs2016-KMP,
author = {Krishna, Shankara Narayanan and Madnani, Khushraj
and Pandya, Paritosh K.},
title = {Metric Temporal Logic with Counting},
editor = {Jacobs, Bart and L{\"o}ding, Christof},
booktitle = {{P}roceedings of the 19th {I}nternational
{C}onference on {F}oundations of {S}oftware
{S}cience and {C}omputation {S}tructure
({FoSSaCS}'16)},
acronym = {{FoSSaCS}'16},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9634},
pages = {335-352},
year = {2016},
month = apr,
doi = {10.1007/978-3-662-49630-5_20},
}
[KPV16]
OrnaKupferman,
GiuseppePerelli, and
Moshe Y.Vardi.
Synthesis with rational environments.
Annals of Mathematics and Artificial Intelligence 78(1):3-20. Kluwer Academic, September 2016.
@article{amai78(1)-KPV,
author = {Kupferman, Orna and Perelli, Giuseppe and Vardi,
Moshe Y.},
title = {Synthesis with rational environments},
publisher = {Kluwer Academic},
journal = {Annals of Mathematics and Artificial Intelligence},
volume = {78},
number = {1},
pages = {3-20},
year = {2016},
month = sep,
doi = {10.1007/s10472-016-9508-8},
}
@inproceedings{cav2016-LR,
author = {Lin, Anthony W. and R{\"u}mmer, Philipp},
title = {Liveness of Randomised Parameterised Systems under
Arbitrary Schedulers},
editor = {Chaudhuri, Swarat and Farzan, Azadeh},
booktitle = {{P}roceedings of the 28th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'16)},
acronym = {{CAV}'16},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9779},
pages = {112-133},
year = {2016},
month = jul,
doi = {10.1007/978-3-319-41540-6_7},
}
[PPT+16]
SrinivasPinisetty,
ViorelPreoteasa,
StavrosTripakis,
ThierryJéron,
YlièsFalcone, and
HervéMarchand.
Predictive Runtime Enforcement.
In SAC'16,
pages 1628-1633.
ACM Press, April 2016.
@inproceedings{sac2016-PPTJFM,
author = {Pinisetty, Srinivas and Preoteasa, Viorel and
Tripakis, Stavros and J{\'e}ron, Thierry and
Falcone, Yli{\`e}s and Marchand, Herv{\'e}},
title = {Predictive Runtime Enforcement},
editor = {Ossowski, Sascha},
booktitle = {{P}roceedings of the 31st {A}nnual {ACM} {S}ymposium
on {A}pplied {C}omputing ({SAC}'16)},
acronym = {{SAC}'16},
publisher = {ACM Press},
pages = {1628-1633},
year = {2016},
month = apr,
doi = {10.1145/2851613.2851827},
}
[PS16]
NicolasPerrin and
PhilippSchlehuber-Caissier.
Fast diffeomorphic matching to learn globally
asymptotically stable nonlinear dynamical systems.
Systems & Control Letters 96:51-59. Elsevier, October 2016.
@phdthesis{phd-vdb2016,
author = {Van{~}den{ }Bogaard, Marie},
title = {Motifs de flot d'information dans les jeux {\`a}
information imparfaite},
year = {2016},
month = dec,
school = {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
France},
type = {Th\`ese de doctorat},
}
We study pure-strategy Nash equilibria in
multiplayer concurrent games, for a variety of
omega-regular objectives. For simple objectives
(e.g. reachability, Bü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{lmcs11(2)-BBMU,
author = {Bouyer, Patricia and Brenguier, Romain and Markey,
Nicolas and Ummels, Michael},
title = {Pure {N}ash Equilibria in Concurrent Games},
journal = {Logical Methods in Computer Science},
volume = {11},
number = {2:9},
year = {2015},
month = jun,
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.},
}
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{tcs563()-BMS,
author = {Bouyer, Patricia and Markey, Nicolas and Sankur,
Ocan},
title = {Robust Reachability in Timed Automata and Games:
A~Game-based Approach},
publisher = {Elsevier},
journal = {Theoretical Computer Science},
volume = {563},
pages = {43-74},
year = {2015},
month = jan,
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.},
}
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.
We show that our
extension ATLsc is very expressive, but that its
decision problems are quite hard: model checking is
k-EXPTIME-complete when the formula has k
nested strategy quantifiers; satisfiability is
undecidable, but we prove that it is decidable when
restricting to turn-based games. Our algorithms are
obtained through a very convenient translation to
QCTL (the computation-tree logic CTL extended with
atomic quantification), which we show also applies
to Strategy Logic, as well as when strategy
quantification ranges over memoryless strategies.
@article{icomp245()-LM,
author = {Laroussinie, Fran{\c c}ois and Markey, Nicolas},
title = {Augmenting {ATL} with strategy contexts},
publisher = {Elsevier},
journal = {Information and Computation},
volume = {245},
pages = {98-123},
year = {2015},
month = dec,
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.},
}
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{formats2015-AM,
author = {Andr{\'e}, {\'E}tienne and Markey, Nicolas},
title = {Language Preservation Problems in Parametric Timed
Automata},
editor = {Sankaranarayanan, Sriram and Vicario, Enrico},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'15)},
acronym = {{FORMATS}'15},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9268},
pages = {27-43},
year = {2015},
month = sep,
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.},
}
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{avocs2015-BFM,
author = {Bouyer, Patricia and Fang, Erwin and Markey,
Nicolas},
title = {Permissive strategies in timed automata and games},
editor = {Grov, Gudmund and Ireland, Andrew},
booktitle = {{P}roceedings of the 15th {I}nternational {W}orkshop
on {A}utomated {V}erification of {C}ritical
{S}ystems ({AVOCS}'15)},
acronym = {{AVOCS}'15},
publisher = {European Association of Software Science and
Technology},
series = {Electronic Communications of the EASST},
volume = {72},
year = {2015},
month = sep,
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.},
}
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
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{fsttcs2015-BGM,
author = {Bouyer, Patricia and Gardy, Patrick and Markey,
Nicolas},
title = {Weighted strategy logic with boolean goals over
one-counter games},
editor = {Harsha, Prahladh and Ramalingam, G.},
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)},
acronym = {{FSTTCS}'15},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {45},
pages = {69-83},
year = {2015},
month = dec,
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.},
}
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.
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{concur2015-BJM,
author = {Bouyer, Patricia and Jaziri, Samy and Markey,
Nicolas},
title = {On~the Value Problem in Weighted Timed Games},
editor = {Aceto, Luca and de Frutos{-}Escrig, David},
booktitle = {{P}roceedings of the 26th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'15)},
acronym = {{CONCUR}'15},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {42},
pages = {311-324},
year = {2015},
month = sep,
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.},
}
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 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{formats2015-BMPS,
author = {Bouyer, Patricia and Markey, Nicolas and Perrin,
Nicolas and Schlehuber{-}Caissier, Philipp},
title = {Timed automata abstraction of switched dynamical
systems using control funnels},
editor = {Sankaranarayanan, Sriram and Vicario, Enrico},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'15)},
acronym = {{FORMATS}'15},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9268},
pages = {60-75},
year = {2015},
month = sep,
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.},
}
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{gandalf2015-BMRLL,
author = {Bouyer, Patricia and Markey, Nicolas and Randour,
Mickael and Larsen, Kim Guldstrand and Laursen,
Simon},
title = {Average-energy games},
editor = {Esparza, Javier and Tronci, Enrico},
booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics and {F}ormal
{V}erification ({GandALF}'15)},
acronym = {{GandALF}'15},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {193},
pages = {1-15},
year = {2015},
month = sep,
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.},
}
Alternating-time temporal logic with strategy
contexts (ATLsc) is a
powerful formalism for expressing properties of
multi-agent systems: it extends CTL with
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
uniform incomplete observation (where all
players have the same observation) preserves
decidability of the model checking problem, even for
very expressive logics such as
ATLsc.
@inproceedings{gandalf2015-LMS,
author = {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
Sangnier, Arnaud},
title = {{{\(\textsf{ATL}_{\textsf{sc}}\)}} with partial
observation},
editor = {Esparza, Javier and Tronci, Enrico},
booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics and {F}ormal
{V}erification ({GandALF}'15)},
acronym = {{GandALF}'15},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {193},
pages = {43-57},
year = {2015},
month = sep,
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}}\)}}.},
}
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).
@proceedings{dagrep5(2)-CLMT,
title = {Non-Zero-Sum-Games and Control ({D}agstuhl
Seminar~15061)},
editor = {Chatterjee, Krishnendu and Lafortune, St{\'e}phane
and Markey, Nicolas and Thomas, Wolfgang},
booktitle = {Non-Zero-Sum-Games and Control ({D}agstuhl
Seminar~15061)},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
journal = {Dagstuhl Reports},
volume = {5},
number = {2},
pages = {1-25},
year = {2015},
month = jun,
doi = {10.4230/DagRep.5.2.1},
url = {http://drops.dagstuhl.de/opus/volltexte/2015/5042},
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).},
}
[AAG+15]
ManindraAgrawal,
S.Akshay,
BlaiseGenest, and
P. S.Thiagarajan.
Approximate Verification of the Symbolic Dynamics of
Markov Chains.
Journal of the ACM 62(1):183-235. ACM Press, February 2015.
@article{jacm62(1)-AAGT,
author = {Agrawal, Manindra and Akshay, S. and Genest, Blaise
and Thiagarajan, P. S.},
title = {Approximate Verification of the Symbolic Dynamics of
{M}arkov Chains},
publisher = {ACM Press},
journal = {Journal of the~ACM},
volume = {62},
number = {1},
pages = {183-235},
year = {2015},
month = feb,
doi = {10.1145/2629417},
}
@inproceedings{concur2015-ABG,
author = {Aiswarya, C. and Bollig, Benedikt and Gastin, Paul},
title = {An automata-theoretic approach to the verification
of distributed algorithms},
editor = {Aceto, Luca and de Frutos{-}Escrig, David},
booktitle = {{P}roceedings of the 26th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'15)},
acronym = {{CONCUR}'15},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {42},
pages = {340-353},
year = {2015},
month = sep,
doi = {10.4230/LIPIcs.CONCUR.2015.340},
}
[AKK15]
ShaullAlmagor,
DenisKuperberg, and
OrnaKupferman.
The Sensing Cost of Monitoring and Synthesis.
In FSTTCS'15,
Leibniz International Proceedings in Informatics 45, pages 380-393. Leibniz-Zentrum für Informatik, December 2015.
@inproceedings{fsttcs2015-AKK,
author = {Almagor, Shaull and Kuperberg, Denis and Kupferman,
Orna},
title = {The~Sensing Cost of Monitoring and Synthesis},
editor = {Harsha, Prahladh and Ramalingam, G.},
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)},
acronym = {{FSTTCS}'15},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {45},
pages = {380-393},
year = {2015},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2015.380},
}
@inproceedings{lpar2015-ARZ,
author = {Aminof, Benjamin and Rubin, Sasha and Zuleger,
Florian},
title = {On the Expressive Power of Communication Primitives
in Parameterised Systems},
editor = {Davis, Martin and Fehnker, Ansgar and McIver,
Annabelle K. and Voronkov, Andrei},
booktitle = {{P}roceedings of the 20th {I}nternational
{C}onference {L}ogic {P}rogramming and {A}utomated
{R}easoning ({LPAR}'15)},
acronym = {{LPAR}'15},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9450},
pages = {313-328},
year = {2015},
month = nov,
doi = {10.1007/978-3-662-48899-7_22},
}
[BBL+15]
NikolaBeneš,
PetrBezdek,
Kim GuldstrandLarsen, and
JiříSrba.
Language Emptiness of Continuous-Time Parametric
Timed Automata.
In ICALP'15,
Lecture Notes in Computer Science 9135, pages 69-81. Springer-Verlag, July 2015.
@inproceedings{icalp2015-BBLS,
author = {Bene{\v{s}}, Nikola and Bezdek, Petr and Larsen, Kim
Guldstrand and Srba, Ji{\v r}{\'\i}},
title = {Language Emptiness of Continuous-Time Parametric
Timed Automata},
editor = {Halld{\'o}rsson, Magn{\'u}s M. and Iwana, Kazuo and
Kobayashi, Naoki and Speckmann, Bettina},
booktitle = {{P}roceedings of the 42nd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'15)~-- Part~{II}},
acronym = {{ICALP}'15},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9135},
pages = {69-81},
year = {2015},
month = jul,
doi = {10.1007/978-3-662-47666-6_6},
}
[BBM+15]
ThomasBrihaye,
VéroniqueBruyère,
NoëmieMeunier, and
Jean-FrançoisRaskin.
Weak Subgame Perfect Equilibria and their
Application to Quantitative Reachability.
In CSL'15,
Leibniz International Proceedings in Informatics 41, pages 504-518. Leibniz-Zentrum für Informatik, September 2015.
@inproceedings{stacs2015-BEGM,
author = {Boros, Endre and Elbassioni, Khaled and Gurvich,
Vladimir and Makino, Kazuhisa},
title = {{M}arkov Decision Processes and Stochastic Games
with Total Effective Payoff},
editor = {Mayr, Ernst W. and Ollinger, Nicolas},
booktitle = {{P}roceedings of the 32nd {S}ymposium on
{T}heoretical {A}spects of {C}omputer {S}cience
({STACS}'15)},
acronym = {{STACS}'15},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {30},
pages = {103-115},
year = {2015},
month = mar,
doi = {10.4230/LIPIcs.STACS.2015.103},
}
[BFA15]
UmangBhaskar,
LisaFleischer, and
ElliotAnshelevich.
A Stackelberg strategy for routing flow over time.
Games and Economic Behavior 92:232-247. July 2015.
@article{geb92()-BFA,
author = {Bhaskar, Umang and Fleischer, Lisa and Anshelevich,
Elliot},
title = {A~{S}tackelberg strategy for routing flow over time},
journal = {Games and Economic Behavior},
volume = {92},
pages = {232-247},
year = {2015},
month = jul,
doi = {10.1016/j.geb.2013.09.004},
}
[BFS15]
NathalieBertrand,
PaulinFournier, and
ArnaudSangnier.
Distributed Local Strategies in Broadcast Networks.
In CONCUR'15,
Leibniz International Proceedings in Informatics 42, pages 44-57. Leibniz-Zentrum für Informatik, September 2015.
@inproceedings{concur2015-BFS,
author = {Bertrand, Nathalie and Fournier, Paulin and
Sangnier, Arnaud},
title = {Distributed Local Strategies in Broadcast Networks},
editor = {Aceto, Luca and de Frutos{-}Escrig, David},
booktitle = {{P}roceedings of the 26th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'15)},
acronym = {{CONCUR}'15},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {42},
pages = {44-57},
year = {2015},
month = sep,
doi = {10.4230/LIPIcs.CONCUR.2015.44},
}
[BGH+15]
ThomasBrihaye,
GillesGeeraerts,
AxelHaddad,
EngelLefaucheux, and
BenjaminMonmege.
Simple priced timed games are not that simple.
In FSTTCS'15,
Leibniz International Proceedings in Informatics 45, pages 278-292. Leibniz-Zentrum für Informatik, December 2015.
@inproceedings{fsttcs2005-BGHLM,
author = {Brihaye, {\relax Th}omas and Geeraerts, Gilles and
Haddad, Axel and Lefaucheux, Engel and Monmege,
Benjamin},
title = {Simple priced timed games are not that simple},
editor = {Harsha, Prahladh and Ramalingam, G.},
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)},
acronym = {{FSTTCS}'15},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {45},
pages = {278-292},
year = {2015},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2015.278},
}
@inproceedings{atva2015-BMV,
author = {Berwanger, Dietmar and Mathew, Anup Basil and
Van{~}den{ }Bogaard, Marie},
title = {Hierarchical Information Patterns and Distributed
Strategy Synthesis},
editor = {Finkbeiner, Bernd and Pu, Geguang and Zhang, Lijun},
booktitle = {{P}roceedings of the 13th {I}nternational
{S}ymposium on {A}utomated {T}echnology for
{V}erification and {A}nalysis ({ATVA}'15)},
acronym = {{ATVA}'15},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9364},
pages = {378-393},
year = {2015},
month = oct,
}
@article{icomp242()-CDRR,
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},
publisher = {Elsevier},
journal = {Information and Computation},
volume = {242},
pages = {25-52},
year = {2015},
month = jun,
doi = {10.1016/j.ic.2015.03.010},
}
@inproceedings{aaai2015-CLM,
author = {{\v{C}}erm{\'a}k, Petr and Lomuscio, Alessio and
Murano, Aniello},
title = {Verifying and Synthesising Multi-Agent Systems
against One-Goal Strategy Logic Specifications},
editor = {Bonet, Blai and Koenig, Sven},
booktitle = {{P}roceedings of the 29th {AAAI} {C}onference on
{A}rtificial {I}ntelligence ({AAAI}'15)},
acronym = {{AAAI}'15},
publisher = {AAAI Press},
pages = {2038-2044},
year = {2015},
month = jan,
}
@inproceedings{cav2015-DEGM,
author = {Durand{-}Gasselin, Antoine and Esparza, Javier and
Ganty, Pierre and Majumdar, Rupak},
title = {Model Checking Parameterized Asynchronous
Shared-Memory Systems},
editor = {Kroening, Daniel and Pasareanu, Corina S.},
booktitle = {{P}roceedings of the 27th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'15)},
acronym = {{CAV}'15},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9206},
pages = {67-84},
year = {2015},
month = jul,
doi = {10.1007/978-3-319-21690-4_5},
}
[DJL+15]
AlexandreDavid,
Peter GjølJensen,
Kim GuldstrandLarsen,
MariusMikučionis, and
Jakob HaarTaankvist.
Uppaal Stratego.
In TACAS'15,
Lecture Notes in Computer Science 9035, pages 206-211. Springer-Verlag, April 2015.
@inproceedings{tacas2015-DLLMW,
author = {David, Alexandre and Jensen, Peter Gj{\o}l and
Larsen, Kim Guldstrand and Miku{\v{c}}ionis, Marius
and Taankvist, Jakob Haar},
title = {Uppaal Stratego},
editor = {Baier, {\relax Ch}ristel and Tinelli, Cesare},
booktitle = {{P}roceedings of the 21st {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'15)},
acronym = {{TACAS}'15},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9035},
pages = {206-211},
year = {2015},
month = apr,
doi = {10.1007/978-3-662-46681-0_16},
}
[DKM+15]
SamirDatta,
RaghavKulkarni,
AnishMukherjee,
ThomasSchwentick, and
ThomasZeume.
Reachability is in DynFO.
In ICALP'15,
Lecture Notes in Computer Science 9135, pages 159-170. Springer-Verlag, July 2015.
@inproceedings{icalp2015-DKMSZ,
author = {Datta, Samir and Kulkarni, Raghav and Mukherjee,
Anish and Schwentick, Thomas and Zeume, Thomas},
title = {Reachability is in {D}yn{F}O},
editor = {Halld{\'o}rsson, Magn{\'u}s M. and Iwana, Kazuo and
Kobayashi, Naoki and Speckmann, Bettina},
booktitle = {{P}roceedings of the 42nd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'15)~-- Part~{II}},
acronym = {{ICALP}'15},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9135},
pages = {159-170},
year = {2015},
month = jul,
doi = {10.1007/978-3-662-47666-6_13},
}
[DSQ+15]
AnkushDesai,
Sanjit A.Seshia,
ShazQadeer,
DavidBroman, and
John C.Eidson.
Approximate synchrony: An abstraction for
distributed almost-synchronous systems.
In CAV'15,
Lecture Notes in Computer Science 9206, pages 429-448. Springer-Verlag, July 2015.
@inproceedings{cav2015-DSQBE,
author = {Desai, Ankush and Seshia,Sanjit A. and Qadeer, Shaz
and Broman, David and Eidson, John C.},
title = {Approximate synchrony: An abstraction for
distributed almost-synchronous systems},
editor = {Kroening, Daniel and Pasareanu, Corina S.},
booktitle = {{P}roceedings of the 27th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'15)},
acronym = {{CAV}'15},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9206},
pages = {429-448},
year = {2015},
month = jul,
doi = {10.1007/978-3-319-21668-3_25},
}
[EGL+15]
JavierEsparza,
PierreGanty,
JérômeLeroux, and
RupakMajumdar.
Verification of Population Protocols.
In CONCUR'15,
Leibniz International Proceedings in Informatics 42, pages 470-482. Leibniz-Zentrum für Informatik, September 2015.
@inproceedings{concur2015-EGLM,
author = {Esparza, Javier and Ganty, Pierre and Leroux,
J{\'e}r{\^o}me and Majumdar, Rupak},
title = {Verification of Population Protocols},
editor = {Aceto, Luca and de Frutos{-}Escrig, David},
booktitle = {{P}roceedings of the 26th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'15)},
acronym = {{CONCUR}'15},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {42},
pages = {470-482},
year = {2015},
month = sep,
doi = {10.4230/LIPIcs.CONCUR.2015.470},
}
@phdthesis{phd-fournier,
author = {Fournier, Paulin},
title = {Parameterized verification of networks of many
identical processes},
year = {2015},
month = dec,
school = {Universit{\'e} Rennes~1, France},
type = {Th\`ese de doctorat},
}
[FT15]
JieFu and
UfukTopcu.
Computational methods for stochastic control with
metric interval temporal logic specifications.
Research Report 1503.07193, arXiv, March 2015.
@techreport{arxiv1503.07193-FT,
author = {Fu, Jie and Topcu, Ufuk},
title = {Computational methods for stochastic control with
metric interval temporal logic specifications},
number = {1503.07193},
year = {2015},
month = mar,
institution = {arXiv},
type = {Research Report},
}
@inproceedings{fossacs2015-Gan,
author = {Ganardi, Moses},
title = {Parity Games of Bounded Tree- and Clique-Width},
editor = {Pitts, Andrew},
booktitle = {{P}roceedings of the 18th {I}nternational
{C}onference on {F}oundations of {S}oftware
{S}cience and {C}omputation {S}tructure
({FoSSaCS}'15)},
acronym = {{FoSSaCS}'15},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9034},
pages = {390-404},
year = {2015},
month = apr,
doi = {10.1007/978-3-662-46678-0_25},
}
[HT15]
FrédéricHerbreteau and
Thanh-TungTran.
Improving Search Order for Reachability Testing in
Timed Automata.
In FORMATS'15,
Lecture Notes in Computer Science 9268, pages 124-139. Springer-Verlag, September 2015.
@inproceedings{formats2015-HT,
author = {Herbreteau, Fr{\'e}d{\'e}ric and Tran, Thanh-Tung},
title = {Improving Search Order for Reachability Testing in
Timed Automata},
editor = {Sankaranarayanan, Sriram and Vicario, Enrico},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'15)},
acronym = {{FORMATS}'15},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9268},
pages = {124-139},
year = {2015},
month = sep,
doi = {10.1007/978-3-319-22975-1_9},
}
@article{tse41(5)-JLR,
author = {Jovanovi{\'c}, Aleksandra and Lime, Didier and Roux,
Olivier H.},
title = {Integer Parameter Synthesis for Timed Automata},
publisher = {IEEE Comp. Soc. Press},
journal = {IEEE Transactions on Software Engineering},
volume = {41},
number = {5},
pages = {445-461},
year = {2015},
month = may,
doi = {10.1109/TSE.2014.2357445},
}
[JLS15]
MarcinJurdziński,
RankoLazić, and
SylvainSchmitz.
Fixed-Dimensional Energy Games are in
Pseudo-Polynomial Time.
In ICALP'15,
Lecture Notes in Computer Science 9135, pages 260-272. Springer-Verlag, July 2015.
@inproceedings{icalp2015-JLS,
author = {Jurdzi{\'n}ski, Marcin and Lazi{\'c}, Ranko and
Schmitz, Sylvain},
title = {Fixed-Dimensional Energy Games are in
Pseudo-Polynomial Time},
editor = {Halld{\'o}rsson, Magn{\'u}s M. and Iwana, Kazuo and
Kobayashi, Naoki and Speckmann, Bettina},
booktitle = {{P}roceedings of the 42nd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'15)~-- Part~{II}},
acronym = {{ICALP}'15},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9135},
pages = {260-272},
year = {2015},
month = jul,
doi = {10.1007/978-3-662-47666-6_21},
}
@inproceedings{icalp2015-KS,
author = {Kuperberg, Denis and Skrzypczak, Michal},
title = {On determinisation of good-for-games automata},
editor = {Halld{\'o}rsson, Magn{\'u}s M. and Iwana, Kazuo and
Kobayashi, Naoki and Speckmann, Bettina},
booktitle = {{P}roceedings of the 42nd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'15)~-- Part~{II}},
acronym = {{ICALP}'15},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9135},
pages = {299-310},
year = {2015},
month = jul,
doi = {10.1007/978-3-662-47666-6_24},
}
@inproceedings{cav2015-KVW,
author = {Konnov, Igor V. and Veith, Helmut and Widder, Josef},
title = {{SMT} and {POR} bea Counter Abstraction:
Parameterized Model Checking of Threshold-Based
Distributed Algorithms},
editor = {Kroening, Daniel and Pasareanu, Corina S.},
booktitle = {{P}roceedings of the 27th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'15)},
acronym = {{CAV}'15},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9206},
pages = {85-102},
year = {2015},
month = jul,
doi = {10.1007/978-3-319-21690-4_6},
}
[LLZ15]
Kim GuldstrandLarsen,
SimonLaursen, and
MartinZimmermann.
Limit Your Consumption! Finding Bounds in
Average-energy Games.
Research Report 1510.05774, arXiv, October 2015.
@techreport{arxiv-1510.05774,
author = {Larsen, Kim Guldstrand and Laursen, Simon and
Zimmermann, Martin},
title = {Limit Your Consumption! Finding Bounds in
Average-energy Games},
number = {1510.05774},
year = {2015},
month = oct,
institution = {arXiv},
type = {Research Report},
}
[MVZ15]
PabloMuñoz,
NilsVortmeier, and
ThomasZeume.
Dynamic Graph Queries.
Research Report 1512.05511, arXiv, December 2015.
@techreport{arxiv-1512.05511,
author = {Mu{\~n}oz, Pablo and Vortmeier, Nils and Zeume,
Thomas},
title = {Dynamic Graph Queries},
number = {1512.05511},
year = {2015},
month = dec,
institution = {arXiv},
type = {Research Report},
}
[San15]
OcanSankur.
Symbolic Quantitative Robustness Analysis of Timed
Automata.
In TACAS'15,
Lecture Notes in Computer Science 9035, pages 484-498. Springer-Verlag, April 2015.
@inproceedings{tacas2015-San,
author = {Sankur, Ocan},
title = {Symbolic Quantitative Robustness Analysis of Timed
Automata},
editor = {Baier, {\relax Ch}ristel and Tinelli, Cesare},
booktitle = {{P}roceedings of the 21st {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'15)},
acronym = {{TACAS}'15},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9035},
pages = {484-498},
year = {2015},
month = apr,
doi = {10.1007/978-3-662-46681-0_48},
}
[Thi15]
YannThierry-Mieg.
Symbolic Model-Checking Using ITS-Tools.
In TACAS'15,
Lecture Notes in Computer Science 9035, pages 231-237. Springer-Verlag, April 2015.
@inproceedings{tacas2015-Thi,
author = {Thierry{-}Mieg, Yann},
title = {Symbolic Model-Checking Using {ITS}-Tools},
editor = {Baier, {\relax Ch}ristel and Tinelli, Cesare},
booktitle = {{P}roceedings of the 21st {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'15)},
acronym = {{TACAS}'15},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9035},
pages = {231-237},
year = {2015},
month = apr,
doi = {10.1007/978-3-662-46681-0_20},
}
[VCD+15]
YaronVelner,
KrishnenduChatterjee,
LaurentDoyen,
Thomas A.Henzinger,
AlexanderRabinovich, and
Jean-FrançoisRaskin.
The complexity of multi-mean-payoff and multi-energy
games.
Information and Computation 241:177-196. Elsevier, April 2015.
@article{icomp241()-VCDHRR,
author = {Velner, Yaron and Chatterjee, Krishnendu and Doyen,
Laurent and Henzinger, Thomas A. and Rabinovich,
Alexander and Raskin, Jean-Fran{\c c}ois},
title = {The complexity of multi-mean-payoff and multi-energy
games},
publisher = {Elsevier},
journal = {Information and Computation},
volume = {241},
pages = {177-196},
year = {2015},
month = apr,
doi = {10.1016/j.ic.2015.03.001},
}
[Ves15]
SteenVester.
On the Complexity of Model-checking Branching and
Alternating-time Temporal Logics in One-counter
systems.
In ATVA'15,
Lecture Notes in Computer Science 9364, pages 361-377. Springer-Verlag, October 2015.
@inproceedings{atva2015-Ves,
author = {Vester, Steen},
title = {On the Complexity of Model-checking Branching and
Alternating-time Temporal Logics in One-counter
systems},
editor = {Finkbeiner, Bernd and Pu, Geguang and Zhang, Lijun},
booktitle = {{P}roceedings of the 13th {I}nternational
{S}ymposium on {A}utomated {T}echnology for
{V}erification and {A}nalysis ({ATVA}'15)},
acronym = {{ATVA}'15},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9364},
pages = {361-377},
year = {2015},
month = oct,
doi = {10.1007/978-3-319-24953-7_27},
}
@article{toplas37(3)-WSH,
author = {Wang, Farn and Schewe, Sven and Huang, Chung-Hao},
title = {An~extension of~{ATL} with Strategy Interaction},
publisher = {ACM Press},
journal = {ACM Transactions on Programming Languages and
Systems},
volume = {37},
number = {3},
year = {2015},
month = jun,
doi = {10.1145/2734117},
}
We investigate a number of problems related to
infinite runs of weighted timed automata (with a
single weight variable), subject to lower-bound
constraints on the accumulated weight. Closing an
open problem from an earlier paper, we show that the
existence of an infinite lower-bound-constrained run
is–for us somewhat unexpectedly–undecidable for
weighted timed automata with four or more
clocks.
This undecidability result assumes a
fixed and known initial credit. We show that the
related problem of existence of an initial credit
for which there exists a feasible run is decidable
in PSPACE. We also investigate the variant of these
problems where only bounded-duration runs are
considered, showing that this restriction makes our
original problem decidable in NEXPTIME. We prove
that the universal versions of all those problems
(i.e, checking that all the considered runs satisfy
the lower-bound constraint) are decidable in
PSPACE.
Finally, we extend this study to
multi-weighted timed automata: the existence of a
feasible run becomes undecidable even for bounded
duration, but the existence of initial credits
remains decidable (in PSPACE).
@article{peva73()-BLM,
author = {Bouyer, Patricia and Larsen, Kim Guldstrand and
Markey, Nicolas},
title = {Lower-Bound Constrained Runs in Weighted Timed
Automata},
publisher = {Elsevier},
journal = {Performance Evaluation},
volume = {73},
pages = {91-109},
year = {2014},
month = mar,
doi = {10.1016/j.peva.2013.11.002},
abstract = {We investigate a number of problems related to
infinite runs of weighted timed automata (with a
single weight variable), subject to lower-bound
constraints on the accumulated weight. Closing an
open problem from an earlier paper, we show that the
existence of an infinite lower-bound-constrained run
is--for us somewhat unexpectedly--undecidable for
weighted timed automata with four or more
clocks.\par This undecidability result assumes a
fixed and known initial credit. We show that the
related problem of existence of an initial credit
for which there exists a feasible run is decidable
in PSPACE. We also investigate the variant of these
problems where only bounded-duration runs are
considered, showing that this restriction makes our
original problem decidable in NEXPTIME. We prove
that the universal versions of all those problems
(i.e, checking that all the considered runs satisfy
the lower-bound constraint) are decidable in
PSPACE.\par Finally, we extend this study to
multi-weighted timed automata: the existence of a
feasible run becomes undecidable even for bounded
duration, but the existence of initial credits
remains decidable (in~PSPACE).},
}
While it was defined long ago, the extension of CTL
with quantification over atomic propositions has
never been studied extensively. Considering two
different semantics (depending whether propositional
quantification refers to the Kripke structure or to
its unwinding tree), we study its expressiveness
(showing in particular that QCTL coincides with
Monadic Second-Order Logic for both semantics) and
characterise the complexity of its model-checking
and satisfiability problems, depending on the number
of nested propositional quantifiers (showing that
the structure semantics populates the polynomial
hierarchy while the tree semantics populates the
exponential hierarchy).
@article{lmcs10(4)-LM,
author = {Laroussinie, Fran{\c c}ois and Markey, Nicolas},
title = {Quantified~{CTL}: expressiveness and complexity},
journal = {Logical Methods in Computer Science},
volume = {10},
number = {4},
year = {2014},
month = dec,
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).},
}
We define and study a new approach to the
implementability of timed automata, where the
semantics is perturbed by imprecisions and finite
frequency of the hardware. In order to circumvent
these effects, we introduce parametric
shrinking of clock constraints, which corresponds
to tightening the guards. We propose symbolic
procedures to decide the existence of (and then
compute) parameters under which the shrunk version
of a given timed automaton is non-blocking and can
time-abstract simulate the exact semantics. We then
define an implementation semantics for timed
automata with a digital clock and positive reaction
times, and show that for shrinkable timed automata,
non-blockingness and time-abstract simulation are
preserved in implementation.
@article{icomp234()-SBM,
author = {Sankur, Ocan and Bouyer, Patricia and Markey,
Nicolas},
title = {Shrinking Timed Automata},
publisher = {Elsevier},
journal = {Information and Computation},
volume = {234},
pages = {107-132},
year = {2014},
month = feb,
doi = {10.1016/j.ic.2014.01.002},
abstract = {We define and study a new approach to the
implementability of timed automata, where the
semantics is perturbed by imprecisions and finite
frequency of the hardware. In order to circumvent
these effects, we introduce \emph{parametric
shrinking} of clock constraints, which corresponds
to tightening the guards. We propose symbolic
procedures to decide the existence of (and then
compute) parameters under which the shrunk version
of a given timed automaton is non-blocking and can
time-abstract simulate the exact semantics. We then
define an implementation semantics for timed
automata with a digital clock and positive reaction
times, and show that for shrinkable timed automata,
non-blockingness and time-abstract simulation are
preserved in implementation.},
}
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{atva2014-BGM,
author = {Bouyer, Patricia and Gardy, Patrick and Markey,
Nicolas},
title = {Quantitative verification of weighted {K}ripke
structures},
editor = {Cassez, Franck and Raskin, Jean-Fran{\c c}ois},
booktitle = {{P}roceedings of the 12th {I}nternational
{S}ymposium on {A}utomated {T}echnology for
{V}erification and {A}nalysis ({ATVA}'14)},
acronym = {{ATVA}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8837},
pages = {64-80},
year = {2014},
month = nov,
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.},
}
[BMM14]
PatriciaBouyer,
NicolasMarkey, and
Raj MohanMatteplackel.
Averaging in LTL.
In CONCUR'14,
Lecture Notes in Computer Science 8704, pages 266-280. Springer-Verlag, September 2014.
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!
In a
recent line of works, several authors have proposed
quantitative semantics for temporal logics, using
e.g. discounting modalities (which give less
importance to distant events). In the present paper,
we define and study a quantitative semantics of LTL
with averaging modalities, either on the long
run or within an until modality. This, in a way,
relaxes the classical Boolean semantics of LTL, and
provides a measure of certain properties of a model.
We prove that computing and even approximating the
value of a formula in this logic is undecidable.
@inproceedings{concur2014-BMM,
author = {Bouyer, Patricia and Markey, Nicolas and
Matteplackel, Raj~Mohan},
title = {Averaging in~{LTL}},
editor = {Baldan, Paolo and Gorla, Daniele},
booktitle = {{P}roceedings of the 25th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'14)},
acronym = {{CONCUR}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8704},
pages = {266-280},
year = {2014},
month = sep,
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.},
}
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.
@inproceedings{fsttcs2014-BMS,
author = {Bouyer, Patricia and Markey, Nicolas and Stan,
Daniel},
title = {Mixed {N}ash Equilibria in Concurrent Games},
editor = {Raman, Venkatesh and Suresh, S. P.},
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)},
acronym = {{FSTTCS}'14},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {29},
pages = {351-363},
year = {2014},
month = dec,
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.},
}
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{sr2014-BMV,
author = {Bouyer, Patricia and Markey, Nicolas and Vester,
Steen},
title = {Nash Equilibria in Symmetric Games with Partial
Observation},
booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop
on {S}trategic {R}easoning ({SR}'14)},
acronym = {{SR}'14},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {146},
pages = {49-55},
year = {2014},
month = mar,
doi = {10.4204/EPTCS.146.7},
abstract = {We investigate a model for representing large
multiplayer games, which satisfy strong symmetry
properties. This model is made of multiple copies of
an arena; each player plays in his own arena, and
can partially observe what the other players do.
Therefore, this game has partial information and
symmetry constraints, which make the computation of
Nash equilibria difficult. We show several
undecidability results, and for bounded-memory
strategies, we precisely characterize the complexity
of computing pure Nash equilibria (for qualitative
objectives) in this game model.},
}
The problem of synchronizing automata is concerned
with the existence of a word that sends all states
ofM 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.
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{fsttcs2014-DJLMS,
author = {Doyen, Laurent and Juhl, Line and Larsen, Kim
Guldstrand and Markey, Nicolas and Shirmohammadi,
Mahsa},
title = {Synchronizing words for weighted and timed automata},
editor = {Raman, Venkatesh and Suresh, S. P.},
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)},
acronym = {{FSTTCS}'14},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {29},
pages = {121-132},
year = {2014},
month = dec,
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
ofM 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.},
}
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*, 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*.
@inproceedings{atva2014-MV,
author = {Markey, Nicolas and Vester, Steen},
title = {Symmetry Reduction in Infinite Games with Finite
Branching},
editor = {Cassez, Franck and Raskin, Jean-Fran{\c c}ois},
booktitle = {{P}roceedings of the 12th {I}nternational
{S}ymposium on {A}utomated {T}echnology for
{V}erification and {A}nalysis ({ATVA}'14)},
acronym = {{ATVA}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8837},
pages = {281-296},
year = {2014},
month = nov,
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{*}.},
}
Formal methods (e.g. Timed Automata or Linear Hybrid
Automata) can be used to analyse a real-time system
by performing a reachability analysis on the model.
The advantage of using formal methods is that they
are more expressive than classical analytic models
used in schedulability analysis. For example, it is
possible to express state-dependent behaviour,
arbitrary activation patterns, etc.
In this
paper we use the formalism of Linear Hybrid Automata
to encode a hierarchical scheduling system. In
particular, we model a dynamic server algorithm and
the tasks contained within, abstracting away the
rest of the system, thus enabling component-based
scheduling analysis. We prove the correctness of the
model and the decidability of the reachability
analysis for the case of periodic tasks. Then, we
compare the results of our model against classical
schedulability analysis techniques, showing that our
analysis performs better than analytic methods in
terms of resource utilisation. We further present
two case studies: a component with state-dependent
tasks, and a simplified model of a real avionics
system. Finally, through extensive tests with
various configurations, we demonstrate that this
approach is usable for medium size components.
@inproceedings{rtcsa2014-SLSFM,
author = {Sun, Youcheng and Lipari, Giuseppe and Soulat,
Romain and Fribourg, Laurent and Markey, Nicolas},
title = {Component-Based Analysis of Hierarchical Scheduling
using Linear Hybrid Automata},
booktitle = {{P}roceedings of the 20th {I}nternational
{C}onference on {R}eal-{T}ime {C}omputing {S}ystems
and {A}pplications ({RTCSA}'14)},
acronym = {{RTCSA}'14},
publisher = {IEEE Comp. Soc. Press},
year = {2014},
month = aug,
doi = {10.1109/RTCSA.2014.6910502},
abstract = {Formal methods (e.g. Timed Automata or Linear Hybrid
Automata) can be used to analyse a real-time system
by performing a reachability analysis on the model.
The advantage of using formal methods is that they
are more expressive than classical analytic models
used in schedulability analysis. For example, it is
possible to express state-dependent behaviour,
arbitrary activation patterns,~etc.\par In this
paper we use the formalism of Linear Hybrid Automata
to encode a hierarchical scheduling system. In
particular, we model a dynamic server algorithm and
the tasks contained within, abstracting away the
rest of the system, thus enabling component-based
scheduling analysis. We prove the correctness of the
model and the decidability of the reachability
analysis for the case of periodic tasks. Then, we
compare the results of our model against classical
schedulability analysis techniques, showing that our
analysis performs better than analytic methods in
terms of resource utilisation. We further present
two case studies: a~component with state-dependent
tasks, and a simplified model of a real avionics
system. Finally, through extensive tests with
various configurations, we demonstrate that this
approach is usable for medium size components.},
}
[ABK14]
ShaullAlmagor,
UdiBoker, and
OrnaKupferman.
Discounting in LTL.
In TACAS'14,
Lecture Notes in Computer Science 8413, pages 424-439. Springer-Verlag, April 2014.
@inproceedings{tacas2014-ABK,
author = {Almagor, Shaull and Boker, Udi and Kupferman, Orna},
title = {Discounting in~{LTL}},
editor = {{\'A}brah{\'a}m, Erikz and Havelund, Klaus},
booktitle = {{P}roceedings of the 20th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'14)},
acronym = {{TACAS}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8413},
pages = {424-439},
year = {2014},
month = apr,
doi = {10.1007/978-3-642-54862-8_37},
}
[AJK+14]
BenjaminAminof,
SwenJacobs,
AyratKhalimov, and
SashaRubin.
Parametrized Model Checking of Token-Passing
Systems.
In VMCAI'14,
Lecture Notes in Computer Science 8318, pages 262-281. Springer-Verlag, January 2014.
@inproceedings{vmcai2014-AJKR,
author = {Aminof, Benjamin and Jacobs, Swen and Khalimov,
Ayrat and Rubin, Sasha},
title = {Parametrized Model Checking of Token-Passing
Systems},
editor = {McMillan, Kenneth L. and Rival, Xavier},
booktitle = {{P}roceedings of the 15th {I}nternational {W}orkshop
on {V}erification, {M}odel {C}hecking, and
{A}bstract {I}nterpretation ({VMCAI}'14)},
acronym = {{VMCAI}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8318},
pages = {262-281},
year = {2014},
month = jan,
doi = {10.1007/978-3-642-54013-4_15},
}
[AKR+14]
BenjaminAminof,
TomerKotek,
SashaRubin,
FrancescoSpegni, and
HelmutVeith.
Parameterized Model Checking of Rendezvous Systems.
In CONCUR'14,
Lecture Notes in Computer Science 8704, pages 109-124. Springer-Verlag, September 2014.
@inproceedings{concur2014-AKRSV,
author = {Aminof, Benjamin and Kotek, Tomer and Rubin, Sasha
and Spegni, Francesco and Veith, Helmut},
title = {Parameterized Model Checking of Rendezvous Systems},
editor = {Baldan, Paolo and Gorla, Daniele},
booktitle = {{P}roceedings of the 25th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'14)},
acronym = {{CONCUR}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8704},
pages = {109-124},
year = {2014},
month = sep,
doi = {10.1007/978-3-662-44584-6_9},
}
[AR14]
BenjaminAminof and
SashaRubin.
First Cycle Games.
In SR'14,
Electronic Proceedings in Theoretical Computer
Science 146, pages 83-90. March 2014.
@inproceedings{sr2014-AR,
author = {Aminof, Benjamin and Rubin, Sasha},
title = {First Cycle Games},
booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop
on {S}trategic {R}easoning ({SR}'14)},
acronym = {{SR}'14},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {146},
pages = {83-90},
year = {2014},
month = mar,
doi = {10.4204/EPTCS.146.11},
}
[BBB+14]
NathalieBertrand,
PatriciaBouyer,
ThomasBrihaye,
QuentinMenet,
ChristelBaier,
MarcusGrößer, and
MarcinJurdziński.
Stochastic Timed Automata.
Logical Methods in Computer Science 10(4).
December 2014.
@article{lmcs10(4)-BBBMBGJ,
author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye,
{\relax Th}omas and Menet, Quentin and Baier,
{\relax Ch}ristel and Gr{\"o}{\ss}er, Marcus and
Jurdzi{\'n}ski, Marcin},
title = {Stochastic Timed Automata},
journal = {Logical Methods in Computer Science},
volume = {10},
number = {4},
year = {2014},
month = dec,
doi = {10.2168/LMCS-10(4:6)2014},
}
[BBD14]
ThomasBrihaye,
VéroniqueBruyère, and
JulieDe Pril.
On Equilibria in Quantitative Games with
Reachability/Safety Objectives.
Theory of Computing Systems 54(2):150-189. Springer-Verlag, February 2014.
@article{tcsyst54(2)-BBD,
author = {Brihaye, {\relax Th}omas and Bruy{\`e}re,
V{\'e}ronique and De{~}Pril, Julie},
title = {On Equilibria in Quantitative Games with
Reachability{{\slash}}Safety Objectives},
publisher = {Springer-Verlag},
journal = {Theory of Computing Systems},
volume = {54},
number = {2},
pages = {150-189},
year = {2014},
month = feb,
}
@inproceedings{BBJKNN-isola2014,
author = {Bohlender, Dimitri and Bruintjes, Harold and Junges,
Sebastian and Katelaan, Jens and Nguyen, Viet Yen
and Noll, Thomas},
title = {A~Review of Statistical Model Checking Pitfalls on
Real-Time Stochastic Models},
editor = {Margaria, Tiziana and Steffen, Bernhard},
booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium
on {L}everaging {A}pplications of {F}ormal
{M}ethods, {V}erification and {V}alidation
({IS}o{LA}'14)~-- {P}art~{II}: {S}pecialized
{T}echniques and {A}pplications},
acronym = {{IS}o{LA}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8803},
pages = {177-192},
year = {2014},
month = oct,
doi = {10.1007/978-3-662-45231-8_13},
}
[BCH+14]
UdiBoker,
KrishnenduChatterjee,
Thomas A.Henzinger, and
OrnaKupferman.
Temporal Specifications with Accumulative Values.
ACM Transactions on Computational Logic 15(4):27:1-27:25. ACM Press, August 2014.
@article{tocl15(4)-BCHK,
author = {Boker, Udi and Chatterjee, Krishnendu and Henzinger,
Thomas A. and Kupferman, Orna},
title = {Temporal Specifications with Accumulative Values},
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
volume = {15},
number = {4},
pages = {27:1-27:25},
year = {2014},
month = aug,
doi = {10.1145/2629686},
}
@article{acta51(3-4)-BDLL,
author = {Bulychev, Peter and David, Alexandre and Larsen, Kim
Guldstrand and Li, Guangyuan},
title = {Efficient Controller Synthesis for a fragment of
{{\(\textsf{MTL}_{0,\infty}\)}}},
publisher = {Springer-Verlag},
journal = {Acta Informatica},
volume = {51},
number = {3-4},
pages = {165-192},
year = {2014},
month = jun,
doi = {10.1007/s00236-013-0189-z},
}
@inproceedings{fossacs2014-BFS,
author = {Bertrand, Nathalie and Fournier, Paulin and
Sangnier, Arnaud},
title = {Playing with Probabilities in Reconfigurable
Broadcast Networks},
editor = {Muscholl, Anca},
booktitle = {{P}roceedings of the 17th {I}nternational
{C}onference on {F}oundations of {S}oftware
{S}cience and {C}omputation {S}tructure
({FoSSaCS}'14)},
acronym = {{FoSSaCS}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8412},
pages = {134-148},
year = {2014},
month = apr,
doi = {10.1007/978-3-642-54830-7_9},
}
[BGN+14]
ThomasBrihaye,
GillesGeeraerts,
ShankaraNarayanan Krishna,
LakshmiManasa,
BenjaminMonmege, and
AshutoshTrivedi.
Adding negative prices to priced timed games.
In CONCUR'14,
Lecture Notes in Computer Science 8704, pages 560-575. Springer-Verlag, September 2014.
@inproceedings{concur2014-BGKMMT,
author = {Brihaye, {\relax Th}omas and Geeraerts, Gilles and
Narayanan Krishna, Shankara and Manasa, Lakshmi and
Monmege, Benjamin and Trivedi, Ashutosh},
title = {Adding negative prices to priced timed games},
editor = {Baldan, Paolo and Gorla, Daniele},
booktitle = {{P}roceedings of the 25th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'14)},
acronym = {{CONCUR}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8704},
pages = {560-575},
year = {2014},
month = sep,
doi = {10.1007/978-3-662-44584-6_38},
}
[BGS14]
BenediktBollig,
PaulGastin, and
JanaSchubert.
Parameterized verification of communicating automata
under context bounds.
In RP'14,
Lecture Notes in Computer Science 8762, pages 45-57. Springer-Verlag, September 2014.
@inproceedings{rp2014-BGS,
author = {Bollig, Benedikt and Gastin, Paul and Schubert,
Jana},
title = {Parameterized verification of communicating automata
under context bounds},
editor = {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell,
James},
booktitle = {{P}roceedings of the 8th {W}orkshop on
{R}eachability {P}roblems in {C}omputational
{M}odels ({RP}'14)},
acronym = {{RP}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8762},
pages = {45-57},
year = {2014},
month = sep,
doi = {10.1007/978-3-319-11439-2_4},
}
@inproceedings{fsttcs2014-BHL,
author = {Bertrand, Nathalie and Haddad, Serge and Lefaucheux,
Engel},
title = {Foundation of Diagnosis and Predictability in
Probabilistic Systems},
editor = {Raman, Venkatesh and Suresh, S. P.},
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)},
acronym = {{FSTTCS}'14},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {29},
pages = {417-429},
year = {2014},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2014.417},
}
[BHM14]
BernardBoigelot,
FrédéricHerbreteau, and
IsabelleMainz.
Acceleration of Affine Hybrid Transformations.
In ATVA'14,
Lecture Notes in Computer Science 8837, pages 31-46. Springer-Verlag, November 2014.
@inproceedings{atva2014-BHM,
author = {Boigelot, Bernard and Herbreteau, Fr{\'e}d{\'e}ric
and Mainz, Isabelle},
title = {Acceleration of Affine Hybrid Transformations},
editor = {Cassez, Franck and Raskin, Jean-Fran{\c c}ois},
booktitle = {{P}roceedings of the 12th {I}nternational
{S}ymposium on {A}utomated {T}echnology for
{V}erification and {A}nalysis ({ATVA}'14)},
acronym = {{ATVA}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8837},
pages = {31-46},
year = {2014},
month = nov,
doi = {10.1007/978-3-319-11936-6_4},
}
[BKK+14]
TomášBrázdil,
DavidKlaška,
AntonínKučera, and
PetrNovotný.
Minimizing Running Costs in Consumption Systems.
In CAV'14,
Lecture Notes in Computer Science 8559, pages 457-472. Springer-Verlag, July 2014.
@inproceedings{csllics2014-BMR,
author = {Bruy{\`e}re, V{\'e}ronique and Meunier, No{\"e}mie
and Raskin, Jean-Fran{\c c}ois},
title = {Secure Equilibria in Weighted Games},
booktitle = {{P}roceedings of the Joint Meeting of the 23rd
{EACSL} {A}nnual {C}onference on {C}omputer
{S}cience {L}ogic and the 29th {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer
{S}cience ({CSL\slash LICS}'14)},
acronym = {{CSL\slash LICS}'14},
publisher = {ACM Press},
chapter = {26},
year = {2014},
month = jul,
doi = {10.1145/2603088.2603109},
}
[BRS14]
RomainBrenguier,
Jean-FrançoisRaskin, and
MathieuSassolas.
The complexity of admissibility in omega-regular
games.
In CSL/ LICS'14,
pages 23:1-23:10.
ACM Press, July 2014.
@inproceedings{csllics2014-BRS,
author = {Brenguier, Romain and Raskin, Jean-Fran{\c c}ois and
Sassolas, Mathieu},
title = {The complexity of admissibility in omega-regular
games},
booktitle = {{P}roceedings of the Joint Meeting of the 23rd
{EACSL} {A}nnual {C}onference on {C}omputer
{S}cience {L}ogic and the 29th {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer
{S}cience ({CSL\slash LICS}'14)},
acronym = {{CSL\slash LICS}'14},
publisher = {ACM Press},
pages = {23:1-23:10},
year = {2014},
month = jul,
doi = {10.1145/2603088.2603143},
}
[CDF+14]
KrishnenduChatterjee,
LaurentDoyen,
EmmanuelFiliot, and
Jean-FrançoisRaskin.
Doomsday Equilibria for Omega-Regular Games.
In VMCAI'14,
Lecture Notes in Computer Science 8318, pages 78-97. Springer-Verlag, January 2014.
@inproceedings{vmcai2014-CDFR,
author = {Chatterjee, Krishnendu and Doyen, Laurent and
Filiot, Emmanuel and Raskin, Jean-Fran{\c c}ois},
title = {Doomsday Equilibria for Omega-Regular Games},
editor = {McMillan, Kenneth L. and Rival, Xavier},
booktitle = {{P}roceedings of the 15th {I}nternational {W}orkshop
on {V}erification, {M}odel {C}hecking, and
{A}bstract {I}nterpretation ({VMCAI}'14)},
acronym = {{VMCAI}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8318},
pages = {78-97},
year = {2014},
month = jan,
doi = {10.1007/978-3-642-54013-4_5},
}
@mastersthesis{master14-Cer,
author = {{\v{C}}erm{\'a}k, Petr},
title = {A~Model Checker for Strategy Logic},
year = {2014},
month = jun,
school = {Dept. of Computing, Imperial College London, UK},
}
[CG14]
NamitChaturvedi and
MarcusGelderie.
Weak ω-Regular Trace Languages.
Research Report 1402.3199, arXiv, February 2014.
@techreport{arxiv1402.3199,
author = {Chaturvedi, Namit and Gelderie, Marcus},
title = {Weak {{\(\omega\)}}-Regular Trace Languages},
number = {1402.3199},
year = {2014},
month = feb,
institution = {arXiv},
type = {Research Report},
}
@inproceedings{rp2014-CH,
author = {Carayol, Arnaud and Hague, Matthew},
title = {Regular Strategies In Pushdown Reachability Games},
editor = {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell,
James},
booktitle = {{P}roceedings of the 8th {W}orkshop on
{R}eachability {P}roblems in {C}omputational
{M}odels ({RP}'14)},
acronym = {{RP}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8762},
pages = {58-71},
year = {2014},
month = sep,
doi = {10.1007/978-3-319-11439-2_5},
}
[Cha14]
NamitChaturvedi.
Toward a structure theory of regular infinitary
trace languages.
In ICALP'14,
Lecture Notes in Computer Science 8573, pages 134-145. Springer-Verlag, July 2014.
@inproceedings{icalp2014-Cha,
author = {Chaturvedi, Namit},
title = {Toward a structure theory of regular infinitary
trace languages},
editor = {Esparza, Javier and Fraigniaud, Pierre and
Koutsoupias, Elias},
booktitle = {{P}roceedings of the 41st {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'14)~-- Part~{II}},
acronym = {{ICALP}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8573},
pages = {134-145},
year = {2014},
month = jul,
doi = {10.1007/978-3-662-43951-7_12},
}
@inproceedings{cav2014-CLMM,
author = {{\v{C}}erm{\'a}k, Petr and Lomuscio, Alessio and
Mogavero, Fabio and Murano, Aniello},
title = {{MCMAS-SLK}: A~Model Checker for the Verification of
Strategy Logic Specifications},
editor = {Biere, Armin and Bloem, Roderick},
booktitle = {{P}roceedings of the 26th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'14)},
acronym = {{CAV}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8559},
pages = {525-532},
year = {2014},
month = jul,
doi = {10.1007/978-3-319-08867-9_34},
}
@article{acta51(3-4)-CRR,
author = {Chatterjee, Krishnendu and Randour, Mickael and
Raskin, Jean-Fran{\c c}ois},
title = {Strategy Synthesis for Multi-dimensional
Quantitative Objectives},
publisher = {Springer-Verlag},
journal = {Acta Informatica},
volume = {51},
number = {3-4},
pages = {129-163},
year = {2014},
month = jun,
doi = {10.1007/s00236-013-0182-6},
}
[DMS14]
LaurentDoyen,
ThierryMassart, and
MahsaShirmohammadi.
Limit synchronization in Markov decision
processes.
In FoSSaCS'14,
Lecture Notes in Computer Science 8412, pages 58-72. Springer-Verlag, April 2014.
@inproceedings{fossacs2014-DMS,
author = {Doyen, Laurent and Massart, {\relax Th}ierry and
Shirmohammadi, Mahsa},
title = {Limit synchronization in {M}arkov decision
processes},
editor = {Muscholl, Anca},
booktitle = {{P}roceedings of the 17th {I}nternational
{C}onference on {F}oundations of {S}oftware
{S}cience and {C}omputation {S}tructure
({FoSSaCS}'14)},
acronym = {{FoSSaCS}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8412},
pages = {58-72},
year = {2014},
month = apr,
doi = {10.1007/978-3-642-54830-7_4},
}
[Esp14]
JavierEsparza.
Keeping a Crowd Safe: On the Complexity of
Parameterized Verification (Invited Talk).
In STACS'14,
Leibniz International Proceedings in Informatics 25, pages 1-10. Leibniz-Zentrum für Informatik, March 2014.
@inproceedings{stacs2014-Esp,
author = {Esparza, Javier},
title = {Keeping a Crowd Safe: On the Complexity of
Parameterized Verification (Invited Talk)},
editor = {Mayr, Ernst W. and Portier, Natacha},
booktitle = {{P}roceedings of the 31st {S}ymposium on
{T}heoretical {A}spects of {C}omputer {S}cience
({STACS}'14)},
acronym = {{STACS}'14},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {25},
pages = {1-10},
year = {2014},
month = mar,
doi = {10.4230/LIPIcs.STACS.2014.1},
}
[FPS14]
AchilleFrigeri,
LilianaPasquale, and
PaolaSpoletini.
Fuzzy Time in Linear Temporal Logic.
ACM Transactions on Computational Logic 15(4):30:1-30:22. ACM Press, August 2014.
@article{tocl15(4)-FPS,
author = {Frigeri, Achille and Pasquale, Liliana and
Spoletini, Paola},
title = {Fuzzy Time in Linear Temporal Logic},
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
volume = {15},
number = {4},
pages = {30:1-30:22},
year = {2014},
month = aug,
}
[Gel14]
MarcusGelderie.
Strategy Machines – Representation and Complexity
of Strategies in Infinite Games.
PhD thesis,
RWTH Aachen, Germany,
February 2014.
@phdthesis{phd-gelderie,
author = {Gelderie, Marcus},
title = {Strategy Machines~-- Representation and Complexity
of Strategies in Infinite Games},
year = {2014},
month = feb,
school = {RWTH Aachen, Germany},
type = {{PhD} thesis},
}
[HLL+14]
HenriHansen,
Shang-WeiLin,
YangLiu,
Truong KhanhNguyen, and
JunSun.
Diamonds Are a Girl's Best Friend: Partial Order
Reduction for Timed Automata with Abstractions.
In CAV'14,
Lecture Notes in Computer Science 8559, pages 391-406. Springer-Verlag, July 2014.
@inproceedings{cav2014-HLLNS,
author = {Hansen, Henri and Lin, Shang{-}Wei and Liu, Yang and
Nguyen, Truong Khanh and Sun, Jun},
title = {Diamonds Are a Girl's Best Friend: Partial Order
Reduction for Timed Automata with Abstractions},
editor = {Biere, Armin and Bloem, Roderick},
booktitle = {{P}roceedings of the 26th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'14)},
acronym = {{CAV}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8559},
pages = {391-406},
year = {2014},
month = jul,
doi = {10.1007/978-3-319-08867-9_26},
}
@inproceedings{fsttcs2014-HR,
author = {Hunter, Paul and Raskin, Jean-Fran{\c c}ois},
title = {Quantitative games with interval objectives},
editor = {Raman, Venkatesh and Suresh, S. P.},
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)},
acronym = {{FSTTCS}'14},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {29},
pages = {365-377},
year = {2014},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2014.365},
}
[JLS+14]
Peter GjølJensen,
Kim GuldstrandLarsen,
JiříSrba,
Mathias GrundSørensen, and
Jakob HaarTaankvist.
Memory Efficient Data Structures for Explicit
Verification of Timed Systems.
In NFM'14,
Lecture Notes in Computer Science 8430, pages 307-312. Springer-Verlag, April 2014.
@inproceedings{nasaFM2014-JLSST,
author = {Jensen, Peter Gj{\o}l and Larsen, Kim Guldstrand and
Srba, Ji{\v r}{\'\i} and S{\o}rensen, Mathias Grund
and Taankvist, Jakob Haar},
title = {Memory Efficient Data Structures for Explicit
Verification of Timed Systems},
editor = {Badger, Julia M. and Rozier, Kristin Yvonne},
booktitle = {{P}roceedings of the 6th {NASA} {F}ormal {M}ethods
{S}ymposium ({NFM}'14)},
acronym = {{NFM}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8430},
pages = {307-312},
year = {2014},
month = apr,
doi = {10.1007/978-3-319-06200-6_26},
}
@article{tcs515-LLTW,
author = {Larsen, Kim Guldstrand and Legay, Axel and
Traonouez, Louis-Marie and W{\k a}sowski, Andrzej},
title = {Robust synthesis for real-time systems},
publisher = {Elsevier},
journal = {Theoretical Computer Science},
volume = {515},
pages = {96-122},
year = {2014},
month = jan,
}
[LP14]
JunLiu and
PavithraPrabhakar.
Switching control of dynamical systems from metric
temporal logic specifications.
In ICRA'01,
pages 5333-5338.
IEEE Robotics & Automation Soc., May 2014.
@inproceedings{icra2014-LP,
author = {Liu, Jun and Prabhakar, Pavithra},
title = {Switching control of dynamical systems from metric
temporal logic specifications},
booktitle = {{P}roceedings of the 2014 {IEEE} {I}nternational
{C}onference on {R}obotics and {A}utomation
({ICRA}'14)},
acronym = {{ICRA}'01},
publisher = {IEEE Robotics~\& Automation Soc.},
pages = {5333-5338},
year = {2014},
month = may,
doi = {10.1109/ICRA.2014.6907643},
}
@article{tocl15(4)-MMPV,
author = {Mogavero, Fabio and Murano, Aniello and Perelli,
Giuseppe and Vardi, Moshe Y.},
title = {Reasoning About Strategies: On the Model-Checking
Problem},
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
volume = {15},
number = {4},
pages = {34:1-34:47},
year = {2014},
month = aug,
doi = {10.1145/2631917},
}
@inproceedings{clima2014-MMS,
author = {Mogavero, Fabio and Murano, Aniello and Sauro,
Luigi},
title = {A Behavioral Hierarchy of Strategy Logic},
editor = {Bulling, Nils and van der Torre, Leendert W. N. and
Villata, Serena and Jamroga, Wojciech and
Vasconcelos, Wamberto Weber},
booktitle = {{P}roceedings of the 15th {I}nternational {W}orkshop
on {C}omputational {L}ogic in {M}ulti-{A}gent
{S}ystems ({CLIMA}'14)},
acronym = {{CLIMA}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Artificial Intelligence},
volume = {8624},
pages = {148-165},
year = {2014},
month = aug,
doi = {10.1007/978-3-319-09764-0_10},
}
[ORS14]
YoussoufOualhadj,
Pierre-AlainReynier, and
OcanSankur.
Probabilistic Robust Timed Games.
In CONCUR'14,
Lecture Notes in Computer Science 8704, pages 203-217. Springer-Verlag, September 2014.
@phdthesis{phd-shirmohammadi,
author = {Shirmohammadi, Mahsa},
title = {Qualitative analysis of synchronizing probabilistic
systems},
year = {2014},
month = dec,
school = {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
France and D{\'e}partement d'Informatique,
Universit{\'e} Libre de Bruxelles, Belgium},
type = {Th\`ese de doctorat},
}
@mastersthesis{sorensen-master14,
author = {S{\o}rensen, Mathias Grund},
title = {Controller synthesis for home automation},
year = {2014},
school = {Computer Science Department, Aalborg University,
Denmark},
}
@mastersthesis{sorensen-master14,
author = {S{\o}rensen, Mathias Grund},
title = {Controller synthesis for home automation},
year = {2014},
school = {Computer Science Department, Aalborg University,
Denmark},
}
[WJ14]
WeifengWang and
LiJiao.
Trace Abstraction Refinement for Timed Automata.
In ATVA'14,
Lecture Notes in Computer Science 8837, pages 396-410. Springer-Verlag, November 2014.
Weighted timed automata extend timed automata with
cost variables that can be used to model the
evolution of various quantities. Although
cost-optimal reachability is decidable (in
polynomial space) on this model, it becomes
undecidable on weighted timed games. This paper
studies cost-optimal reachability problems on
weighted timed automata and games under robust
semantics. More precisely, we consider two
perturbation game semantics that introduce
imprecisions in the standard semantics, and bring
robustness properties w.r.t. timing imprecisions to
controllers. We give a polynomial-space algorithm
for weighted timed automata, and prove the
undecidability of cost-optimal reachability on
weighted timed games, showing that the problem is
robustly undecidable.
@inproceedings{formats2013-BMS,
author = {Bouyer, Patricia and Markey, Nicolas and Sankur,
Ocan},
title = {Robust Weighted Timed Automata and Games},
editor = {Braberman, V{\'\i}ctor and Fribourg, Laurent},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'13)},
acronym = {{FORMATS}'13},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8053},
pages = {31-46},
year = {2013},
month = aug,
doi = {10.1007/978-3-642-40229-6_3},
abstract = {Weighted timed automata extend timed automata with
cost variables that can be used to model the
evolution of various quantities. Although
cost-optimal reachability is decidable (in
polynomial space) on this model, it becomes
undecidable on weighted timed games. This paper
studies cost-optimal reachability problems on
weighted timed automata and games under robust
semantics. More precisely, we consider two
perturbation game semantics that introduce
imprecisions in the standard semantics, and bring
robustness properties w.r.t. timing imprecisions to
controllers. We give a polynomial-space algorithm
for weighted timed automata, and prove the
undecidability of cost-optimal reachability on
weighted timed games, showing that the problem is
robustly undecidable.},
}
Various extensions of the temporal logic ATL have
recently been introduced to express rich properties
of multi-agent systems. Among these, ATLsc extends
ATL with strategy contexts, while Strategy
Logic has first-order quantification over
strategies. There is a price to pay for the rich
expressiveness of these logics: model-checking is
non-elementary, and satisfiability is
undecidable.
We prove in this paper that
satisfiability is decidable in several special
cases. The most important one is when restricting to
turn-based games. We prove that decidability
also holds for concurrent games if the number of
moves available to the agents is bounded. Finally,
we prove that restricting strategy quantification to
memoryless strategies brings back undecidability.
@inproceedings{gandalf2013-LM,
author = {Laroussinie, Fran{\c c}ois and Markey, Nicolas},
title = {Satisfiability of {ATL} with strategy contexts},
editor = {Puppis, Gabriele and Villa, Tiziano},
booktitle = {{P}roceedings of the 4th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics and {F}ormal
{V}erification ({GandALF}'13)},
acronym = {{GandALF}'13},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {119},
pages = {208-223},
year = {2013},
month = aug,
doi = {10.4204/EPTCS.119.18},
abstract = {Various extensions of the temporal logic ATL have
recently been introduced to express rich properties
of multi-agent systems. Among these, ATLsc extends
ATL with \emph{strategy contexts}, while Strategy
Logic has \emph{first-order quantification} over
strategies. There is a price to pay for the rich
expressiveness of these logics: model-checking is
non-elementary, and satisfiability is
undecidable.\par We prove in this paper that
satisfiability is decidable in several special
cases. The most important one is when restricting to
\emph{turn-based} games. We~prove that decidability
also holds for concurrent games if the number of
moves available to the agents is bounded. Finally,
we~prove that restricting strategy quantification to
memoryless strategies brings back undecidability.},
}
We consider the fundamental problem of Büchi
acceptance in timed automata in a robust setting.
The problem is formalised in terms of controller
synthesis: timed automata are equipped with a
parametrised game-based semantics that models the
possible perturbations of the decisions taken by the
controller. We characterise timed automata that are
robustly controllable for some parameter, with a
simple graph theoretic condition, by showing the
equivalence with the existence of an aperiodic lasso
that satisfies the winning condition (aperiodicity
was defined and used earlier in different contexts
to characterise convergence phenomena in timed
automata). We then show decidability and
PSPACE-completeness of our problem.
@inproceedings{concur2013-SBMR,
author = {Sankur, Ocan and Bouyer, Patricia and Markey,
Nicolas and Reynier, Pierre-Alain},
title = {Robust Controller Synthesis in Timed Automata},
editor = {D{'}Argenio, Pedro R. and Melgratt, Hern{\'a}n C.},
booktitle = {{P}roceedings of the 24th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'13)},
acronym = {{CONCUR}'13},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8052},
pages = {546-560},
year = {2013},
month = aug,
doi = {10.1007/978-3-642-40184-8_38},
abstract = {We consider the fundamental problem of B{\"u}chi
acceptance in timed automata in a robust setting.
The problem is formalised in terms of controller
synthesis: timed automata are equipped with a
parametrised game-based semantics that models the
possible perturbations of the decisions taken by the
controller. We characterise timed automata that are
robustly controllable for some parameter, with a
simple graph theoretic condition, by showing the
equivalence with the existence of an aperiodic lasso
that satisfies the winning condition (aperiodicity
was defined and used earlier in different contexts
to characterise convergence phenomena in timed
automata). We then show decidability and
PSPACE-completeness of our problem.},
}
In this paper we survey several approaches to the
robustness of timed automata, that is, the ability
of a system to resist to slight perturbations or
errors. We will concentrate on robustness against
timing errors which can be due to measuring errors,
imprecise clocks, and unexpected runtime behaviors
such as execution times that are longer or shorter
than expected.
We consider the perturbation
model of guard enlargement and formulate several
robust verification problems that have been studied
recently, including robustness analysis, robust
implementation, and robust control.
@inproceedings{rp2013-BMS,
author = {Bouyer, Patricia and Markey, Nicolas and Sankur,
Ocan},
title = {Robustness in timed automata},
editor = {Abdulla, Parosh Aziz and Potapov, Igor},
booktitle = {{P}roceedings of the 7th {W}orkshop on
{R}eachability {P}roblems in {C}omputational
{M}odels ({RP}'13)},
acronym = {{RP}'13},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8169},
pages = {1-18},
year = {2013},
month = sep,
doi = {10.1007/978-3-642-41036-9_1},
abstract = {In this paper we survey several approaches to the
robustness of timed automata, that~is, the ability
of a system to resist to slight perturbations or
errors. We will concentrate on robustness against
timing errors which can be due to measuring errors,
imprecise clocks, and unexpected runtime behaviors
such as execution times that are longer or shorter
than expected.\par We consider the perturbation
model of guard enlargement and formulate several
robust verification problems that have been studied
recently, including robustness analysis, robust
implementation, and robust control.},
}
[ABK13]
ShaullAlmagor,
UdiBoker, and
OrnaKupferman.
Formalizing and Reasoning about Quality.
In ICALP'13,
Lecture Notes in Computer Science 7966, pages 15-27. Springer-Verlag, July 2013.
@inproceedings{icalp2013-ABK,
author = {Almagor, Shaull and Boker, Udi and Kupferman, Orna},
title = {Formalizing and Reasoning about Quality},
editor = {Fomin, Fedor V. and Freivalds, Rusins and
Kwiatkowska, Marta and Peleg, David},
booktitle = {{P}roceedings of the 40th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'13)~-- Part~{II}},
acronym = {{ICALP}'13},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {7966},
pages = {15-27},
year = {2013},
month = jul,
}
[BBF+13]
AaronBohy,
VéroniqueBruyère,
EmmanuelFiliot, and
Jean-FrançoisRaskin.
Synthesis from LTL Specifications with Mean-Payoff
Objectives.
In TACAS'13,
Lecture Notes in Computer Science 7795, pages 169-184. Springer-Verlag, March 2013.
@inproceedings{tacas2013-BBFR,
author = {Bohy, Aaron and Bruy{\`e}re, V{\'e}ronique and
Filiot, Emmanuel and Raskin, Jean-Fran{\c c}ois},
title = {Synthesis from {LTL} Specifications with Mean-Payoff
Objectives},
editor = {Piterman, Nir and Smolka, Scott A.},
booktitle = {{P}roceedings of the 19th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'13)},
acronym = {{TACAS}'13},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {7795},
pages = {169-184},
year = {2013},
month = mar,
}
@inproceedings{mfcs2013-BBLM,
author = {Bacci, Giorgio and Bacci, Giovanni and Larsen, Kim
Guldstrand and Mardare, Radu},
title = {Computing Behavioral Distances, Compositionally},
editor = {Chatterjee, Krishnendu and Sgall, Ji{\v r}{\'\i}},
booktitle = {{P}roceedings of the 38th {I}nternational
{S}ymposium on {M}athematical {F}oundations of
{C}omputer {S}cience ({MFCS}'13)},
acronym = {{MFCS}'13},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8087},
pages = {74-85},
year = {2013},
month = aug,
doi = {10.1007/978-3-642-40313-2_9},
}
@inproceedings{qest2013-BBLM,
author = {Bacci, Giorgio and Bacci, Giovanni and Larsen, Kim
Guldstrand and Mardare, Radu},
title = {The BisimDist Library: Efficient Computation of
Bisimilarity Distances for {M}arkovian Models},
booktitle = {{P}roceedings of the 10th {I}nternational
{C}onference on {Q}uantitative {E}valuation of
{S}ystems ({QEST}'13)},
acronym = {{QEST}'13},
publisher = {IEEE Comp. Soc. Press},
pages = {278-281},
year = {2013},
month = aug,
doi = {10.1007/978-3-642-40196-1_23},
}
[BG13]
NilsBulling and
ValentinGoranko.
How to Be Both Rich and Happy: Combining
Quantitative and Qualitative Strategic Reasoning
about Multi-Player Games (Extended Abstract).
In SR'13,
Electronic Proceedings in Theoretical Computer
Science 112, pages 33-41. March 2013.
@inproceedings{sr2013-BG,
author = {Bulling, Nils and Goranko, Valentin},
title = {How to Be Both Rich and Happy: Combining
Quantitative and Qualitative Strategic Reasoning
about Multi-Player Games (Extended Abstract)},
booktitle = {{P}roceedings of the 1st {I}nternational {W}orkshop
on {S}trategic {R}easoning ({SR}'13)},
acronym = {{SR}'13},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {112},
pages = {33-41},
year = {2013},
month = mar,
doi = {10.4204/EPTCS.112.8},
}
@article{jcss79(5)-BGH,
author = {Bournez, Olivier and Gra{\c c}a, Daniel S. and
Hainry, Emmanuel},
title = {Computation with perturbed dynamical systems},
publisher = {Elsevier},
journal = {Journal of Computer and System Sciences},
volume = {79},
number = {5},
pages = {714-724},
year = {2013},
month = aug,
}
[BKK+13]
UdiBoker,
DenisKuperberg,
OrnaKupferman, and
MichalSkrzypczak.
Nondeterminism in the Presence of a Diverse or
Unknown Future.
In ICALP'13,
Lecture Notes in Computer Science 7966, pages 89-100. Springer-Verlag, July 2013.
@inproceedings{icalp2013-BKKS,
author = {Boker, Udi and Kuperberg, Denis and Kupferman, Orna
and Skrzypczak, Michal},
title = {Nondeterminism in the Presence of a Diverse or
Unknown Future},
editor = {Fomin, Fedor V. and Freivalds, Rusins and
Kwiatkowska, Marta and Peleg, David},
booktitle = {{P}roceedings of the 40th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'13)~-- Part~{II}},
acronym = {{ICALP}'13},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {7966},
pages = {89-100},
year = {2013},
month = jul,
doi = {10.1007/978-3-642-39212-2_11},
}
[BRS13]
Marcello MariaBersani,
MatteoRossi, and
PierluigiSan Pietro.
Deciding the Satisfiability of MITL
Specifications.
In GandALF'13,
Electronic Proceedings in Theoretical Computer
Science 119, pages 64-78. August 2013.
@inproceedings{gandalf2013-BRS,
author = {Bersani, Marcello Maria and Rossi, Matteo and
San{~}Pietro, Pierluigi},
title = {Deciding the Satisfiability of {MITL}
Specifications},
editor = {Puppis, Gabriele and Villa, Tiziano},
booktitle = {{P}roceedings of the 4th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics and {F}ormal
{V}erification ({GandALF}'13)},
acronym = {{GandALF}'13},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {119},
pages = {64-78},
year = {2013},
month = aug,
doi = {10.4204/EPTCS.119.8},
}
[Bru13]
BenediktBrütsch.
Synthesizing structured reactive programs via
deterministic tree automata.
In SR'13,
Electronic Proceedings in Theoretical Computer
Science 112, pages 107-113. March 2013.
@inproceedings{sr2013-Bru,
author = {Br{\"u}tsch, Benedikt},
title = {Synthesizing structured reactive programs via
deterministic tree automata},
booktitle = {{P}roceedings of the 1st {I}nternational {W}orkshop
on {S}trategic {R}easoning ({SR}'13)},
acronym = {{SR}'13},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {112},
pages = {107-113},
year = {2013},
month = mar,
doi = {10.4204/EPTCS.112.16},
}
@inproceedings{acsd2013-CB,
author = {Cassez, Franck and B{\'e}chennec, Jean-Luc},
title = {Timing Analysis of Binary Programs with {UPPAAL}},
editor = {Carmona, Josep and Lazarescu, Mihai T. and
Pietkiewicz-Koutny, Marta},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onference on {A}pplication of {C}oncurrency to
{S}ystem {D}esign ({ACSD}'13)},
acronym = {{ACSD}'13},
publisher = {IEEE Comp. Soc. Press},
pages = {41-50},
year = {2013},
month = jul,
doi = {10.1109/ACSD.2013.7},
}
[CBC13]
ChristopheChareton,
JulienBrunel, and
DavidChemouil.
Towards an Updatable Strategy Logic.
In SR'13,
Electronic Proceedings in Theoretical Computer
Science 112, pages 91-98. March 2013.
@inproceedings{sr2013-BCC,
author = {Chareton, Christophe and Brunel, Julien and
Chemouil, David},
title = {Towards an Updatable Strategy Logic},
booktitle = {{P}roceedings of the 1st {I}nternational {W}orkshop
on {S}trategic {R}easoning ({SR}'13)},
acronym = {{SR}'13},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {112},
pages = {91-98},
year = {2013},
month = mar,
doi = {10.4204/EPTCS.112.14},
}
[CBK+13]
MaximilienColange,
SouheibBaarir,
FabriceKordon, and
YannThierry-Mieg.
Towards Distributed Software Model-Checking using
Decision Diagrams.
In CAV'13,
Lecture Notes in Computer Science 8044, pages 830-845. Springer-Verlag, July 2013.
@inproceedings{atva2013-CDRR,
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},
editor = {Hung, Dang Van and Ogawa, Mizuhito},
booktitle = {{P}roceedings of the 11th {I}nternational
{S}ymposium on {A}utomated {T}echnology for
{V}erification and {A}nalysis ({ATVA}'13)},
acronym = {{ATVA}'13},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8172},
pages = {118-132},
year = {2013},
month = oct,
}
[CHO+13]
KrishnenduChatterjee,
Thomas A.Henzinger,
JanOtop, and
AndreasPavlogiannis.
Distributed synthesis for LTL fragments.
In FMCAD'13,
pages 18-25.
IEEE Comp. Soc. Press, October 2013.
@inproceedings{fmcad2013-CHOP,
author = {Chatterjee, Krishnendu and Henzinger, Thomas A. and
Otop, Jan and Pavlogiannis, Andreas},
title = {Distributed synthesis for {LTL} fragments},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onference on {F}ormal {M}ethods in
{C}omputer-{A}ided {D}esign ({FMCAD}'13)},
acronym = {{FMCAD}'13},
publisher = {IEEE Comp. Soc. Press},
pages = {18-25},
year = {2013},
month = oct,
}
[CHR13]
PavolČerný,
Thomas A.Henzinger, and
ArjunRadhakrishna.
Quantitative abstraction refinement.
In POPL'13,
pages 115-128.
ACM Press, January 2013.
@inproceedings{popl2013-CHR,
author = {{\v{C}}ern{\'y}, Pavol and Henzinger, Thomas A. and
Radhakrishna, Arjun},
title = {Quantitative abstraction refinement},
editor = {Giacobazzi, Roberto and Cousot, Radhia},
booktitle = {Conference Record of the 40th {ACM}
{SIGPLAN}-{SIGACT} {S}ymposium on {P}rinciples of
{P}rogramming {L}anguages ({POPL}'13)},
acronym = {{POPL}'13},
publisher = {ACM Press},
pages = {115-128},
year = {2013},
month = jan,
doi = {10.1145/2429069.2429085},
}
@inproceedings{nasafm2013-DDLLM,
author = {David, Alexandre and Du, Dehui and Larsen, Kim
Guldstrand and Legay, Axel and Miku{\v{c}}ionis,
Marius},
title = {Optimizing Control Strategy Using Statistical Model
Checking},
editor = {Brat, Guillaume and Rungta, Neha and Venet, Arnaud},
booktitle = {{P}roceedings of the th {NASA} {F}ormal {M}ethods
{S}ymposium ({NFM}'13)},
acronym = {{NFM}'13},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {7871},
pages = {352-367},
year = {2013},
month = may,
doi = {10.1007/978-3-642-38088-4_24},
}
@article{jcss79(1)-DJLL,
author = {Demri, St{\'e}phane and Jurdzi{\'n}ski, Marcin and
Lachish, Oded and Lazi{\'c}, Ranko},
title = {The covering and boundedness problems for branching
vector addition systems},
publisher = {Elsevier},
journal = {Journal of Computer and System Sciences},
volume = {79},
number = {1},
pages = {23-38},
year = {2013},
month = feb,
doi = {10.1016/j.jcss.2012.04.002},
}
@inproceedings{avocs2013-DLLP,
author = {David, Alexandre and Larsen, Kim Guldstrand and
Legay, Axel and Poulsen, Danny B{\o}gsted},
title = {Statistical Model Checking of Dynamic Networks of
Stochastic Hybrid Automata},
editor = {Schneider, Steve and Treharne, Helen},
booktitle = {{P}roceedings of the 13th {I}nternational {W}orkshop
on {A}utomated {V}erification of {C}ritical
{S}ystems ({AVOCS}'13)},
acronym = {{AVOCS}'13},
publisher = {European Association of Software Science and
Technology},
series = {Electronic Communications of the EASST},
volume = {10},
year = {2013},
month = sep,
}
[DLM+13]
Peter H.Dalsgaard,
ThibaultLe Guilly,
DanielMiddelhede,
PeturOlsen,
ThomasPedersen,
Anders P.Ravn, and
ArneSkou.
A Toolchain for Home Automation Controller
Development.
In SEAA'13,
pages 122-129.
September 2013.
@inproceedings{HLMOPRS-seaa2013,
author = {Dalsgaard, Peter H. and Le{~}Guilly, Thibault and
Middelhede, Daniel and Olsen, Petur and Pedersen,
Thomas and Ravn, Anders P. and Skou, Arne},
title = {A Toolchain for Home Automation Controller
Development},
editor = {Demir{\"o}rs, Onur and T{\"u}retken, Oktay},
booktitle = {{P}roceedings of the 39th {E}uromicro {C}onference
on {S}oftware {E}ngineering and {A}dvanced
{A}pplications ({SEAA}'13)},
acronym = {{SEAA}'13},
pages = {122-129},
year = {2013},
month = sep,
}
@mastersthesis{master13-EF,
author = {Ejsing{-}Dunn, Daniel and Fontani, Lisa},
title = {Infinite Runs in Recharge Automata},
year = {2013},
month = jun,
school = {Computer Science Department, Aalborg University,
Denmark},
}
@inproceedings{cav2013-EGM,
author = {Esparza, Javier and Ganty, Pierre and Majumdar,
Rupak},
title = {Parameterized verification of asynchronous
shared-memory systems},
editor = {Sharygina, Natasha and Veith, Helmut},
booktitle = {{P}roceedings of the 25th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'13)},
acronym = {{CAV}'13},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8044},
pages = {124-140},
year = {2013},
month = jul,
doi = {10.1007/978-3-642-39799-8_8},
}
@inproceedings{icalp2013-FJ,
author = {Fearnley, John and Jurdzi{\'n}ski, Marcin},
title = {Reachability in two-clock timed automata is
{PSPACE}-complete},
editor = {Fomin, Fedor V. and Freivalds, Rusins and
Kwiatkowska, Marta and Peleg, David},
booktitle = {{P}roceedings of the 40th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'13)~-- Part~{II}},
acronym = {{ICALP}'13},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {7966},
pages = {212-223},
year = {2013},
month = jul,
doi = {10.1007/978-3-642-39212-2_21},
}
10.1007/978-3-031-74234-7_16
PDF