% IMPORTANT: The following is UTF-8 encoded. This means that in the presence
% of non-ASCII characters, it will not work with BibTeX 0.99 or older.
% Instead, you should use an up-to-date BibTeX implementation like “bibtex8” or
% “biber”.
@PHDTHESIS{Chaturvedi:461238,
author = {Chaturvedi, Namit},
othercontributors = {Thomas, Wolfgang and Muscholl, Anca},
title = {{C}lassifications of {R}ecognizable {I}nfinitary {T}race
{L}anguages and the {D}istributed {S}ynthesis {P}roblem},
address = {Aachen},
publisher = {Publikationsserver der RWTH Aachen University},
reportid = {RWTH-2015-00319},
pages = {X, 105 S. : Ill., graph. Darst.},
year = {2015},
note = {Prüfungsjahr: 2014. - Publikationsjahr: 2015; Aachen,
Techn. Hochsch., Diss., 2014},
abstract = {The classification of recognizable ω-word languages into
Borel levels is the basis of many specialized solutions in
the fields of formal verification and algorithmic controller
synthesis. Each of these levels is characterized by a class
of deterministic ω-automata, namely deterministic weak
(reachability and safety), deterministic Büchi, and
deterministic Muller automata. This thesis analyses the more
general setting of infinitary Mazurkiewicz traces, which
model nonterminating, concurrent computation of distributed
systems. The study of finitary trace-languages generalizes
that of word-languages, and numerous results have been
extended to infinitary trace-languages (due to Gastin,
Petit, Diekert, Muscholl, and others). However, the current
definitions of asynchronous ω-automata fail to yield a
classification of ω-trace languages that is compatible with
the Borel hierarchy. We close this gap, which had been open
since the 1990's, by introducing the family of
"synchronization aware'' automata. We also demonstrate the
semi-decidability of the problem to determine whether a
given recognizable ω-trace language is also recognized by a
deterministic synchronization aware Büchi
automaton.Although asynchronous automata are useful in
implementing distributed monitors and distributed
controllers, their constructions are prohibitively expensive
even by automata-theoretic standards. On the other hand,
"linearizations'' of infinitary trace languages, which
invoke the framework of "trace-closed'' ω-word languages,
can find immediate applications in model checking and formal
verification of distributed systems. This is because word
automata recognizing trace-closed languages support more
efficient analyses of most of the interesting properties
pertaining to distributed computations. In this setting, we
present another classification of ω-trace languages in
terms of a Borel-like hierarchy of trace-closed ω-word
languages.Finally, we introduce a distributed version of
Church's synthesis problem and compare it with two well
known variants of distributed controller synthesis, viz.
action-based control (due to Gastin, Lerman, and Zeitoun)
and process-based control (due to Madhusudan, Thiagarajan,
and Yang). While the algorithmic solution of these problems
remains an open area of investigation, we build upon the
work of Muscholl, Walukiewicz, and Zeitoun, and compare
their problem classes with variants of distributed Church's
synthesis problem by demonstrating suitable reductions in
the sense that a solution of any one problem can be
converted into a solution of the other.},
cin = {122110 / 120000},
ddc = {510},
cid = {$I:(DE-82)122110_20140620$ / $I:(DE-82)120000_20140620$},
typ = {PUB:(DE-HGF)11},
urn = {urn:nbn:de:hbz:82-rwth-2015-003199},
url = {https://publications.rwth-aachen.de/record/461238},
}
guest ::