Temporal query checking is an extension of temporal model checking where one asks what propositional formulae can be inserted
in a temporal query (a temporal formula with a placeholder) so that the resulting formula is satisfied in the model at hand.
We study the problem of computing all minimal solutions to a temporal query without restricting to so-called “valid” queries
(queries guaranteed to have a unique minimal solution). While this problem is intractable in general, we show that deciding
uniqueness of the minimal solution (and computing it) can be done in polynomial-time.
Now at Lab. GRAVIR, INRIA Rhône-Alpes, Montbonnot, France. Email: Samuel.Hornus@inria.fr. The research described in this paper
was conducted while S. Hornus was at LSV.
When the system does not satisfy the temporal formula, most model checkers provide a diagnostic, e.g. as a trace showing one possible way of violating the property.