A language-based approach to modelling and analysis of Twitter interactions

More than a personal microblogging site, Twitter has been transformed by common use to an information publishing venue, which public characters, media channels and common people daily rely on for, e.g., news reporting and consumption, marketing, and social messaging. The use of Twitter in a cooperative and interactive setting calls for the precise awareness of the dynamics regulating message spreading. In this paper, we describe Twitlang, a language for modelling the interactions among Twitter accounts. The associated operational semantics allows users to precisely determine the effects of their actions on Twitter, such as post, reply-to or delete tweets. The language is implemented in the form of a Maude interpreter, Twitlanger, which takes a language term as an input and explores the computations arising from the term. By combining the strength of Twitlanger and the Maude model checker, it is possible to automatically verify communication properties of Twitter accounts. We illustrate the benefits of our executable formalisation by means of an application scenario inspired from real life. While the scenario highlights the benefits of adopting Twitter for a cooperative use in the everyday life, our analysis shows that appropriate settings are essential for a proper usage of the platform, in respect of fulfilling those communication properties expected within collaborative and interactive contexts.