arXiv subjects

David Rosenblum

Publications and source records attributed to David Rosenblum.

3 recordsLinked to original sources

arXiv2018

Efficient LTL Decentralized Monitoring Framework Using Formula Simplification Table

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 all possible simplifications of the formula under different truth assignments of its variables. The advantages of constructing a simplification table of a formula are two-fold. First, it can be used to compute the logical influence weight of each variable in the formula, which is a metric that shows the importance of the variable in affecting the outcome of the formula. Second, it can be used to identify variables that have the highest logical influences on the outcome of the formula. %The simplification table can be used to optimize %existing solutions for several interesting %LTL verification problems. We demonstrate the effectiveness of formula simplification table in the context of software verification by developing efficient framework to the well-known decentralized LTL monitoring problem.

cs.LO↗

arXiv2018

Efficient Decentralized LTL Monitoring Framework Using Tableau Technique

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.

cs.LO↗

arXiv2018

Computing Maximal Expected Termination Time of Probabilistic Timed Automata

The paper addresses the problem of computing maximal expected time to termination of probabilistic timed automata (PTA) models, under the condition that the system will, eventually, terminate. This problem can exhibit high computational complexity, in particular when the automaton under analysis contains cycles that may be repeated very often (due to very high probabilities, e.g. p =0.999). Such cycles can degrade the performance of typical model checking algorithms, as the likelihood of repeating the cycle converges to zero arbitrarily slowly. We introduce an acceleration technique that can be applied to improve the execution of such cycles by collapsing their iterations. The acceleration process of a cyclic PTA consists of several formal steps necessary to handle the cumulative timing and probability information that result from successive executions of a cycle. The advantages of acceleration are twofold. First, it helps to reduce the computational complexity of the problem without adversely affecting the outcome of the analysis. Second, it can bring the "worst case execution time" problem of PTAs within the bounds of feasibility for model checking techniques. To our knowledge, this is the first work that addresses the problem of accelerating execution of cycles that exhibit both timing and probabilistic behavior.

cs.FL↗