Model-Checking techniques for efficently querying semistructured temporal data