# Minimal Deterministic Buchi Automata Product

Problem:

Let $\varphi = \varphi_1 \land \varphi_2$ be Deterministic Buchi Automata (DBA) expressible LTL formulas.

Let $A$, $A_1$ and $A_2$ be translated DBAs such that ${\cal{L}}(A) = {\cal{L}}(A_1) \cap {\cal{L}}(A_2)$.

What can be said about the relation between the number of states in $A$ and that in the synchronous product $A_1 \otimes A_2$?

Some background:

I found two definitions of the Buchi product, the one given by Vardi in An Automata-Theoretic Approach to Linear Temporal Logic that uses $S = S_1 \times S_2 \times \{1, 2\}$ while the one demonstrated in this presentation uses $S = S_1 \times S_2 \times \{1, 2, 3\}$.

Also, Ehlers has proposed an approach to minimize the DBA in this paper.

However, I have been unsuccessful in finding any rigorous mathematical relation between the sizes of translated DBA $A$ and the minimal synchronous product of $A_1 \otimes A_2$.

My question:

I would like to know about

1. Any work regarding the size of Minimal DBA Product

2. Any work about the relation between the number of states.

3. How to construct the minimal DBA Product, given $A_1$ and $A_2$.

• Can you formulate the question a little more precisely? As it stands you allow $A$ to be any DBA such that ${\cal{L}}(A) = {\cal{L}}(A_1) \cap {\cal{L}}(A_2)$, so I think it could have arbitrarily many states (just add extra useless states). Do you mean that $A$ is the minimal DBA such that ${\cal{L}}(A) = {\cal{L}}(A_1) \cap {\cal{L}}(A_2)$? – D.W. Nov 22 '17 at 0:58

1. First of all, note that when taking the conjunction of two automata with $n$ and $m$ states, the result having $nm - o(n) - o(m)$ states cannot be avoided. This follows pretty much from the fact that for deterministic automata over finite words, such a blow-up can also not be avoided. At the same time, we have an upper bound on $2nm$ many states for the product. For automata theory researchers, this is actually pretty tight.
• Can you clarify what "cannot be avoided" means? Do you mean that the result always has at least $nm-o(n)-o(m)$ states? Do you mean that the minimal automaton always has at least $nm-o(n)-o(m)$ states? – D.W. Nov 22 '17 at 0:57
• Cannot be avoided means that there exists a family of pairs of automata of increasing sizes such that for no pair with $n$ and $m$ states in the family, there exists an automaton for their intersection with fewer than $nm - o(n) - o(m)$ states. So not intersection algorithm can be better than that in the worst case. The intersection can be smaller for some pairs of automata. In particular if their language intersection is empty, the minimal automaton for the intersection will have 0 or 1 states, depending on the details of the automaton type definition. – DCTLib Nov 22 '17 at 14:38
• Do you mean the minimal automaton requires at least $nm - o(n) - o(m)$ states? Your answer makes it sound like you are giving a lower bound, but your comment states an upper bound. I'm still confused. – D.W. Nov 22 '17 at 16:24
• @D.W. It's a lower bound for the general case. The upper bound is $2nm$. The second part of my comment referred to your question part asking if the minimal automaton always has at least $nm - o(n) - o(m)$ states. This is not the case, as there are some problem instances where the minimal product automata have fewer states. But in the general case, $nm - o(n) - o(m)$ is a lower bound. – DCTLib Nov 24 '17 at 9:13
• So you are saying that for all $n,m$ there exists $A_1$ of size $n$, $A_2$ of size $m$, such that the minimal automaton for $L(A_1) \cap L(A_2)$ has size $nm-o(n)-o(m)$? Am I correctly understanding what you mean by general case? – D.W. Nov 24 '17 at 17:24