Aplicações práticas de jogos de paridade

Existem exemplos de aplicações práticas de jogos de paridade, isto é, sistemas, no mundo real, que podem ser representados como jogos de paridade?

A documentação geralmente relacionada aos jogos de paridade quase nunca tem um exemplo prático desse aplicativo.

Aqui está um aplicativo bastante diferente do que você pode ter em mente. A programação linear tem muitas aplicações práticas. Existem muitos algoritmos para programação linear e aqueles baseados no método simplex de George Dantzig estão entre os mais implementados. Um parâmetro importante do simplex é chamado de regra de rotação. Victor Klee e George Minty fornecem um conjunto de polítopos nos quais a regra de rotação sugerida por Dantzig exigiria um número exponencial de etapas de rotação. Desde então, exemplos demonstrando um limite inferior exponencial foram descobertos para quase todas as regras de rotação determinísticas.

No entanto, o Simplex pode usar regras de rotação aleatória. Gil Kalai, em 1992, introduziu uma regra de rotação aleatória e provou ser um limite superior subexponencial para simplex com essa regra. Também em 1992, Micha Sharir e Emo Welzl definiram problemas do tipo LP que incluem programação linear padrão e, com Jiří Matoušek, também propuseram variantes aleatórias de limites superiores simplex e comprovados subexponenciais para essa variante. Limites inferiores subexponenciais também foram descobertos em problemas do tipo LP, mas até cerca de 2010 não havia exemplos concretos de programas lineares nos quais esses limites inferiores pudessem ser demonstrados. Veja esses dois posts no blog de Gil Kalai, para mais uma narrativa dessa história, a conexão com a conjectura de Hirsch e os links para a literatura.

O que isso tem a ver com jogos de paridade? São necessárias algumas etapas para configurar uma conexão. Um problema aberto na pesquisa de jogos de paridade até 2009 foi determinar se determinados algoritmos de iteração de políticas para resolver jogos de paridade podem ter comportamento exponencial. Veja os documentos de Marcin Jurdziński para mais informações. Oliver Friedmann, a partir de 2009 , exibiu exemplos de jogos de paridade nos quais determinados algoritmos de iteração de políticas exigiam tempo exponencial. Ao explorar uma conexão entre jogos de paridade e certos problemas do tipo LP, ele derivou limites inferiores subexponenciais para várias regras de rotação para simplex. (Observe, porém, que um dos resultados, referente ao algoritmo Random Facet, foi mostrado por Oliver Friedmann, Thomas Hansen e Uri Zwick estar errado.)

Espero que você concorde que esse é um exemplo fascinante e convincente de uma aplicação de jogos de paridade.

Há uma resposta mais direta à sua pergunta também. Suponha que se queira projetar um controlador discreto que regule como um sistema físico (termostato, fábrica de produtos químicos etc.) se comporta com base no estado do sistema e no estado do ambiente. A questão de saber se existe um controlador para fornecer as garantias que um designer deseja pode ser reduzida à resolução de jogos de paridade. Então você pode pensar em um jogo de paridade em termos de sistemas, ambientes e controladores.

Outra configuração é a análise do programa. Suponha que você queira determinar automaticamente se um programa satisfaz alguma propriedade de correção no modal -calculus. A verificação de modelo é uma abordagem para solucionar esse problema e a verificação do modelo -calculus está profundamente conectada aos jogos de paridade. $\mu$$\mu$