Efficient Decentralized LTL Monitoring Framework Using Tableau Technique

TL;DR

This paper introduces a new decentralized LTL monitoring framework using tableau techniques to optimize communication and observation strategies, improving efficiency and flexibility over existing methods.

Contribution

It proposes a novel tableau-based approach for decentralized LTL monitoring that enhances efficiency, flexibility, and simplicity compared to prior techniques.

Findings

Optimized round-robin communication policy for processes.

Processes propagate observations based on tableau structure.

Framework outperforms existing methods in efficiency and flexibility.

Abstract

This paper presents a novel framework for decentralized monitoring of Linear Temporal Logic (LTL), under the situation where processes are synchronous, uniform (i.e. all processes are peers), and the formula is represented as a tableau. The tableau technique allows one to construct a semantic tree for the input formula, which can be used to optimize the decentralized monitoring of LTL in various ways. Given a system P and an LTL formula L, we construct a tableau for L. The tableauis used for two purposes: (a) to synthesize an efficient round-robin communication policy for processes, and (b) to allow processes to propagate their observations in an optimal way. In our framework, processes can propagate truth values of atomic formulas, compound formulas, and temporal formulas depending on the syntactic structure of the input LTL formula and the observation power of processes. We demonstrate that this approach of decentralized monitoring based on tableau construction is more straightforward, more flexible, and more likely to yield efficient solutions than alternative approaches.