La Programacion Concurrente por Restricciones (ccp) es un formalismo para modelar sistemas concurrentes en el cual agentes (procesos) interactuan con otros agregando (telling) y leyendo (asking) informacion representada como restricciones en un medio compartido (store). La Programacion Concurrente Temporal por Restricciones (tcc), extiende el modelo ccp agregrandole constructores temporales para modelar agentes temporales y sistemas reactivos. La verificacion formal cumple un papel muy importante en la deteccion de errores en sistemas concurrentes, ya que permite determinar si el modelo de un sistema satisface o no una propiedad. Model checking es una tecnica de verificacion formal que, dado el modelo de un sistema y una propiedad, comprueba sistematicamente si el modelo satisface o no la formula. Este proyecto de grado investiga la tecnica de model checking como un metodo formal para la verificacion de programas tcc. La investigacion se lleva a cabo mediante la definicion de un algoritmo de model checking para el calculo tcc. Para lograr esto, nosotros extendemos el algoritmo clasico de model checking para LTL. Primero definimos una estructura llamada tcc Structure la cual permite modelar el comportamiento de un sistema tcc, ademas describimos una logica que permite razonar sobre programas tcc. Luego se presenta el grafo de model checking y las propiedades que debe cumplir para determinar que el modelo satisface la propiedad. Al final, se presenta un prototipo que implementa el algoritmo propuesto.