Temporal Logic for Social Networks

TL;DR

This paper develops a temporal logic framework for social networks based on LTL, enabling the use of existing model checkers for analysis, with formal foundations and complexity considerations.

Contribution

It introduces a new temporal logic for social networks, including axiomatization, soundness, completeness, and model checking aspects, extending LTL applications.

Findings

Logic is sound and complete via propositional translation

Model checking is feasible with complexity analysis

Framework leverages existing LTL model checkers

Abstract

This paper introduces a logic with a class of social network models that is based on standard Linear Temporal Logic (LTL), leveraging the power of existing model checkers for the analysis of social networks. We provide a short literature overview, and then define our logic and its axiomatization, present some simple motivational examples of both models and formulas, and show its soundness and completeness via a translation into propositional formulas. Lastly, we briefly discuss model checking and time complexity analysis.