اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدTemporal Logic as Filtering
73
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
We show that metric temporal logic can be viewed as linear time-invariant filtering, by interpreting addition, multiplication, and their neutral elements, over the (max,min,0,1) idempotent dioid. Moreover, by interpreting these operators over the field of reals (+,*,0,1), one can associate various quantitative semantics to a metric-temporal-logic formula, depending on the filters kernel used: square, rounded-square, Gaussian, low-pass, band-pass, or high-pass. This remarkable connection between filtering and metric temporal logic allows us to freely navigate between the two, and to regard signal-feature detection as logical inference. To the best of our knowledge, this connection has not been established before. We prove that our qualitative, filtering semantics is identical to the classical MTL semantics. We also provide a quantitative semantics for MTL, which measures the normalized, maximum number of times a formula is satisfied within its associated kernel, by a given signal. We show that this semantics is sound, in the sense that, if its measure is 0, then the formula is not satisfied, and it is satisfied otherwise. We have implemented both of our semantics in Matlab, and illustrate their properties on various formulas and signals, by plotting their computed measures.
قيم البحث
اقرأ أيضاً
Whereas standard treatments of temporal logic are adequate for closed systems, having no run-time interactions with their environment, they fall short for reactive systems, interacting with their environments through synchronisation of actions. This
paper introduces reactive temporal logic, a form of temporal logic adapted for the study of reactive systems. I illustrate its use by applying it to formulate definitions of a fair scheduler, and of a correct mutual exclusion protocol. Previous definitions of these concepts were conceptually much more involved or less precise, leading to debates on whether or not a given protocol satisfies the implicit requirements.
We propose a measure and a metric on the sets of infinite traces generated by a set of atomic propositions. To compute these quantities, we first map properties to subsets of the real numbers and then take the Lebesgue measure of the resulting sets.
We analyze how this measure is computed for Linear Temporal Logic (LTL) formulas. An implementation for computing the measure of bounded LTL properties is provided and explained. This implementation leverages SAT model counting and effects independence checks on subexpressions to compute the measure and metric compositionally.
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 propose a new logic for expressing and reasoning about probabilistic hyperproperties. Hyperproperties characterize the relation between different independent executions of a system. Probabilistic hyperproperties express quantitative
dependencies between such executions. The standard temporal logics for probabilistic systems, i.e., PCTL and PCTL* can refer only to a single path at a time and, hence, cannot express many probabilistic hyperproperties of interest. The logic proposed in this paper, HyperPCTL, adds explicit and simultaneous quantification over multiple traces to PCTL. Such quantification allows expressing probabilistic hyperproperties. A model checking algorithm for the proposed logic is also given for discrete-time Markov chains.
Linear temporal logic was introduced in order to reason about reactive systems. It is often considered with respect to infinite words, to specify the behaviour of long-running systems. One can consider more general models for linear time, using words
indexed by arbitrary linear orderings. We investigate the connections between temporal logic and automata on linear orderings, as introduced by Bruy`ere and Carton. We provide a doubly exponential procedure to compute from any LTL formula with Until, Since, and the Stavi connectives an automaton that decides whether that formula holds on the input word. In particular, since the emptiness problem for these automata is decidable, this transformation gives a decision procedure for the satisfiability of the logic.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
