PDF de programación - PROGRAMACION CONCURRENTE Y DISTRIBUIDA - V.2 Redes de Petri: Análisis y validación.

PROGRAMACION CONCURRENTE Y

DISTRIBUIDA

V.2 Redes de Petri: Análisis y validación.

J.M. Drake

Notas:

1

Capacidad de modelado y capacidad de análisis

El éxito de un método de modelado es consecuencia de su
capacidad de modelar y de la capacidad de análisis:
Capacidad de modelado es la capacidad de describir de forma sencilla

el comportamiento de sistemas complejos sobre los que tenemos
interés.

Capacidad de análisis es la capacidad de deducir características y

propiedades cualitativas y cuantitativas del sistema a partir del estudio
del modelo.

La complejidad de los actuales sistemas, requieren que entre
la fase de concepción o diseño y la fase de realización, se
introduzca una fase de modelado y análisis del modelo que
garantice no pasar a la fase de realización sobre un diseño
erróneo.

Procodis’08: V.2- Análisis y validación de redes de Petri

José M.Drake

2

Notas:

2

Validación y verificación funcional.

Validación o análisis de validez: Determina si el modelo
cumple una serie de propiedades que caracteriza su buen
funcionamiento:
Ausencia de bloqueos
Finitud del espacio de estados.
Ausencia de conflictos
....
Verificación: Se determina a través del modelo si el sistema
satisface la especificación previamente definida.

Requiere una definición formalizada de la la semántica y significado
de cada operación elemental, para poder comprobar los requisitos
propuesto para el sistema.

Procodis’08: V.2- Análisis y validación de redes de Petri

José M.Drake

3

Notas:

3

Propiedades básicas de un sistema concurrente

Vivacidad: permite que ciertas operaciones siempre tienen
posibilidad de ser ejecutadas
Ausencia de bloqueos: El sistema siempre tiene capacidad de
seguir evolucionando
Finitud del espacio de estados: Que garantiza su
implementación con una cantidad limitada de recursos.
Conflictividad: Define los niveles de ambigüedad en la
evolución del sistema
Exclusión mutua: Permite garantizar que ciertas situaciones
no pueden ser alcanzadas simultáneamente.

Procodis’08: V.2- Análisis y validación de redes de Petri

José M.Drake

4

Notas:

4

Vivacidad

Una transición t es viva para un marcado inicial Mo si, y solo si, partiendo
de cualquier marcado M sucesor de Mo, existe una secuencia de disparo σ
que comprenda a t.

∈∀

MRMM

(

,

)

o

:
σ
∃

M

σ

⎯→⎯

t

talM

que

t

∈

σ

Una RdeP es viva si y solo si todas sus transiciones son vivas para Mo

t1

RdeP no viva

5

RdeP viva

Procodis’08: V.2- Análisis y validación de redes de Petri

José M.Drake

Notas:

5

RdeP parcialmente viva

Una RdeP es libre de bloqueos para el
marcado inicial Mo, si y sólo si, para
cualquier marcado M alcanzable desde
Mo, existe al menos una
transición
activada
Una red viva no presenta nunca bloqueo.
Una red sin bloqueos puede ser no viva, y
entonces es parcialmente viva .
Una RdeP es parcialmente viva para el
marcado inicial Mo si y sólo si para
cualquier marcado M alcanzable desde Mo
existe al menos una transición viva y otra
no viva.
Una RdeP es estructuralmente viva si si
existe al menos un marcado inicial Mo
para el que la RdeP es viva.

RdeP parcialmente viva

Procodis’08: V.2- Análisis y validación de redes de Petri

José M.Drake

6

Notas:

6

Ciclicidad

Una RdeP es posee un comportamiento globalmente cíclico para el marcado
inicial Mo, si y solo si, existe una secuencia de disparos que permita
alcanzar el marcado inicial Mo, a partir de cualquier marcado M alcanzable
desde Mo.

∈∀

MRMM

(

,

σ)

∃

tal

Mque

σ

⎯→⎯

M

o

o

La ciclicidad garantiza que no existe subconjuntos finales de marcados, que
contenga conjuntos de marcados mutuamente alcanzables entre sí, y de los
que no es posible alcanzar el estado inicial Mo

Red cíclica

Subred final

Procodis’08: V.2- Análisis y validación de redes de Petri

José M.Drake

7

Notas:

7

Redes limitadas

Una plaza p es K-limitada para el marcado inicial Mo si y solo
existe un número entero K, talque M(p)≤K para cualquier
marcado alcanzable desde Mo.
Se denomina limite de la plaza p al menor entero k que
verifica la desigualdad anterior.
Una RdeP es K-limitada para Mo, si y solo si todas sus plazas
son k-limitadas para Mo.
Una red 1-limitada se denomina red binaria.
El interes de las k-limitación de una red es que garantiza la
finitud de sus marcados alcanzables.
Desde un punto de vista práctico una red k_limitada puede
implementarse con un conjunto de recursos finitos.

Procodis’08: V.2- Análisis y validación de redes de Petri

José M.Drake

8

Notas:

8

Ejemplos de RdeP k-limitadas

P1

a
P4
c

P2

P5

P3

b

P6

d

RdeP 3-Limitada

RdeP binaria

RdeP no limitada

Procodis’08: V.2- Análisis y validación de redes de Petri

José M.Drake

9

Notas:

9

RdeP estructuralmente limitada

Una RdeP es estructuralmente limitada si es limitada para cualquier
marcado inicial y finito.
La limitación estructural es una condición suficiente para la limitación,
pero la limitación estructural no es una condición necesaria para la
limitación.

RdeP limitada para Mo= (0,3,0)
RdeP no limitada para Mo=(0,4,0)

Procodis’08: V.2- Análisis y validación de redes de Petri

José M.Drake

10

Notas:

10

La limitación, vivacidad y ciclicidad son independientes

LVC

LVC

LVC

LVC

LVC

LVC

LVC

LVC

Procodis’08: V.2- Análisis y validación de redes de Petri

José M.Drake

11

Notas:

11

Conflictividad

Una RdeP tiene un conflicto estructural si en ella existe una plaza que tenga mas de
una transición de salida.
Dos transiciones ti y tj están en conflicto efectivo para un marcado inicial Mo, si y
sólo si:
Existe un M∈M(R,Mo) que sensibiliza ti y tj.
Al disparar ti (o tj) el marcado que resulta no sensibiliza la transicion tj (o ti en su caso).
La existencia de un conflicto efectivo representa una ambigüedad en la evolución
del sistema.

Conflicto estructural sin conflicto efectivo

Conflicto estructural y conflicto efectivo

Procodis’08: V.2- Análisis y validación de redes de Petri

José M.Drake

12

Notas:

12

Exclusión mutua

Dos plazas de una RdeP están en exclusión mutua para un marcado inicial Mo,
sin en ningún marcado M∈M(R,Mo) pueden tener testigos simultáneamente.

Una aplicación típica de lugares con
exclusión mutua es el modelado de
recursos compartidos por múltiples
usuarios.

- R Recurso disponible
- R1 recurso tomado por Π1
- R2 recurso tomado por Π2

Procodis’08: V.2- Análisis y validación de redes de Petri

José M.Drake

13

Notas:

13

Relaciones de sincronización

de

( )itσ

disparo

Sea la red marcada <R,Mo> y sea
L(R,Mo) el conjunto de todas las
secuencias
de
transiciones aplicables.
Sea el número e disparos en
la transición ti en la secuencia de
disparo s∈L/(R,Mo) .
Se define el avance sincrónico de
la
la
transición tj en la red marcada
<R,Mo> como el valor máximo
que
las
secuencias de disparo posible,
pueden tomar la diferencia entre el
número de disparo de ti y el de tj:
])
AV

transicion ti

considerando

respecto de

[
(
σσ

t
)(
i

−

todas

(
tMR
,
;

0

,

t

t

j

(

max

MoRL
(

,

σ
∈

)

)

j

=

i

AV(R,Mo;t1,t2) = ∞
AV(R,Mo;t2,t3) = 1

Procodis’08: V.2- Análisis y validación de redes de Petri

José M.Drake

14

Notas:

14

Métodos de análisis de propiedades de RdeP

Métodos estáticos: Conducen a resultados exactos
Análisis por enumeración: Se basan en la construcción de los grafos de

alcanzabilidad que representa los marcados y las secuencias de
disparo.

Análisis por transformación: Se basa en transformar la red en otra mas

sencilla que mantenga las mismas propiedades pero sea mas facil de
analizar.

Análisis estructural: Permite obtener propiedades de la red en función

de la topología de la red y con independencia de los marcados.

Métodos dinámicos: No de muestran propiedades, permiten
conocer la propiedades con niveles de confianza.
Análisis por simulación: Se basa en deducir la evolución de la RdeP

utilizando herramientas que la simulan. Es muy utilizado en redes
especiales (temporizadas, probabilísticas, coloreadas, etc.) para las que
no existen técnicas de análisis exactas

Procodis’08: V.2- Análisis y validación de redes de Petri

José M.Drake

15

Notas:

15

Grafo de alcanzabilidad

Es el grafo en el que cada nudo representa un marcado
alcanzable a partir de Mo, y cada arco el disparo de una
transición.
Se representa un arco etiquetado con tk, que va del nudo Mi al
nudo Mj, si al disparar la transición tk con el marcado Mi se
obtiene el marcado Mj
Si la RdeP es limitada y viva el proceso de construcción del
grafo de alcanzabilidad es elemental. Culmina cuando se han
considerado todas la evoluciones posibles a partir de los
marcados alcanzables.
Si RdeP es no limitada se utilizan el grafo de cobertura

Procodis’08: V.2- Análisis y validación de redes de Petri

José M.Drake

16

Notas:

16

Grafo de alcanzabilidad

(1,0,0,0,0)

a

(0,1,1,0,0)
c

b

d

(0,0,1,1,0)

c

e

e

(0,1,0,0,1)

b

(0,0,0,1,1)

Procodis’08: V.2- Análisis y validación de redes de Petri

José M.Drake

17

Notas:

17

Ejemplo de grafo de marcado

(0,3,0)

(3,0,0)

(1,0,3)

(1,1,1)

(0,0,6)

(0,1,4)

(0,2,2)

Procodis’08: V.2- Análisis y validación de redes de Petri

José M.Drake

18

Notas:

18

Grafo de cobertura

Consiste en un grafo finito que describe la evolución de una
RdeP que no es limitada, y que en consecuencia, no puede
describirse por su grafo de marcados que es infinito.
Se basa en construir el grafo de marcados, y colapsar en un
único marcado genérico, todos aquellos que tienen la misma
evolución futura, aunque se diferencien porque el número de
testigos en ciertas plazas es diferentes en ellos.
Se utiliza el símbolo ω para representar que el marcado de una
plaza es un entero arbitrariament