Temporal Logics for Diffusion in Social Networks

Esta tese apresenta LTL-SN, um framework baseado em lógica para modelar redes sociais usando a Lógica Temporal Linear (LTL). O LTL-SN incorpora propriedades de redes sociais de adoção, onde os agentes adotam comportamentos baseados no comportamento de seus amigos. Além disso, ele explora variações do modelo para analisar a propagação de doenças em populações usando modelos compartimentais. A tese aproveita linguagens de especificação existentes e implementações de verificação de modelos, representando redes sociais como caminhos LTL especificados com modelos nuXmv. Os resultados de pesquisas publicadas são referenciados. Fornecemos axiomatização e provas de correção e completude para cada variante lógica apresentada, incluindo os modelos compartimentais SIR e SIRS.