propiedad de tiempo lineal
En la comprobación de modelos , una rama de la informática , las propiedades de tiempo lineal se utilizan para describir los requisitos de un modelo de un sistema informático . Las propiedades de ejemplo incluyen "la máquina expendedora no dispensa una bebida hasta que se haya ingresado el dinero" (una propiedad de seguridad ) o "el programa de computadora eventualmente termina" (una propiedad de vida).). Las propiedades de imparcialidad se pueden utilizar para descartar rutas poco realistas de un modelo. Por ejemplo, en un modelo de dos semáforos, la propiedad de vivacidad "ambos semáforos son verdes infinitamente a menudo" solo puede ser cierta bajo la restricción de imparcialidad incondicional "cada semáforo cambia de color infinitamente a menudo" (para excluir el caso en que un semáforo es "infinitamente más rápido" que el otro). [1]
Formalmente, una propiedad de tiempo lineal es un lenguaje ω sobre el conjunto de potencia de "proposiciones atómicas". Es decir, la propiedad contiene secuencias de conjuntos de proposiciones, cada secuencia conocida como "palabra". Cada propiedad se puede reescribir como " P y Q ocurren tanto" para alguna propiedad de seguridad P y propiedad de vida Q. Un invariante para un sistema es algo que es verdadero o falso para un estado particular. Las propiedades invariantes describen una invariante que cada estado alcanzable de un modelo debe satisfacer, mientras que las propiedades de persistencia son de la forma "eventualmente, para siempre, alguna invariante se mantiene".
Las lógicas temporales , como la lógica temporal lineal, describen tipos de propiedades de tiempo lineal mediante fórmulas.
Sea AP un conjunto de proposiciones atómicas. Una palabra sobre (el conjunto potencia de AP ) es una secuencia infinita de conjuntos de proposiciones, como (para las proposiciones atómicas ). Una propiedad de tiempo lineal (LT) sobre AP es un subconjunto de , por ejemplo, un conjunto de palabras. [2] Un ejemplo de una propiedad LT sobre el conjunto es "el conjunto de palabras que contienen una frecuencia infinita". La palabra w está en este conjunto porque a está contenida en , lo que ocurre infinitamente a menudo. Una palabra que no está en este conjunto es , ya que a solo aparece una vez (en el primer conjunto).
Una propiedad LT es un lenguaje ω sobre el alfabeto (y viceversa).
Denotamos por pref ( w ) los prefijos finitos de w (es decir , en el caso anterior). El cierre de una propiedad LT P es:
