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

Improve this question
$\endgroup$
1
  • $\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. ♦
    Commented Nov 22, 2017 at 0:58

1 Answer 1

Reset to default
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.
Improve this answer
$\endgroup$
5
  • $\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. ♦
    Commented Nov 22, 2017 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
    Commented Nov 22, 2017 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. ♦
    Commented Nov 22, 2017 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
    Commented Nov 24, 2017 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. ♦
    Commented Nov 24, 2017 at 17:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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