Hardware Reference
In-Depth Information
Then
A
1
\
!
A
2
accepts the intersection of the
!
-languages accepted respectively
by
A
2
.
Notice the major differences between the operators for standard intersection of
finitary languages and
A
1
and
!
-intersection.
4.2.4.4
!
-Parallel Composition of
!
-Automata
Proposition 4.22.
Given two B uchi automata
A
1
D
.Q
1
;I
[
U
[
V;
1
;q
01
;F
1
/
and
A
2
D
.Q
2
;U
[
V
[
O;
2
;q
02
;F
2
/
accepting respectively the given
!
-regular
languages
L
1
and
L
2
, and the alphabet
E
I
[
V
[
O
, consider the B uchi
automaton
A
1
˘
!E
A
2
D
..
A
1
/
*
!O
\
!
.
A
2
/
*
!I
/
+
!E
:
Then
A
1
˘
!E
A
2
accepts the parallel composition of the
!
-languages accepted
respectively by
A
1
and
A
2
, with respect to alphabet
E
.
4.2.4.5
!
-Parallel Complementation of
!
-Automata
We omit the procedure for deriving the Buchi automaton that accepts the comple-
ment of the language accepted by a given Buchi automaton, because it is quite
complicated. For a discussion on the topic we refer to [42, 53, 122].
The problem of complementation may be simplified in special cases, as done in
Chap. 18, where a subset construction is used to obtain a deterministic Buchi over-
approximation of an ND Buchi automaton. Therefore, the final complementation,
done by simply complementing the acceptance conditions to obtain a co-Buchi
automaton, yields a subset of the most general solution automaton.
4.2.4.6
Summing it up
The following theorem has been proved in [24].
Theorem 4.23.
Given the pairwise disjoint alphabets
I;U;V
and
O
,the
!
-regular
C
.I
[
U
[
V/
!
,
S
.I
[
V
[
O/
!
, and the sets
E
D
I
[
V
[
O
languages
H
D
U
[
V
[
O
A
C
and
A
S
are Buchi automata accepting
and
, suppose that
respectively
C
and
S
, then the largest solution of the
!
-regular parallel equation
C
˘
!E
X
S
is the
!
-regular language accepted by the B uchi automaton
A
C
˘
!H
A
S
:
Search WWH ::
Custom Search