Decentralized Asynchronous Crash-Resilient Runtime Verification

Pierre Fraigniaud (1, 2) , Borzoo Bonakdarpour (3) , Sergio Rajsbaum (4) , David Rosenblueth (5) , Corentin Travers (6)

1 GANG - Networks, Graphs and Algorithms
2 IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale
3 ECE - Department of Electrical and Computer Engineering [Waterloo]
4 Instituto de Matematicas [México]
5 UNAM - Instituto de Matematicas
6 LaBRI - Laboratoire Bordelais de Recherche en Informatique

Runtime Verification (RV) is a lightweight method for monitoring the formal specification of a system during its execution. It has recently been shown that a given state predicate can be monitored consistently by a set of crash-prone asynchronous \emph{distributed} monitors, only if sufficiently many different verdicts can be emitted by each monitor. We revisit this impossibility result in the context of \LTL semantics for RV. We show that employing the four-valued logic \RVLTL will result in inconsistent distributed monitoring for some formulas. Our first main contribution is a family of logics, called \LTLk, that refines \RVLTL incorporating $2k + 4$ truth values, for each $k\geq 0$. The truth values of \LTLk\/ can be effectively used by each monitor to reach a consistent global set of verdicts for each given formula, provided $k$ is sufficiently large. Our second main contribution is an algorithm for monitor construction enabling fault-tolerant distributed monitoring based on the aggregation of the individual verdicts by each monitor.

Domaines: Algorithme et structure de données [cs.DS]; Calcul parallèle, distribué et partagé [cs.DC]

Pierre Fraigniaud, Borzoo Bonakdarpour, Sergio Rajsbaum, David Rosenblueth, Corentin Travers. Decentralized Asynchronous Crash-Resilient Runtime Verification. 27th International Conference on Concurrency Theory (CONCUR), 2016, Québec, Canada. ⟨hal-01423646⟩