Mediating for Reduction (On Minimizing Alternating Büchi Automata)
Result description
We propose a new approach for minimizing alternating Büchi automata
(ABA). The approach is based on the so called mediated equivalence on
states of ABA, which is the maximal equivalence contained in the so called mediated
preorder. Two states pand q can be related by the mediated preorder if there
is a mediator (mediating state) which forward simulates p and backward simulates
q. Under some further conditions, letting a computation on some word jump
from q to p (due to they get collapsed) preserves the language as the automaton
can anyway already accept the word without jumps by runs through the mediator.
We further show how the mediated equivalence can be computed efficiently.
Finally, we show that, compared to the standardforward simulation equivalence,
the mediated equivalence can yield much more significant reductions when applied
within the process of complementing Büchi automata where ABA are used
as an intermediate model.
Keywords
The result's identifiers
Result code in IS VaVaI
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
čeština
Original language name
Zprostředkování pro redukci (Za minimalizací alternujících automatů)
Original language description
Navrhli jsme novou metodu redukce alternujících Büchi automatů slučováním stavů ekvivalentních podle podle nové relace, takzvane zprostředkované (mediated) ekvivalenece. Zprostředkovaná ekvivalece je kombinací dopředné a zpětné simulace. Efektivitu metody jsme otestovali na experiementech s alternujícími automaty vznikajícími v rámci komplementace Büchi automatů.
Czech name
Zprostředkování pro redukci (Za minimalizací alternujících automatů)
Czech description
Navrhli jsme novou metodu redukce alternujících Büchi automatů slučováním stavů ekvivalentních podle podle nové relace, takzvane zprostředkované (mediated) ekvivalenece. Zprostředkovaná ekvivalece je kombinací dopředné a zpětné simulace. Efektivitu metody jsme otestovali na experiementech s alternujícími automaty vznikajícími v rámci komplementace Büchi automatů.
Classification
Type
D - Article in proceedings
CEP classification
JC - Computer hardware and software
OECD FORD branch
—
Result continuities
Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)
Others
Publication year
2009
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009)
ISBN
978-3-939897-13-2
ISSN
—
e-ISSN
—
Number of pages
12
Pages from-to
—
Publisher name
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Place of publication
Wadern
Event location
Kanpur
Event date
Dec 14, 2009
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—
Basic information
Result type
D - Article in proceedings
CEP
JC - Computer hardware and software
Year of implementation
2009