Cálculo do processo - Process calculus

Na ciência da computação , os cálculos de processo (ou álgebras de processo ) são uma família diversa de abordagens relacionadas para modelar formalmente sistemas concorrentes . Os cálculos de processo fornecem uma ferramenta para a descrição de alto nível de interações, comunicações e sincronizações entre uma coleção de agentes ou processos independentes. Eles também fornecem leis algébricas que permitem que as descrições dos processos sejam manipuladas e analisadas, e permitem o raciocínio formal sobre equivalências entre os processos (por exemplo, usando bisimulação ). Os principais exemplos de cálculos de processo incluem CSP , CCS , ACP e LOTOS . As adições mais recentes à família incluem o cálculo π , o cálculo ambiental , PEPA , o cálculo de fusão e o cálculo de junção .

Caracteristicas essenciais

Embora a variedade de cálculos de processos existentes seja muito grande (incluindo variantes que incorporam comportamento estocástico , informações de tempo e especializações para estudar interações moleculares), existem várias características que todos os cálculos de processos têm em comum:

Representar interações entre processos independentes como comunicação ( troca de mensagens ), em vez de modificação de variáveis compartilhadas.
Descrever processos e sistemas usando uma pequena coleção de primitivas e operadores para combinar essas primitivas.
Definição de leis algébricas para os operadores do processo, que permitem que as expressões do processo sejam manipuladas usando o raciocínio equacional .

Matemática de processos

Para definir um cálculo de processo , começa-se com um conjunto de nomes (ou canais ) cujo objetivo é fornecer meios de comunicação. Em muitas implementações, os canais têm uma estrutura interna rica para melhorar a eficiência, mas isso é abstraído na maioria dos modelos teóricos. Além dos nomes, é necessário um meio de formar novos processos a partir dos antigos. Os operadores básicos, sempre presentes de uma forma ou de outra, permitem:

composição paralela de processos
especificação de quais canais usar para enviar e receber dados
sequencialização de interações
ocultação de pontos de interação
recursão ou replicação de processo

Composição paralela

A composição paralela de dois processos e , geralmente escrita , é a chave primitiva que distingue os cálculos do processo dos modelos sequenciais de computação. Composição paralelo permite a computação em e para proceder simultaneamente, e de forma independente. Mas também permite a interação, ou seja, a sincronização e o fluxo de informações de para (ou vice-versa) em um canal compartilhado por ambos. Crucialmente, um agente ou processo pode ser conectado a mais de um canal ao mesmo tempo. ${\ displaystyle {\ mathit {P}}}$ ${\ displaystyle {\ mathit {Q}}}$ ${\ displaystyle P \ vert Q}$ ${\ displaystyle {\ mathit {P}}}$ ${\ displaystyle {\ mathit {Q}}}$ ${\ displaystyle {\ mathit {P}}}$ ${\ displaystyle {\ mathit {Q}}}$

Os canais podem ser síncronos ou assíncronos. No caso de um canal síncrono, o agente que envia a mensagem espera até que outro agente receba a mensagem. Os canais assíncronos não requerem tal sincronização. Em alguns cálculos de processo (notavelmente o π-cálculo ), os próprios canais podem ser enviados em mensagens por meio de (outros) canais, permitindo que a topologia das interconexões do processo mude. Alguns cálculos de processo também permitem que canais sejam criados durante a execução de um cálculo.

Comunicação

A interação pode ser (mas nem sempre) um fluxo direcionado de informações. Ou seja, a entrada e a saída podem ser distinguidas como primitivas de interação dupla. Os cálculos de processo que fazem tais distinções normalmente definem um operador de entrada ( por exemplo ) e um operador de saída ( por exemplo ), os quais nomeiam um ponto de interação (aqui ) que é usado para sincronizar com uma primitiva de interação dual. ${\ displaystyle x (v)}$ ${\ displaystyle x \ langle y \ rangle}$ ${\ displaystyle {\ mathit {x}}}$

Se as informações forem trocadas, elas fluirão da saída para o processo de entrada. A primitiva de saída especificará os dados a serem enviados. Em , esses dados são . Da mesma forma, se uma entrada espera receber dados, uma ou mais variáveis associadas atuarão como espaços reservados a serem substituídos por dados, quando eles chegarem. Em , desempenha esse papel. A escolha do tipo de dados que podem ser trocados em uma interação é uma das principais características que distinguem diferentes cálculos de processo. ${\ displaystyle x \ langle y \ rangle}$ ${\ displaystyle y}$ ${\ displaystyle x (v)}$ ${\ displaystyle v}$

Composição sequencial

Às vezes, as interações devem ser ordenadas temporalmente. Por exemplo, pode ser desejável especificar algoritmos como: primeiro receba alguns dados e, em seguida, envie esses dados ${\ displaystyle {\ mathit {x}}}$ ${\ displaystyle {\ mathit {y}}}$ . A composição sequencial pode ser usada para tais fins. É bem conhecido por outros modelos de computação. Em cálculos de processo, o operador de sequencialização é geralmente integrado com entrada ou saída, ou ambos. Por exemplo, o processo aguardará uma entrada em . Somente quando esta entrada ocorrer o processo será acionado, com os dados recebidos por meio de substituídos por identificador . ${\ displaystyle x (v) \ cdot P}$ ${\ displaystyle {\ mathit {x}}}$ ${\ displaystyle {\ mathit {P}}}$ ${\ displaystyle {\ mathit {x}}}$ ${\ displaystyle {\ mathit {v}}}$

Semântica de redução

A principal regra de redução operacional, contendo a essência computacional dos cálculos do processo, pode ser dada apenas em termos de composição paralela, sequencialização, entrada e saída. Os detalhes dessa redução variam entre os cálculos, mas a essência permanece praticamente a mesma. A regra de redução é:

{\ displaystyle x \ langle y \ rangle \ cdot P \; \ vert \; x (v) \ cdot Q \ longrightarrow P \; \ vert \; Q [^ {y} \! / \! _ {v}] }

A interpretação para esta regra de redução é:

O processo manda uma mensagem, aqui , ao longo do canal . Duplamente, o processo recebe essa mensagem no canal . ${\ displaystyle x \ langle y \ rangle \ cdot P}$ ${\ displaystyle {\ mathit {y}}}$ ${\ displaystyle {\ mathit {x}}}$ ${\ displaystyle x (v) \ cdot Q}$ ${\ displaystyle {\ mathit {x}}}$
Uma vez enviada a mensagem, passa a ser o processo , enquanto passa a ser o processo , que fica com o placeholder substituído pelos dados recebidos em . ${\ displaystyle x \ langle y \ rangle \ cdot P}$ ${\ displaystyle {\ mathit {P}}}$ ${\ displaystyle x (v) \ cdot Q}$ ${\ displaystyle Q [^ {y} \! / \! _ {v}]}$ ${\ displaystyle {\ mathit {Q}}}$ ${\ displaystyle {\ mathit {v}}}$ ${\ displaystyle {\ mathit {y}}}$ ${\ displaystyle {\ mathit {x}}}$

A classe de processos que pode variar conforme a continuação da operação de saída influencia substancialmente as propriedades do cálculo. ${\ displaystyle {\ mathit {P}}}$

Se escondendo

Os processos não limitam o número de conexões que podem ser feitas em um determinado ponto de interação. Mas os pontos de interação permitem interferência (ou seja, interação). Para a síntese de sistemas compactos, mínimos e composicionais, a capacidade de restringir a interferência é crucial. As operações de ocultamento permitem o controle das conexões feitas entre os pontos de interação ao compor os agentes em paralelo. Ocultar pode ser denotado de várias maneiras. Por exemplo, no cálculo π, a ocultação de um nome em pode ser expressa como , enquanto em CSP pode ser escrita como . ${\ displaystyle {\ mathit {x}}}$ ${\ displaystyle {\ mathit {P}}}$ ${\ displaystyle (\ nu \; x) P}$ ${\ displaystyle P \ setminus \ {x \}}$

Recursão e replicação

As operações apresentadas até agora descrevem apenas interação finita e, conseqüentemente, são insuficientes para computabilidade total, que inclui comportamento não finalizável. Recursão e replicação são operações que permitem descrições finitas de comportamento infinito. A recursão é bem conhecida no mundo sequencial. A replicação pode ser entendida como abreviar a composição paralela de um número infinito de processos: ${\ displaystyle! P}$ ${\ displaystyle {\ mathit {P}}}$

{\ displaystyle! P = P \ mid! P}

Processo nulo

Cálculos de processos geralmente também incluem um processo nulo (variadamente designado como , , , , ou algum outro símbolo apropriado), que não tem pontos de interacção. É totalmente inativo e seu único propósito é atuar como a âncora indutiva no topo da qual processos mais interessantes podem ser gerados. ${\ displaystyle {\ mathit {nil}}}$ ${\ displaystyle 0}$ ${\ displaystyle {\ mathit {PARAR}}}$ ${\ displaystyle \ delta}$

Álgebra de processo discreto e contínuo

A álgebra de processo foi estudada para tempo discreto e tempo contínuo (tempo real ou tempo denso).

História

Na primeira metade do século 20, vários formalismos foram propostos para capturar o conceito informal de uma função computável , com funções μ-recursivas , sendo as máquinas de Turing e o cálculo lambda possivelmente os exemplos mais conhecidos hoje. O fato surpreendente de que eles são essencialmente equivalentes, no sentido de que todos são codificáveis uns nos outros, apóia a tese de Church-Turing . Outro recurso compartilhado é mais raramente comentado: todos eles são mais facilmente entendidos como modelos de computação sequencial . A consolidação subsequente da ciência da computação exigiu uma formulação mais sutil da noção de computação, em particular representações explícitas de concorrência e comunicação. Modelos de concorrência, como os cálculos de processo, as redes de Petri em 1962 e o modelo do ator em 1973, surgiram dessa linha de investigação.

A pesquisa sobre cálculos de processos começou a sério com Robin Milner 'trabalho seminal s no cálculo de sistemas de comunicação (CCS) durante o período de 1973 a 1980. CAR Hoare ' s processos comunicantes Sequential (CSP) apareceu pela primeira vez em 1978, e foi posteriormente desenvolvido em um cálculo de processo completo durante o início dos anos 1980. Houve muita fertilização cruzada de ideias entre CCS e CSP à medida que se desenvolviam. Em 1982, Jan Bergstra e Jan Willem Klop começaram a trabalhar no que veio a ser conhecido como Álgebra de Processos de Comunicação (ACP) e introduziram o termo álgebra de processo para descrever seu trabalho. CCS, CSP e ACP constituem os três ramos principais da família dos cálculos de processo: a maioria dos outros cálculos de processo pode traçar suas raízes em um desses três cálculos.

Pesquisa atual

Vários cálculos de processos foram estudados e nem todos se encaixam no paradigma esboçado aqui. O exemplo mais proeminente pode ser o cálculo ambiental . Isso é esperado, uma vez que os cálculos de processo são um campo ativo de estudo. Atualmente, a pesquisa sobre cálculos de processos concentra-se nos seguintes problemas.

Desenvolvimento de novos cálculos de processos para melhor modelagem de fenômenos computacionais.
Encontrar subcálculos bem comportados de um determinado cálculo de processo. Isso é valioso porque (1) a maioria dos cálculos são bastante selvagens no sentido de que são bastante gerais e não se pode dizer muito sobre processos arbitrários; e (2) aplicações computacionais raramente esgotam todo o cálculo. Em vez disso, eles usam apenas processos que são muito restritos na forma. Restringir a forma dos processos é principalmente estudado por meio de sistemas de tipos .
Lógicas de processos que permitem raciocinar sobre (essencialmente) propriedades arbitrárias de processos, seguindo as ideias da lógica de Hoare .
Teoria comportamental: o que significa dois processos serem iguais? Como podemos decidir se dois processos são diferentes ou não? Podemos encontrar representantes para classes de equivalência de processos? Geralmente, os processos são considerados iguais se nenhum contexto, ou seja, outros processos em execução em paralelo, podem detectar uma diferença. Infelizmente, tornar essa intuição precisa é sutil e, em geral, produz caracterizações pesadas de igualdade (que na maioria dos casos também devem ser indecidíveis, como consequência do problema da parada ). As bisimulações são uma ferramenta técnica que auxilia no raciocínio sobre equivalências de processos.
Expressividade dos cálculos. A experiência de programação mostra que certos problemas são mais fáceis de resolver em algumas linguagens do que em outras. Este fenômeno exige uma caracterização mais precisa da expressividade da computação de modelagem de cálculos do que aquela oferecida pela tese de Church-Turing . Uma maneira de fazer isso é considerar codificações entre dois formalismos e ver quais codificações de propriedades podem potencialmente preservar. Quanto mais propriedades podem ser preservadas, mais expressivo é o alvo da codificação. Para cálculos de processo, os resultados celebrados são que o cálculo π síncrono é mais expressivo do que sua variante assíncrona, tem o mesmo poder expressivo que o cálculo π de ordem superior , mas é menor que o cálculo ambiente .
Usando cálculo de processos para modelar sistemas biológicos (cálculo π estocástico, BioAmbientes, Beta Binders, BioPEPA, cálculo de Brane). Alguns pensam que a composicionalidade oferecida pelas ferramentas teóricas do processo pode ajudar os biólogos a organizar seu conhecimento de maneira mais formal.

Implementações de software

As ideias por trás da álgebra de processo deram origem a várias ferramentas, incluindo:

Relacionamento com outros modelos de simultaneidade

O monóide de história é o objeto livre que é genericamente capaz de representar as histórias de processos de comunicação individuais. Um cálculo de processo é, então, uma linguagem formal imposta a um monóide histórico de maneira consistente. Ou seja, um monóide histórico só pode registrar uma sequência de eventos, com sincronização, mas não especifica as transições de estado permitidas. Assim, um cálculo de processo é para um monóide de história o que uma linguagem formal é para um monóide livre (uma linguagem formal é um subconjunto do conjunto de todas as sequências de comprimento finito possíveis de um alfabeto gerado pela estrela de Kleene ).

O uso de canais de comunicação é uma das características que distinguem os cálculos do processo de outros modelos de concorrência , como as redes de Petri e o modelo do ator (ver Modelo de ator e cálculos do processo ). Uma das motivações fundamentais para incluir canais nos cálculos do processo era habilitar certas técnicas algébricas, tornando mais fácil raciocinar sobre os processos algebricamente.

Veja também

Referências

Leitura adicional

Matthew Hennessy : Algebraic Theory of Processes , The MIT Press , ISBN 0-262-08171-7 .
CAR Hoare : Communicating Sequential Processes , Prentice Hall , ISBN 0-13-153289-8 .
- Este livro foi atualizado por Jim Davies no Oxford University Computing Laboratory e a nova edição está disponível para download como um arquivo PDF no site Using CSP .
Robin Milner : A Calculus of Communicating Systems , Springer Verlag, ISBN 0-387-10235-3 .
Robin Milner : Communicating and Mobile Systems: the Pi-Calculus , Springer Verlag, ISBN 0-521-65869-1 .
Valk, Rüdiger ; Moldt, Daniel; Köhler-Bußmeier, Michael, eds. (2011). "Capítulo 5: Prozessalgebra - Parallele und kommunizierende Prozesse" (PDF) . Formale Grundlagen der Informatik II: Modellierung und Analyze von Informatiksystemen . Theoretische Grundlagen der Informatik (em alemão). Parte 2. Universidade de Hamburgo . FGI2. Arquivado (PDF) do original em 09/07/2019 . Página visitada em 13/07/2019 .

Languages

In other projects