g
y
p
Lógica Modal Aplicada
a Grafo a Eventos
Modal Logic Applied to Events Graph
JOSÉ CARLOS MAGOSSI
Universidade Metodista de Piracicaba e
Faculdade de Tecnologia de Americana (CEETEPS)
[email protected]
RESUMO – O objetivo deste texto é mostrar uma aplicação de um sistema lógico modal, denominado sistema lógico NK,
na modelagem de grafos a eventos (classe particular de redes de Petri). Esses modelos lógicos de grafos a eventos aplicamse, por sua vez, em análise de especificações de sistemas dinâmicos a eventos discretos. Dada uma especificação (descrição
de alguma restrição do sistema), utiliza-se das ferramentas advindas do sistema lógico NK, particularmente o método
tableau analítico, para verificar se a especificação é satisfeita ou não no sistema modelado. Após noções sobre grafo a
eventos, sistema lógico NK e a relação entre eles, um exemplo simples é exposto ao final. A principal característica deste
texto consiste em explicar o processo de modelagem de grafo a eventos por meio de fórmulas do sistema lógico NK de
maneira sucinta, sem abusar de demonstrações, esperando, com isso, que o estudante iniciante possa adquirir algum
conhecimento em questões que envolvam lógica e grafo a eventos.
Palavras-chave: LÓGICA MODAL – TABLEAUX – REDES DE PETRI – GRAFO A EVENTOS – SISTEMAS DINÂMICOS – EVENTOS
DISCRETOS.
ABSTRACT – The objective of this paper is to show how we can apply modal logic, named NK-logical system, to events
graphs (particularly class of Petri nets). Those events graphs logical models are applied in turn to the verification of specification of discrete event dynamic systems. Given an specification (a description of a certain system constraint), we are
able to use tools taken from the NK-logical system (especially analytic tableau) to verifies if the specification is satisfiable
or not in the modeled system. After showing notions of events graph, NK-logical system and the relation between them,
we present in the end a simple example. Our aim is to explain the events graph modeling process in a direct way rather
than through many proofs. We hope with this that beginners will be able to get some knowledge on logic and eventsgraph related matters.
Keywords: MODAL LOGIC – TABLEAUX – PETRI NETS – EVENTS GRAPH – DYNAMIC SYSTEM – DISCRETE EVENT.
REVISTA DE CIÊNCIA & TECNOLOGIA • V. 8, Nº 16 – pp. 65-76
65
g
y
p
INTRODUÇÃO
E
ste texto tem por objetivo explicar o processo
de modelagem de grafo a eventos via lógica
modal. Tais modelos aplicam-se em sistemas
de manufatura, automação industrial etc. Como as
aplicações desses modelos lógicos são direcionadas a
sistemas dinâmicos, num primeiro momento, é feito
um breve relato sobre sistemas dinâmicos e análise
de verificações em sistemas dinâmicos a eventos discretos. Na seqüência, são abordados grafos a eventos, o sistema lógico NK, a relação entre eles e, ao
final, faz-se uma aplicação a sistemas dinâmicos a
eventos discretos.
Sistemas Dinâmicos
Um sistema pode ser descrito como um aglomerado de coisas; ele é dinâmico se houver uma
evolução delas com o passar do tempo. Os sistemas
dinâmicos podem ser divididos em duas classes:
contínuos e discretos (Cassandras, 1993). Os sistemas contínuos são aqueles cuja evolução é medida
em função de componentes contínuos (como o
tempo) e sistemas discretos têm a sua evolução
medida em função de componentes discretos. Um
sistema caracterizado, por exemplo, pelo fluxo de
óleo em uma tubulação será um sistema contínuo se
a quantidade de fluído for o fator de sua evolução.
Já um sistema de montagem de peças, em uma
fábrica de cadeiras, será discreto se o número de
cadeiras montadas for o fator de sua evolução.
Entre os sistemas dinâmicos discretos estão aqueles
cuja dinâmica é dirigida pela ocorrência de eventos
discretos, chamados sistemas dinâmicos a eventos
discretos (SDED) (Baccelli et al., 1991 e Cohen et
al., 1989).
A ocorrência de um evento pode ser entendida como o acontecimento de uma situação declarativa, ou seja, algo que pode ser identificado como
ocorrido, ou não ocorrido, como sim, ou não. Um
evento é um acontecimento instantâneo, que não
tem tempo, apenas caracteriza um marco entre o
acontecer e o não acontecer. Exemplos de eventos
bastante simples: ligar a chave de uma máquina,
desligar a chave de uma máquina, aberto ou
fechado, quebrado ou não quebrado etc. Sistemas
cuja dinâmica é dirigida pela ocorrência de eventos
são muito difundidos atualmente, por conta da
66
quantidade de situações nas quais predomina o
caráter discreto, como no caso de redes de computadores, sistemas de manufaturas, automação industrial etc. Em resumo, qualquer sistema envolvendo
uma quantidade discreta de componentes, de tal
forma que a evolução seja medida em função da
ocorrência de eventos discretos, é denominado sistema dinâmico a eventos discretos.
Uma questão importante relacionada aos
modelos de SDED é a capacidade deles de desempenhar tarefas que sirvam para verificar especificações do sistema. A verificação de especificações em
sistemas dinâmicos significa analisar se determinada
condição (restrição ao sistema) é satisfeita ou não no
sistema. Por exemplo, um SDED que representa
uma seqüência de máquinas numa fábrica com a
seguinte restrição: a máquina de número 4 não
pode iniciar suas operações antes que as máquinas
de números 1, 2 e 3 tenham terminado suas tarefas.
Esse é um caso de restrição, que pode representar,
entre outros, uma fábrica de cadeiras em que a
máquina 4 faz a montagem final da cadeira e a
máquinas 1, 2 e 3 fazem o assento, a base e o
encosto, respectivamente.
O processo de verificação de especificações
consiste na análise da satisfação ou não de certa
especificação do sistema, tendo um modelo como
base. No exemplo citado, independentemente da
ferramenta escolhida para a modelagem, deve-se
contemplar a restrição, sob pena de se ter cadeiras
sem encosto, cadeiras sem assento etc. No entanto,
algumas especificações podem não estar tão explícitas e só no decorrer do processo de manufatura (ou
automação) se percebe que alguma condição tem de
ser satisfeita. Por isso, o desenvolvimento de ferramentas capazes de fazer análise é muito útil e difundido atualmente.
O estudo aqui apresentado fundamenta-se,
para as aplicações práticas, na análise de sistemas
dinâmicos a eventos discretos. Nesse processo, devese primeiramente definir o processo de modelagem
do sistema dinâmico, ou seja, a linguagem utilizada
para descrever os sistemas dinâmicos envolvidos, e, a
partir daí, fazer a análise de verificações.
Existem muitas maneiras de se modelar sistemas dinâmicos; a utilizada neste trabalho fundamenta-se em grafo a eventos. O sistema lógico NK (a
Dezembro • 2000
g
y
p
ser exibido) servirá de ferramenta de análise de
verificações, partindo de modelos via grafo a eventos.
um grafo a eventos, com dois lugares e três transições. Os lugares são denotados por p1 e p2. As transições são denotadas por t1, t2 e t3.
Fig. 1. Grafo a eventos.
DESENVOLVIMENTO
Os modelos baseados em redes de Petri foram
desenvolvidos por C.A. Petri, em 1962, e podem ser
encontrados em textos de Peterson (1981), Murata
(1989) e Cassandras (1993). Desde então, muito se
tem desenvolvido no que diz respeito a redes de
Petri, principalmente pela versatilidade de análise
que essa técnica matemática de representação de sistemas permite, incluindo a modelagem de sistemas
paralelos, não determinísticos, assíncronos, concorrentes etc. Este trabalho se interessa por uma classe
particular de redes de Petri, denominada Grafo a
Eventos, útil na modelagem de sistemas a eventos
discretos (Cassandras, 1993; Peterson, 1981; e
Murata, 1989).
No presente estudo, os grafos a eventos
podem ser vistos como constituídos de cinco elementos fundamentais: um conjunto de lugares, um
conjunto de transições, um conjunto de arcos, uma
marcação inicial e uma temporização. Os lugares
são utilizados para representar o estado do sistema e
as condições que habilitam as ocorrências dos eventos. As transições estão associadas aos eventos. Em
grafos a eventos temporizados, as ocorrências de
eventos relacionam-se aos disparos das transições.
Costuma-se rotular um tipo de evento pelo nome
da transição correspondente.
Para que uma transição dispare,1 algumas
condições devem ser satisfeitas. As informações
referentes a essas condições estão contidas nos lugares do grafo. Alguns deles são vistos como entrada
da transição e a eles estão associadas as condições
exigidas para que a transição se torne habilitada a
disparar. Outros lugares são vistos como saída de
uma transição e a eles se relacionam condições que
serão afetadas com o disparo da transição. Transições, lugares e relações entre eles constituem os
componentes básicos de um grafo a eventos. A
figura 1 mostra uma típica representação gráfica de
1 O disparo de uma transição representa a ocorrência do evento associado à transição, cujo nome é o nome da transição.
REVISTA DE CIÊNCIA & TECNOLOGIA • V. 8, Nº 16 – pp. 65-76
A transição t1 recebe o nome de transição de
entrada da rede (ou do grafo a eventos) ou transição
de entrada do lugar p1; a transição de saída da rede é
indicada por t3, que também é a transição de saída
do lugar p2. Os arcos indicam as relações entre lugares e transições. Por exemplo, a realização da ação
representada pela transição t2 está associada às
informações contidas no lugar p1. Por outro lado, as
informações contidas no lugar p2 serão alteradas
assim que ocorrer a ação designada em t2. As
marcações no lugar p1 representam a condição de
habilitação da transição t2 (simbolizada pela ficha •)
e o tempo de espera gasto antes da habilitação da
transição t2 (simbolizado pela barra ). Essas marcações constituem parametrizações e são formalmente
representadas como pares (n,t), em que n representa
a condição de habilitação e t, o tempo de espera. A
definição formal de um grafo a eventos é dada a
seguir.
Definição 1: Um grafo a eventos é uma quíntupla
<P, T, A, w, X>, de tal forma que:
• P é um conjunto finito de lugares;
• T é um conjunto finito de transições;
• A é um conjunto de arcos, o qual é um subconjunto de (P × T) ∪ (T × P);
• w é uma função peso, w: A → {1};
¥ X é uma parametrização, ou seja, uma função
X: P→N×N.
O processo dinâmico de um grafo a eventos é
exemplificado na figura 2.
67
g
y
p
Fig. 2. Processo dinâmico.
Grafo A
Grafo B
Na figura 2, a transição t2 do grafo a eventos
A está habilitada a disparar, devendo aguardar uma
unidade de tempo antes do disparo. Após o disparo,
a transição t2 consome uma ficha e passa esta ao
lugar p2 (como mostra o grafo a eventos B). O cará-
ter dinâmico em um grafo a eventos é determinado
pela circulação das fichas.
De modo geral, uma transição habilitada consumirá tantas fichas quantos forem os lugares de sua
chegada e distribui tantas fichas quantos forem os
lugares de sua saída (Cassandras, 1993). A figura 3
ilustra tal procedimento.
Na figura 3, a seqüência (Grafo A)→(Grafo
B)→(Grafo C) determina a evolução dinâmica do
grafo a eventos. No Grafo A, a transição t4 está
habilitada, ou seja, os lugares p1, p2 e p3 fornecem
condições para que o evento associado à transição t4
ocorra. Essas condições são representadas pela
ocorrência de fichas em todos os lugares de entrada
de t4. Assim, após a espera de uma unidade de
tempo (condição em p3), a transição t4 torna-se apta
a disparar.
Fig. 3. Comportamento dinâmico de um grafo a eventos.
Grafo C
68
Dezembro • 2000
g
y
p
Depois do disparo, tem-se o grafo B, em que
uma ficha é consumida de cada lugar de entrada de
t4 e uma ficha é distribuída para cada lugar de saída
de t4.2 No grafo B, a transição t4 ainda continua
habilitada, ou seja, o evento associado à transição t4
pode ocorrer a qualquer momento. Após o disparo
da transição t4 no grafo B, é consumida uma ficha de
cada lugar de entrada de t4 e distribuída uma ficha
para cada lugar de saída de t4. Nota-se que as barras
representando unidades de tempo não se deslocam
no decorrer do processo, e sim permanecem onde
são alocadas no modelo inicial. O grafo C indica a
situação depois do disparo da transição t4 no grafo B
e do consumo de uma unidade de tempo. Já no
grafo C, a transição t4 não está habilitada. Em B e em
C, as transições t5 e t6 estão habilitadas.
Em resumo, partindo de um sistema dinâmico
a eventos discretos, um grafo a eventos é uma ferramenta que se adapta à sua modelagem.
Fig. 4. Processo de Modelagem.
associada ao evento “atendimento do paciente”.
Note que se essa transição estiver habilitada significa
que o paciente na sala de espera pode ser atendido.
Assim que ele for atendido, a transição deixa de estar
habilitada. O lugar p2 representa o médico. Se nesse
lugar houver uma ficha, então o médico está ocioso;
caso contrário, está atendendo. O lugar p3 representa
a sala de consultas. Uma barra indica o tempo dispensado para o atendimento. O lugar p4 é a saída e as
condições para possíveis contatos com as secretárias
dos médicos. A transição t3 estará habilitada sempre
que a consulta terminar, fazendo com que o médico
volte a ficar ocioso, dando margem a que um outro
paciente, do lugar p1, seja atendido. A figura 6 traz
uma possível seqüência de um consultório, com o
dinamismo do grafo a eventos.
Fig. 5. Grafo a eventos do exemplo 1.
Sistema
Dinâmico
Modelo via grafo a eventos
O exemplo seguinte é simples, com preocupação voltada à elucidação do processo de modelagem,
e não à resolução de problemas de grande porte.
Exemplo 1: Pretende-se analisar o fluxo de pacientes juntamente com a disponibilidade de um médico
em um consultório. Espera-se responder perguntas
tais como:
i) Quantos pacientes foram atendidos em um
determinado período de tempo?
ii) Quando determinado paciente será atendido?
Um modelo que forneça essas respostas com
precisão será projetado, utilizando-se para isso um
grafo a eventos (ver fig. 5).
No grafo a eventos da figura 5, o lugar p1
representa os pacientes na sala de espera, aguardando
serem chamados para a consulta. A transição t2 está
2
A situação de consumo e distribuição de fichas é diferente quando
se trata de redes de Petri (não de grafo a eventos), pois nelas a função
peso pode ser diferente de um. Então, o consumo e a distribuição de
fichas relacionam-se diretamente com a função peso de cada arco
(Cassandras, 1993).
REVISTA DE CIÊNCIA & TECNOLOGIA • V. 8, Nº 16 – pp. 65-76
A seqüência da figura 6 mostra que dois pacientes estão na sala de espera enquanto o médico está
ocioso (grafo A). No grafo B, o primeiro paciente é
atendido e o médico deixa de estar ocioso (sai uma
ficha do lugar p1 e do lugar p2), entra uma ficha no
lugar p3 (o médico está atendendo o paciente). Uma
unidade de tempo é requerida para o lugar p3 (tempo
de demora da consulta). Ainda em B, a transição t3
está habilitada, o que significa que a secretária está
pronta para receber o paciente após a consulta. Já no
grafo C, o paciente deixa a sala de consultas, habilita
a transição t4 (saída do consultório) e habilita a transição t2 (um novo paciente pode ser atendido), pois
uma ficha é colocada no lugar p2 (indicando que o
médico está ocioso). Tal esquema caracteriza o processo dinâmico desse grafo a eventos que modela o
problema do consultório médico.
69
g
y
p
Fig. 6. Evolução dinâmica do grafo do exemplo 1.
Partindo de uma simples simulação, possível
nesse exemplo, verifica-se que o gráfico 1, no plano
de 2 dimensões, representa o comportamento dos
disparos da transição t4, ou seja, a trajetória dos disparos e seus tempos correspondentes. Nesse gráfico,
a abscissa representa os disparos das transições e a
ordenada, o tempo de disparo das transições. A
cada transição do grafo a eventos pode-se associar
um conjunto de informações disponíveis sobre as
ocorrências de eventos relacionados a essa transição.
Esse conjunto será chamado pelo nome da transição. Por exemplo, se “tj” é o nome de uma transição, então tj representa, num gráfico de duas
dimensões, o conjunto de informações disponíveis
sobre as ocorrências de eventos relacionados a essa
transição. Esse elemento tj descreve o comportamento dinâmico da trajetória de disparos associada
à transição de nome “tj” (Cohen et al., 1989).
Esse gráfico responde às perguntas iniciais do
exemplo 1. O ponto (3,4) pode, no caso, ser lido
como:
• o terceiro disparo da transição t4 ocorreu, no
mínimo, no instante 4; ou
• no instante 4 ocorreram, no máximo, três disparos.
Assim, para saber quantos pacientes foram
atendidos num determinado período de tempo, é
necessária uma simples análise do gráfico. Do
mesmo modo, é possível, por esse gráfico, visualizar
70
quando o n-ésimo paciente será atendido. A descrição da trajetória de transições de um grafo a
eventos em um gráfico de duas dimensões nem
sempre é uma tarefa simples e imediata - detalhes
mais sofisticados podem ser encontrados em Cohen
et al. (1989), Baccelli et al. (1991) e Magossi (1998).
No entanto, para o grafo a eventos da figura
5, não é tão difícil visualizar a trajetória da transição
t4 num gráfico de duas dimensões. Nota-se que, ao
se acrescentar uma ficha no lugar p1, a transição t2
ficará habilitada. Após o disparo da transição t2, o
lugar p2 terá uma ficha e uma barra (representando
uma unidade de tempo). Isso acarretará uma
demora de uma unidade de tempo antes que a transição t3 dispare. O disparo de t3 acarreta a inclusão
de uma ficha no lugar p3, habilitando a transição t4.
Assim, a cada ficha colocada em p1, sai uma ficha
em t4 com o atraso de uma unidade.
Verifica-se, então, que o primeiro disparo
ocorre no mínimo em 2 unidades de tempo, uma
referente ao 0-ésimo disparo, e outra referente ao
primeiro disparo. Ou seja, o 0-ésimo disparo
ocorre, no mínimo, em uma unidade de tempo; o
primeiro disparo ocorre, no mínimo, em 2 unidades
de tempo (a primeira, que já existia, mais uma); o
segundo disparo ocorre, no mínimo, em 3 unidades
de tempo; o terceiro disparo ocorre, no mínimo,
em 4 unidades de tempo; e assim sucessivamente.
Dezembro • 2000
g
y
p
Grafico 1. Trajetória da transição t4 do exemplo 1.
Sistema lógico NK
Nessa seção, apresenta-se o sistema lógico que
será utilizado para modelar grafo a eventos. Inicialmente, há uma apresentação da lógica NK e dos
métodos de demonstração, adotados na análise de
sistemas dinâmicos. Segue-se explicitando a maneira
de descrever grafo a eventos via lógica NK.
A lógica modal proposicional NK será apresentada do ponto de vista dos tableaux analíticos.
Há grande variedade de sistemas modais na literatura. Revisões compreensivas são dadas por Hughes
& Cresswell (1968 e 1984) e por Fitting (1983). O
sistema proposto nesse trabalho foi desenvolvido
visando especificamente a modelagem de grafo a
eventos. Avalia-se que pode ser facilmente estendido, de modo a descrever sistemas mais complexos. O ponto de vista dos tableaux analíticos,
difundido por Smullyan (1968) e, posteriormente,
empregado por Bell & Machover (1977) e Fitting
(1983 e 1990), constitui uma alternativa à apresentação de um sistema lógico através de axiomas. Sua
principal vantagem é a simplicidade no desenvolvimento das provas de uma fórmula válida. Basicamente, o método do tableau é uma prova por
refutação, ou seja, tenta-se falsear a fórmula que se
deseja provar e, caso isso resulte em contradição,
deduz-se que a fórmula é válida. A seguir, são apresentados os principais elementos do sistema lógico
NK e algumas de suas propriedades.
A linguagem da lógica modal proposicional
NK tem um alfabeto consistindo de:
a) variáveis proposicionais - letras minúsculas x, y,
z, p, q, r, ...;
b) conectivos - G, D, ¬, →;
c) sinais de pontuação - (e);
REVISTA DE CIÊNCIA & TECNOLOGIA • V. 8, Nº 16 – pp. 65-76
d) constante lógica - ⊥.
Observação: os conectivos G e D são operadores modais. Eles têm comportamentos semelhantes aos dos operadores modais clássicos de
necessidade (Fitting, 1983), a menos que se apliquem a um único mundo possível acessível, ao
passo que os operadores modais clássicos aplicam-se
a infinitos mundos possíveis acessíveis. Os conectivos ¬ e → são a negação e a condicional clássicas,
respectivamente.
O conjunto F das fórmulas da linguagem é
definido como segue:
i) qualquer variável proposicional pertence a F;
ii) se X e Y pertencem a F, então (X → Y) também
pertence a F;
iii) se X pertence a F, então ¬X, GX e DX também
pertencem a F;
iv) só é fórmula o que advém das condições i), ii) e
iii) acima descritas.
A semântica de uma lógica modal estende,
usualmente, a semântica da lógica proposicional
clássica através da definição de um conjunto W,
comumente denominado conjunto dos mundos
possíveis, e uma (ou mais) relações entre seus elementos. Ao se interpretar a lógica, diz-se que uma
fórmula é verdadeira ou não num mundo possível,
sendo admissível que essa fórmula seja verdadeira
num mundo e falsa em outro, na mesma interpretação ou modelo. O que distingue uma lógica modal
de outra é o tipo de relação admissível entre os elementos de W. Na lógica NK, serão consideradas
duas relações binárias R e S, satisfazendo à propriedade: para todo w∈W, existem w', w'', w''' únicos e
distintos tais que wRw', wSw'', w''Rw''' e w'Sw'''.
Essas relações permitem estabelecer uma correspondência biunívoca entre qualquer W admissível e o conjunto Z2 dos pares ordenados de inteiros.
Conseqüentemente, os elementos de W serão associados a pares ordenados de inteiros: W = {w(i,j)
(i,j) ∈ Z2}.
Mais rigorosamente, um modelo proposicional modal para NK é uma quadra <W,R,S,V>,
onde W é um conjunto de mundos possíveis, V é
uma função valoração de F×W em {t,f} e R e S são
relações binárias em W, de tal forma que as seguintes
condições sejam satisfeitas, para quaisquer fórmulas
X e Y:
71
g
y
p
a) se X for uma variável proposicional, V(X,w)=t
ou V(X,w)=f, mas não ambos;3
b) V((¬X),w)=t sse V(X,w)=f;
c) V((X→Y),w)=t sse V(X,w)=f ou V(Y,w)=t;
d) V(DX,w) = t sse para w' ∈ W tal que wSw' temse V(X,w')=t;
e) V(GX,w) = t sse para w'∈ W tal que wRw' temse V(X,w')=t;
Diz-se que uma fórmula X é verdadeira em
um modelo se é verdadeira em cada mundo desse
modelo, e é válida se verdadeira em todos os modelos (notação: |=X se X é válida).
Sejam S um conjunto de fórmulas e X uma
fórmula qualquer. Diz-se que X é conseqüência
lógica de S (em símbolos, S|=X) se X é válida em
cada modelo em que todos os membros de S são
válidos.
Uma fórmula assinalada é uma fórmula X precedida dos símbolos “T” ou “F”. Intuitivamente, a
fórmula TX comporta-se como X e a fórmula FX
como ¬X. As fórmulas assinaladas permitem a classificação de todas as fórmulas da lógica proposicional
clássica em dois tipos: fórmulas do tipo α e fórmulas
do tipo β. As fórmulas do tipo α são aquelas com
comportamento conjuntivo (com componentes α1 e
α2) e as do tipo β são as que se comportam disjuntivamente (com componentes β1 e β2). Um exemplo de
fórmula do tipo α é F(X→Y), cujos componentes são
TX e FY. Outros exemplos são F(X∨Y) e T(X∧Y).
Um exemplo de fórmula do tipo β é T(X→Y), cujos
componentes são FX e TY. Também são exemplos
T(X∨Y) e F(X∧Y) (Smullyan, 1968).
Os tableaux analíticos são procedimentos de
prova elaborados em forma de árvores binárias. As
árvores contêm sempre um número finito de ramos.
Cada ramo, por sua vez, é constituído de um conjunto de nós, de tal forma que em cada nó ocorra
uma fórmula assinalada da lógica e a cada nó esteja
associado um mundo (i,j). O objetivo de uma prova
tableau é verificar se uma dada fórmula X da lógica é
ou não válida. Para tanto, inicia-se o tableau falseando
X e prossegue-se aplicando regras de extensão de
ramos. A impossibilidade de falsear a fórmula X é
caracterizada pela ocorrência de contradições em
todos os ramos do tableau, denotando assim que X
3
V(X,w) pode ser lido como o valor verdade da fórmula X no
mundo w.
72
é uma fórmula válida. Se algum ramo não contiver
contradições entre suas fórmulas, então existe a possibilidade de falsear a fórmula; portanto, X não é
válida.
Para o desenvolvimento de uma prova tableau,
procede-se segundo as seguintes regras clássicas de
extensão de ramos:
i) quando uma fórmula de tipo α ocorrer num
ramo de um tableau, deve-se acrescentar a esse
ramo suas duas componentes;
ii) quando ocorrer uma fórmula de tipo β, deve-se
proceder uma bifurcação no tableau, cada novo
ramo iniciado por uma das componentes da fórmula.
Diz-se que as fórmulas do tipo TGX e FGX
são de tipo ν com componentes TX e FX, respectivamente; e as fórmulas do tipo TDX e FDX são de
tipo π com componentes TX e FX, respectivamente.
Em função da sua natureza modal, essas fórmulas
não se reduzem aos tipos descritos anteriormente. As
regras de extensão de ramos para os casos não clássicos (modais) são as seguintes:
iii) quando uma fórmula de tipo ν ocorre num
ramo de um tableau num mundo (i,j), sua componente deve ser escrita no mesmo ramo no
mundo (i-1,j);
iv) quando uma fórmula de tipo π ocorre num
ramo de um tableau num mundo (i,j), sua componente deve ser escrita no mesmo ramo no
mundo (i,j-1).
Um ramo de um tableau é dito fechado se
ocorrem no mesmo ramo e para o mesmo mundo
as fórmulas TX e FX. Um tableau é fechado se
todos os seus ramos são fechados. Um ramo é dito
completo se nele não existe nenhuma fórmula para
a qual se possa aplicar uma das regras acima. Um
tableau é completado se todos os seus ramos são
completos ou fechados.
Sejam S um conjunto de fórmulas não assinaladas e X uma fórmula não assinalada. Um tableau
para X, usando S como um conjunto de afirmações
globais, significa um tableau começado por FX, e de
tal forma que a fórmula TZ pode ser adicionada em
qualquer ponto do tableau para qualquer Z∈S e
qualquer mundo (i,j). Diz-se que X é dedutíveltableaux a partir de S (em símbolos, S|–dtX) se e
somente se existir um tableau fechado para X
Dezembro • 2000
g
y
p
usando S como um conjunto de afirmações globais.
A lógica NK, definida dessa maneira, é um sistema
modal proposicional correto e completo no sentido
forte4 (Magossi, 1998).
Seja o seguinte exemplo de tableau para o sistema lógico NK. Ele mostra que existe um tableau
fechado para a fórmula DGA→GDA, indicando
que esta é válida.
(1) F(DGA→GDA)
(2) TDGA
(3) FGDA
(4) TGA
(5) TA
(6) FDA
(7) FA
(i,j)
(i,j)
(i,j)
(i,j-1)
(i-1,j-1)
(i-1,j)
(i-1,j-1)
regra α em 1
regra α em 1
regra π em 2
regra ν em 4
regra ν em 3
regra π em 6
Essa fórmula indica a equivalência entre uma
transição qualquer t0 e a disjunção (representada
pelo ∨ grande) de todas as transições que chegam
em t0, acompanhadas dos G’s e D’s cujos expoentes
representam o número de fichas (m) e o número de
unidades de tempo (d) para cada transição que
chega em t0.
Exemplo 2: Seja o grafo a eventos, descrito na figura
8, para um sistema a eventos discretos.
Fig. 8. Grafo a eventos do exemplo 2.
Fórmulas da Lógica NK associadas a
um Grafo a Eventos
Nessa seção, é apresentado o procedimento
de modelagem de um grafo a eventos. Ele permite o
desenvolvimento de sistemas de fórmulas da lógica
NK associadas a um grafo a eventos. Objetiva-se
mostrar que todo grafo a eventos pode ser modelado por um sistema de fórmulas da lógica NK.
Na figura 7, o par (m,d) representa uma parametrização do grafo a eventos, ou seja, m é a condição de habilitação da transição (fichas) e d é o
tempo de espera (barras).
Fig. 7. Descrição na lógica NK de um grafo a eventos.
As equações associadas a esse grafo a eventos
são:
x1↔u∨Gx2
x2↔GDu∨Dx1
y↔x2∨GD2y
Aplicações em sistemas dinâmicos a
eventos discretos
As fórmulas associadas ao grafo a eventos da
figura 7 são dadas por:
k
mj dj
t0 ↔ V G D tj
j = 1
Usualmente, define-se G0D0ti como simplesmente ti.
4 Correção e completude no sentido forte significa que S| X se e
–dt
somente se S|=X.
REVISTA DE CIÊNCIA & TECNOLOGIA • V. 8, Nº 16 – pp. 65-76
Essa seção traz uma aplicação do sistema
lógico NK na verificação de especificações em sistemas dinâmicos a eventos discretos. Como é clássico
na literatura de trabalhos envolvendo lógica e problemas de automação, se uma especificação (apropriadamente descrita como uma fórmula da lógica)
for conseqüência lógica do conjunto de fórmulas
que define (modela) o sistema dinâmico, então a
especificação será satisfeita (Manna & Pnuelli, 1979
e 1992). Isso significa que, na linguagem da lógica,
sempre que as fórmulas do sistema dinâmico forem
verdadeiras a especificação também o será.
Isso garante legitimidade, pois impede o caso
de as fórmulas do sistema serem verdadeiras e a
73
g
y
p
especificação falsa. Em outras palavras, seja Γ o conjunto de fórmulas da lógica NK, que descreve o sistema dinâmico em questão, e X a fórmula da lógica
que descreve a especificação. A especificação será
satisfeita se e somente se X for conseqüência lógica
de Γ, ou seja, se todo modelo de Γ for também
modelo de X.
Assim, o problema de verificação de especificações se resume em, dado o grafo a eventos que
representa o sistema dinâmico a eventos discretos,
associar a ele um conjunto Γ de fórmulas da lógica
NK e relacionar à especificação a ser verificada uma
fórmula X da lógica NK. Procede-se, então, verificando se X é conseqüência lógica de Γ:
• em caso afirmativo, conclui-se que a especificação é satisfeita;
• em caso negativo, conclui-se que a especificação
não é satisfeita.
Para determinar se uma especificação X é
conseqüência lógica de um conjunto Γ de fórmulas
que representa um grafo a eventos é necessária a elaboração de um algoritmo baseado em tableaux que
efetivamente determine se X é ou não conseqüência
lógica de Γ (Magossi, 1998 e Magossi & Santos
Mendes, 1998).
A seguir, é mostrado um exemplo de especificação que é satisfeita juntamente com sua resolução
algorítmica via tableaux.
Exemplo 2: Seja o exemplo referente à figura 5.
Para esse sistema, pode-se escrever as seguintes
fórmulas da lógica NK:
t2↔(t1∨Gt3)
t3↔Dt2
t4↔t3
Além dessas, as seguintes fórmulas devem
valer para qualquer transição:5
ti→Dti
Gti→ti,
para i = 0, 1,...4.
Essas fórmulas descrevem um grafo a eventos
em um sistema a eventos discretos através da lógica
modal NK. Supõe-se que se deseja verificar que, no
5 Essas fórmulas caracterizam a linearidade do sistema. Ver Magossi
(1998); Magossi & Santos Mendes (1998); Cohen et al. (1989); e
Baccelli et al. (1991).
74
grafo a eventos da figura 5, descrito acima, um
tempo de espera estipulado para a transição t1 não
acarretará uma espera na saída do sistema, ou seja,
na transição t4. Essa condição pode ser expressa
pela fórmula Dt1→t4 (Magossi, 1998).
A verificação de que a especificação é satisfeita
por intermédio de tableaux analíticos resume-se em
mostrar que a fórmula X=(Dt1→t4) é conseqüência
lógica do conjunto Γ={Dt2↔t3, t3↔t4, t2↔
(t1∨Gt3), Gti→ti, ti→Dti}. Esta, por sua vez, estabelecerá que não existe modelo no qual as fórmulas do
conjunto Γ sejam verdadeiras e a fórmula X=
(Dt1→t4) seja falsa. Isso implica o fato de que a especificação será sempre satisfeita quando as fórmulas
que definem o sistema (grafo a eventos) o forem.
Para tal verificação, utiliza-se o método
tableaux. Ao se desenvolver o tableaux, as fórmulas
de Γ podem ser adicionadas em qualquer nó da
árvore, pois são entendidas como verdadeiras em
qualquer modelo. Ver Magossi (1998), e Magossi
& Santos Mendes (1998).
Essa árvore é construída como segue. Inicia-se
por falsear a especificação a ser verificada; nesse
caso, a especificação é descrita pela fórmula
Dt1→t4. Na seqüência, são aplicadas regras de
extensão de ramos à fórmula do nó de origem, qual
seja, F(Dt1→t4). A essa fórmula aplica-se a regra
clássica α, cuja extensão produz as fórmulas dos
dois nós seguintes, TDt1 e Ft4, respectivamente.
Como essa regra é clássica, não se muda de mundo,
representados os mundos por pares (i,j). À fórmula
TDt1 deve-se aplicar uma regra não clássica (modal)
π, cuja extensão é a fórmula Tt1 no mundo (i,j-1). A
fórmula (t3→t4) é uma fórmula do conjunto Γ,6 e
pode ser adicionada em qualquer ponto do tableau,
desde que sinalizada por T. Assim, acrescenta-se
T(t3→t4). A regra a ser aplicada a essa fórmula é
uma regra clássica β, que produz como extensões
dois ramos, o da esquerda, com a fórmula Ft3, e o
da direita, com a fórmula Tt4. Como a fórmula
T(t3→t4) foi acrescentada no mundo (i,j), as extensões, por serem clássicas, não ocasionam mudança
de mundo.
6
Note que a fórmula t3↔t4 equivale a (t3→t4)∧(t4→t3).
Dezembro • 2000
g
y
p
FDt1→t4
TDt1
Ft4
Tt1
T(t3→t4)
(i,j)
(i,j)
Ft3
T(Dt2→t3)
FDt2
Ft2
T(t2→t3)
FDt1
(i,j-1)
(i,j)
(i,j-1)
(i,j-1)
Tt2
O tableau continua desse modo, até que todas
as fórmulas tenham sofrido a aplicação de alguma
regra tableau de extensão de ramos (clássica ou não
clássica). E nesse tableau, como todos os ramos produziram contradição (ocorrência no mesmo (i,j) de
FX e TX para alguma fórmula X), o tableau é dito
fechado. Portanto, a fórmula X=(Dt1→t4) é conseqüência lógica do conjunto Γ. Logo, não existe um
modelo em que as fórmulas de Γ sejam verdadeiras
e a fórmula Dt1→t4 seja falsa, ou seja, a especificação X é satisfeita.
CONCLUSÃO
Introduziu-se neste trabalho uma lógica
modal, denominada lógica modal NK, apropriada
para modelagem de grafo a eventos. Suas principais
características são a simplicidade e uma completa
correspondência com grafos a eventos. Considerese um sistema a eventos discretos, para o qual se
conhece um grafo a eventos que modela seu comportamento. É possível para esse sistema escrever
um conjunto de fórmulas da lógica NK, completamente equivalente ao sistema dinâmico modelado.
Tt3
(i,j)
(i,j)
(i,j)
(i,j-1)
(i,j)
Tt4
(i,j)
(i,j)
(i,j-1)
O problema de verificação pode, então, ser tratado
através da metodologia dos tableaux analíticos,
método de prova em lógica, utilizado para a lógica
NK. Escreve-se uma nova fórmula, correspondente
à especificação que se quer verificar, e tenta-se mostrar que essa fórmula é conseqüência lógica do conjunto de fórmulas que descreve o sistema.
Essa abordagem abre caminho para um problema interessante, o de se modelar não somente
grafo a eventos, mas redes de Petri. Ela permite também investigar problemas de síntese de controladores, os quais têm sido estudados em Magossi (1998).
O problema de síntese de controladores pode ser
colocado da seguinte maneira: dado um grafo a
eventos com um conjunto de transições ditas de
“entrada” e com um conjunto de transições de
“saída”, projetar um novo grafo a eventos (controlador), tendo como entradas a saída do sistema dado
e como saídas as entradas do sistema dado, tal que
uma certa especificação, não atendida pelo sistema
original, seja satisfeita pelo sistema em “malha
fechada”.
REFERÊNCIAS BIBLIOGRÁFICAS
BACCELLI, F.L. et al. Synchronization and Linearity: an Algebra for Discrete Event Systems. New York: John Wiley and Sons,
1991.
REVISTA DE CIÊNCIA & TECNOLOGIA • V. 8, Nº 16 – pp. 65-76
75
g
y
p
BELL, J.L. & MACHOVER, M. A Course in Mathematical Logic. Amsterdan: North Holland Publishing Company, 1977.
CASSANDRAS, C.G. Discrete Event Systems: Modeling and Performance Analysis. Boston: Aksen Associates Incorporated
Publishers, 1993.
COHEN,G. et al. Algebraic tools for performance evaluation of discrete event systems. Proceedings of the IEEE. 77 (1): 39-58,
1989.
FITTING, Melvin. First-Order Logic and Automated Theorem Proving. 2.a ed. New York: Springer-Verlag, 1990.
_____________. Proof Methods for Modal and Intuitionistic Logics. Dordrecht: D. Reidel Publishing Co., 1983.
HUGHES,G.E. & CRESSWELL, M.J. A Companion to Modal Logic. London: Methuen and Co. Ltd., 1984.
_____________. An Introduction to Modal Logic. London: Methuen and Co. Ltd., 1968.
MAGOSSI, J.C. Análise e Síntese de Sistemas Dinâmicos a Eventos Discretos via Lógica Modal. Campinas, 1998. [Tese de Doutorado, DCA/FEEC, Unicamp].
MAGOSSI, J.C. & SANTOS-MENDES, R. Modal Logic Based Algorithms for the Verification of Specifications in Discrete
Event Systems. IV Workshop on Discrete Event Systems, Aug./26-28, Cagliary, Italy, 1998.
______________. Verificações de Especificações em Sistemas Dinâmicos a Eventos Discretos via Lógica Modal. Proceedings of
XII Brazilian Automatic Control Conference-XII CBA, Sep./14-18, Uberlândia, v. III, pp. 931-936, 1998.
MANNA, Z. & PNUELLI, A.. The Modal Logic of Programs. Proc. 6th Int. Colloq. Aut. Lang. Prog: Lec. Notes in Comp. Sci.,
Berlin, 71: 385-409, 1979.
______________. The Temporal Logic of Reactive and Concurrent Systems: Specification. New York: Springer-Verlag, 1992.
MURATA,T. Petri Nets: Properties, analysis and applications. Proceedings of the IEEE, 77: 541-580, 1989.
PETERSON, J.L. Petri Net Theory and the Modeling of Systems. Englewood Cliffs, NJ: Prentice-Hall, 1981.
SMULLYAN, Raymond. First Order Logic. Berlin/Heidelberg: Springer-Verlag, 1968.
76
Dezembro • 2000