ﻻ يوجد ملخص باللغة العربية
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.
This paper presents a new technique for optimizing formal analysis of propositional logic formulas and Linear Temporal Logic (LTL) formulas, namely the formula simplification table. A formula simplification table is a mathematical table that shows al
Propositional linear time temporal logic (LTL) is the standard temporal logic for computing applications and many reasoning techniques and tools have been developed for it. Tableaux for deciding satisfiability have existed since the 1980s. However, t
In recent years, there is growing need and interest in formalizing and reasoning about the quality of software and hardware systems. As opposed to traditional verification, where one handles the question of whether a system satisfies, or not, a given
This continuously extended technical report collects and compares commonly used formulae from the literature and provides them in a machine readable way.
For many applications, we are unable to take full advantage of the potential massive parallelisation offered by supercomputers or cloud computing because it is too hard to work out how to divide up the computation task between processors in such a wa