# generic technique to build LTL/CTL formula that satisfy specific inputs to a model

I have an automaton, for example the below automaton and would like to generate a single formula (LTL or CTL, or some other representation) that satisfy exactly the traces provided. e.g.,

$t_1 = i^*f_4f_5f_7f_8f_7f_5f_4i^+$

$t_2 = i^*f_4f_6f_7f_9f_7f_6f_4i^+$

$t_3 = t_1^*t_2^*t_1^*$

$T = \{t_1 ...t_x\}$

I may have the notation wrong here, what I am trying to express is that any combination of $t_1$ and $t_2$ is acceptable, so long as INIT is visited between each. There could be any number of $t_x$, but they will all be known.

for example the traces

$i^*f_4f_5f_7f_9f_7f_5f_4i^+ \not\in T$ and

$i^*f_4f_5f_7f_8f_7f_5f_4f_5f_7f_8f_7f_5f_4i^+ \not\in T$ and

$i^*f_4(f_5f_7)^+ \not\in T$

Is there a technique of building a single formula(LTL, CTL, etc) $\psi$ such that $t \models \psi \iff t \in T$

• First of all, it is not clear what a CTL formula would correspond to, since CTL is interpreted over trees (or structures), and not over words. Of course words are also trees, but I assume this isn't what you mean. In addition, automata are more expressive that both LTL and CTL, and therefore there may not be a corresponding formula at all. If, however, your automaton is Alternating-Weak with only self loops (AWW[1]), than it can be converted to LTL, using some form of "reverse engineering" on the translation from LTL to AWW[1]. – Shaull Aug 25 '16 at 16:45
• @Shaull In all honesty I'm not sure if what I'm asking is possible or even practical. It's likely that I could express each trace as a regular expression, it is possible that a trace could contain a loop within itself (though not in the example given). What I was hoping for was a better way of checking an unknown trace than to directly compare to each of the known traces. – Zack Newsham Aug 25 '16 at 16:48
• Check the proof for LTL/CTL being equivalent to the resp. automata models. Use the construction you find there. That said, I think asking about the real problem you are trying to solve may be more helpful. – Raphael Aug 25 '16 at 16:55
• So, you have no a-priori specification of the desired behaviour? I'm not sure what use formal methods will be to you if you feed them with test data only. That said, every single trace is a formula; just $\lor$ them. – Raphael Aug 25 '16 at 17:22
• Since even minimization of regular expression is hard, I doubt minimizing $\omega$-regular expressions (which is what you seem to have there) will be any easier. But there are constructions from automaton to formlua; as I said, I'd look there. – Raphael Aug 25 '16 at 22:07