Hispanopedia Wiki
Articulo de referencia

Propiedad de tiempo lineal

En la verificación de modelos , una rama de la informática , se utilizan propiedades de tiempo lineal para describir los requisitos de un modelo de un sistema informático . Algu...

Hispanopedia WikiContenido en espanolLectura gratuita

En la verificación de modelos , una rama de la informática , se utilizan propiedades de tiempo lineal para describir los requisitos de un modelo de un sistema informático . Algunos ejemplos de propiedades son: "la máquina expendedora no dispensa una bebida hasta que se haya introducido el dinero" (una propiedad de seguridad ) o "el programa informático finaliza eventualmente" (una propiedad de vivacidad ). Las propiedades de equidad se pueden utilizar para descartar trayectorias poco realistas de un modelo. Por ejemplo, en un modelo de dos semáforos, la propiedad de vivacidad "ambos semáforos están en verde infinitas veces" solo puede ser verdadera bajo la restricción de equidad incondicional "cada semáforo cambia de color infinitas veces" (para excluir el caso en que un semáforo sea "infinitamente más rápido" que el otro). [ 1 ]

Formalmente, una propiedad de tiempo lineal es un lenguaje ω sobre el conjunto potencia de "proposiciones atómicas". Es decir, la propiedad contiene secuencias de conjuntos de proposiciones, cada secuencia conocida como "palabra". Toda propiedad puede reescribirse como " P y Q ocurren" para alguna propiedad de seguridad P y una propiedad de vivacidad Q. Un invariante para un sistema es algo que es verdadero o falso para un estado particular. Las propiedades invariantes describen un invariante que todo estado alcanzable de un modelo debe satisfacer, mientras que las propiedades de persistencia tienen la forma "eventualmente para siempre se cumple algún invariante".

Las lógicas temporales, como la lógica temporal lineal, describen tipos de propiedades temporales lineales mediante fórmulas.

Este artículo trata sobre propiedades proposicionales de tiempo lineal y no puede manejar predicados sobre estados del programa, por lo que no puede definir una propiedad como: el valor actual de y determina la cantidad de veces que x cambia entre 0 y 1 antes de la terminación. El formalismo más general utilizado en las propiedades de seguridad y vivacidad sí puede manejar esto.

Definición

Sea AP un conjunto de proposiciones atómicas. Una palabra sobre2APAG{\displaystyle 2^{AP}}(el conjunto potencia de AP ) es una secuencia infinita de conjuntos de proposiciones, comow:={a}{a,b}∅{a,b}ω{\displaystyle w:=\{a\}\{a,b\}\emptyset \{a,b\}^{\omega }}(para las proposiciones atómicas)APAG={a,b}{\displaystyle AP=\{a,b\}}). Una propiedad de tiempo lineal (LT) sobre AP es un subconjunto de(2APAG)ω{\displaystyle (2^{AP})^{\omega }}es decir, un conjunto de palabras. [ 2 ] Un ejemplo de una propiedad LT sobre el conjunto{a,b}{\displaystyle \{a,b\}}es "el conjunto de palabras que contienen una a infinitas veces". La palabra w está en este conjunto, porque a está contenida en{a,b}{\displaystyle \{a,b\}}, que ocurre infinitamente a menudo. Una palabra que no está en este conjunto esincógnita:={a}({b}∅)ω{\displaystyle x:=\{a\}(\{b\}\emptyset )^{\omega }}, ya que solo ocurre una vez (en el primer conjunto).

Una propiedad LT es un lenguaje ω sobre el alfabeto.Σ=2APAG{\displaystyle \Sigma =2^{AP}}(y viceversa).

Denotamos por pref ( w ) los prefijos finitos de w (es decir,{{a},{a}{a,b},{a}{a,b}∅,...}{\displaystyle \{\{a\},\{a\}\{a,b\},\{a\}\{a,b\}\emptyset ,...\}}en el caso anterior). El cierre de una propiedad LT P es:

dolostúrmi(PAG):={σ∈(2APAG)ω∣pagrmiF(σ)⊆pagrmiF(PAG)}{\displaystyle {\mathit {closure}}(P):=\{\sigma \in (2^{AP})^{\omega }\mid {\mathit {pref}}(\sigma )\subseteq {\mathit {pref}}(P)\}}

Aplicaciones

Estructura de Kripke
Una estructura de Kripke sobre{pag,q}{\displaystyle \{p,q\}}. No satisface la propiedad LT "infinitamente a menudo q ", debido a la trayectorias1s2s3ω{\displaystyle s_{1}s_{2}s_{3}^{\omega }}. Satisface la propiedad "infinitamente a menudo p ", porque todos los caminos posibles entrans1{\displaystyle s_{1}}os3{\displaystyle s_{3}}infinitas veces.

Utilizando la teoría de máquinas de estados finitos , un programa o sistema informático puede modelarse mediante una estructura de Kripke . Las propiedades LT describen entonces restricciones en las trazas (salidas) de una estructura de Kripke. Por ejemplo, si dos semáforos en una intersección se representan mediante una estructura de Kripke, las proposiciones atómicas pueden ser los posibles colores de cada luz y puede ser deseable que las trazas satisfagan la propiedad LT "los semáforos no pueden estar ambos en verde al mismo tiempo" (para evitar colisiones de vehículos). [ 3 ]

Si cada traza de la estructura de Kripke TS es una traza de TS ', entonces cada propiedad LT que TS ' satisface es satisfecha por TS . Esto es útil en la verificación de modelos para permitir la abstracción: si un modelo simplificado del sistema satisface una propiedad LT, entonces el modelo real del sistema también la satisfará. [ 4 ]

Clasificación de las propiedades del tiempo lineal

Propiedades de seguridad

Una propiedad de seguridad es informalmente de la forma "no ocurre nada malo". [ 5 ] Por ejemplo, si un sistema modela un cajero automático (ATM), entonces dicha propiedad es "no se debe dispensar dinero a menos que se haya introducido un PIN". [ 6 ] Formalmente, una propiedad de seguridad es una propiedad LT tal que cualquier palabra que viole la propiedad tiene un "prefijo malo", para el cual ninguna palabra con ese prefijo satisface la propiedad. Es decir, [ 7 ]

∀σ∈(2APAG)ω∖PAG ∃ un prefijo finito σ^:PAG∩{σ′∣σ^ es un prefijo de σ′}=∅{\displaystyle \forall \sigma \in (2^{AP})^{\omega }\setminus P\ \exists {\text{ un prefijo finito}}\ {\hat {\sigma }}:P\cap \{\sigma '\mid {\hat {\sigma }}\ {\text{es un prefijo de}}\ \sigma '\}=\emptyset }

En el ejemplo del cajero automático, un prefijo malo mínimo es un conjunto finito de pasos realizados en los que se dispensa dinero en el último paso y no se introduce un PIN en ningún paso. Para verificar una propiedad de seguridad, basta con considerar únicamente las trazas finitas de una estructura de Kripke y comprobar si alguna de dichas trazas es un prefijo malo. [ 8 ]

Una propiedad LT P es una propiedad de seguridad si y solo sidolostúrmi(PAG)=PAG{\displaystyle {\mathit {cierre}}(P)=P}. [ 9 ]

Propiedades invariantes

Una propiedad invariante es un tipo de propiedad de seguridad en la que la condición solo se refiere al estado actual. [ 10 ] Por ejemplo, el ejemplo del cajero automático no es invariante porque no podemos saber si la propiedad se viola al ver que el estado actual es "dispensar dinero", solo al ver que el estado actual es "dispensar dinero" y que ningún estado anterior fue "leer PIN". Un ejemplo de invariante es la condición del semáforo "los semáforos no pueden estar ambos en verde al mismo tiempo" mencionada anteriormente. Otro ejemplo es "la variable x nunca es negativa", en un modelo de un programa informático.

Formalmente, un invariante tiene la forma:

PAG={A0A1....∈(2APAG)ω∣∀j∈norte:Aj Satisface Φ}{\displaystyle P=\{A_{0}A_{1}....\in (2^{AP})^{\omega }\mid \forall j\in \mathbb {N} :A_{j}\ {\text{satisface}}\ \Phi \}}

para alguna fórmula de lógica proposicionalΦ{\displaystyle \Phi }. [ 10 ]

Una estructura de Kripke satisface un invariante si y solo si todo estado alcanzable satisface el invariante, lo cual puede verificarse mediante una búsqueda en amplitud o una búsqueda en profundidad . [ 11 ] Las propiedades de seguridad pueden verificarse inductivamente utilizando invariantes. [ 12 ]

Propiedades de Liveness

Una propiedad de vivacidad tiene informalmente la forma "algo bueno sucede eventualmente". [ 5 ] Formalmente, P es una propiedad de vivacidad sipagrmiF(PAG)=(2APAG)∗{\displaystyle {\mathit {pref}}(P)=(2^{AP})^{*}}Es decir, cualquier cadena finita puede continuarse en una traza válida. [ 13 ] [ 7 ] Un ejemplo de una propiedad de vivacidad es la propiedad LT anterior "el conjunto de palabras que contienen una a infinitas veces". Ningún prefijo finito de una palabra puede probar que la palabra no satisface esta propiedad, ya que la palabra podría continuar teniendo infinitas a s.

En términos de programas informáticos, las propiedades de vivacidad útiles incluyen "el programa eventualmente termina" y, en computación concurrente , "cada proceso debe ser atendido eventualmente". [ 14 ]

Propiedades de persistencia

Una propiedad de persistencia es una propiedad de vivacidad de la forma "eventualmente para siempre"Φ{\displaystyle \Phi }". Es decir, una propiedad de la forma: [ 15 ]

PAG={A0A1...∈(2APAG)ω∣∃norte∈norte:∀norte≥norte:Anorte Satisface Φ}{\displaystyle P=\{A_{0}A_{1}...\in (2^{AP})^{\omega }\mid \exists N\in \mathbb {N} :\forall n\geq N:A_{n}\ {\text{satisface}}\ \Phi \}}

Relación entre las propiedades de seguridad y vivacidad

Ninguna propiedad LT que no sea(2APAG)ω{\displaystyle (2^{AP})^{\omega }}(el conjunto de todas las palabras más2APAG{\displaystyle 2^{AP}}) es tanto una propiedad de seguridad como una propiedad de vivacidad. [ 16 ] Aunque no toda propiedad es una propiedad de seguridad o una propiedad de vivacidad (considere " a ocurre exactamente una vez"), toda propiedad es la intersección de una propiedad de seguridad y una propiedad de vivacidad. [ 5 ]

En topología , el conjunto de todas las palabras(2APAG)ω{\displaystyle (2^{AP})^{\omega }}puede equiparse con la métrica :

d(w,incógnita):=inf{2−|s|∣s∈pagrmiF(w)∩pagrmiF(incógnita)}{\displaystyle d(w,x):=\inf\{2^{-|s|}\mid s\in {\mathit {pref}}(w)\cap {\mathit {pref}}(x)\}}

Entonces, una propiedad de seguridad es un conjunto cerrado y una propiedad de vivacidad es un conjunto denso . [ 17 ]

Propiedades de equidad

Las propiedades de equidad son precondiciones impuestas a un sistema para descartar trazas irreales. [ 18 ] [ 19 ] La equidad incondicional tiene la forma "cada proceso tiene su turno infinitamente a menudo". La equidad fuerte tiene la forma "cada proceso tiene su turno infinitamente a menudo si se habilita infinitamente a menudo". La equidad débil tiene la forma "cada proceso tiene su turno infinitamente a menudo si se habilita continuamente desde un punto particular". [ 20 ]

En algunos sistemas, una restricción de equidad se define mediante un conjunto de estados, y un "camino justo" es aquel que pasa por algún estado de la restricción de equidad infinitas veces. Si hay múltiples restricciones de equidad, entonces un camino justo debe pasar infinitas veces por un estado por cada restricción. [ 21 ] Un programa "satisface justamente" una propiedad LT P con respecto a un conjunto de condiciones de equidad si para cada camino, o bien el camino no cumple una condición de equidad o bien satisface P. Es decir, la propiedad P se satisface para todos los caminos justos. [ 22 ]

Una propiedad de equidad es realizable para una estructura de Kripke si cada estado alcanzable tiene un camino justo que parte de ese estado. Siempre que un conjunto de condiciones de equidad sea realizable, son irrelevantes para las propiedades de seguridad. [ 23 ]

Lógica temporal

Las lógicas temporales, como la lógica de árbol de computación (CTL), pueden utilizarse para especificar algunas propiedades LT. [ 24 ] Todas las fórmulas de lógica temporal lineal (LTL) son propiedades LT. Mediante un argumento de conteo, vemos que cualquier lógica en la que cada fórmula sea una cadena finita no puede representar todas las propiedades LT, ya que debe haber una cantidad numerable de fórmulas, pero hay una cantidad incontable de propiedades LT.

Notas

Referencias

  • Alpern, B.; Schneider, FB (1987). "Reconociendo seguridad y vivacidad". Computación distribuida . 2 (3): 117. CiteSeerX 10.1.1.20.5470 . doi : 10.1007/BF01782772 . S2CID 9717112 .  
  • Baier, Christel ; Katoen, Joost-Pieter (2008). Principios de verificación de modelos . Prensa del MIT. ISBN 9780262026499.
  • Clarke, Edmund M .; Grumberg, Orna ; Kroening, Daniel (2018). Model Checking . MIT Press. ISBN 9780262038836.
  • D'Silva, Vijay; Kroening, Daniel ; Weissenbacher, Georg (2008). "Un estudio de técnicas automatizadas para la verificación formal de software" . IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems . 27 (7): 1165– 1178. doi : 10.1109/TCAD.2008.923410 . S2CID 8921624 . 
  • Finkbeiner, Bernd; Torfah, Hazem (2017). "La densidad de propiedades de tiempo lineal". Lecture Notes in Computer Science . Automated Technology for Verification and Analysis. Vol.  10482. Springer.
  • Kern, Christoph; Greenstreet, Mark R. (1999). "Verificación formal en el diseño de hardware: una revisión". ACM Transactions on Design Automation of Electronic Systems . 4 (2). Association for Computing Machinery. doi : 10.1145/307988.307989 . ISSN 1084-4309 . S2CID 13994730 .  

Lecturas adicionales

  • Emerson, E. Allen (1990). "Lógica temporal y modal". Manual de informática teórica . B.
  • Pnueli, Amir (1986). «Aplicaciones de la lógica temporal a la especificación y verificación de sistemas reactivos: Un estudio de las tendencias actuales». En JW Bakker; W.-P. Roever; G. Rozenberg (eds.). Tendencias actuales en concurrencia . Lecture Notes in Computer Science. Vol.  224. Springer. pp. 510–584 . doi : 10.1007/BFb0027047 . ISBN  978-3-540-16488-3.