40. SBAI - Simpósio Brasileiro de Automação Inteligente, São Paulo, Sp, 08-10de Setembrodê 1999
Utilizando redes de Petri multiplexadas na síntese de supervisores de
sistemas a eventos discretos
E.M.M. Costa
A.M.N.Lima
[email protected]
[email protected]
Laboratório de Instrumentação Eletr ônica
Departamento de Engenharia Elétrica
Universidade Federal da Paraíba 58109 -970 Campina Grande. PB. Brasil. Caixa Postal 10.053
Fax: ++55-83-3101015
Resumo - Entre os paradigmas usados na modelagem e síntese
de Sistemas a Eventos Discretos. as Redes de Petri tomaram-se
de grande utilidade . A lógica temporal. por sua vez. tornou-se
usual pela sua grande abrangência. substituindo as linguagens
formais na especificação de comportamentos. Sendo assim. apresentamos aqui. as Redes de Petri Multiplexadas. introduzindoas na modelagem. análise e síntese de SEDs, juntamente com a
C'IL na especificação de comportamentos. para resolver o problema de controle supervisório.
na fase de síntese do supervisor (Barroso 1996, Sreenivas and
Krogh 1992, Sreenivas 1997). Assim, apresentamos aqui uma
nova classe de RP, denominada de Rede de Petri Multiplexada
(RPM) (Costa 1998), a qual pode compactar várias transições
em uma única. com uma função associada, onde os arcos são
independentes, definindo uma multiplexação sobre os mesmo
em seu disparo. Logo , nossa motivação para seu uso. são as
vantagens dela ter as mesmas características (expressividade),
das RP LugarfTransição (LzTr), podendo ser usada nos mesmos
desígnios ; dar-nos uma visão do sistema tendo uma transição
como uma central comandando suas partes ; compactar em fórmulas lógicas as funções de uma RP com Função de Habilitação de Transições (RPFHT). nas subfunções; modelagem direta com as partes de SEDs, que apresentam compartilhamento;
compactar várias transições em uma única, sem perda de informação, facilitando a visualização. e manter a abordagem de Barroso (Barroso 1996). na síntese de supervisores (modificação
mínima nos algoritmos de síntese: AMArA e ACGS. onde. só
há mudanças de transições t por subfunções 7). Também, as
linguagens de RP são válidas para a RPM. podendo usar tanto
as linguagens formais (Hopcroft and Ullman 1979), como a
lógica temporal (LT) (Emerson and Halpern 1986. Abadi and
Manna 1987. Fix and Grumberg 1996. Galton 1987. Grumberg
and Long 1994. Iwanska 1996. Heljanko May, 1997, Knight
and Passino 1990. McMillan 1992. Nicola and Vaandrager 1995,
Ostroff 1989, Racloz and Buchs 1997. Sakalauskaité 1996.
Uchihira and Honiden 1990) na especificação de comportamentos. No caso da LT, especificamente a CTL, não há modificação
no algoritmo APLT. desenvolvido por Costa (Costa 1997).
Keywor ds : Redes de Petri, Controle Supervisório, Lógica Temporal. Sistemas a Eventos Discretos
1 INTRODUÇÃO
Dentre os paradigmas utilizados para a primeira fase da resolução do problema de controle na Teoria de Controle Supervisório (TCS) (Ramadge and Wonham 1982. Wonham 1987.
Ramadge 1989. Ramadge and Wonham 1989. Kumar et ai.
1992). a modelagem. temos as Redes de Petri (RP) (Reisig 1985.
Murata 1989. Reisig 1992). Estas são ferramentas matemáticas
e gráficas que apresentam muitas vantagens em modelagem e
síntese de supervisores de Sistemas a Eventos Discretos (SED)
(Zhou and DiCesare 1993. DiCesare et ai. 1993. Evans 1993,
Freedman 1991. Holloway et alo 1997. Jensen and Rozenberg
1991. Kumar and Holloway 1996. Proth and Xie 1996. Peterson
1981. Desrochers and Al-Jaar 1995. Zhou and DiCesare 1993.
Giua and DiCesare 1994. Balemi et alo 1992). desde que.
seu desenvolvimento teórico se modelou às necessidades básicas como temporização (Cofrancesco et ai. 1991. Baccelli et
ai. 1992. Cohen et ai. 1995. Gaubert et ai. 1995. Gaubert and
Mairesse 1997. Felder et ai. 1995. Nicol and Mao 1991. Cofer
and Garg 1995. Figueiredo 1994). controle de evolução dinâmica
(Krogh 1987. Papelisand Casavant 1992). linguagens (Jantzen
1987, Lilius June , 1993. Lilius September, 1994) e compactação
de subsistemas semelhantes (Jensen 1992. Lilius 1995). Elas já
foram utilizadas tanto na primeira fase da resolução do problema
de controle supervisório (PCS), quanto nas outras duas: pela
característica de definição de uma linguagem associada, para
a especificação de comportamentos (Costa 1997. Uchihira and
Honiden 1990, Jantzen 1987). e peJas características de controle.
Assim, dividimos o artigo como se segue: na seção 2. apresentamos as noções de RP LzTr, RPFHT e CTL; na seção 3 introduzimos o conceito de RPM e suas linguagens; na seção 4 apresentamos o uso das RPM na TCS e os algoritmos de modelagem
. e síntese; na seção 5 exemplificamos seu uso e. concluímos este
trabalho na seção 6.
2 PRELIMINARES
Definição 1 Uma rede de Petri é uma sextupla
RP=(P.T, A,K,W ,Mo) onde:
P={PltP2•...'Pm} é um
533
40. SBAI - Simpósio Brasileirode Automação Inteligente, São Paulo, SP, 08-10 de Setembrode 1999
conjunto finito de lugares; T={t 1,t2,"" t n} é um conjunto finito
de transições; A Ç(P x T)U(T x pré um conjunto de arcos;
K:P -+ NU{oo} é a função de capacidade; W:A -+ N+ é a
. função de ponderação; Mo :P -+ N é a função de marcação
inicial, que satisfaz Vp E P:Mo(p) 5: X(p).
que), F (eventualmente), A (necessariamente), E (possívelmente) e G (sempre). As regras básicas de construção são:
i) uma proposição atômicapEProp é uma fórmula; ii), se],
g são fórmulas, também são [U g,f /\ g, »], X g. Ff abrevia trueUf; Gf abrevia -.F-./; I V 9 abrevia -.(-.1/\ -.g);
I:::> 9 abrevia -'1 V 9 e I<=? 9 abrevia (f :::> g) /\ (9 :::> f).
Estrutura de RP, Erp=(P,T,A,K,W) é uma rede sem marcação
inicial . As regras de disparo de transições para sua evolução
dinâmica são:
2. Semântica: X I é lido como I é verdadeiro no próximo estado, [U 9 é lido como I é verdadeiro até que 9
seja verdadeiro, AI é lido como I é necessariamente verdadeira e AOI é lido como necessariamente I é sempre
verdadeira (ver (Racloz and Buchs 1997, McMillan 1992,
Costa 1997)).
Definição 2 A variação da marcação da rede de Petri segue as
seguintes regras de disparo das transições:
1. Uma transição t é dita estar habilitada (pronta para disparar)
em uma marcação M se e s6 se Vp E P que é entrada de
t:W(p,t) 5: M(P) e Vp E P que é saída de t:M(p) 5:
K(P)-W(t,p);
2. Uma transição habilitada pode ou não disparar;
3. O disparo de uma transição t E T, habilitada na marcação M , é instantânea e resulta em uma nova marcação M' da rede dada pela equação M'(P)=M(P)W(p,t)+W(t,p),'v'p E P;
4. A ocorrência do disparo de t , que modifica a marcação
M da rede para uma nova marcação M', é denotada por
M[t)M' .
Definição 3 Uma rede de Petri com Função de Habilitação de
Transição, é uma qu ádrupla RPFHT=(Erp,I,Mo,ip) em que
é a função que etiE rp é uma estrutura de RP; l:T -+
é um alfabeto; Mo é a marcação
queta as transições, onde
...,t/>m}:R(Erp.Mo) -+{O,l} é a função de hainicial e
bilitação das transições, que mapeia o conjunto de marcações
alcançáveis em ou 1;
3
REDES DE PETRI MULTIPLEXADAS
Definição 6 Uma Rede de Petri Multiplexada, é uma quintupla RPM=(Erp,RA,RT,Mo,iI!)onde: E rp é uma estrué a função que etiqueta os artura de RP; RA:A -+
é um alfabeto; RT : T -+
é a função
cos, onde
que etiqueta as transições; Mo é a marcação inicial e
iI!={1/Jv...,'l/Jd:R(Erp, Mo, RA, RT) -+{O,l} é a função de habilitação das transições para o conjunto de arcos da rede.
As funções 'l/Jk, são funções referentes às transições t», compostas por subfunções TI(M(Pj),Wiai), formadas por if... then
(:::}), dependentes da marcação do lugar Pj, que
o arco
ai (arco entre uma transição e um lugar), e ui; é o peso deste
arco. Os índices i, i. k e L são as cardinalidades de A, P, T e T
respectivamente, onde 1 depende de T entre os lugares e os arcos a que estas subfunções se ligam. Então, 'l/Jk é definida por
'ljJk(TI(M(Pj),Wiai))=V TI(lv.f(Pj),Wiai).
I
a
Com a introdução das funções de multiplexagem , habilitação
de uma transição para um conjunto de arcos que a ela se liga é
dada por:
°
Sua regra de disparos de transições é:
Definição 7 A ma rcação de uma Rede de Petri Multiplexada,
varia de acordo com a seguinte regra de disparos de transições:
Definição 4 O estado, ou marcação, de uma RPFHT varia de
acordo com a seguinte regra de disparo das transições:
1. Uma transição tk é dita estar habilitada (para disparar)
na marcação M, para um arco ai, se e somente se:
VPj E P que é entrada de tk:W(Pj, tk) 5: M(pj),
VPj E P que é saída de tk:M(Pj) 5: K(pj)-W(tk,Pj) e
'l/J k (TI (M (Pj ),Wiai) )=1
1. Uma transição tj é dita habilitada (para disparar) em M se
e s6 se Vp E P que é entrada de tj :W(p, tj) 5: M(P); Vp E
P que é saída de tj:M(p) 5: K(P)-W(P, tj) ; t/>j=l;
2. Uma transição tk habilitada, pode ou não disparar;
2. Uma transição habilitada pode ou não disparar;
3. O disparo de uma transição tk E T, habilitada na marcação
M, é instantânea e resulta em uma nova marcação M' , dada
pela equação M'(pj)=M(pj)-W(Pj,tk)+W(tk,pj),'v'Pj E
P;
3. O disparo de uma transição tj E T , habilitada na marcação
M , é instantânea e resulta em uma nova marcação M' dada
pela equação M'(P)=M(P) -W(p,tj)+W(tj,p),Vp E P;
4. A ocorrência do disparo de tj, que modifica a marcação
M da rede para uma nova marcação M', é denotado por
M[t)M'.
4. A ocorrência do disparo de tk, que modifica a marcação
M da rede para uma nova marcação M', é denotada por
M[tk)M'.
Definição 5 Computation Tree Logic - CTL
Observamos que, nesta nova classe de RP, a marcação da rede
varia com a função da transição que define quais arcos devem
.ser acionados, de um conjunto de lugares para outro. Assim,
esta rede difere das demais, por que, quando uma transição dispara, não depende de todo o conjunto de lugares de entrada e de
1. Sintaxe: Fórmulas CTL são construídas a partir de um conjunto de proposições atômicas Prop={Pl ,...}, conectivos
l6gicos V, /\, -. e operadores temporais X (próximo), U (até
534
40. SBAI - Simpósio Brasileirode Automação Inteligente, São Paulo, SP, 08-10 de Setembrode-1999
·'
ts, onde ts desabilita os arcos a6 e as, procedendo ao que faz a
função tps da RPFHT.
(a)
3.1
RPM
Uma RPM tem uma linguagem associada representada por seqüências de disparos das transições, associando as palavras com
as subfunções dadas em suas transições, juntamente com transições (caso sempre 7/J=I). definindo um caminho que nos leva
de uma marcação para outra, denotada por M[S>M' , onde S
é uma palavra, pertencente ao conjunto de transições t E T e
de subfunções T E 7/J. formada de acordo com as regras 'da teoria de linguagens formais. Na figura 2 temos uma RPM e sua
linguagem.
.
'
,.,
11,1
(ç)
lJ
4 TCS E ALGORITMOS
A idéia apresentada por Barroso (Barroso 1996). é sintetizar um
supervisor para um SED modelado por uma RP LzTr, onde, com
a análise da árvore de alcançabilidade da mesma, gerada pelo
AMArA, e com a especificação de comportamento, determinamos funções de habilitação de transições, pelo ACaS , para
criar a RPFHTsupervisora que tem a mesma estrutura da RP
que modela o SED. Assim, usando o mesmo procedimento, e
uma RPM como modelo do sistema, criamos outra RPM que
irá supervisioná-lo. Logo, modelamos o SED e, a partir deste,
geramos a árvore de alcançabilidade, definimos a 'tarefa a ser
executada em CTL, como feito em Costa (Costa 1997), e sintetizamos o supervisor, resolvendo o PCS. Logo, os algoritmos de
modelagem e síntese por RPM, são: .
Figure 1: Exemplo 1
P,
saída da transição e toda transição tem uma função lógica associada. Se esta não aparece, a mesma tem valor sempre verdadeiro
(7/J=I), e está sempre habilitada para todos os seus arcos. Com
este valor, o lugar que recebe um arco tem capacidade infinita,
se não for declarado. De outra forma, a função capacidade normalmente é definida na própria função 7/J. Todas as propriedades
das RP Ltrr são válidas para as RPMs, só que em relação às subfunções T que compõem as funções 7/J. Também, vemos que a
RPM pode incluir uma função de habilitação de transição como
umaRPFHT.
Algoritmo 1 Algoritmopara Modelagemde SEDs
1. Para cada parte (máquinas, esteiras, buffers, lugares de armazenamento de recursos, lugares de entrada de material
para processamento, lugares de saída do produto final, etc.)
do SED, crie um lugar;
2. Para cada evento, crie uma subfunção T, da seguinte forma :
a) Coloque as condições que levam o evento a acontecer;
Na figura I(a), temos uma RPM, com suas equivalentes RPFHT
(fig. 1(b» e RP Lffr (fig. 1(c». Na RP Lffr. temos
capacidade em alguns lugares, o que impede das transições
h e ts dispararem, quando esta marcação é alcançada. Na
RPFHT, as funções ligadas a estas transições são definidas por
tpl=[M(Pd<4] e tps=[M(P4)<5], e garantem suas desabilita ções, eliminando a função de capacidade. Na RPM, temos uma
compactação das transições da rede . As funções definidas para
suas transições são dadas por
7/Js={(M(P4)=4 V M(ps)=O)
=}
b) Determine quais as subfunções que irão formar as multitransições associadas ;
c) Coloque os arcos que ligam o evento às partes do sistema no acontecimento do mesmo, com as respectivas multitransições e una os lugares com a transição t
pelos respectivos arcos;
d) Una as subfunções T com funções lógicas OR (V) e faça
a função 7/Jk' referente a cada multitransição;
3. Coloque a marcação inicial para o sistema.
tS:-.(a6 1\ as)} e,
7/J2={(M(pI)=3 =} -.t2) V (M(ps)=O
=}
Linguagens de RPMs
t2:-.aS)} .
Algoritmo 2 Algoritmoda Arvore de Alcançabilidade
Vemos que as funções das transições t2 e ts (7/J-i e 7/Js respectivamente), são constituídas por subfunções T, formadas por
=}, que dependem das marcações em alguns lugares, e dos arcos ligados a estas transições. Então , as funções eliminam a
função de capacidade e compactam a rede. Assim, na marcação
Mo = [2000]T, as transições habilitadas são tI e t2. e t2 vale
só para o arco' a4, o que equivale a transição tI da RPFHT, e
na marcação M = [OOI4]T, as transições habilitadas são tz e
. Passo 1) Rotule a marcação inicial Mo de raiz e sinalize-a com
f1ova;
Passo 2) Enquanto houver marcações nova, faça:
1. Escolha uma nova marcação M ;
535
40. SBAI - SimpósioBrasileiro de Automação Inteligente, São Paulo, Sp, 08-10de Setembro de 1999
2. Se M for idêntica a outra marcação no caminho da raiz até
M, sinalize-a com antiga e vá para uma outra marcação;
O passo 5 se processa da seguinte forma:
3. Se nenhuma transição que tenha uma função 'I/J que esteja
com todos os valores de suas subfunções 7 falsos em M, '
sinalize-a como bloqueada;
Algoritmo 4 Passo 5 do ACGS
• Dados o gerador trim e o gerador H (especificação), faça:
4. Enquanto existirem transições com funções respectivas 'I/J e
subfunções 7 verdadeiras em M, para cada transição habilitada, faça o seguinte:
I. Adicione à lista-bloc os estados que não satisfazem
L: (H (x)) n s, ç L: (x);
2. Para cada estado xi, na lista-bloc, adicione à lista-bloc :
i) Obtenha a marcação M' que resulta do disparo da transição t com um valor verdadeiro em uma das subfunções 7 de 'I/J em M ;
a) os estados zq : (30'u E L:u)Xi=Ç(lTu,Xj);
b) os estados Xk : (30'c E L: c) Xi=Ç (O'c,Xk)/\Xk
ii) Se no caminho da raiz até M' existir uma marcação Mil
tal que M'(p)
M"(P) para cada lugar p M' :f=
Mil , então substitua M' (P) por w para cada p tal que
e
1L:(Xk)l=l;
rt X m /\
.
3. Encontre a componente acessível do gerador resultante.
M'(P»M"(P);
ili) Introduza M' como um nó, desenhe um arco com rótulo t (caso sua função associada 'I/J sempre tiver valor
padrão 1), ou 7 (caso a transição t tenha uma função 'I/J
composta por subfunções 7), de M para M' e etiquete
M' com nova;
.
Temos que, neste algoritmo falamos de transições, e não de subfunções. Porém, da mesma maneira que dizemos que uma transição está habilitada, é para um determinado conjunto de subfunções 7 que a compõe, o mesmo deve ser visto considerandose as funções 'I/J das transições.
Neste algoritmo usamos t quando sua função associada é sempre 'I/J=1 (não há etiquetamento da função na transição). Caso
contrário, colocamos a subfunção que muda a marcação.
5
Algoritmo 3 Algoritmo para a Construção da Suprema Linguagem Controlável
1. Criar uma lista dinâmica, lista-bloc, e incluir na mesma os'
estados ou marcações bloqueadas, incluindo as marcações
do tipo não-permitida, onde M:M[tj>O é uma marcação
bloqueada e M :M(Pi)=W é uma marcação não-permitida;
20 Adicionar à lista-bloc os estados, não marcados, cuja única
transição habilitada, se disparada, leva o sistema a um estado bloqueado, ou seja, M:M[tj>M', tj é única transição habilitada em M,M rt Qm e M' Elista-bloc ;
3. Criar uma lista, lista-perigo, com os estados antecessores
dos elementos (estados) da lista-bloc, juntamente com o
evento que os liga, desde que o antecessor não esteja na
lista-bloco Esses eventos deverão estar sempre desabilitados quando o sistema se encontrar nesses estados, ou .
seja, 3{3 E L: cJl(tj)={3 e M[tj>M', eM rtlista-bloc e
M' Elista-bloc;
EXEMPLO DE APLICAÇÃO
Seja o sistema de manufatura, visto na figura 3(a), o qual é um
ambiente em que temos um braço robótico central (megatran- .
sição t) programado para estar levando itens de um lugar para
outro, usando recursos do sistema (lugar P7) , executando tarefas. Pelo algoritmo 1, modelamos o sistema por uma RPM (fig.
3(b». Podemos ver como a RPM nos dá a forma de ver o sistema igual ao ambiente real, resolvendo a primeira fase do PCS.
·Vemos no modelo, que o sistema tem seis usuários e oito recursos disponíveis, onde os usuários compartilham estes recursos
(que são indistinguíveis), e estes são limitados a um máximo de
cinco por usuário. Então, as fichas do lugar P1 são as peças que
serão processadas pelas outras estações (lugares ]J2,P3,P4,P5 e
P6), e o lugar P7 contém as ferramentas para processar os itens
(fichas em P1). Temos que, para o fim do processamento de uma
peça, o SED está com cinco ferramentas em uso. Após o término deste, todas elas são devolvidas. Também vemos que mais
de uma peça pode ser processada em paralelo. Mas, para o estado inicial do sistema, M o=[6000008]T , temos um bloqueio se
seguirmos a seqüência 7172717271717373727371, onde seu estado será M'=[l203000]T, e neste a função
'Ij; =
(«M(P1)
«M(P3)
«M(P4)
«M(ps)
4. Adicionar à lista-perigo os estados nos quais exista pelo
menos uma transição habilitada, etiquetada por um evento
não controlável, cujo disparo da transição leve o sistema para uma marcação na lista-bloc, ou seja 30: E
L:u,l(tj)=O: e M[tj>M',M' Elista-bloc;
1/\ M(P7) 1) => t : a1/\ a12/\ a3)V
1/\ MCP7} 2) => t : a2/\ 2a12/\ as)V
1) => t : a4 /\ all /\ a7)V
1/\ M(P7) 3) => t : a6 /\ 3a12 /\ a9)V
1) => t : as /\ 5all /\ alO)}
da transição t é falsa para todas as subfunções que a compõe (71,
respectivamente).
... , 7S,
5. Dada a especificação desejada para o sistema, encontre a
suprema linguagem controlávet- SupC(L);
o algoritmo 2 nos dá a árvore de alcançabilidade deste modelo
que tem 162 marcações distintas alcançáveis. Nosso interesse,
é a marcação M=[0000068]T, isto é, todos os usuários completaram a tarefa . Logo, damos como especificação de comportamento: todas as peças devem ser processadas, até no máximo, duas em paralelo . Em CTL , temos Al71/\ G/(71U7'i) /\
X(-"T1 UA /75).
6. Adicionar à lista-perigo os estados e seus respectivos eventos de saída a serem desabilitados para que a linguagem
executada, desde que estes estados não estejam ainda na
lista-perigo, ou seja, 3{3 E I: cJl(t j )={3 e M[tj>M', e
M rtlista-perigo e M' rt G(Sup C(L)) .
536
40. SBAI - Simpósio Brasileirode Automação Inteligente, São Paulo, Sp, 08-10 de Setembrode'1999
A execução do ACGS (algoritmo 3), dá-nos a lista-perigo vista
O . O
na figura 4. Nela, temos todos os estados que não podem
ser alcançados, os quais levam o sistema a bloqueio. Pela especificação de comportamento dada, vemos que a mesma não
se encontra na lista-perigo, o que quer dizer que temos uma
seqüência aceitável que não leva o sistema a bloqueio se a
subfunção TI for modificada, de tal forma que a RPM siga
sempre uma das seqüências: (TITIT2T2TSTST4TST4TS)* ou
0""""
,,2
MlquW I
g
R
8
==
'O
lUqoW'
(a)
D
Bnço-
(TITIT2T2TST4TSTST4TS)* '
Logo, ficamos com uma nova RPM, igual na estrutura, mas que
tem só a subfunção TI diferente no valor de teste sobre o lugar
P7, dada pOfTl=(M(pl)
=> t :al A a12 A as.
Esta, impede que o sistema pare de operar, fazendo a tarefa
como requerido. Com isto, vemos que a RPM pode ser usada na mesma abordagem de Barroso (Barroso 1996) utilizando
como especificação de comportamentos, a CTL, como em Costa
(Costa 1997). Vemos também, que a estrutura para análise visual não aparenta simplicidade, pois que a rede trabalha como se
estivéssemos numa central de comandos, nos comunicando com
cada parte do sistema, onde mandamos e recebemos mensagens.
6
CONCLUSÃO
(b)
Figure 3: Sistema de manufatura com um braço robótico e modeloemRPM
Introduzimos aqui o uso da RPM na resolução do PCS, onde
encontramos, como em todos os métodos, vantagens como: a
mesma expressividade, das RP Llfr, a visualização do sistema
como um sistema centralizado enviando comandos às partes do
sistema, a compactação em fórmulas lógicas das funções de
habilitação de .transições das RPFHT, modelagem direta com
as partes de' SEDs que apresentam compartilhamento, a compactação de transições sem perdas de informação, facilitando a
visualização, e abordagem igual a de Barroso (Barroso 1996) , na
síntese de supervisores, desde que os algoritmos de sín tese não
têm grandes diferenças, além de podermos usar tanto as linguagens formais como a CTL na especificação de comportamentos
e, desvantagens, as quais são em termos de análise de evolução
dinâmica, pois há a necessidade da avaliação das funções das
transições', como as RP de alto nível. Logo, temos que o uso da
RPM é também um paradigma válido para a TCS.
Eventos a
dtsabiliUt
"1
u'::.f<'
Mmtaç6es
plp2D3p4pSp6p1
Eventos.
dcs:1bili1U
2 4 0 0 0 0 4
23 10 0 02
2301003
1400014
I 3 1 O O I 2
1 3 O I O I 3
11110 2 2
1 1 02023
11
MIlC3Ç6cs
pl p2p3p4pSp6p7
2 310002
23 0 1 0 0 3
I 3 I OO I 2
1 3 O1 O I 3
0310022
0301023
O I I I O3 2
0 10 20 33
I I I I O 2 2
110 20 23
l
I
I
't1
1:'1
Figure 4: Lista das marcações e eventos a serem desabilitados
Isaac New ton Institute (Cambridge UniversityPress l. GunawarEd.).
dena
Costa, E. M. M. (1997). Contribuiçãoao uso da lógica temporal na especifica ção de comportamentos de sistemas a eventos discretos.
Master's tbesis. Universidade Federal da Paraíba · Campus II Campina Grande, Paraíba, BR.
REFERÊNCIAS BIBLIOGRÁFICAS
Abadí, M. and Z . Manna (1987). Temporal logic programming. Proceedings 1987 Symposium on Logic Programming pp. 4-1 6.
Costa, E. M. M. (1998). Sintese de Supervisores para Sistemas a Even-
Baccelli, F., G. Coben and B. Gaujal (1992). Recursive equations and
basic properties of timed petri nets. Discrete Event Dynamical
Systems: Theory and Applications pp. 415-439.
tos Discretos: Uma Abordagem via Redes de Petri Multiplexadas.
Relatório de Projeto e Pesquisa. UniversidadeFederal da Paraíba,
COPELE, Campina Grande, PB, Brasil.
Balerni, S., Kozák, P. and R.Smedinga, Eds.) (1992). Discrete Event
.
Systems: Modeling and Control. Birkhãuser - Proceedings of a
Joint WorksbopHeld in Prage.
Desrocbers, A. A. and R. Y. Al-laar (1995). Applications of Petri Nets
in Manufacturing Systems: Modeling, Control, and Performance
Anaiysis. IEEE Press.
Barroso, G. C. (1996). Uma Nova Abordagem para a Síntese de Supervisoresde Sistemas a Eventos Discretos. PhD thesís. Universidade
Federal da Paraíba - Campus n. Campina Grande, Paraíba - BR.
DiCesare, F., G. Harbalakis, l. M. Protb, M. Silva and F. B. Vernadat
(1993) . Practice of Petri Nets in Manufacturing, Cbapman and
Hall .
Cofer, D. D. and V. K. Garg (1995). Supervisory control of real time
discrete-event systems sing lattice tbeory. IEEE Transactions 011
Automatic Contro141(2), 199-209.
Emerson, E. A. and J. Y. Halpem (1986). "sometimes" and "not never"
revisited: on brancbing versus linear time temporallogic. Journal
oftheACM33(1),151-178.
Cofrancesco, P., A. Cristoforetti and R. Scattolini (1991). Petri nets
based approacbto softwaredevelopment for real-timecontrol. IEE
Proceedings-D Control The01Y and Applications 138(5), 474478.
.
Evans, J. B. (1993). The Devnet: a Petri Netfor Discrete Event Simulation . Springer-Verlag.
Felder, M., A. Gargantini and A. Morzenti (1995). A tbeory of implementationand refinementin timed petri nets.Tecbnicalreporto PoIitecnico di Milano.
Coben, G., S. Gaubert and J. P. Quadrat (1995). AIgebraic system
analysis of timed petri nets. In : Idempotency - Collection of the
537
40. SBAI - Simpósio Brasileirode Automação Inteligente, São Paulo, Sp,08-10 de Setembrode 1999
Figueiredo, J. C. A. (1994) . Redes de Petri com Temporização Nebulosa. PhD thesis. Universidade Federal da Paraíba - Campus II.
Campina Grande, Paraíba - BR.
. Fix, L. and O. Grumberg (1996). Verification of temporal properties.
Ioumal ofLogic anti Computation 6(3), 343- 361.
Murata, T. (1989) . Petri nets: Properties, analysis and applications. Proceedings ofthe IEEE 77(4), 541-580.
Nicol, D. M. and W. Mao (1991). Automated parallelization of timed
petrí-net simulations. In: Proceedingsofthe 1991 WinterSimulation Conference.
Freedman, P. (1991). Time, petri nets, and robotics.IEEE Transactions
on Automatic ControI7(4), 417-433.
Nicola, R. De and F. Vaandrager (1995). Three logics for branching
bisimulation. Joumal ofthe ACM 42(2),458-487.
Galton, A. (1987). Temporal Logics anti their Applications. Academic
Press.
Ostroff, J. S. (1989) . Temporal Logic for Real-Time Systems. Research
Studies Press Lld.
Gaubert, S. and J. Mairesse (1997) . Modeling and analysis of timed
petri nets using heaps of pieces. To appear on the IEEE Transactions on Automatic Control.
Papelis, A. and T. L. Casavant (1992) . Specification and analysis ofparallelldistributedsoftware and systems by petri nets with transition
enabling functions. IEEE Transactions on Software Engineering
.
Gaubert, S., J. P. Quadrat and G. Cohen (1995) . Asymptotic throughput
of continuous timed petri nets. In: Proc. Of the 34th Conference
on Decision and Control, New Orleans.
Giua, A. and F. DiCesare (1994) . Blocking and controllability of petri
nets in supervisorycontroI.IEEE Transactionson Automatic ControI39(4), 818-823.
Grumberg, O. and D. E. Long (1994 ). Model checking and modular
verification. ACM Transactions on Programming Languages anti
Systems 16(3), 843-871.
Heljanko, K. (May, 1997) . Model checking the branching time temporal
logic ctl. TechnicalReport 45. Helsinki University of Technology
- Otaniemi, Finland.
18(3),252-261.
Peterson, J. L. (1981). PetriNet Theory anti Modeling ofSystems. Prentice Hall.
Proth, J-M and X. Xie (1996). Petri Nets: A Toolfor Design and Management ofManufacturingSystems. John Wiley e Sons Ltd.
RacIoz, P. and D. Buchs (1997) . Symbolic proof of ctl formulae over
petri nets. Technical reporto C.U.I. University of Geneva.
Ramadge, P. J. G. (1989). Some tractable supervisory control problems for discreteevent systems modeled by büchi automata. IEEE
Transactions on Automatic CdntroI34(l), 10-19.
Ramadge, P. J. G. and W. M. Wonham (1982). Supervision of discrete
event processes. Procedings of21st Conference on Decision anti
Control pp. 1228-1229.
Holloway, L. E., B. H. Krogh and A. Giua (1997). A survey of petri
net methods for controlled discrete event systems. Discrete Event
Systems: Theory and Applications pp. 131-190.
Ramadge, P. J. G. and W. M. Wonham (1989). The control of discrete
event systems. Proceedings ofthe IEEE 77(1 ),81-98.
Hopcroft, J. E. and J. D. Ullman (1979 ). Introductionto Automata Theory, Languages and Computation. Addison-Wesley, USA.
Reisig, W. (1985) . Petri Nets: an Introduction. Springer-Verlag Berlin
Heidelberg.
Iwanska, L. (1996) . Natural (language) temporal logic: Reasoning
about absolute and relative time. Intema tional Journal of Expert
Reisig, W. (1992). A Primer in Petri Net Design. Springer-Verlag.
Sakalauskaité, J. (1996) . Nonclasual resolution system for branching
temporal logic. Technical reportoInstitute of Matematics and Informatic. Lithuania.
Systems 9(1) , 113-149.
Jantzen, M. (1987). Language theory of petri nets, central models and
their properties. In: Advances in Petri Nets, Lectures Notes in
ComputerSciences. pp. 397-412.
Sreenivas, R. S. (1997). On the existence of supervisory policies that
enforces liveness in discrete-event dynarnic systems modeled by
controlled petri nets, IEEE Transactions on Automatic ControI
Jensen, K. (1992) . Coloured Petri Nets - Basic Concepts, Analysis
Methods and Practical Use. VoI. 1 : Basic Concepts, SpringerVerlag.
42(7), 928-945.
Sreenivas, S. R. and B. H. Krogh (1992). On petri net models of infinite state supervisors. IEEE Transactions on Automatic Control
Jensen, K. and G. Rozenberg (1991) . High Levei Petri Nets Theory and
Applications. Springer Verlag.
37(2),818-823.
. Knight, J. F. and K. M. Passino (1990). Decidability for a temporallogic
used in discrete-event system analysis. IntemationaI JoumaI of
ControI52(6), 1489-1506.
Uchihira, N. and S. Honiden (1990) . Verificationand synthesis of concurrent programs using petri nets and temporal logic. Technical
reporto Institute for New Generation Computer Technology.
Krogh, B. H. (1987) . Controlled petri nets and maximally permissive
feedback logic. In: 25th AnnuaI Allerton Conference. University
oflllinois Urbana, USA. pp. 317-326.
Wonham,P.J. G. Ramadge E W. M. (1987) . Modular feedback logic for
discrete event systems. SIAM JoumaI ofControl and Optimization
Kumar, R. and L. E. Holloway (1996). Supervisory control of deterministic petri nels with regular specification languages. IEEE Transactions on Automatic ControI41(2), 245-249.
Zhou, MC. and F. DiCesare (1993). Petri Net Synthesis for Discrete
Event ControlofManufacturing Systems. Kluwer Academic PubIishers.
25(5), 1202-1218.
Kumar, R., V. Garg and S. I. Marcus (1992). On supervisory control
of sequential behaviors, IEEE Transactionson Automatic ControI
37(12), 1978-1985.
Lilius, J. (1995). On The Structure of High-Level Nets. PhD thesis.
Helsinki University of Technology - Otanierni, Finland.
Lilius, J. (June, 1993). A sheaf semantics for petri nets. Technical Report 23. Helsinki University ofTechnology - Otaniemi, Finland.
Lilius, J. (September, 1994). On the folding of algebraic nets, Technical
Report 30. Helsinki University ofTechnology - Otaniemi, Finland.
McMillan, K. L. (1992). Symbolic Model Checking: An Approach to
the State Explosion Problem. PhD thesis. Carnegie Mellon University.
538