En informática , la reducción de orden parcial es una técnica para reducir el tamaño del espacio de estados que se buscará mediante un algoritmo de verificación de modelos o de planificación y programación automatizada . Aprovecha la conmutatividad de las transiciones ejecutadas simultáneamente que dan como resultado el mismo estado cuando se ejecutan en órdenes diferentes.
En la exploración explícita del espacio de estados, la reducción de orden parcial suele referirse 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 de conjunto obstinado, [2] el método de conjunto amplio, [1] y el método de 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 separada de dependencia . Dos transiciones se consideran independientes solo si no pueden deshabilitar a otra cuando se habilitan 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 dando condiciones sobre cuándo un conjunto de transiciones es "amplio" en un estado determinado.
C0
C1 Si una transición depende de alguna relación de transición en , 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 bloqueos en el espacio de estados. Se necesitan más restricciones para preservar propiedades más matizadas. Por ejemplo, para preservar las propiedades de la lógica temporal lineal , se necesitan las dos condiciones siguientes:
C2 Si , cada transición en el conjunto amplio es invisible.
C3 No se permite un ciclo si contiene un estado en el que se habilita alguna transición, pero nunca se incluye en las muestras para ningún estado del 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 es (débilmente) obstinado en s, si se cumple lo siguiente.
D0 , si la ejecución de la secuencia es posible y conduce al estado , entonces la ejecución de la secuencia es posible y conducirá al estado .
D1 O bien es un bloqueo, o bien tal que , la ejecución de es posible.
Estas condiciones son suficientes para preservar todos los bloqueos , al igual que C0 y C1 en el método de conjuntos amplios. Sin embargo, son algo más débiles y, como tal, pueden conducir a conjuntos más pequeños. Las condiciones C2 y C3 también pueden debilitarse aún más con respecto a lo que son en el método de conjuntos amplios, pero el método de conjuntos tenaces es compatible con C2 y C3.
Existen también otras notaciones para la reducción de orden parcial. Una de las más utilizadas es el algoritmo de conjunto persistente/conjunto inactivo. Se puede encontrar información detallada en la tesis de Patrice Godefroid. [3]
En la verificación de modelos simbólicos, la reducción de orden parcial se puede lograr agregando más restricciones (reforzamiento de la protección). Otras aplicaciones de la reducción de orden parcial implican la planificación automatizada.
