An automata-based approach for synchronizable mailbox communication

Resumo Técnico: Uma Abordagem Baseada em Autômatos para Comunicação de Caixa de Correio Sincronizável

Declaração do Problema
O artigo investiga sistemas de comunicação de estados finitos (CFMs) operando sob semântica de caixa de correio, onde cada processo possui um único buffer FIFO (caixa de correio) multiplexando mensagens de todos os outros processos. Isso contrasta com a semântica padrão ponto a ponto (p2p), onde cada canal possui um buffer dedicado. Os autores focam em comunicação baseada em rodadas, especificamente rodadas sr (enviar-então-receber), onde os processos executam uma sequência de envios seguida de uma sequência de recebimentos dentro de uma única rodada.

Um sistema é definido como mb-sincronizável se toda execução possível (trilha) puder ser reprogramada em uma execução equivalente que seja uma sequência de tais rodadas sr. O problema central abordado é determinar se um CFM dado é mb-sincronizável. Trabalhos anteriores (por exemplo, [BEJQ18, GLL20, GLL23]) estabeleceram a decidibilidade para este problema, mas frequentemente impunham limites fixos nos tamanhos das rodadas ou recorriam a estruturas lógicas complexas (como LCPDL ou lógica MSO) com limites de complexidade elevados (por exemplo, Exptime). Uma lacuna significativa permanecia quanto à complexidade precisa da mb-sincronizabilidade sem restrições de tamanho nas rodadas, e quanto à decidibilidade de problemas de verificação relacionados (alcançabilidade, verificação de modelo) neste cenário ilimitado.

Metodologia
Os autores propõem uma abordagem baseada em autômatos inovadora que evita a alta complexidade dos métodos lógicos anteriores. O núcleo de sua técnica baseia-se na análise de sequências de envio marcadas (ms-sequências).

1. Sequências de Envio Marcadas: Os autores observam que, para sistemas mb-sincronizáveis, o conjunto de trilhas não é regular, mas sua projeção sobre as ações de envio (anotadas para distinguir envios correspondentes de não correspondentes) é regular. Eles definem um alfabeto estendido $\mathcal{S} \cup \overline{\mathcal{S}}$, onde $\overline{\mathcal{S}}$ denota envios não correspondentes.
2. LTS em Diamante-R: Eles utilizam a propriedade de sistemas de transição rotulados (LTS) em diamante-R, onde a ordem das ações de recebimento por processos distintos não afeta a alcançabilidade. Isso permite que eles construam autômatos que operam sobre ms-sequências em vez de trilhas completas, efetivamente "adivinhando" a estrutura das rodadas.
3. Trocas Atômicas e Grafos de Comunicação: Para detectar violações de sincronizabilidade, os autores analisam trocas atômicas (sequências que não podem ser decompostas em trocas menores). Eles introduzem um grafo de comunicação $H_{mb}(u)$ para uma sequência $u$. Uma sequência é atômica se e somente se este grafo for fortemente conexo. Eles constroem autômatos ($B_p$ e $B_{all}$) para verificar a conexidade forte e a existência de caminhos específicos (rotulações adequadas) dentro desses grafos, garantindo que a sequência corresponda a uma troca válida e não decomponível.
4. Testemunhas Mínimas: O algoritmo para verificar mb-sincronizabilidade busca uma testemunha mínima de não sincronizabilidade. Esta testemunha é uma trilha mb-viável $u = v \cdot r$ (onde $r$ é uma ação de recebimento) tal que $v$ é mb-sincronizável, mas $u$ não é. A existência de tal testemunha é caracterizada pela estrutura de fatores atômicos em $v$ e sua ordenação causal em relação a $r$.

Principais Contribuições e Resultados

• Completude Pspace da mb-Sincronizabilidade: O resultado principal (Teorema 5.15) estabelece que verificar se um CFM é mb-sincronizável é Pspace-completo. Isso fornece um limite de complexidade apertado, melhorando os limites superiores de Exptime anteriores derivados de caracterizações lógicas.
• Alcançabilidade de Estado Global: O artigo prova que a alcançabilidade de estado global para CFMs mb-sincronizáveis é Pspace-completa (Teorema 3.6).
• Verificação de Modelo: Os autores mostram que a verificação de modelo de CFMs mb-sincronizáveis contra uma classe de propriedades regulares R-fechadas (propriedades invariantes sob a reordenação de ações de recebimento independentes) é Pspace-completa (Teorema 4.3).
• Semelhança de Caixa de Correio: Eles abordam a questão de saber se um sistema p2p pode ser simulado sob semântica de caixa de correio (semelhança de caixa de correio). Embora indecidível em geral, eles provam que é Pspace-completo para CFMs mb-sincronizáveis (Teorema 4.10).
• Contagem Fixa de Processos: Um subproduto notável da abordagem é que, se o número de processos for fixo, todos os problemas acima tornam-se solúveis em Ptime (especificamente Nlogspace).
• k-Mb-Sincronizabilidade: O artigo estende os resultados para k-mb-sincronizabilidade (rodadas limitadas pelo tamanho k), mostrando que este problema também é Pspace-completo (Teorema 5.16), e aborda a existência de algum k para o qual um sistema é sincronizável (Teorema 5.17).

Significado e Alegações
O artigo alega que sua abordagem baseada em autômatos oferece um método mais direto e eficiente para raciocinar sobre comunicação de caixa de correio em comparação com abordagens lógicas anteriores (MSO, LCPDL). Ao focar na projeção de trilhas sobre ações de envio e utilizar as propriedades estruturais de trocas atômicas, os autores alcançam limites de complexidade ótimos (Pspace) para problemas fundamentais de verificação.

Os autores enfatizam que sua definição de mb-sincronizabilidade (sem tamanhos de rodada fixos) é praticamente relevante porque, embora limites nos tamanhos das rodadas possam ser inferidos, eles são frequentemente exponenciais no número de processos, tornando suposições de tamanho fixo impraticáveis. O artigo também esclarece a relação entre sua noção de sincronizabilidade e outras noções existentes (sincronizabilidade fraca, sincronizabilidade de envio), demonstrando que essas noções são incomparáveis e que sua definição específica é necessária para a decidibilidade de certas propriedades regulares.

Finalmente, os autores sugerem que suas técnicas são potencialmente mais fáceis de implementar do que abordagens anteriores e poderiam ser adaptadas para cenários dinâmicos, embora não apresentem uma implementação específica ou avaliação experimental neste trabalho.