|
Journal of Automata, Languages and Combinatorics
formerly:
Journal of Information Processing and Cybernetics /
Elektronische Informationsverarbeitung und Kybernetik
|
|
@article{jalc050312,
author = {Schmitz, Heinz},
title = {Restricted Temporal Logic and Deterministic Languages},
journal = jalc,
year = 2000,
volume = 5,
number = 3,
pages = {325--341},
keywords = {temporal logic, finite automata, deterministic languages,
forbidden pattern},
abstract = {In formulas of restricted temporal logic (RTL) arbitrary
use of the temporal operators \emph{next} ({\bf X}),
\emph{eventually} ({\bf F}) and Boolean connectives is
allowed. We show in detail to what extent the \emph{next}
operator contributes to the expressive power of this logic
and reveal close connections to formal languages and finite
automata.\par
Let ${\rm TL}[{\rm\bf X}(k),{\bf F}]$ denote the class of
formulas with nesting depth at most $k$ in ${\rm\bf X}$.
For all $k\geq 0$ we characterize the class of
${\rm TL}[{\rm\bf X}(k),{\bf F}]$-definable languages
(1) in terms of a formal language representation involving a
generalization of the notion of deterministic languages, and
(2) in terms of a certain pattern that must not appear in the
transition graph of deterministic finite automata. This leads
to concise proofs of strictness and decidability results for
this \emph{next} hierarchy, which exhausts the class of
RTL-definable languages. We discuss relations to languages
having dot-depth one.}
}