The size and complexity of software systems are continuously increasing, which makes them difficult and labor-intensive to develop, test and evolve. Since concurrent systems are particularly hard to verify by hand, achieving effective, automated verification tools for concurrent software has become an important topic of research. Model checking is a popular automated verification technology which allows us to determine the properties of a software system and enables more thorough and less costly testing. In this work, we improve the model-checking methodology previously developed for the timed concurrent constraint programming language tccp so that more sophisticated, quantitative properties can be verified by the model-checking tools. First, we refine the notion of global store and the entailment relation which are inherent to the concurrent constraint paradigm, by formulating a notion of just entailed constraint. Then, we define a real-time extension to the linear-time temporal logic that is used to specify the software properties by annotating discrete-time marks to formulae. Finally, we illustrate by means of one example the improved ability to check real-time properties, which cannot be currently checked within previous model-checking frameworks for tccp.