episciences.org_1645_1634928769
1634928769
episciences.org
raphael.tournoy+crossrefapi@ccsd.cnrs.fr
episciences.org
Logical Methods in Computer Science
1860-5974
08
04
2016
Volume 12, Issue 3
Reasoning about Data Repetitions with Counter Systems
Stephane
Demri
Diego
Figueira
M
Praveen
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.
08
04
2016
1645
arXiv:1604.02887
10.2168/LMCS-12(3:1)2016
https://lmcs.episciences.org/1645