Efficient Decentralized LTL Monitoring Framework Using Tableau Technique
Omar Al-Bataineh, David Rosenblum

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…
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.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Logic, Reasoning, and Knowledge
