Verificación de modelos

El sistema es descrito mediante un modelo, que debe satisfacer una especificación formal descrita mediante una fórmula, a menudo escrita en alguna variedad de lógica temporal.Un conjunto de proposiciones atómicas se asocia a cada nodo.Así pues, los nodos representan los estados posibles de un sistema, los arcos posibles evoluciones del mismo, mediante ejecuciones permitidas, que alteran el estado, mientras que las proposiciones representan las propiedades básicas que se satisfacen en cada punto de la ejecución.Formalmente, el problema se representa de la siguiente manera: Dada una propiedad deseada, expresada como una fórmula en lógica temporal p, y un modelo M con un estado inicial s; decidir siPara evitarlo, diversos investigadores han desarrollado técnicas basadas en algoritmos simbólicos, abstracción, reducción de orden parcial y model checking al vuelo.