TY - GEN
T1 - Vectorial languages and linear temporal logic
AU - Serre, Olivier
PY - 2002/1/1
Y1 - 2002/1/1
N2 - Determining for a given deterministic complete automaton the sequence of visited states while reading a given word is the core of important problems with automata-based solutions, such as approximate string matching. The main difficulty is to do this computation efficiently, especially when dealing with very large texts. Considering words as vectors and working on them using vectorial (parallel) operations allows 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 relate them with languages defined by fragments of linear temporal logic. Finally, we consider the converse problem of constructing an automaton 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.
AB - Determining for a given deterministic complete automaton the sequence of visited states while reading a given word is the core of important problems with automata-based solutions, such as approximate string matching. The main difficulty is to do this computation efficiently, especially when dealing with very large texts. Considering words as vectors and working on them using vectorial (parallel) operations allows 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 relate them with languages defined by fragments of linear temporal logic. Finally, we consider the converse problem of constructing an automaton 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.
KW - Linear temporal logic and extensions
KW - Parallel automata simulation
U2 - 10.1007/978-0-387-35608-2_47
DO - 10.1007/978-0-387-35608-2_47
M3 - Conference contribution
AN - SCOPUS:84891130985
SN - 9781475752755
T3 - IFIP Advances in Information and Communication Technology
SP - 576
EP - 587
BT - Foundations of Information Technology in the Era of Network and Mobile Computing - IFIP 17th World Computer Congress - TC1 Stream / 2nd IFIP Int. Conference on Theoretical Computer Science (TCS 2002)
PB - Springer New York LLC
T2 - IFIP 17th World Computer Congress - TC1 Stream / 2nd IFIP International Conference on Theoretical Computer Science, TCS 2002
Y2 - 25 August 2002 through 30 August 2002
ER -