3
$\begingroup$

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$.

$\endgroup$
  • $\begingroup$ 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)$? $\endgroup$ – D.W. Nov 22 '17 at 0:58
4
$\begingroup$

This is only a partial answer (as I believe that the state of the art is insufficient to answer your questions completely - I am happy to be proven wrong here), but I hope that it helps you anyway.

  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.
  2. The constructions given in the Vardi paper and the one given in the slide set you referred to are slightly different. Both have counters for keeping track of for which automaton an accepting state has to be visited next. In the slide set construction, after both automata have seen accepting states, goes to the counter value of 3, where in the product an accepting state is visited and then switches back to 1. Vardi (who attributes the construction to earlier work by another researcher) does it differently. In a nutshell, the idea is to recycle the accepting states from the factor automata, and to switch the counter only after an accepting state has just been seen. In this way, the "3" counter value is not neccessary, and the construction still works anyway.
  3. As far as I know, there is no research that answers your questions completely. But you may be interested in Schewe's paper that shows that minimizing deterministic Buchi automata is NP-hard (The ArXiV version of the paper can be found here). I would not be surprised if you could base a proof that your problem 3 is NP-hard on his proof ideas. For the case that the factor automata are not already minimal, this proof would be trivial, but I assume that you want to start with minimally-sized automata.
$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – D.W. Nov 22 '17 at 0:57
  • $\begingroup$ 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. $\endgroup$ – DCTLib Nov 22 '17 at 14:38
  • $\begingroup$ 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. $\endgroup$ – D.W. Nov 22 '17 at 16:24
  • $\begingroup$ @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. $\endgroup$ – DCTLib Nov 24 '17 at 9:13
  • $\begingroup$ 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? $\endgroup$ – D.W. Nov 24 '17 at 17:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.