اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدOn Sufficient and Necessary Conditions in Bounded CTL: A Forgetting Approach
140
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
Computation Tree Logic (CTL) is one of the central formalisms in formal verification. As a specification language, it is used to express a property that the system at hand is expected to satisfy. From both the verification and the system design points of view, some information content of such property might become irrelevant for the system due to various reasons, e.g., it might become obsolete by time, or perhaps infeasible due to practical difficulties. Then, the problem arises on how to subtract such piece of information without altering the relevant system behaviour or violating the existing specifications over a given signature. Moreover, in such a scenario, two crucial notions are informative: the strongest necessary condition (SNC) and the weakest sufficient condition (WSC) of a given property. To address such a scenario in a principled way, we introduce a forgetting-based approach in CTL and show that it can be used to compute SNC and WSC of a property under a given model and over a given signature. We study its theoretical properties and also show that our notion of forgetting satisfies existing essential postulates of knowledge forgetting. Furthermore, we analyse the computational complexity of some basic reasoning tasks for the fragment CTL_AF in particular.
قيم البحث
اقرأ أيضاً
Quantum supermaps are a higher-order generalization of quantum maps, taking quantum maps to quantum maps. It is known that any completely positive, trace non-increasing (CPTNI) map can be performed as part of a quantum measurement. By providing an ex
plicit counterexample we show that, instead, not every quantum supermap sending a quantum channel to a CPTNI map can be realized in a measurement on quantum channels. We find that the supermaps that can be implemented in this way are exactly those transforming quantum channels into CPTNI maps even when tensored with the identity supermap. We link this result to the fact that the principle of causality fails in the theory of quantum supermaps.
We formulate explicitly the necessary and sufficient conditions for the local invertibility of a field transformation involving derivative terms. Our approach is to apply the method of characteristics of differential equations, by treating such a tra
nsformation as differential equations that give new variables in terms of original ones. The obtained results generalise the well-known and widely used inverse function theorem. Taking into account that field transformations are ubiquitous in modern physics and mathematics, our criteria for invertibility will find many useful applications.
Matrix regularity is a key to various problems in applied mathematics. The sufficient conditions, used for checking regularity of interval parametric matrices, usually fail in case of large parameter intervals. We present necessary and sufficient con
ditions for regularity of interval parametric matrices in terms of boundary parametric hypersurfaces, parametric solution sets, determinants, real spectral radiuses. The initial n-dimensional problem involving K interval parameters is replaced by numerous problems involving 1<= t <= min(n-1, K) interval parameters, in particular t=1 is most attractive. The advantages of the proposed methodology are discussed along with its application for finding the interval hull solution to interval parametric linear system and for determining the regularity radius of an interval parametric matrix.
Convergence of the gradient descent algorithm has been attracting renewed interest due to its utility in deep learning applications. Even as multiple variants of gradient descent were proposed, the assumption that the gradient of the objective is Lip
schitz continuous remained an integral part of the analysis until recently. In this work, we look at convergence analysis by focusing on a property that we term as concavifiability, instead of Lipschitz continuity of gradients. We show that concavifiability is a necessary and sufficient condition to satisfy the upper quadratic approximation which is key in proving that the objective function decreases after every gradient descent update. We also show that any gradient Lipschitz function satisfies concavifiability. A constant known as the concavifier analogous to the gradient Lipschitz constant is derived which is indicative of the optimal step size. As an application, we demonstrate the utility of finding the concavifier the in convergence of gradient descent through an example inspired by neural networks. We derive bounds on the concavifier to obtain a fixed step size for a single hidden layer ReLU network.
We develop necessary and sufficient conditions and a novel provably consistent and efficient algorithm for discovering topics (latent factors) from observations (documents) that are realized from a probabilistic mixture of shared latent factors that
have certain properties. Our focus is on the class of topic models in which each shared latent factor contains a novel word that is unique to that factor, a property that has come to be known as separability. Our algorithm is based on the key insight that the novel words correspond to the extreme points of the convex hull formed by the row-vectors of a suitably normalized word co-occurrence matrix. We leverage this geometric insight to establish polynomial computation and sample complexity bounds based on a few isotropic random projections of the rows of the normalized word co-occurrence matrix. Our proposed random-projections-based algorithm is naturally amenable to an efficient distributed implementation and is attractive for modern web-scale distributed data mining applications.
الأسئلة المقترحة
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
