اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدA traditional tree-style tableau for LTL
58
0
0.0
(
0
)
تأليف
Mark Reynolds
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
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, the tableaux for this logic do not look like traditional tree-shaped tableau systems and their processing is often quite complicated. We present a new simple traditional-style tree-shaped tableau for LTL and prove that it is sound and complete. As well as being simple to understand, to introduce to students and to use manually, it also seems simple to implement and promises to be competitive in its automation. It is particularly suitable for parallel implementations.
قيم البحث
اقرأ أيضاً
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 t
echnique 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.
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
y to minimise the need for communication. However, a recently developed branch-independent tableaux for the common LTL temporal logic should intuitively be easy to parallelise as each branch can be developed independently. Here we describe a simple technique for partitioning such a tableau such that each partition can be processed independently without need for interprocess communication. We investigate the extent to which this technique improves the performance of the LTL tableau on standard benchmarks and random formulas.
In this paper we present a portfolio LTL-satisfiability solver, called Polsat. To achieve fast satisfiability checking for LTL formulas, the tool integrates four representative LTL solvers: pltl, TRP++, NuSMV, and Aalta. The idea of Polsat is to run
the component solvers in parallel to get best overall performance; once one of the solvers terminates, it stops all other solvers. Remarkably, the Polsat solver utilizes the power of modern multi-core compute clusters. The empirical experiments show that Polsat takes advantages of it. Further, Polsat is also a testing plat- form for all LTL solvers.
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
specification, reasoning about quality addresses the question of emph{how well} the system satisfies the specification. One direction in this effort is to refine the eventually operators of temporal logic to {em discounting operators}: the satisfaction value of a specification is a value in $[0,1]$, where the longer it takes to fulfill eventuality requirements, the smaller the satisfaction value is. In this paper we introduce an augmentation by discounting of Linear Temporal Logic (LTL), and study it, as well as its combination with propositional quality operators. We show that one can augment LTL with an arbitrary set of discounting functions, while preserving the decidability of the model-checking problem. Further augmenting the logic with unary propositional quality operators preserves decidability, whereas adding an average-operator makes some problems undecidable. We also discuss the complexity of the problem, as well as various extensions.
This continuously extended technical report collects and compares commonly used formulae from the literature and provides them in a machine readable way.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
