Temporal Logic for Social Networks
Vitor Machado, Mario Benevides

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
