Reducción de orden parcial

En informática , la reducción de orden parcial es una técnica para disminuir el tamaño del espacio de estados que debe explorar un algoritmo de verificación de modelos o de planificación y programación automatizada . Aprovecha la conmutatividad de las transiciones ejecutadas concurrentemente que dan como resultado el mismo estado cuando se ejecutan en diferentes órdenes.

En la exploración explícita del espacio de estados, la reducción de orden parcial generalmente se refiere a la técnica específica de expandir un subconjunto representativo de todas las transiciones habilitadas. Esta técnica también se ha descrito como verificación de modelos con representantes. ^{[ 1 ]} Existen varias versiones del método, el llamado método del conjunto obstinado, ^{[ 2 ]} el método del conjunto amplio, ^{[ 1 ]} y el método del conjunto persistente. ^{[ 3 ]}

Los conjuntos amplios son un ejemplo de verificación de modelos con representantes. Su formulación se basa en una noción de dependencia independiente . Dos transiciones se consideran independientes solo si no pueden deshabilitar a la otra cuando están habilitadas mutuamente. La ejecución de ambas da como resultado un estado único, independientemente del orden en que se ejecuten. Las transiciones que no son independientes son dependientes. En la práctica, la dependencia se aproxima mediante análisis estático .

Se pueden definir conjuntos amplios para diferentes propósitos estableciendo condiciones sobre cuándo un conjunto de transiciones es "amplio" en un estado dado.

C0${\displaystyle {ejemplo(s)=\varnothing }\iff {habilitado(s)=\varnothing }}$

C1 Si una transición${\displaystyle \alpha }$depende de alguna relación de transición en${\displaystyle amplitud(es)}$Esta transición no se puede invocar hasta que se ejecute alguna transición en el conjunto amplio.

Las condiciones C0 y C1 son suficientes para preservar todos los interbloqueos en el espacio de estados. Se necesitan restricciones adicionales para preservar propiedades más específicas. Por ejemplo, para preservar las propiedades de la lógica temporal lineal , se requieren las dos condiciones siguientes:

C2 Si${\displaystyle enabled(s)\neq ample(s)}$Cada transición en el conjunto amplio es invisible.

C3 No se permite un ciclo si contiene un estado en el que alguna transición${\displaystyle \alpha }$ está habilitado, pero nunca se incluye en ample(s) para ningún estado s en el ciclo.

Estas condiciones son suficientes para un conjunto amplio, pero no son condiciones necesarias. ^{[ 4 ]}

Los conjuntos obstinados no utilizan una relación de independencia explícita. En cambio, se definen únicamente a través de la conmutatividad sobre secuencias de acciones. Un conjunto${\displaystyle T(s)}$es (débilmente) terco en s, si se cumplen las siguientes condiciones.

D0${\displaystyle \forall a\in T(s)\forall b_{1},...,b_{n}\notin T(s)}$, si se ejecuta la secuencia${\displaystyle b_{1},...,b_{n},a}$es posible y conduce al estado${\displaystyle s'}$, luego ejecución de la secuencia${\displaystyle a,b_{1},...,b_{n}}$es posible y conducirá al estado${\displaystyle s'}$.

D1 Cualquiera${\displaystyle s}$es un punto muerto, o${\displaystyle \exists a\in T(s)}$de tal manera que${\displaystyle \forall b_{1},...,b_{n}\notin T(s)}$, la ejecución de${\displaystyle b_{1},...,b_{n},a}$es posible.

Estas condiciones son suficientes para preservar todos los interbloqueos , al igual que C0 y C1 en el método del conjunto amplio. Sin embargo, son algo más débiles y, por lo tanto, pueden dar lugar a conjuntos más pequeños. Las condiciones C2 y C3 también pueden debilitarse aún más con respecto a su configuración en el método del conjunto amplio, pero el método del conjunto obstinado es compatible con C2 y C3.

También existen otras notaciones para la reducción de orden parcial. Una de las más utilizadas es el algoritmo de conjunto persistente/conjunto de reposo. Se puede encontrar información detallada en la tesis de Patrice Godefroid. ^{[ 3 ]}

En la verificación simbólica de modelos, la reducción parcial del orden se puede lograr agregando más restricciones (reforzando las condiciones de guarda). Otras aplicaciones de la reducción parcial del orden incluyen la planificación automatizada.

• Clarke, Edmund M. ; Grumberg, Orna ; Peled, Doron A. (1999). Model Checking . MIT Press.
• Flanagan, Cormac; Godefroid, Patrice (2005). "Reducción dinámica de orden parcial para software de verificación de modelos" . Actas de POPL '05, 32.º Simposio ACM sobre Principios de Lenguajes de Programación . págs. 110–121 . 
• Godefroid, Patrice (1994). Métodos de orden parcial para la verificación de sistemas concurrentes: un enfoque al problema de la explosión de estados (PostScript) (Tesis doctoral). Universidad de Lieja, Departamento de Informática.
• Holzmann, Gerard J (1993). The Spin Model Checker: Primer and Reference Manual . Addison-Wesley. ISBN 978-0-321-22862-8.
• Peled, Doron A. (1993). "Todos de uno, uno para todos: verificación de modelos mediante representantes". Actas de CAV '93, LNCS 697, Springer 1993. págs. 409–423 . doi : 10.1007/3-540-56922-7_34 . 
• Valmari, Antti (1990). "Conjuntos obstinados para la generación de espacios de estados reducidos". Advances in Petri Nets 1990, LNCS 483, Springer 1991. pp. 491–515 . doi : 10.1007/3-540-53863-1_36 .