Vectorial languages an linear temporal logic: Version with proofs. http://www.liafa.jussieu.fr/~serre

Determining for a given deterministic complete automaton the se-quence of visited states while reading a given word is the core of im-portant problems with automata-based solutions, such as approximate string matching. The main difficulty is to do this computation effi-ciently, especially when dealing with very large texts. Considering words as vectors and working on them using vectorial (parallel) operations al-lows to solve the problem faster than in linear time using sequential computations. In this paper, we show first that the set of vectorial operations needed by an algorithm representing a given automaton depends only on the language accepted by the automaton. We give precise characterizations of vectorial algorithms for star-free, solvable and regular languages in terms of the vectorial operations allowed. We also consider classes of languages associated with restricted sets of vectorial operations and re-late them with languages defined by fragments of linear temporal logic. Finally, we consider the converse problem of constructing an automa-ton from a given vectorial algorithm. As a byproduct, we show that the satisfiability problem for some extensions of linear-time temporal logic characterizing solvable and regular languages is PSPACE-complete