Formal Analysis of Reddit Network Interactions

Abstract

[EN] With the rise in popularity of social media platforms in the last couple of decades, there is a demand for a more thorough and formal understanding of how these networks operate due to how quickly information is disseminated in these networks. The operations of these networks ought to be consistent and correct and with as few inconsistencies as possible to keep information accessible and clear. Reddit, the platform chosen for this project, has risen in popularity in the last few years and, although it is not the most used platform in the market, it is one of the most powerful networks in terms of allowing information to spread thanks to it’s divided-into-categories nature. This work focuses on analyzing the properties and characteristics of the social media platform Reddit. Firstly, a formal model is developed for Reddit in the high-performance specification language Maude. "After this, a reachability analysis is performed in the Maude system, which ensures the safety of the system by proving that no states considered unsafe can be reached. Finally, liveness properties are checked by using the Maude LTL logical model checker (LMC)."

[ES] Con el aumento de la popularidad de las plataformas de redes sociales en las últimas dos décadas, existe una demanda de una comprensión más completa y formal de cómo operan estas redes debido a la rapidez con que se difunde la información en estas redes. Las operaciones de estas redes deben ser consistentes y correctas y con la menor cantidad de inconsistencias posibles para mantener la información accesible y clara. Reddit, la plataforma elegida para este proyecto, ha ganado popularidad en los últimos años y, aunque no es la plataforma más utilizada en el mercado, es una de las redes más poderosas en cuanto a permitir que la información se difunda gracias a su naturaleza de división por categorías. Este trabajo se centra en analizar las propiedades y características de la plataforma de redes sociales Reddit. En primer lugar, se desarrolla un modelo formal para Reddit en el lenguaje de especificación de alto rendimiento Maude. "Posteriormente, se realiza un análisis de accesibilidad en el sistema Maude, que garantiza la seguridad del sistema al demostrar que no se puede alcanzar ningún estado considerado inseguro. Por último, las propiedades de vivacidad se comprueban utilizando el verificador de modelo lógico (LMC) de Maude LTL."

[CA] Amb l’augment de popularitat de les plataformes de xarxes socials en les darreres dècades, es demana una comprensió més exhaustiva i formal del funcionament d’aquestes xarxes a causa de la rapidesa amb què es difon l’informació en aquestes xarxes. Les operacions d’aquestes xarxes haurien de ser consistents i correctes i amb el mínim d’incongruències possibles per mantindre la informació accessible i clara. Reddit, la plataforma escollida per a aquest projecte, ha augmentat en popularitat en els darrers anys i, tot i que no és la plataforma més utilitzada al mercat, és una de les xarxes més potents pel que fa a la difusió de la informació gràcies a la seva natura de dividir per categories. Aquest treball es centra en analitzar les propietats i característiques de la plataforma de xarxes socials Reddit. En primer lloc, es desenvolupa un model formal per a Reddit en el llenguatge d’especificació d’alt rendiment Maude. "Després d’això, es realitza una anàlisi d’accessibilitat al sistema Maude, que garanteix la seguretat del sistema demostrant que no es pot assolir cap estat considerat insegur. Finalment, es comproven les propietats de la vivència mitjançant el comprovador de models lògics (LMC) de Maude LTL."