@inproceedings{BLW01-tacas,
address = {Genova, Italy},
month = apr,
year = 2001,
volume = 2031,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Margaria, Tiziana and Yi, Wang},
acronym = {{TACAS}'01},
booktitle = {{P}roceedings of the 7th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'01)},
author = {Bollig, Benedikt and Leucker, Martin and
Weber, Michael},
title = {Parallel Model Checking for the Alternation
Free Mu-Calculus},
pages = {543-558},
abstract = {In this paper, we describe
the design and implementation of a parallel
model checking algorithm for the
alternation free fragment of the
mu-calculus. It exploits a characterisation
of the model checking problem for this
fragment in terms of two-person games. Our
algorithm determines the corresponding
winner in parallel. It is designed to run
on a network of workstations. An
implementation within the verification tool
Truth shows promising results.}
}
@inproceedings{BL01b-time,
address = {Cividale del Friuli, Italy},
month = jun,
year = 2001,
publisher = {{IEEE} Computer Society Press},
acronym = {{TIME}'01},
booktitle = {{P}roceedings of the 8th {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'01)},
author = {Bollig, Benedikt and Leucker, Martin},
title = {Modelling, Specifying, and Verifying Message Passing
Systems},
pages = {240-247},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BL-time01b.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BL-time01b.ps},
abstract = {We present a model for Message Passing
Systems unifying concepts of message sequence charts
(MSCs) and Lamport diagrams. Message passing systems may
be defined ---~similarly to MSCs~--- without having a
concrete communication medium in mind. Our main
contribution is that we equip such systems with a tool
set of specification and verification procedures. We
provide a global linear time temporal logic which may be
employed for specifying message passing systems. In an
independent step, a communication channel may be
specified. Given both specifications, we construct a
B{\"u}chi automaton accepting those linearisations of MSCs
which satisfy the given formula and correspond to a
fixed but arbitrary channel.}
}
@inproceedings{BL01a-time,
address = {Cividale del Friuli, Italy},
month = jun,
year = 2001,
publisher = {{IEEE} Computer Society Press},
acronym = {{TIME}'01},
booktitle = {{P}roceedings of the 8th {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'01)},
author = {Bollig, Benedikt and Leucker, Martin},
title = {Deciding {LTL} over {M}azurkiewicz Traces},
pages = {189-197},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BL-time01.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BL-time01.ps},
abstract = {Linear time temporal logic (LTL) has
become a well established tool for specifying the
dynamic behaviour of reactive systems with an
interleaving semantics, and the automata-theoretic
approach has proven to be a very useful mechanism
for performing automatic verification in this
setting. Especially alternating automata turned out
to be a powerful tool in constructing efficient yet
simple to understand decision procedures and
directly yield further on-the-fly model checking
procedures. In this paper we exhibit a decision
procedure for LTL over Mazurkiewicz traces which
generalises the classical automata-theoretic
approach to a linear time temporal logic interpreted
no longer over sequences but certain partial orders.
Specifically, we construct a (linear) alternating
B{\"u}chi automaton accepting the set of linearisations
of traces satisfying the formula at hand. The
salient point of our technique is to apply a notion
of independence-rewriting to formulas of the logic.
Furthermore, we show that the class of linear and
trace-consistent alternating B{\"u}chi automata
corresponds exactly to LTL formulas over
Mazurkiewicz traces, lifting a similar result from
L{\"o}ding and Thomas formulated in the framework of
LTL over words.}
}
@inproceedings{BLW02,
address = {Grenoble, France},
month = apr,
year = 2002,
volume = 2318,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Bosnacki, Dragan and Leue, Stefan},
acronym = {{SPIN}'02},
booktitle = {{P}roceedings of the 9th {I}nternational
{SPIN} {W}orkshop on {M}odel {C}hecking {S}oftware
({SPIN}'02)},
author = {Bollig, Benedikt and Leucker, Martin and Weber, Michael},
title = {Local Parallel Model Checking for the
Alternation-Free \({{\mu}}\)-Calculus},
pages = {128-147},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLW-spin02.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLW-spin02.pdf},
absrtact = {We describe the design of (several
variants of) a local parallel model-checking
algorithm for the alternation-free fragment of the
\(\mu\)-calculus. It exploits a characterisation of the
problem for this fragment in terms of two-player
games. For the corresponding winner, our algorithm
determines in parallel a winning strategy, which may
be employed for interactively debugging the
underlying system, and is designed to run on a
network of workstations. Depending on the variant,
its complexity is linear or quadratic. A prototype
implementation within the verification tool Truth
shows promising results in practice.}
}
@inproceedings{BolligLeuckerNoll02,
address = {Grenoble, France},
month = apr,
year = 2002,
volume = 2303,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Nielsen, Mogens and Engberg, Uffe},
acronym = {{FoSSaCS}'02},
booktitle = {{P}roceedings of the 5th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'02)},
author = {Bollig, Benedikt and Leucker, Martin and Noll, Thomas},
title = {Generalised Regular {MSC} Languages},
pages = {52-66},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BLN02-fossacs.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BLN02-fossacs.ps},
abstract = {We establish the concept of
regularity for languages consisting of Message
Sequence Charts (MSCs). To this aim, we
formalise their behaviour by string languages
and give a natural definition of regularity in
terms of an appropriate Nerode right
congruence. Moreover, we present a class of
accepting automata and establish several
decidability and closure properties of MSC
languages. We also provide a logical
characterisation by a monadic second-order
logic interpreted over MSCs. In contrast to
existing work on regular MSC languages, our
approach is neither restricted to a certain
class of MSCs nor tailored to a fixed
communication medium (such as a FIFO channel).
It explicitly allows MSCs with message
overtaking and is thus applicable to a broad
range of channel types like mixtures of stacks
and FIFOs.}
}
@inproceedings{BLL02,
address = {Tbilisi, Georgia},
month = oct,
year = 2002,
volume = 2514,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Baaz, Matthias and Voronkov, Andrei},
acronym = {{LPAR}'02},
booktitle = {{P}roceedings of the 9th {I}nternational
{C}onference on {L}ogic for {P}rogramming,
{A}rtificial {I}ntelligence, and {R}easoning
({LPAR}'02)},
author = {Bollig, Benedikt and Leucker, Martin and Lucas, {\relax Ph}ilipp},
title = {Extending Compositional Message Sequence Graphs},
pages = {68-85},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BLL-lpar.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BLL-lpar.ps},
abstract = {We extend the formal developments for
message sequence charts (MSCs) to support scenarios
with lost and found messages. We define a notion of
extended compositional message sequence charts
(ECMSCs) which subsumes the notion of compositional
message sequence charts in expressive power but
additionally allows to define lost and found
messages explicitly. As usual, ECMSCs might be
combined by means of choice and repetition towards
(extended) compositional message sequence graphs.
We show that ---~despite extended expressive
power~--- model checking of monadic second-order
logic (MSO) for this framework remains to be
decidable. The key technique to achieve our results
is to use an extended notion for linearizations.}
}
@inproceedings{BL03b-asian,
address = {Mumbai, India},
month = dec,
year = 2003,
volume = 2896,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Saraswat, Vijay A.},
acronym = {{ASIAN}'03},
booktitle = {{P}roceedings of the 8th {A}sian
{C}omputing {S}cience {C}onference
({ASIAN}'03)},
author = {Bollig, Benedikt and Leucker, Martin},
title = {Model Checking Probabilistic Distributed Systems},
pages = {291-304},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/asian03.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/asian03.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/asian03.ps},
abstract = {Protocols for distributed systems
make often use of random transitions to achieve a
common goal. A popular example are randomized
leader election protocols. We introduce
probabilistic product automata (PPA) as a natural
model for this kind of systems. To reason about
these systems, we propose to use a product version
of linear temporal logic~(PLTL). The main result
of the paper is a model-checking procedure for PPA
and~PLTL. With its help, it is possible to check
qualitative properties of distributed systems
automatically.}
}
@article{BL03,
publisher = {Elsevier Science Publishers},
journal = {Data \& Knowledge Engineering},
author = {Bollig, Benedikt and Leucker, Martin},
title = {Deciding {LTL} over {M}azurkiewicz Traces},
year = 2003,
volume = 44,
number = 2,
pages = {221-240},
month = feb,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BL-time01.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BL-time01.ps},
doi = {10.1016/S0169-023X(02)00136-2},
abstract = {Linear temporal logic (LTL) has become a
well established tool for specifying the dynamic
behaviour of reactive systems with an interleaving
semantics, and the automatatheoretic approach has proven
to be a very useful mechanism for performing automatic
verification in this setting. Especially alternating
automata turned out to be a powerful tool in
constructing efficient yet simple to understand decision
procedures and directly yield further on-the-fly model
checking procedures. In this paper, we exhibit a
decision procedure for LTL over Mazurkiewicz traces that
generalises the classical automatatheoretic approach to
a LTL interpreted no longer over sequences but certain
partial orders. Specifically, we construct a (linear)
alternating B{\"u}chi automaton (ABA) accepting the set of
linearisations of traces satisfying the formula at hand.
The salient point of our technique is to apply a notion
of independence-rewriting to formulas of the logic.
Furthermore, we show that the class of linear and
trace-consistent ABA corresponds exactly to LTL formulas
over Mazurkiewicz traces, lifting a similar result from
L{\"o}ding and Thomas formulated in the framework of LTL
over words.}
}
@incollection{BL03a,
year = 2004,
volume = 2925,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baier, {\relax Ch}ristel and Haverkort, Boudewijn R.
and Hermanns, Holger and Katoen, Joost-Pieter and
Siegle, Markus and Vaandrager, Frits},
acronym = {{V}alidation of {S}tochastic {S}ystems},
booktitle = {{V}alidation of {S}tochastic {S}ystems: {A} {G}uide
to {C}urrent {R}esearch},
author = {Bollig, Benedikt and Leucker, Martin},
title = {Verifying Qualitative Properties of Probabilistic Programs},
pages = {124-146},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BL_VOSS04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BL_VOSS04.pdf},
abstract = {We present procedures for
checking linear temporal logic and
automata specifications of sequential and
concurrent probabilistic programs. We
follow two different approaches: For LTL
and sequential probabilistic programs,
our method proceeds in a tableau style
fashion, while the remaining procedures
are based on automata theory.}
}
@inproceedings{BGLBC04,
address = {Toulouse, France},
month = aug,
year = 2004,
series = {IFIP Conference Proceedings},
publisher = {Kluwer Academic Publishers},
editor = {L{\'e}vy, Jean-Jacques and Mayr, Ernst W. and
Mitchell, John C.},
acronym = {{IFIP~TCS}'04},
booktitle = {{P}roceedings of the 3rd {IFIP} {I}nternational
{C}onference on {T}heoretical {C}omputer
{S}cience
({IFIP~TCS}'04)},
author = {Baier, Christel and Gr{\"o}{\ss}er, Marcus and Leucker, Martin and Bollig, Benedikt
and Ciesinski, Franck},
title = {Probabilistic controller synthesis},
pages = {493-506},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGLBC_IFIPTCS04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGLBC_IFIPTCS04.pdf},
abstract = {Controller synthesis addresses the
question of how to limit the internal behaviour of a
given implementation to meet its specification,
regardless of the behaviour enforced by the
environment. In this paper, we consider a model with
probabilism and nondeterminism where the
nondeterministic choices in some states are assumed to
be controllable, while the others are under the
control of an unpredictable environment. We first
consider probabilistic computation tree logic as
specification formalism, discuss the role of the
strategy-types for the controller and show the
NP-hardness of the controller synthesis problem. The
second part of the paper presents a controller
synthesis algorithm for automata-specifications.}
}
@inproceedings{BL04,
address = {London, UK},
month = aug,
year = 2004,
volume = 3170,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gardner, {\relax Ph}ilippa and Yoshida, Nobuko},
acronym = {{CONCUR}'04},
booktitle = {{P}roceedings of the 15th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'04)},
author = {Bollig, Benedikt and Leucker, Martin},
title = {Message-Passing Automata are Expressively Equivalent to {EMSO} Logic},
pages = {146-160},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BL04-MPA.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BL04-MPA.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BL04-MPA.ps},
doi = {10.1007/978-3-540-28644-8_10},
abstract = {We study the expressiveness of
finite message-passing automata with a priori
unbounded channels and show them to capture
exactly the class of MSC languages that are
definable in existential monadic second-order
logic interpreted over MSCs. Moreover, we prove
the monadic quantifier-alternation hierarchy
over MSCs to be infinite and conclude that the
class of MSC languages accepted by
message-passing automata is not closed under
complement. Furthermore, we show that
satisfiability for (existential) monadic
seconder-order logic over MSCs is undecidable.}
}
@inproceedings{BL-forte05,
address = {Taipei, Taiwan},
month = oct,
year = 2005,
volume = 3731,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Wang, Farn},
acronym = {{FORTE}'05},
booktitle = {{P}roceedings of 25th {IFIP} {WG6.1}
{I}nternational {C}onference on {F}ormal
{T}echniques for {N}etworked and {D}istributed {S}ystems
({FORTE}'05)},
author = {Bollig, Benedikt and Leucker, Martin},
title = {A Hierarchy of Implementable {MSC} Languages},
pages = {53-67},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BL-forte05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BL-forte05.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BL-forte05.ps},
doi = {10.1007/11562436_6},
abstract = {We develop a unifying theory of
message-passing automata (MPAs) and MSC
languages. We study several variants of
regular as well as product MSC languages,
their closure under finite union and their
intersection. Furthermore, we analyse the
expressive power of several variants of MPAs
and characterize the language classes of
interest by the corresponding classes
of~MPAs.}
}
@inproceedings{Bollig05,
address = {L{\"u}beck, Germany},
month = aug,
year = 2005,
volume = 3623,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Liskiewicz, Maciej and Reischuk, R{\"u}diger},
acronym = {{FCT}'05},
booktitle = {{P}roceedings of the 15th {I}nternational {S}ymposium
on {F}undamentals of {C}omputation {T}heory
({FCT}'05)},
author = {Bollig, Benedikt},
title = {On the Expressiveness of Asynchronous Cellular Automata},
pages = {528-539},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bol-fct05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bol-fct05.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bol-fct05.ps},
doi = {10.1007/11537311_23},
abstract = {We show that a slightly extended version
of asynchronous cellular automata, relative to any
class of pomsets and dags without autoconcurrency, has
the same expressive power as the existential fragment
of monadic second-order logic. In doing so, we provide
a framework that unifies many approaches to modeling
distributed systems such as the models of asynchronous
trace automata and communicating finite-state machines.
As a byproduct, we exhibit classes of pomsets and dags
for which the radius of graph acceptors can be reduced
to~1.}
}
@phdthesis{Bollig05-Thesis,
author = {Bollig, Benedikt},
title = {Automata and Logics for Message Sequence Charts},
year = 2005,
month = may,
school = {Department of Computer Science, RWTH Aachen, Germany},
type = {Th{\`e}se de doctorat},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bollig-phd.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bollig-phd.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bollig-phd.ps}
}
@inproceedings{BKSS-tacas06,
address = {Vienna, Austria},
month = mar,
year = 2006,
volume = {3920},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hermanns, Holger and Palsberg, Jens},
acronym = {{TACAS}'06},
booktitle = {{P}roceedings of the 12th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'06)},
author = {Bollig, Benedikt and Kern, Carsten and
Schl{\"u}tter, Markus and Stolz, Volker},
title = {{MSC}an: A Tool for Analyzing {MSC} Specifications},
pages = {455-458},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSCan.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSCan.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MSCan.ps},
doi = {10.1007/11691372_32},
abstract = {We present the tool MSCan, which supports MSC-based
system development. In particular, it automatically checks
high-level MSC specifications for implementability.}
}
@book{Bollig06,
author = {Bollig, Benedikt},
title = {Formal Models of Communicating Systems~--- Languages, Automata,
and Monadic Second-Order Logic},
year = {2006},
month = jun,
publisher = {Springer},
isbn = {3-540-32922-6},
otherurl = {http://www.springer.com/978-3-540-32922-6},
url = {http://www.lsv.ens-cachan.fr/~bollig/fmcs/},
abstract = {This book studies the relationship between automata and
monadic second-order logic, focusing on classes of automata that
describe the concurrent behavior of distributed systems.\par
It provides a unifying theory of communicating automata and their
logical properties. Based on Hanf's Theorem and Thomas's graph
acceptors, it develops a result that allows us to characterize many
popular models of distributed computation in terms of the existential
fragment of monadic second-order logic. In particular, the book covers
finite automata, asynchronous (cellular) automata, communicating
finite-state machines, and lossy channel systems. Model behavior is
described using graphs and partial orders, leading to the notions of
Mazurkiewicz traces, message sequence charts, and live sequence
charts.\par
This book is suitable for senior undergraduate and graduate courses on
advanced automata theory, concurrency and communication issues. It can
also be used as a reference by researchers concerned with the formal
modeling of concurrent systems. Some knowledge of automata theory is a
prerequisite. Numerous exercises, chapter summaries, and suggested
reading allow for self-study, while the book is supported with a website
containing course material and solutions.}
}
@article{BL-tcs05,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Bollig, Benedikt and Leucker, Martin},
title = {Message-Passing Automata are Expressively Equivalent to {EMSO}
Logic},
year = 2006,
month = aug,
volume = 358,
number = {2-3},
pages = {150-172},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BL04-MPA.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BL04-MPA.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BL04-MPA.ps},
doi = {10.1016/j.tcs.2006.01.014},
abstract = {We study the expressiveness of
finite message-passing automata with \emph{a priori}
unbounded FIFO channels and show them to
capture exactly the class of MSC languages
that are definable in existential monadic
second-order logic interpreted over MSCs.
Furthermore, we prove the monadic
quantifier-alternation hierarchy over MSCs to
be infinite and conclude that the class of
MSC languages accepted by message-passing
automata is not closed under complement. }
}
@techreport{LSV:06:11,
author = {Bollig, Benedikt and Kuske, Dietrich},
title = {Distributed {M}uller Automata and Logics},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = 2006,
month = may,
type = {Research Report},
number = {LSV-06-11},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-11.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-11.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2006-11.ps},
note = {23~pages},
abstract = {We consider Muller asynchronous cellular automata running on
infinite dags over distributed alphabets. We show that they have the same
expressive power as the existential fragment of a monadic second-order logic
featuring a first-order quantifier to express that there are infinitely many
elements satisfying some property. Our result is based on an extension of the
classical Ehrenfeucht-Fra{\"\i}ss{\'e} game to cope with infinite structures
and the new first-order quantifier. As a byproduct, we obtain a logical
characterization of unbounded Muller message-passing automata running on
infinite message sequence charts.}
}
@inproceedings{ABG-fsttcs07,
address = {New~Delhi, India},
month = dec,
year = 2007,
volume = 4855,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Arvind, V. and Prasad, Sanjiva},
acronym = {{FSTTCS}'07},
booktitle = {{P}roceedings of the 27th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'07)},
author = {Akshay, S. and Bollig, Benedikt and Gastin, Paul},
title = {Automata and Logics for Timed Message Sequence Charts},
pages = {290-302},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABG-fsttcs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABG-fsttcs07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ABG-fsttcs07.ps},
doi = {10.1007/978-3-540-77050-3_24},
abstract = {We provide a framework for distributed systems that impose timing constraints
on their executions. We~propose a timed model of communicating finite-state machines,
which communicate by exchanging messages through channels and use event clocks to
generate collections of timed message sequence charts~(T-MSCs). As~a specification
language, we~propose a monadic second-order logic equipped with timing predicates and
interpreted over~T-MSCs. We establish expressive equivalence of our automata and logic.
Moreover, we prove that, for (existentially) bounded channels, emptiness and
satisfiability are decidable for our automata and logic.}
}
@inproceedings{BKM-fsttcs07,
address = {New~Delhi, India},
month = dec,
year = 2007,
volume = 4855,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Arvind, V. and Prasad, Sanjiva},
acronym = {{FSTTCS}'07},
booktitle = {{P}roceedings of the 27th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'07)},
author = {Bollig, Benedikt and Kuske, Dietrich and Meinecke, Ingmar},
title = {Propositional Dynamic Logic for Message-Passing Systems},
pages = {303-315},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKM-fsttcs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKM-fsttcs07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BKM-fsttcs07.ps},
doi = {10.1007/978-3-540-77050-3_25},
abstract = {We examine a bidirectional Propositional Dynamic Logic~(PDL) for message
sequence charts~(MSCs) extending LTL and~TLC\textsuperscript{-}.
Every formula is translated into an equivalent communicating finite-state
machine~(CFM) of exponential size. This synthesis problem is solved in full generality,
i.e.,~also for MSCs with unbounded channels. The model checking problems for CFMs and
for HMSCs against PDL formulas are shown to be in PSPACE for existentially
bounded~MSCs. It~is shown that CFMs are to weak to capture the semantics of PDL with
intersection.}
}
@inproceedings{BK-lata2007,
address = {Tarragona, Spain},
month = mar # {-} # apr,
year = 2007,
futureseries = {Lecture Notes in Computer Science},
nmnote = {published as Report 35/07 Research Group on Mathematical
Linguistics, Universitat Rovira i Virgili, Tarragona},
editor = {{\'E}sik, Zolt{\'a}n and Mart{\'\i}n-Vide, Carlos and
Mitrana, Victor},
acronym = {{LATA}'07},
booktitle = {{P}reliminary {P}roceedings of the 1st {I}nternational {C}onference on {L}anguage
and {A}utomata {T}heory and {A}pplications ({LATA}'07)},
author = {Bollig, Benedikt and Kuske, Dietrich},
title = {{M}uller Message-Passing Automata and Logics},
nopages = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BK-lata07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BK-lata07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BK-lata07.ps},
abstract = {We study nonterminating message-passing automata whose behavior
is described by infinite message sequence charts. As~a~first result, we
show that Muller, B{\"u}chi, and termination-detecting Muller acceptance are
equivalent for these devices. To describe the expressive power of these
automata, we give a logical characterization. More precisely, we show that
they have the same expressive power as the existential fragment of a
monadic second-order logic featuring a first-order quantifier to express
that there are infinitely many elements satisfying some property. Our
result is based on a new extension of the classical Ehrenfeucht-Fra{\"\i}ss{\'e}
game to cope with infinite structures and the new first-order quantifier.}
}
@inproceedings{BM-lfcs2007,
address = {New~York, New~York, USA},
month = jun,
year = 2007,
volume = 4514,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Artemov, Sergei N. and Nerode, Anil},
acronym = {{LFCS}'07},
booktitle = {{P}roceedings of the {S}ymposium on {L}ogical {F}oundations of
{C}omputer {S}cience ({LFCS}'07)},
author = {Bollig, Benedikt and Meinecke, Ingmar},
title = {Weighted Distributed Systems and Their Logics},
pages = {54-68},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BM-lfcs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BM-lfcs07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BM-lfcs07.ps},
doi = {10.1007/978-3-540-72734-7_5},
abstract = {We provide a model of weighted distributed systems and give a
logical characterization thereof. Distributed systems are represented as
weighted asynchronous cellular automata. Running over directed acyclic
graphs, Mazurkiewicz traces, or (lossy) message sequence charts, they
allow for modeling several communication paradigms in a unifying
framework, among them probabilistic shared-variable and probabilistic
lossy-channel systems. We~show that any such system can be described by a
weighted existential MSO formula and, vice versa, any formula gives rise
to a weighted asynchronous cellular automaton.}
}
@inproceedings{BKKL-tacas07,
address = {Braga, Portugal},
month = mar,
year = 2007,
volume = {4424},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Grumberg, Orna and Huth, Michael},
acronym = {{TACAS}'07},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'07)},
author = {Bollig, Benedikt and Katoen, Joost-Pieter and Kern, Carsten
and Leucker, Martin},
title = {Replaying Play in and Play out: Synthesis of Design Models
from Scenarios by Learning},
pages = {435-450},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-tacas07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-tacas07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BKKL-tacas07.ps},
doi = {10.1007/978-3-540-71209-1_33},
abstract = {This paper is concerned with bridging the
gap between requirements, provided
as a set of scenarios, and conforming design models. The~novel aspect
of our approach is to exploit learning for the synthesis of design
models. In particular, we present a procedure that infers a
message-passing automaton~(MPA) from a given set of positive and
negative scenarios of the systems behavior provided as message
sequence
charts~(MSCs). The~paper investigates which classes of regular MSC
languages and corresponding MPAs can (not) be learned, and presents a
dedicated tool based on the learning library LearnLib that supports
our approach.}
}
@article{BB-lmcs08,
journal = {Logical Methods in Computer Science},
author = {Bollig, Benedikt},
title = {On the Expressive Power of {\(2\)}-Stack Visibly Pushdown Automata},
volume = 4,
number = {4\string:16},
month = dec,
year = 2008,
nopages = {},
doi = {10.2168/LMCS-4(4:16)2008},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BB-lmcs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BB-lmcs08.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BB-lmcs08.ps},
abstract = {Visibly pushdown automata are input-driven pushdown automata
that recognize some non-regular context-free languages while
preserving the nice closure and decidability properties of
finite automata. Visibly pushdown automata with multiple
stacks have been considered recently by La~Torre,
Madhusudan, and Parlato, who exploit the concept of
visibility further to obtain a rich automata class that can
even express properties beyond the class of context-free
languages. At the same time, their automata are closed under
boolean operations, have a decidable emptiness and inclusion
problem, and enjoy a logical characterization in terms of a
monadic second-order logic over words with an additional
nesting structure. These results require a restricted
version of visibly pushdown automata with multiple stacks
whose behavior can be split up into a fixed number of
phases. In this paper, we~consider 2-stack visibly pushdown
automata (i.e., visibly pushdown automata with two stacks)
in their unrestricted form. We show that they are
expressively equivalent to the existential fragment of
monadic second-order logic. Furthermore, it turns out that
monadic second-order quantifier alternation forms an
infinite hierarchy wrt.~words with multiple nestings.
Combining these results, we conclude that 2-stack visibly
pushdown automata are not closed under complementation.
Finally, we discuss the expressive power of B{\"u}chi
2-stack visibly pushdown automata running on infinite
(nested) words. Extending the logic by an infinity
quantifier, we can likewise establish equivalence to
existential monadic second-order logic.}
}
@misc{dots-3.1,
author = {Bollig, Benedikt and Bouyer, Patricia and Cassez, Franck and
Chatain, {\relax Th}omas and Gastin, Paul and Haddad, Serge
and Jard, Claude},
title = {Model for distributed timed systems},
howpublished = {Deliverable DOTS~3.1 (ANR-06-SETI-003)},
year = 2008,
month = sep
}
@inproceedings{ABH-dlt08,
address = {Kyoto, Japan},
month = sep,
year = 2008,
volume = 5257,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ito, Masami and Toyama, Masafumi},
acronym = {{DLT}'08},
booktitle = {{P}roceedings of the 12th {I}nternational
{C}onference on {D}evelopments in {L}anguage {T}heory
({DLT}'08)},
author = {Atig, Mohamed Faouzi and Bollig, Benedikt and Habermehl, Peter},
title = {Emptiness of multi-pushdown automata is \(2\){ETIME}-complete},
pages = {121-133},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABH-dlt08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABH-dlt08.pdf},
doi = {10.1007/978-3-540-85780-8_9},
abstract = {We consider multi-pushdown automata, a multi-stack extension of
pushdown automata that comes with a constraint on stack operations: a pop
can only be performed on the first non-empty stack (which implies that we
assume a linear ordering on the collection of stacks). We show that the
emptiness problem for multi-pushdown automata is 2ETIME-complete wrt.~the
number of stacks. Containment in 2ETIME is shown by translating an
automaton into a grammar for which we can check if the generated language
is empty. The lower bound is established by simulating the behavior of an
alternating Turing machine working in exponential space. We also compare
multi-pushdown automata with the model of bounded-phase multi-stack
(visibly) pushdown automata.}
}
@inproceedings{BKKL-concur08,
address = {Toronto, Canada},
month = aug,
year = 2008,
volume = 5201,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {van Breugel, Franck and Chechik, Marsha},
acronym = {{CONCUR}'08},
booktitle = {{P}roceedings of the 19th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'08)},
author = {Bollig, Benedikt and Katoen, Joost-Pieter and Kern, Carsten and
Leucker, Martin},
title = {{\itshape Smyle}: A Tool for Synthesizing Distributed Models from
Scenarios by Learning},
pages = {162-166},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-concur08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-concur08.pdf},
doi = {10.1007/978-3-540-85361-9_15}
}
@inproceedings{ABGMN-concur08,
address = {Toronto, Canada},
month = aug,
year = 2008,
volume = 5201,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {van Breugel, Franck and Chechik, Marsha},
acronym = {{CONCUR}'08},
booktitle = {{P}roceedings of the 19th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'08)},
author = {Akshay, S. and Bollig, Benedikt and Gastin, Paul and Mukund,
Madhavan and Narayan Kumar, K.},
title = {Distributed Timed Automata with Independently Evolving
Clocks},
pages = {82-97},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABGMN-concur08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABGMN-concur08.pdf},
doi = {10.1007/978-3-540-85361-9_10},
abstract = { We propose a model of distributed timed systems where each
component is a timed automaton with a set of local clocks that evolve at a
rate independent of the clocks of the other components. A clock can be
read by any component in the system, but it can only be reset by the
automaton it belongs to.\par
There are two natural semantics for such systems. The \emph{universal}
semantics captures behaviors that hold under any choice of clock rates for
the individual components. This is a natural choice when checking that a
system always satisfies a positive specification. However, to check if a
system avoids a negative specification, it is better to use the
\emph{existential} semantics---the set of behaviors that the system can
possibly exhibit under some choice of clock rates.\par
We show that the existential semantics always describes a regular set of
behaviors. However, in the case of universal semantics, checking emptiness
turns out to be undecidable. As an alternative to the universal semantics,
we propose a \emph{reactive} semantics that allows us to check positive
specifications and yet describes a regular set of behaviors. }
}
@article{BK-IC08,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Bollig, Benedikt and Kuske, Dietrich},
title = {{M}uller Message-Passing Automata and Logics},
volume = 206,
number = {9-10},
pages = {1084-1094},
year = 2008,
month = sep # {-} # oct,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BK-IC08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BK-IC08.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BK-IC08.ps},
doi = {10.1016/j.ic.2008.03.010},
abstract = {We study nonterminating message-passing automata whose behavior
is described by infinite message sequence charts. As~a first result, we~show
that Muller, B{\"u}chi, and termination-detecting Muller acceptance are
equivalent for these devices. To~describe the expressive power of these
automata, we give a logical characterization. More precisely, we~show that
they have the same expressive power as the existential fragment of a monadic
second-order logic featuring a first-order quantifier to express that there
are infinitely many elements satisfying some property. This result is based
on Vinner's extension of the classical Ehrenfeucht-Fra{\"\i}ss{\'e} game to
cope with the infinity quantifier.}
}
@article{BKKL-tse09,
publisher = {{IEEE} Computer Society Press},
journal = {IEEE Transactions on Software Engineering},
author = {Bollig, Benedikt and Katoen, Joost-Pieter and Kern, Carsten
and Leucker, Martin},
title = {Learning Communicating Automata from~{MSCs}},
volume = {36},
number = {3},
pages = {390-408},
month = may # {-} # jun,
year = 2010,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-tse09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-tse09.pdf},
doi = {10.1109/TSE.2009.89},
abstract = {This paper is concerned with bridging the gap between
requirements and distributed systems. Requirements are defined as basic
message sequence charts (MSCs) specifying positive and negative scenarios.
Communicating finite-state machines (CFMs), \textit{i.e.}, finite automata
that communicate via FIFO buffers, act as system realizations. The key
contribution is a generalization of Angluin's learning algorithm for
synthesizing CFMs from MSCs. This approach is exact---the resulting CFM
precisely accepts the set of positive scenarions and rejects all negative
ones---and yields fully asynchronous implementations. The paper
investigates for which classes of MSC languages CFMs can be learned,
presents an optimization technique for learning partial orders, and
provides substantial empirical evidence indicating the practical
feasibility of the approach.}
}
@article{BKKL-cai09,
publisher = {Slovak Academy of Sciences},
journal = {Computing and Informatics},
author = {Bollig, Benedikt and Katoen, Joost-Pieter and Kern, Carsten
and Leucker, Martin},
title = {{SMA}---The Smyle Modeling Approach},
volume = {29},
number = {1},
pages = {45-72},
year = 2010,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-cai09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-cai09.pdf},
abstract = {This paper introduces the model-based software development
lifecycle model \emph{SMA}---the Smyle \emph{Modeling Approach}---which is
centered around \emph{Smyle}. \emph{Smyle} is a dedicated learning
procedure to support engineers to interactively obtain design models from
requirements, characterized as either being desired (positive) or unwanted
(negative) system behavior. Within \emph{SMA}, the learning approach is
complemented by so-called \emph{scenario patterns} where the engineer can
specify \emph{clearly} desired or unwanted behavior. This way, user
interaction is reduced to the interesting scenarios limiting the design
effort considerably. In~\emph{SMA}, the learning phase is further
complemented by an effective analysis phase that allows for detecting
design flaws at an early design stage. Using learning techniques allows us
to gradually develop and refine requirements, naturally supporting
evolving requirements, and allows for a rather inexpensive redesign in
case anomalous system behavior is detected during analysis, testing, or
maintenance. This paper describes the approach and reports on first
practical experiences.}
}
@inproceedings{BG-dlt09,
address = {Stuttgart, Germany},
month = jun # {-} # jul,
year = 2009,
volume = {5583},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Diekert, Volker and Nowotka, Dirk},
acronym = {{DLT}'09},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onference on {D}evelopments in {L}anguage {T}heory
({DLT}'09)},
author = {Bollig, Benedikt and Gastin, Paul},
title = {Weighted versus Probabilistic Logics},
pages = {18-38},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BG-dlt09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BG-dlt09.pdf},
doi = {10.1007/978-3-642-02737-6_2},
abstract = {While a mature theory around logics such as MSO, LTL, and CTL
has been developed in the pure boolean setting of finite automata,
weighted automata lack such a natural connection with (temporal) logic and
related verification algorithms. In this paper, we will identify weighted
versions of MSO and CTL that generalize the classical logics and even
other quantitative extensions such as probabilistic CTL. We establish
expressiveness results on our logics giving translations from weighted and
probabilistic CTL into weighted MSO.}
}
@inproceedings{BHKL-ijcai2009,
address = {Pasadena, California, USA},
month = jul,
year = 2009,
publisher = {AAAI Press},
editor = {Boutilier, Craig},
acronym = {{IJCAI}'09},
booktitle = {{P}roceedings of the 21st {I}nternational {J}oint
{C}onference on {A}rtificial {I}ntelligence
({IJCAI}'09)},
author = {Bollig, Benedikt and Habermehl, Peter and Kern, Carsten and
Leucker, Martin},
title = {Angluin-Style Learning of~{NFA}},
pages = {1004-1009},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHKL-ijcai09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHKL-ijcai09.pdf},
abstract = {We introduce NL\(^{*}\), a learning algorithm for inferring
non-deterministic finite-state automata using membership and equivalence
queries. More specifically, residual finite-state automata (RFSA) are
learned similarly as in Angluin's popular L\(^{*}\) algorithm, which,
however, learns deterministic finite-state automata~(DFA). Like in a~DFA,
the~states of an RFSA represent residual languages. Unlike a~DFA, an~RFSA
restricts to prime residual languages, which cannot be described as the
union of other residual languages. In~doing~so, RFSA can be exponentially
more succinct than~DFA. They are, therefore, the preferable choice for
many learning applications. The implementation of our algorithms is
applied to a collection of examples and confirms the expected advantage of
NL\(^{*}\) over L\(^{*}\).}
}
@inproceedings{BGH-Fossacs09,
address = {York, UK},
month = mar,
year = 2009,
volume = 5504,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {de Alfaro, Luca},
acronym = {{FoSSaCS}'09},
booktitle = {{P}roceedings of the 12th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'09)},
author = {Bollig, Benedikt and Grindei, Manuela-Lidia and
Habermehl, Peter},
title = {Realizability of Concurrent Recursive Programs},
pages = {410-424},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGH-fossacs09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGH-fossacs09.pdf},
doi = {10.1007/978-3-642-00596-1_29},
abstract = {We define and study an automata model of concurrent recursive
programs. An~automaton consists of a finite number of pushdown systems
running in parallel and communicating via shared actions. Actually, we
combine multi-stack visibly pushdown automata and Zielonka's asynchronous
automata towards a model with an undecidable emptiness problem. However, a
reasonable restriction allows us to lift Zielonka's Theorem to this
recursive setting and permits a logical characterization in terms of a
suitable monadic second-order logic. Building on results from Mazurkiewicz
trace theory and work by La~Torre, Madhusudan, and Parlato, we thus develop
a framework for the specification, synthesis, and verification of concurrent
recursive processes.}
}
@article{BKM-lmcs10,
journal = {Logical Methods in Computer Science},
author = {Bollig, Benedikt and Kuske, Dietrich and Meinecke, Ingmar},
title = {Propositional Dynamic Logic for Message-Passing Systems},
year = 2010,
month = sep,
volume = 6,
number = {3:16},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BKM-lmcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BKM-lmcs10.pdf},
doi = {10.2168/LMCS-6(3:16)2010},
abstract = {We examine a bidirectional propositional dynamic logic~(PDL) for
finite and infinite message sequence charts~(MSCs) extending
\(\textsf{LTL}\) and \(\textsf{TLC}^{-}\). By~this kind of multi-modal
logic we can express properties both in the entire future and in the past
of an event. Path expressions strengthen the classical until operator of
temporal logic. For every formula defining an MSC language, we construct a
communicating finite-state machine~(CFM) accepting the same language. The
CFM obtained has size exponential in the size of the formula. This
synthesis problem is solved in full generality, \textit{i.e.}, also for
MSCs with unbounded channels. The model checking problem for CFMs and
HMSCs turns out to be in PSPACE for existentially bounded MSCs. Finally,
we show that, for PDL with intersection, the semantics of a formula cannot
be captured by a CFM anymore.}
}
@inproceedings{BGMZ-icalp10,
address = {Bordeaux, France},
month = jul,
year = 2010,
volume = 6199,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abramsky, Samson and Meyer{ }auf{ }der{ }Heide, Friedhelm
and Spirakis, Paul},
acronym = {{ICALP}'10},
booktitle = {{P}roceedings of the 37th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'10)~-- {P}art~{II}},
author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin
and Zeitoun, Marc},
title = {Pebble weighted automata and transitive closure logics},
pages = {587-598},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-icalp10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-icalp10.pdf},
doi = {10.1007/978-3-642-14162-1_49},
abstract = {We introduce new classes of weighted automata on words. Equipped
with pebbles and a two-way mechanism, they go beyond the class of
recognizable formal power series, but capture a weighted version of
first-order logic with bounded transitive closure. In contrast to previous
work, this logic allows for unrestricted use of universal quantification.
Our main result states that pebble weighted automata, nested weighted
automata, and this weighted logic are expressively equivalent. We also
give new logical characterizations of the recognizable series.}
}
@inproceedings{BKKLNP-cav10,
address = {Edinburgh, Scotland, UK},
month = jul,
year = 2010,
volume = {6174},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cook, Byron and Jackson, Paul and Touili, Tayssir},
acronym = {{CAV}'10},
booktitle = {{P}roceedings of the 22nd
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'10)},
author = {Bollig, Benedikt and Katoen, Joost-Pieter and Kern, Carsten
and Leucker, Martin and Neider, Daniel and Piegdon, David R.},
title = {libalf: the Automata Learning Framework},
pages = {360-364},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BKKLNP-cav10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BKKLNP-cav10.pdf},
doi = {10.1007/978-3-642-14295-6_32},
abstract = {This paper presents \texttt{libalf}, a comprehensive,
open-source library for learning formal languages. \texttt{libalf} covers
various well-known learning techniques for finite automata (e.g.
Angluin's~\(\textsf{L}^*\), \textsf{Biermann}, \textsf{RPNI},~etc.) as
well as novel learning algorithms (such as for NFA and visibly one-counter
automata). \texttt{libalf}~is flexible and allows facilely interchanging
learning algorithms and combining domain-specific features in a
plug-and-play fashion. Its modular design and C++ implementation make it a
suitable platform for adding and engineering further learning algorithms
for new target models (\textit{e.g.}, B{\"u}chi automata).}
}
@inproceedings{BH-csr10,
address = {Kazan, Russia},
month = jun,
year = 2010,
volume = 6072,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Mayr, Ernst W.},
acronym = {{CSR}'10},
booktitle = {{P}roceedings of the 5th {I}nternational {C}omputer {S}cience
{S}ymposium in {R}ussia ({CSR}'10)},
author = {Bollig, Benedikt and H{\'e}lou{\"e}t, Lo{\"\i}c},
title = {Realizability of Dynamic {MSC} Languages},
pages = {48-59},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BH-csr10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BH-csr10.pdf},
doi = {10.1007/978-3-642-13182-0_5},
abstract = {We introduce dynamic communicating automata~(DCA), an~extension
of communicating finite-state machines that allows for dynamic creation of
processes. Their behavior can be described as sets of message sequence
charts~(MSCs). We~consider the realizability problem for DCA: given a
dynamic MSC grammar (a~high-level MSC specification), is there a DCA
defining the same set of MSCs? We~show that this problem is decidable in
doubly exponential time, and identify a class of realizable grammars that
can be implemented by \emph{finite} DCA.}
}
@inproceedings{BCGK-fossacs12,
address = {Tallinn, Estonia},
month = mar,
year = 2012,
volume = 7213,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Birkedal, Lars},
acronym = {{FoSSaCS}'12},
booktitle = {{P}roceedings of the 15th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'12)},
author = {Bollig, Benedikt and Cyriac, Aiswarya and Gastin, Paul and
Narayan Kumar, K.},
title = {Model Checking Languages of Data Words},
pages = {391-405},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGK-fossacs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGK-fossacs12.pdf},
doi = {10.1007/978-3-642-28729-9_26},
abstract = {We consider the model-checking problem for data multi-pushdown
automata (DMPA). DMPA generate data words, i.e, strings enriched with
values from an infinite domain. The latter can be used to represent an
unbounded number of process identifiers so that DMPA are suitable to model
concurrent programs with dynamic process creation. To specify properties
of data words, we use monadic second-order (MSO) logic, which comes with a
predicate to test two word positions for data equality. While
satisfiability for MSO logic is undecidable (even for weaker fragments
such as first-order logic), our main result states that one can decide if
all words generated by a DMPA satisfy a given formula from the full MSO
logic.}
}
@inproceedings{BCGZ-mfcs11,
address = {Warsaw, Poland},
month = aug,
year = 2011,
volume = 6907,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Murlak, Filip and Sankowski, Piotr},
acronym = {{MFCS}'11},
booktitle = {{P}roceedings of the 36th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'11)},
author = {Bollig, Benedikt and Cyriac, Aiswarya and Gastin, Paul and Zeitoun, Marc},
title = {Temporal Logics for Concurrent Recursive Programs: Satisfiability
and Model Checking},
pages = {132-144},
url = {http://hal.archives-ouvertes.fr/hal-00591139/en/},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGZ-mfcs11.pdf},
doi = {10.1007/978-3-642-22993-0_15},
abstract = {We develop a general framework for the design of temporal logics
for concurrent recursive programs. A program execution is modeled as a
partial order with multiple nesting relations. To specify properties of
executions, we consider any temporal logic whose modalities are definable
in monadic second-order logic and that, in addition, allows PDL-like path
expressions. This captures, in a unifying framework, a wide range of
logics defined for trees, nested words, and Mazurkiewicz traces that have
been studied separately. We show that satisfiability and model checking
are decidable in EXPTIME and 2EXPTIME, depending on the precise path
modalities.}
}
@inproceedings{Bol-concur11,
address = {Aachen, Germany},
month = sep,
year = 2011,
volume = 6901,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Katoen, Joost-Pieter and K{\"o}nig, Barbara},
acronym = {{CONCUR}'11},
booktitle = {{P}roceedings of the 22nd
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'11)},
author = {Bollig, Benedikt},
title = {An automaton over data words that captures {EMSO} logic},
pages = {171-186},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/B-concur11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/B-concur11.pdf},
doi = {10.1007/978-3-642-23217-6_12},
abstract = {We develop a general framework for the specification and
implementation of systems whose executions are words, or partial orders,
over an infinite alphabet. As a model of an implementation, we introduce
class register automata, a one-way automata model over words with multiple
data values. Our model combines register automata and class memory
automata. It has natural interpretations. In particular, it captures
communicating automata with an unbounded number of processes, whose
semantics can be described as a set of (dynamic) message sequence charts.
On the specification side, we provide a local existential monadic
second-order logic that does not impose any restriction on the number of
variables. We study the realizability problem and show that every formula
from that logic can be effectively, and in elementary time, translated
into an equivalent class register automaton.}
}
@techreport{rr-lsv-11-08,
author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin and
Zeitoun, Marc},
title = {Weighted Expressions and {DFS} Tree Automata},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2011},
month = apr,
type = {Research Report},
number = {LSV-11-08},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-08.pdf},
note = {32~pages},
abstract = {We introduce weighted expressions, a~calculus to express
quantitative properties over unranked trees. They involve products and
sums from a semiring as well as classical boolean formulas. We~show that
weighted expressions are expressively equivalent to a new class of
weighted tree-walking automata. This new automata model is equipped with
pebbles, and follows a depth-first-search policy in the tree.}
}
@inproceedings{BKKL-ceeset2008,
address = {Brno, Czech Republic},
year = 2011,
volume = {4980},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Huzar, Zbigniew and Koc{\'\i}, Radek and Meyer, Bertrand and
Walter, Bartosz and Zendulka, Jaroslav},
acronym = {{CEE-SET}'08},
booktitle = {{R}evised {S}elected {P}apars of the 3rd {IFIP} {TC2} {C}entral and
{E}ast {E}uropean {C}onference on {S}oftware {E}ngineering
{T}echniques ({CEE-SET}'08)},
author = {Bollig, Benedikt and Katoen, Joost-Pieter and Kern,
Carsten and Leucker, Martin},
title = {{SMA}---The {S}myle Modeling Approach},
pages = {103-117},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-ceeset2008.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-ceeset2008.pdf},
doi = {10.1007/978-3-642-22386-0_8},
abstract = {This paper introduces the model-based software development
methodology SMA---the Smyle Modeling Approach---which is centered around
Smyle, a dedicated learning procedure to support engineers to
interactively obtain design models from requirements, characterized as
either being desired (positive) or unwanted (negative) system behavior.
The learning approach is complemented by scenario patterns where the
engineer can specify clearly desired or unwanted behavior. This~way, user
interaction is reduced to the interesting scenarios limiting the design
effort considerably. In~SMA, the learning phase is complemented by an
effective analysis phase that allows for detecting design flaws at an
early design stage. This paper describes the approach and reports on first
practical experiences.}
}
@article{ABG-fmsd12,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Akshay, S. and Bollig, Benedikt and Gastin, Paul},
title = {Event-clock Message Passing Automata: A~Logical
Characterization and an Emptiness-Checking Algorithm},
year = 2013,
month = jun,
volume = 42,
number = {3},
pages = {262-300},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-fmsd12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-fmsd12.pdf},
doi = {10.1007/s10703-012-0179-8},
abstract = {We are interested in modeling behaviors and verifying
properties of systems in which time and concurrency play a crucial
role. We introduce a model of distributed automata which are
equipped with event clocks as in [Alur, Fix,
Henzinger. Event-clock automata: A~determinizable class of timed
automata. TCS 211(1-2):253-273, 1999.], which we call Event Clock
Message Passing Automata (ECMPA). To describe the behaviors of
such systems we use timed partial orders (modeled as message
sequence charts with timing).\par
Our first goal is to extend the classical
B{\"u}chi-Elgot-Trakhtenbrot equivalence to the timed and
distributed setting, by showing an equivalence between ECMPA and a
timed extension of monadic second-order (MSO) logic. We obtain
such a constructive equivalence in two different ways:
(1)~by~restricting the semantics by bounding the set of timed
partial orders (2)~by~restricting the timed MSO logic to its
existential fragment. We next consider the emptiness problem for
ECMPA, which asks if a given ECMPA has some valid timed
execution. In general this problem is undecidable and we show that
by considering only bounded timed executions, we can obtain
decidability. We do this by constructing a timed automaton which
accepts all bounded timed executions of the ECMPA and checking
emptiness of this timed automaton.}
}
@inproceedings{BGMZ-atva12,
address = {Thiruvananthapuram, India},
month = oct,
year = {2012},
volume = {7561},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Mukund, Madhavan and Chakraborty, Supratik},
acronym = {{ATVA}'12},
booktitle = {{P}roceedings of the 10th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'12)},
author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin and
Zeitoun, Marc},
title = {A Probabilistic {K}leene Theorem},
pages = {400-415},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-atva12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-atva12.pdf},
doi = {10.1007/978-3-642-33386-6_31},
abstract = {We provide a Kleene Theorem for (Rabin) probabilistic automata
over finite words. Probabilistic automata generalize deterministic finite
automata and assign to a word an acceptance probability. We provide
probabilistic expressions with probabilistic choice, guarded choice,
concatenation, and a star operator. We prove that probabilistic
expressions and probabilistic automata are expressively equivalent. Our
result actually extends to two-way probabilistic automata with pebbles and
corresponding expressions.}
}
@inproceedings{BDL-tase12,
address = {Beijing, China},
month = jul,
year = 2012,
publisher = {{IEEE} Computer Society Press},
noeditor = {},
acronym = {{TASE}'12},
booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium
on {T}heoretical {A}spects of {S}oftware {E}ngineering
({TASE}'12)},
author = {Bollig, Benedikt and Decker, Normann and Leucker, Martin},
title = {Frequency Linear-time Temporal Logic},
pages = {85-92},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDL-tase12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDL-tase12.pdf},
doi = {10.1109/TASE.2012.43},
abstract = {We propose fLTL, an extension to linear-time temporal logic
(LTL) that allows for expressing relative frequencies by a generalization
of temporal operators. This facilitates the specification of requirements
such as the deadlines in a real-time system must be met in at least~\(95\%\)
of all cases. For our novel logic, we establish an undecidability result
regarding the satisfiability problem but identify a decidable fragment
which strictly increases the expressiveness of LTL by allowing, e.g., to
express non-context-free properties.}
}
@article{BK-jal12,
publisher = {Elsevier Science Publishers},
journal = {Journal of Applied Logic},
author = {Bollig, Benedikt and Kuske, Dietrich},
title = {An optimal construction of {H}anf sentences},
year = {2012},
month = jun,
volume = {10},
number = {2},
pages = {179-186},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BK-jal12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BK-jal12.pdf},
doi = {10.1016/j.jal.2012.01.002},
abstract = {We give a new construction of formulas in Hanf normal form that
are equivalent to first-order formulas over structures of bounded degree.
This is the first algorithm whose running time is shown to be elementary.
The triply exponential upper bound is complemented by a matching lower
bound.}
}
@inproceedings{BKM-lics13,
address = {New-Orleans, Louisiana, USA},
month = jun,
year = 2013,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'13},
booktitle = {{P}roceedings of the 28th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'13)},
author = {Bollig, Benedikt and Kuske, Dietrich and Mennicke, Roy},
title = {The Complexity of Model Checking Multi-Stack Systems},
pages = {163-170},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BKM-lics13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BKM-lics13.pdf},
doi = {10.1109/LICS.2013.22},
abstract = {We consider the linear-time model-checking problem for boolean
concurrent programs with recursive procedure calls. While sequential
recursive programs are usually modeled as pushdown automata, concurrent
recursive programs involve several processes and can be naturally
abstracted as pushdown automata with multiple stacks. Their behavior can
be understood as words with multiple nesting relations, each relation
connecting a procedure call with its corresponding return. To reason about
multiply nested words, we consider the class of all temporal logics as
defined in the book by Gabbay, Hodkinson, and Reynolds~(1994). The
unifying feature of these temporal logics is that their modalities are
defined in monadic second-order~(MSO) logic. In particular, this captures
numerous temporal logics over concurrent and/or recursive programs that
have been defined so far. Since the general model checking problem is
undecidable, we restrict attention to phase bounded executions as proposed
by La~Torre, Madhusudan, and Parlato (LICS~2007). While the MSO model
checking problem in this case is non-elementary, our main result states
that the model checking (and satisfiability) problem for all MSO-definable
temporal logics is decidable in elementary time. More precisely, it is
solvable in \((n+2)\)-EXPTIME where \(n\) is the maximal level of the MSO
modalities in the monadic quantifier alternation hierarchy. We complement
this result and provide, for each level~\(n\), a~temporal logic whose
model checking problem is \(n\)-EXPSPACE-hard.}
}
@inproceedings{BHLM-dlt13,
address = {Marne-la-Vall{\'e}e, France},
month = jun,
year = 2013,
volume = {7907},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {B{\'e}al, Marie-Pierre and Carton, Olivier},
acronym = {{DLT}'13},
booktitle = {{P}roceedings of the 17th {I}nternational
{C}onference on {D}evelopments in {L}anguage {T}heory
({DLT}'13)},
author = {Bollig, Benedikt and Habermehl, Peter and Leucker, Martin and
Monmege, Benjamin},
title = {A~Fresh Approach to Learning Register Automata},
pages = {118-130},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHLM-dlt13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHLM-dlt13.pdf},
doi = {10.1007/978-3-642-38771-5_12},
abstract = {This paper provides an Angluin-style learning algorithm for a
class of register automata supporting the notion of \emph{fresh} data values.
More specifically, we introduce \emph{session automata} which are well suited for
modeling protocols in which sessions using fresh values are of major
interest, like in security protocols or ad-hoc networks. We show that
session automata (i)~have an expressiveness partly extending, partly
reducing that of register automata, (ii)~admit a symbolic regular
representation, and (iii)~have a decidable equivalence and model-checking
problem (unlike register automata). Using these results, we establish a
learning algorithm to infer session automata through membership and
equivalence queries. Finally, we strengthen the robustness of our
automaton by its characterization in monadic second-order logic.}
}
@inproceedings{BCHKS-lata13,
address = {Bilbao, Spain},
month = apr,
year = 2013,
volume = {7810},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Dediu, Adrian Horia and Mart{\'\i}n-Vide, Carlos and Truthe, Bianca},
acronym = {{LATA}'13},
booktitle = {{P}roceedings of the 7th {I}nternational {C}onference on {L}anguage
and {A}utomata {T}heory and {A}pplications ({LATA}'13)},
author = {Bollig, Benedikt and Cyriac, Aiswarya and H{\'e}lou{\"e}t,
Lo{\"\i}c and Kara, Ahmet and Schwentick, {\relax Th}omas},
title = {Dynamic Communicating Automata and Branching High-Level {MSC}s},
pages = {177-189},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHKS-lata13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHKS-lata13.pdf},
doi = {10.1109/REVET.2012.6195253},
abstract = {We study dynamic communicating automata~(DCA), an~extension of
classical communicating finite-state machines that allows for dynamic
creation of processes. The behavior of a DCA can be described as a set of
message sequence charts~(MSCs). While DCA serve as a model of an
implementation, we propose branching high-level MSCs~(bHMSCs) on the
specification side. Our focus is on the implementability problem: given a
bHMSC, can one construct an equivalent DCA? As this problem is
undecidable, we introduce the notion of executability, a decidable
necessary criterion for implementability. We show that executability of
bHMSCs is EXPTIME-complete. We~then identify a class of bHMSCs for which
executability effectively implies implementability.}
}
@inproceedings{BGM-fossacs13,
address = {Rome, Italy},
month = mar,
year = 2013,
volume = {7794},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Pfenning, Frank},
acronym = {{FoSSaCS}'13},
booktitle = {{P}roceedings of the 16th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'13)},
author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin},
title = {Weighted Specifications over Nested Words},
pages = {385-400},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-fossacs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-fossacs13.pdf},
doi = {10.1007/978-3-642-37075-5_25},
abstract = {This paper studies several formalisms to specify quantitative
properties of finite nested words (or~equivalently finite unranked trees).
These can be used for XML documents or recursive programs: for~instance,
counting how often a given entry occurs in an XML document, or~computing
the memory required for a recursive program execution. Our main interest
is to translate these properties, as efficiently as possible, into an
automaton, and to use this computational device to decide problems related
to the properties (e.g.,~emptiness, model checking, simulation) or to
compute the value of a quantitative specification over a given nested
word. The specification formalisms are weighted regular expressions (with
forward and backward moves following linear edges or call-return edges),
weighted first-order logic, and weighted temporal logics. We~introduce
weighted automata walking in nested words, possibly dropping\slash lifting
(reusable) pebbles during the traversal. We prove that the evaluation
problem for such automata can be done very efficiently if the number of
pebble names is small, and we also consider the emptiness problem.}
}
@article{BHLM-lmcs14,
journal = {Logical Methods in Computer Science},
author = {Bollig, Benedikt and Habermehl, Peter and Leucker, Martin
and Monmege, Benjamin},
title = {A~Robust Class of Data Languages and an Application to Learning},
year = {2014},
month = dec,
volume = 10,
number = {4:19},
nopages = {},
url = {http://arxiv.org/abs/1411.6646},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHLM-lmcs14.pdf},
doi = {10.2168/LMCS-10(4:19)2014},
abstract = {We~introduce session automata, an automata model to process data
words, i.e., words over an infinite alphabet. Session automata support the
notion of fresh data values, which are well suited for modeling protocols
in which sessions using fresh values are of major interest, like in
security protocols or ad-hoc networks. Session automata have an
expressiveness partly extending, partly reducing that of classical
register automata. We~show that, unlike register automata and their
various extensions, session automata are robust: They (i)~are closed under
intersection, union, and (resource-sensitive) complementation, (ii)~admit
a symbolic regular representation, (iii)~have a decidable inclusion
problem (unlike register automata), and (iv)~enjoy logical
characterizations. Using these results, we establish a learning algorithm
to infer session automata through membership and equivalence queries.}
}
@inproceedings{BGK-fsttcs14,
address = {New~Dehli, India},
month = dec,
year = 2014,
volume = {29},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Raman, Venkatesh and Suresh, S.~P.},
acronym = {{FSTTCS}'14},
booktitle = {{P}roceedings of the 34th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'14)},
author = {Bollig, Benedikt and Gastin, Paul and Kumar, Akshay},
title = {Parameterized Communicating Automata: Complementation and
Model Checking},
pages = {625-637},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGK-fsttcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGK-fsttcs14.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2014.625},
abstract = {We study the language-theoretical aspects of parameterized
communicating automata (PCAs), in which processes communicate via
rendez-vous. A given PCA can be run on any topology of bounded degree such
as pipelines, rings, ranked trees, and grids. We show that, under a
context bound, which restricts the local behavior of each process, PCAs
are effectively complementable. Complementability is considered a key
aspect of robust automata models and can, in particular, be exploited for
verification. In this paper, we use it to obtain a characterization of
context-bounded PCAs in terms of monadic second-order (MSO) logic. As the
emptiness problem for context-bounded PCAs is decidable for the classes of
pipelines, rings, and trees, their model-checking problem wrt. MSO
properties also becomes decidable. While previous work on model checking
parameterized systems typically uses temporal logics without next
operator, our MSO logic allows one to express several natural next
modalities.}
}
@article{BCGZ-jal14,
publisher = {Elsevier Science Publishers},
journal = {Journal of Applied Logic},
author = {Bollig, Benedikt and Cyriac, Aiswarya and Gastin, Paul and
Zeitoun, Marc},
title = {Temporal logics for concurrent recursive programs:
Satisfiability and model checking},
volume = 12,
number = 4,
pages = {395-416},
month = dec,
year = 2014,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGZ-jal14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGZ-jal14.pdf},
doi = {10.1016/j.jal.2014.05.001},
abstract = {We develop a general framework for the design of temporal logics
for concurrent recursive programs. A program execution is modeled as a
partial order with multiple nesting relations. To specify properties of
executions, we consider any temporal logic whose modalities are definable
in monadic second-order logic and which, in addition, allows PDL-like path
expressions. This captures, in a unifying framework, a wide range of
logics defined for ranked and unranked trees, nested words, and
Mazurkiewicz traces that have been studied separately. We show that
satisfiability and model checking are decidable in EXPTIME and 2EXPTIME,
depending on the precise path modalities.}
}
@inproceedings{BGS-rp14,
address = {Oxford, UK},
month = sep,
year = 2014,
volume = {8762},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell, James},
acronym = {{RP}'14},
booktitle = {{P}roceedings of the 8th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'14)},
author = {Bollig, Benedikt and Gastin, Paul and Schubert, Jana},
title = {Parameterized Verification of Communicating Automata under Context Bounds},
pages = {45-57},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGS-rp14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGS-rp14.pdf},
doi = {10.1007/978-3-319-11439-2_4},
abstract = {We study the verification problem for parameterized
communicating automata~(PCA), in which processes synchronize via message
passing. A~given PCA can be run on any topology of bounded degree (such as
pipelines, rings, or ranked trees), and communication may take place
between any two processes that are adjacent in the topology. Parameterized
verification asks if there is a topology from a given topology class that
allows for an accepting run of the given PCA. In general, this problem is
undecidable even for synchronous communication and simple pipeline
topologies. We therefore consider context-bounded verification, which
restricts the behavior of each single process. For several variants of
context bounds, we show that parameterized verification over pipelines,
rings, and ranked trees is decidable. Our approach is automata-theoretic
and uniform. We introduce a notion of graph acceptor that identifies those
topologies allowing for an accepting run. Depending on the given topology
class, the topology acceptor can then be restricted, or adjusted, so that
the verification problem reduces to checking emptiness of finite automata
or tree automata.}
}
@inproceedings{BGMZ-csllics14,
address = {Vienna, Austria},
month = jul,
year = 2014,
publisher = {ACM Press},
acronym = {{CSL\slash LICS}'14},
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)},
author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin and
Zeitoun, Marc},
title = {Logical Characterization of Weighted Pebble Walking Automata},
nopages = {},
chapter = 19,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-csllics14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-csllics14.pdf},
doi = {10.1145/2603088.2603118},
abstract = {Weighted automata are a conservative quantitative extension of
finite automata that enjoys applications, e.g., in language processing and
speech recognition. Their expressive power, however, appears to be
limited, especially when they are applied to more general structures than
words, such as graphs. To address this drawback, weighted automata have
recently been generalized to weighted pebble walking automata, which
proved useful as a tool for the specification and evaluation of
quantitative properties over words and nested words. In this paper, we
establish the expressive power of weighted pebble walking automata in
terms of transitive closure logic, lifting a similar result by Engelfriet
and Hoogeboom from the Boolean case to a quantitative setting. This result
applies to general classes of graphs, including all the aforementioned
classes.}
}
@inproceedings{BB-csllics14,
address = {Vienna, Austria},
month = jul,
year = 2014,
publisher = {ACM Press},
acronym = {{CSL\slash LICS}'14},
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)},
author = {Bollig, Benedikt},
title = {Logic for Communicating Automata with Parameterized Topology},
nopages = {},
chapter = 18,
exturl = {http://hal.inria.fr/hal-00872807/},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BB-csllics14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BB-csllics14.pdf},
doi = {10.1145/2603088.2603093},
abstract = {We introduce parameterized communicating automata~(PCA) as a
model of systems where finite-state processes communicate through FIFO
channels. Unlike classical communicating automata, a given PCA can be run
on any network topology of bounded degree. The topology is thus a
parameter of the system. We provide various B{\"u}chi-Elgot-Trakhtenbrot
theorems for~PCA, which roughly read as follows: Given a logical
specification~\(\phi\) and a class of topologies~\(T\), there is a~PCA that is
equivalent to~\(\phi\) on all topologies from~\(T\). We~give uniform constructions
which allow us to instantiate~\(T\) with concrete classes such as pipelines,
ranked trees, grids, rings,~etc. The proofs build on a locality theorem
for first-order logic due to Schwentick and Barthelmann, and they exploit
concepts from the non-parameterized case, notably a result by Genest,
Kuske, and Muscholl.}
}
@article{ABGMN-fi13,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {Akshay, S. and Bollig, Benedikt and Gastin, Paul and
Mukund, Madhavan and Narayan Kumar, K.},
title = {Distributed Timed Automata with Independently Evolving Clocks},
volume = {130},
number = {4},
month = apr,
year = 2014,
pages = {377-407},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGMN-fi13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGMN-fi13.pdf},
doi = {10.3233/FI-2014-996},
abstract = {We propose a model of distributed timed systems where each
component is a timed automaton with a set of local clocks that evolve at a
rate independent of the clocks of the other components. A~clock can be
read by any component in the system, but it can only be reset by the
automaton it belongs~to.\par
There are two natural semantics for such systems. The \emph{universal}
semantics captures behaviors that hold under any choice of clock rates for
the individual components. This is a natural choice when checking that a
system always satisfies a positive specification. To check if a system
avoids a negative specification, it is better to use the
\emph{existential} semantics—the set of behaviors that the system
can possibly exhibit under some choice of clock rates.\par
We show that the existential semantics always describes a regular set of
behaviors. However, in the case of universal semantics, checking emptiness
or universality turns out to be undecidable. As an alternative to the
universal semantics, we propose a \emph{reactive} semantics that allows us
to check positive specifications and yet describes a regular set of
behaviors.}
}
@article{BGMZ-tocl13,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin and Zeitoun, Marc},
title = {Pebble Weighted Automata and Weighted Logics},
volume = 15,
number = {2:15},
month = apr,
year = 2014,
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-tocl13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-tocl13.pdf},
doi = {10.1145/2579819},
abstract = {We introduce new classes of weighted automata on words. Equipped
with pebbles, they go beyond the class of recognizable formal power
series: they capture weighted first-order logic enriched with a
quantitative version of transitive closure. In contrast to previous work,
this calculus allows for unrestricted use of existential and universal
quantifications over positions of the input word. We actually consider
both two-way and one-way pebble weighted automata. The latter class
constrains the head of the automaton to walk left-to-right, resetting it
each time a pebble is dropped. Such automata have already been considered
in the Boolean setting, in the context of data words. Our main result
states that two-way pebble weighted automata, one-way pebble weighted
automata, and our weighted logic are expressively equivalent. We also give
new logical characterizations of standard recognizable series.}
}
@inproceedings{B-time15,
address = {Kassel, Germany},
month = sep,
year = 2015,
publisher = {{IEEE} Computer Society Press},
editor = {Grandi, Fabio and Lange, Martin and Lomuscio, Alessio},
acronym = {{TIME}'15},
booktitle = {{P}roceedings of the 22nd {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'15)},
author = {Bollig, Benedikt},
title = {Towards Formal Verification of Distributed Algorithms},
pages = {3},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/B-time15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/B-time15.pdf},
doi = {10.1109/TIME.2015.23}
}
@inproceedings{B-ciaa15,
address = {Ume{\aa}, Sweden},
month = aug,
year = 2015,
volume = {9223},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Drewes, Frank},
acronym = {{CIAA}'15},
booktitle = {{P}roceedings of the 20th {I}nternational
{C}onference on {I}mplementation and
{A}pplication of {A}utomata
({CIAA}'15)},
author = {Bollig, Benedikt},
title = {Automata and Logics for Concurrent Systems: Five Models in Five
Pages},
pages = {3-12},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/B-ciaa15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/B-ciaa15.pdf},
doi = {10.1007/978-3-319-22360-5_1},
abstract = {We~survey various automata models of concurrent systems and
their connection with monadic second-order logic: finite automata, class
memory automata, nested-word automata, asynchronous automata, and
message-passing automata.}
}
@inproceedings{ABG-concur15,
address = {Madrid, Spain},
month = sep,
year = 2015,
volume = {42},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Aceto, Luca and de Frutos-Escrig, David},
acronym = {{CONCUR}'15},
booktitle = {{P}roceedings of the 26th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'15)},
author = {Aiswarya, C. and Bollig, Benedikt and Gastin, Paul},
title = {An Automata-Theoretic Approach to the Verification of Distributed Algorithms},
pages = {340-353},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-concur15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-concur15.pdf},
doi = {10.4230/LIPIcs.CONCUR.2015.340},
abstract = {We introduce an automata-theoretic method for the verification
of distributed algorithms running on ring networks. In a distributed
algorithm, an arbitrary number of processes cooperate to achieve a common
goal (e.g., elect a leader). Processes have unique identifiers (pids) from
an infinite, totally ordered domain. An algorithm proceeds in synchronous
rounds, each round allowing a process to perform a bounded sequence of
actions such as send or receive a pid, store it in some register, and
compare register contents wrt. the associated total order. An algorithm is
supposed to be correct independently of the number of processes. To
specify correctness properties, we introduce a logic that can reason about
processes and pids. Referring to leader election, it may say that, at the
end of an execution, each process stores the maximum pid in some dedicated
register. Since the verification of distributed algorithms is undecidable,
we propose an underapproximation technique, which bounds the number of
rounds. This is an appealing approach, as the number of rounds needed by a
distributed algorithm to conclude is often exponentially smaller than the
number of processes. We provide an automata-theoretic solution, reducing
model checking to emptiness for alternating two-way automata on words.
Overall, we show that round-bounded verification of distributed algorithms
over rings is PSPACE-complete.}
}
@phdthesis{bollig-HDR15,
author = {Bollig, Benedikt},
title = {Automata and Logics for Concurrent Systems: Realizability and Verification},
year = 2015,
month = jun,
type = {M{\'e}moire d'habilitation},
school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-bollig15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-bollig15.pdf}
}
@article{BKM-tocs17,
publisher = {Springer},
journal = {Theory of Computing Systems},
author = {Bollig, Benedikt and
Kuske, Dietrich and
Mennicke, Roy},
title = {The Complexity of Model Checking Multi-Stack Systems},
volume = {60},
number = {4},
pages = {695-736},
year = {2017},
url = {http://link.springer.com/article/10.1007/s00224-016-9700-6?wt_mc=Internal.Event.1.SEM.ArticleAuthorOnlineFirst},
doi = {10.1007/s00224-016-9700-6},
abstract = {We study the linear-time model checking problem for boolean concurrent programs with recursive procedure calls. While sequential recursive programs are usually modeled as pushdown automata, concurrent recursive programs involve several processes and can be naturally abstracted as pushdown automata with multiple stacks. Their behavior can be understood as words with multiple nesting relations, each relation connecting a procedure call with its corresponding return. To reason about multiply nested words, we consider the class of all temporal logics as defined in the book by Gabbay, Hodkinson, and Reynolds. The unifying feature of these temporal logics is that their modalities are defined in monadic second-order (MSO) logic. In particular, this captures numerous temporal logics over concurrent and/or recursive programs that have been defined so far. Since the general model checking problem is undecidable, we restrict attention to phase bounded executions as proposed by La Torre, Madhusudan, and Parlato. While the MSO model checking problem in this case is non-elementary, our main result states that the model checking (and satisfiability) problem for all MSO-definable temporal logics is decidable in elementary time. More precisely, it is solvable in time exponential in the formula and (n+2)-fold exponential in the number of phases where n is the maximal level of the MSO modalities in the monadic quantifier alternation hierarchy (which is a vast improvement over the conference version of this paper from LICS 2013 where the space was also (n+2)-fold exponential in the size of the temporal formula). We complement this result and provide, for each level n, a temporal logic whose model checking problem is n-EXPSPACE-hard.}
}
@inproceedings{Bollig-fsttcs16,
address = {Chennai, India},
month = dec,
year = 2016,
volume = {65},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {S. Akshay and Akash Lal and Saket Saurabh and Sandeep Sen},
acronym = {{FSTTCS}'16},
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)},
author = {Bollig, Benedikt},
title = {One-Counter Automata with Counter Observability},
pages = {20:1-20:14},
url = {http://drops.dagstuhl.de/opus/volltexte/2016/6855/},
doi = {10.4230/LIPIcs.FSTTCS.2016.20},
abstract = {In a one-counter automaton (OCA), one can produce a letter from some finite alphabet, increment and decrement the counter by one, or compare it with constants up to some threshold. It is well-known that universality and language inclusion for OCAs are undecidable. In this paper, we consider OCAs with counter observability: Whenever the automaton produces a letter, it outputs the current counter value along with it. Hence, its language is now a set of words over an infinite alphabet. We show that universality and inclusion for that model are PSPACE-complete, thus no harder than the corresponding problems for finite automata. In fact, by establishing a link with visibly one-counter automata, we show that OCAs with counter observability are effectively determinizable and closed under all boolean operations. Moreover, it turns out that they are expressively equivalent to strong automata, in which transitions are guarded by MSO formulas over the natural numbers with successor.}
}
@comment{{B-arxiv16,
author = Bollig, Benedikt,
affiliation = aff-LSVmexico,
title = One-Counter Automata with Counter Visibility,
institution = Computing Research Repository,
number = 1602.05940,
month = feb,
nmonth = 2,
year = 2016,
type = RR,
axeLSV = mexico,
NOcontrat = "",
url = http://arxiv.org/abs/1602.05940,
PDF = "http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf",
lsvdate-new = 20160222,
lsvdate-upd = 20160222,
lsvdate-pub = 20160222,
lsv-category = "rapl",
wwwpublic = "public and ccsb",
note = 18~pages,
abstract = "In a one-counter automaton (OCA), one can read a letter
from some finite alphabet, increment and decrement the counter by
one, or test it for zero. It is well-known that universality and
language inclusion for OCAs are undecidable. We consider here OCAs
with counter visibility: Whenever the automaton produces a letter,
it outputs the current counter value along with~it. Hence, its
language is now a set of words over an infinite alphabet. We show
that universality and inclusion for that model are in PSPACE, thus
no harder than the corresponding problems for finite automata, which
can actually be considered as a special case. In fact, we show that
OCAs with counter visibility are effectively determinizable and
closed under all boolean operations. As~a~strict generalization, we
subsequently extend our model by registers. The general nonemptiness
problem being undecidable, we impose a bound on the number of
register comparisons and show that the corresponding nonemptiness
problem is NP-complete.",
}}
@inproceedings{BFG-stacs18,
address = {Caen, France},
month = feb,
volume = {96},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Niedermeier, Rolf and Vall{\'e}e, Brigitte},
acronym = {{STACS}'18},
booktitle = {{P}roceedings of the 35th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'18)},
author = {Bollig, Benedikt and Fortin, Marie and Gastin, Paul},
title = {Communicating Finite-State Machines and Two-Variable Logic},
pages = {17:1-17:14},
year = {2018},
doi = {10.4230/LIPIcs.STACS.2018.17},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/8529/pdf/LIPIcs-STACS-2018-17.pdf},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=8529},
abstract = {Communicating finite-state machines are a fundamental, well-studied model of finite-state processes that communicate via unbounded first-in first-out channels. We show that they are expressively equivalent to existential MSO logic with two first-order variables and the order relation.}
}
@inproceedings{BQS-concur17,
address = {Berlin, Germany},
month = sep,
year = 2017,
volume = {85},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Meyer, Roland and Nestmann, Uwe},
acronym = {{CONCUR}'17},
booktitle = {{P}roceedings of the 28th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'17)},
author = {Bollig, Benedikt and Quaas, Karin and Sangnier, Arnaud},
title = {The Complexity of Flat Freeze LTL},
pages = {33:1--33:16},
url = {http://drops.dagstuhl.de/opus/volltexte/2017/7799},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7799/pdf/LIPIcs-CONCUR-2017-33.pdf},
doi = {10.4230/LIPIcs.CONCUR.2017.33},
abstract = {We consider the model-checking problem for freeze LTL on one-counter automata (OCAs). Freeze LTL extends LTL with the freeze quantifier, which allows one to store different counter values of a run in registers so that they can be compared with one another. As the model-checking problem is undecidable in general, we focus on the flat fragment of freeze LTL, in which the usage of the freeze quantifier is restricted. Recently, Lechner et al. showed that model checking for flat freeze LTL on OCAs with binary encoding of counter updates is decidable and in 2NEXPTIME. In this paper, we prove that the problem is, in fact, NEXPTIME-complete no matter whether counter updates are encoded in unary or binary. Like Lechner et al., we rely on a reduction to the reachability problem in OCAs with parameterized tests (OCAPs). The new aspect is that we simulate OCAPs by alternating two-way automata over words. This implies an exponential upper bound on the parameter values that we exploit towards an NP algorithm for reachability in OCAPs with unary updates. We obtain our main result as a corollary.}
}
@article{BGH-fmsd17,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Bollig, Benedikt and Grindei, Manuela-Lidia and Habermehl, Peter},
title = {Realizability of Concurrent Recursive Programs},
volume = {53},
number = {3},
year = {2018},
pages = {339-362},
doi = {10.1007/s10703-017-0282-y},
abstract = {We study the realizability problem for concurrent recursive programs: Given a distributed system architecture and a sequential specification over words, find a distributed automata implementation that is equivalent to the specification. This problem is well-studied as far as finite-state processes are concerned, and it has a solution in terms of Zielonka's Theorem. We lift Zielonka's Theorem to the case where processes are recursive and modeled as visibly pushdown (or, equivalently, nested-word) automata. However, contrarily to the finite-state case, it is undecidable whether a specification is realizable or not. Therefore, we also consider suitable underapproximation techniques from the literature developed for multi-pushdown systems, and we show that they lead to a realizability framework with effective algorithms.
}
}
@article{ABG-ic17,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Aiswarya, C. and Bollig, Benedikt and Gastin, Paul},
title = {An Automata-Theoretic Approach to the Verification of Distributed Algorithms},
volume = {259},
month = apr,
year = {2018},
pages = {305-327},
doi = {10.1016/j.ic.2017.05.006},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-ic17.pdf},
abstract = {We introduce an automata-theoretic method for the verification of distributed algorithms running on ring networks. In a distributed algorithm, an arbitrary number of processes cooperate to achieve a common goal (e.g., elect a leader). Processes have unique identifiers (pids) from an infinite, totally ordered domain. An algorithm proceeds in synchronous rounds, each round allowing a process to perform a bounded sequence of actions such as send or receive a pid, store it in some register, and compare register contents wrt. the associated total order. An algorithm is supposed to be correct independently of the number of processes. To specify correctness properties, we introduce a logic that can reason about processes and pids. Referring to leader election, it may say that, at the end of an execution, each process stores the maximum pid in some dedicated register.
We show that the verification problem of distributed algorithms can be reduced to satisfiability of a formula from propositional dynamic logic with loop and converse (LCPDL), interpreted over grids over a finite alphabet. This translation is independent of any restriction imposed on the algorithm. However, since the verification problem (and satisfiability for LCPDL) is undecidable, we propose an underapproximation technique, which bounds the number of rounds. This is an appealing approach, as the number of rounds needed by a distributed algorithm to conclude is often exponentially smaller than the number of processes. Using our reduction to LCPDL, we provide an automata-theoretic solution, reducing model checking to emptiness for alternating two-way automata on words. Overall, we show that round-bounded verification of distributed algorithms over rings is PSPACE-complete, provided the number of rounds is given in unary.}
}
@article{ABH-ijfcs17,
publisher = {World Scientific},
journal = {International Journal of Foundations of Computer Science},
author = {Atig, Mohamed Faouzi and Bollig, Benedikt and Habermehl, Peter},
title = {Emptiness of ordered multi-pushdown automata is {2ETIME}-complete},
volume = {28},
number = {8},
year = {2017},
pages = {945-975},
doi = {10.1142/S0129054117500332},
url = {http://www.worldscientific.com/doi/abs/10.1142/S0129054117500332},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABH-ijfcs17.pdf},
abstract = {We consider ordered multi-pushdown automata, a multi-stack extension
of pushdown automata that comes with a constraint on stack operations: a pop
can only be performed on the first non-empty stack (which implies that we
assume a linear ordering on the collection of stacks). We show that the
emptiness problem for multi-pushdown automata is 2ETIME-complete.
Containment in 2ETIME is shown by translating an automaton
into a grammar for which we can check if the generated language is empty.
The lower bound is established by simulating the behavior of an alternating
Turing machine working in exponential space. We also compare ordered
multi-pushdown automata with the model of bounded-phase (visibly)
multi-stack pushdown automata, which do not impose an ordering on stacks,
but restrict the number of alternations of pop operations on different
stacks.}
}
@inproceedings{BLS-atva18,
address = {Los Angeles, California, USA},
month = oct,
year = {2018},
volume = {11138},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Shuvendu Lahiri and Chao Wang},
acronym = {{ATVA}'18},
booktitle = {{P}roceedings of the 16th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'18)},
author = {Benedikt Bollig and Mathieu Lehaut and Nathalie Sznajder},
title = {Round-Bounded Control of Parameterized Systems},
pages = {370-386},
url = {https://hal.archives-ouvertes.fr/hal-01849206},
doi = {10.1007/978-3-030-01090-4_22},
abstract = {We consider systems with unboundedly many processes that communicate through shared memory. In that context, simple verification questions have a high complexity or, in the case of pushdown processes, are even undecidable. Good algorithmic properties are recovered under round-bounded verification, which restricts the system behavior to a bounded number of round-robin schedules. In this paper, we extend this approach to a game-based setting. This allows one to solve synthesis and control problems and constitutes a further step towards a theory of languages over infinite alphabets.}
}
@inproceedings{BFG-concur18,
address = {Beijing, China},
month = sep,
year = 2018,
volume = {118},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Schewe, Sven and Zhang, Lijun},
acronym = {{CONCUR}'18},
booktitle = {{P}roceedings of the 29th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'18)},
author = {Bollig, Benedikt and Fortin, Marie and Gastin, Paul},
title = {It Is Easy to Be Wise After the Event: Communicating Finite-State
Machines Capture First-Order Logic with ''Happened Before''},
pages = {7:1-7:17},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9545},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9545/pdf/LIPIcs-CONCUR-2018-7.pdf},
doi = {10.4230/LIPIcs.CONCUR.2018.7},
abstract = {Message sequence charts (MSCs) naturally arise as executions of communicating finite-state machines (CFMs), in which finite-state processes exchange messages through unbounded FIFO channels. We study the first-order logic of MSCs, featuring Lamport's happened-before relation. We introduce a star-free version of propositional dynamic logic (PDL) with loop and converse. Our main results state that (i) every first-order sentence can be transformed into an equivalent star-free PDL sentence (and conversely), and (ii) every star-free PDL sentence can be translated into an equivalent CFM. This answers an open question and settles the exact relation between CFMs and fragments of monadic second-order logic. As a byproduct, we show that first-order logic over MSCs has the three-variable property.}
}
@article{BQS-lmcs19,
journal = {Logical Methods in Computer Science},
author = {Bollig, Benedikt and Quaas, Karin and Sangnier, Arnaud},
title = {The Complexity of Flat Freeze LTL},
volume = {15},
number = {3},
pages = {32:1-32:26},
year = 2019,
doi = {10.23638/LMCS-15(3:32)2019},
pdf = {https://lmcs.episciences.org/5795/pdf},
url = {https://arxiv.org/abs/1609.06124},
abstract = {We consider the model-checking problem for freeze LTL on one-counter automata (OCA). Freeze LTL extends LTL with the freeze quantifier, which allows one to store different counter values of a run in registers so that they can be compared with one another. As the model-checking problem is undecidable in general, we focus on the flat fragment of freeze LTL, in which the usage of the freeze quantifier is restricted. In a previous work, Lechner et al. showed that model checking for flat freeze LTL on OCA with binary encoding of counter updates is decidable and in 2NEXPTIME. In this paper, we prove that the problem is, in fact, NEXPTIME-complete no matter whether counter updates are encoded in unary or binary. Like Lechner et al., we rely on a reduction to the reachability problem in OCA with parameterized tests (OCA(P)). The new aspect is that we simulate OCA(P) by alternating two-way automata over words. This implies an exponential upper bound on the parameter values that we exploit towards an NP algorithm for reachability in OCA(P) with unary updates. We obtain our main result as a corollary. As another application, relying on a reduction by Bundala and Ouaknine, one obtains an alternative proof of the known fact that reachability in closed parametric timed automata with one parametric clock is in NEXPTIME.}
}
@inproceedings{BBR-fossacs19,
address = {Prague, Czech Republic},
month = apr,
year = 2019,
volume = {11425},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Boja{\'n}czyk, Mikolaj and Simpson, Alex},
acronym = {{FoSSaCS}'19},
booktitle = {{P}roceedings of the 22nd {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'19)},
author = {Benedikt Bollig and Patricia Bouyer and Fabian Reiter},
title = {Identifiers in Registers - Describing Network Algorithms with Logic},
pages = {115-132},
url = {https://arxiv.org/abs/1811.08197},
pdf = {https://arxiv.org/pdf/1811.08197.pdf},
doi = {10.1007/978-3-030-17127-8},
abstract = {We propose a formal model of distributed computing based on register automata
that captures a broad class of synchronous network algorithms. The local memory
of each process is represented by a finite-state controller and a fixed number
of registers, each of which can store the unique identifier of some process in
the network. To underline the naturalness of our model, we show that it has the
same expressive power as a certain extension of first-order logic on graphs
whose nodes are equipped with a total order. Said extension lets us define new
functions on the set of nodes by means of a so-called partial fixpoint
operator. In spirit, our result bears close resemblance to a classical theorem
of descriptive complexity theory that characterizes the complexity class PSPACE
in terms of partial fixpoint logic (a proper superclass of the logic we
consider here).}
}
@techreport{KY-arxiv20,
author = {Khmelnitsky, Igor and
Neider, Daniel and
Roy, Rajarshi and
Barbot, Beno{\^{\i}}t and
Bollig, Benedikt and
Finkel, Alain and
Haddad, Serge and
Leucker, Martin and
Ye, Lina },
institution = {Computing Research Repository},
month = sep,
number = {2009.10610},
type = {Research Report},
title = {Property-Directed Verification of Recurrent Neural Networks},
year = {2020},
url = {https://arxiv.org/abs/2009.10610},
pdf = {https://arxiv.org/pdf/2009.10610.pdf}
}
@inproceedings{BRS-csl21,
address = {Ljubljana, Slovenia},
month = jan,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Baier, Christel and Goubault{-}Larrecq, Jean},
acronym = {{CSL}'21},
booktitle = {{P}roceedings of the 29th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'21)},
author = {Benedikt Bollig and Fedor Ryabinin and Arnaud Sangnier},
title = {Reachability in Distributed Memory Automata},
pages = {13:1-13:16},
year = {2021},
doi = {10.4230/LIPIcs.CSL.2021.13},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2021/13447/},
url = {https://drops.dagstuhl.de/opus/volltexte/2021/13447/}
}
@inproceedings{BBBFS-gandalf20,
address = {Brussels, Belgium},
month = sep,
volume = {326},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Bresolin, Davide and Raskin, Jean-Fran\c{c}ois},
acronym = {{GandALF}'20},
booktitle = {{P}roceedings of the 11th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
({GandALF}'20)},
author = {B{\'e}atrice B{\'e}rard and
Benedikt Bollig and
Patricia Bouyer and
Matthias F{\"u}gger and
Nathalie Sznajder},
title = {Synthesis in Presence of Dynamic Links},
pages = {33?49},
year = {2020},
doi = {10.4204/EPTCS.326.3},
pdf = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?GANDALF2020.3.pdf},
url = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?GANDALF2020.3}
}
@inproceedings{BDM-concur20,
address = {Vienna, Austria},
month = sep,
volume = {171},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Igor Konnov and Laura Kovacs},
acronym = {{CONCUR}'20},
booktitle = {{P}roceedings of the 31st
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'20)},
author = {Benedikt Bollig and Alain Finkel and Amrita Suresh},
title = {Bounded Reachability Problems are Decidable in {FIFO} Machines},
pages = {49:1--49:17},
year = 2020,
url = {https://drops.dagstuhl.de/opus/volltexte/2020/12861}
}
@article{BFG-jcss20,
publisher = {Elsevier Science Publishers},
journal = {Journal of Computer and System Sciences},
author = {Benedikt Bollig and Marie Fortin and Paul Gastin},
title = {Communicating Finite-State Machines, First-Order Logic, and Star-Free Propositional Dynamic Logic},
pages = {22-53},
doi = {10.1016/j.jcss.2020.06.006},
year = {2020},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFG20-JCSS.pdf},
abstract = {Message sequence charts (MSCs) naturally arise as executions of communicating
finite-state machines (CFMs), in which finite-state processes exchange
messages through unbounded FIFO channels. We study the first-order logic of
MSCs, featuring Lamport's happened-before relation. To this end, we introduce a star-free
version of propositional dynamic logic (PDL) with loop and converse. Our main
results state that (i) every first-order sentence can be transformed into an
equivalent star-free PDL sentence (and conversely), and (ii) every star-free
PDL sentence can be translated into an equivalent CFM. This answers an open
question and settles the exact relation between CFMs and fragments of monadic
second-order logic. As a byproduct, we show that first-order logic over MSCs
has the three-variable property.}
}
@inproceedings{BBLS-fossacs2020,
address = {Dublin, Ireland},
month = apr,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Barbara K{\"o}nig and Jean Goubault-Larrecq},
acronym = {{FoSSaCS}'20},
booktitle = {{P}roceedings of the 23rd {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'20)},
author = {B{\'e}atrice B{\'e}rard and Benedikt Bollig and Mathieu Lehaut and Nathalie Sznajder},
title = {Parameterized Synthesis for Fragments of First-Order Logic over Data Words},
pages = {97--118},
doi = {10.1007/978-3-030-45231-5_6},
year = 2020
}
This file was generated by bibtex2html 1.98.