Résumé | We study linear-time temporal logics interpreted
over data words with multiple attributes. We restrict the atomic
formulas to equalities of attribute values in successive positions
and to repetitions of attribute values in the future or past.
We demonstrate correspondences between satisfiability problems
for logics and reachability-like decision problems for counter
systems. We show that allowing/disallowing atomic formulas
expressing repetitions of values in the past corresponds to the
reachability/coverability problem in Petri nets. This gives us
2EXPSPACE upper bounds for several satisfiability problems. We
prove matching lower bounds by reduction from a reachability
problem for a newly introduced class of counter systems. This
new class is a succinct version of vector addition systems with
states in which counters are accessed via pointers, a potentially useful feature in other contexts. We strengthen further
the correspondences between data logics and counter systems
by characterizing the complexity of fragments, extensions and
variants of the logic. For instance, we precisely characterize the
relationship between the number of attributes allowed in the logic
and the number of counters needed in the counter system.
This is joint work with Stephane Demri and Diego Figueira.
|