An Abstract Formal Basis for Digital Crowds

TL;DR

This paper proposes a formal description language for digital crowds, enabling the application of formal verification methods to analyze crowd behavior in crowdsourcing platforms.

Contribution

It introduces a novel formal modeling approach for digital crowds that do not involve direct agent communication, facilitating formal analysis and verification.

Findings

Formal description language for digital crowds

Application of formal verification to crowd behavior

Foundation for analyzing large-scale online participation

Abstract

Crowdsourcing, together with its related approaches, has become very popular in recent years. All crowdsourcing processes involve the participation of a digital crowd, a large number of people that access a single Internet platform or shared service. In this paper we explore the possibility of applying formal methods, typically used for the verification of software and hardware systems, in analysing the behaviour of a digital crowd. More precisely, we provide a formal description language for specifying digital crowds. We represent digital crowds in which the agents do not directly communicate with each other. We further show how this specification can provide the basis for sophisticated formal methods, in particular formal verification.