@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},
  year = {2021},
  note = {To appear}
}
@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},
  year = {2020},
  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.},
  note = {To appear}
}
@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.