It is common to use the first-order language as a formal tool for describing properties of various (computational) structures. On the one hand, this language is well understood and easy to use; on the other, many questions that are im-portant from the applications point of view related to this language are algorithmically undecidable, i.e., cannot be answered using a computer program. These days, there exist various alternative languages that can be used for describing computational processes and their properties, for which the corresponding questions are, in contrast to the first-order language, algorithmically decidable. In this paper, we consider one of such languages, – the language of the Computational Tree Logic (CTL). It is commonly used for program verification as it is capable of describing properties of computational processes, – in particular, properties of the binary relation used in the Kripke semantics. The authors investigate the possibility of finding algorithmically first-order formulas defining the same classes of Kripke frames as the formulas of the language of CTL. It is well known the problem of finding first-order correspondents of propositional intuitionistic formulas is algorithmically undecidable. The authors reduce – using the Gödel translation of intuitionistic formulas into modal ones, and subsequently a translation of resultant modal formulas into CTL-formulas – the first-order correspondence problem for propositional intuitionistic formulas to the first-order correspondence problem for CTL-formulas on Kripke frames. As a result of this reduction, they prove that the first-order correspondence problem for CTL-formulas is algorithmically undecidable. In the conclusion, the authors discuss some possible modifications of their construction for fragments of the language of CTL as well as algorithmic decidability of the CTL correspondence problem for first-order formulas.
The article provides information about analysis of data collection using logic-set histogram representation. This type of representation is based on using histogram and a special mathematical system that allows implementing user queries as statements/expressions with logic and set operations. Result of the analysis is a quantitative value of presence of elements (designated in a query) in a data. Moreover, it’s possible to use a sample query to find quantitative values of similarity to an analyzed data. Collection is defined as a list of one-type data (for example, textual documents, images, video or others), which is made up of a universal set elements. Each element of a collection matches with its histogram representation. The paper considers two approaches of analysis of data collection using the logic-set histogram representation.
The article presents a comparative analysis of neural network modeling and regression analysis for forecasting the S & P 500 index. Initially, the forecast of the absolute value of the index is provided, then we justify the use of stationery data, that is, the return of S & P 500. The comparison of two methods is carried out in two stages. Firstly methods are compared by the coefficient of determination on the periods of three and twelve months, and by the quality of trend predictions. Note that the choice of model and its testing is performed at different time intervals (the so-called in-sample and out-of-sample periods). Taking into account the fact that the primary desire of a typical trader is to gain a profit at the second stage we have chosen such trading criteria as profit and profit, weighted on risk (drawdown). On a longer time interval (12 months) regression shows the best results, but in terms of economic gains neural network win. When we consider a shorter period (3 months) neural network has better results. Thus, neural networks are able to assess the dynamics of the stock due to its flexibility and ability to find non-linear patterns.
The paper describes a federated identity management infrastructure based on eduroam. This technology enables secure authentication using single netid for network and resources access in eduroam federation. Major protocols and technologies for transparent user authentication are covered. A way of authorization, based on membership in institutional groups and individual user membership is proposed. For user authentication a service provider sends an authentication request contained the encrypted user name and password to user's institute RADIUS server (identity provider). Identity provider is determined by the domain user name/ The authentication request is passed through th eduroam hierarchy of proxy RADIUS servers. If the service provider provides special access for a certain group of users, it also sends a request to group identity RADIUS-server. A request passes through a hierarchy of group RADIUS servers for group membership checking. Eduroam federation and group RADIUS servers hierarchies are based on the domain name system. The implementation of these mechanisms requires a slight modification of service provider RADIUS server for group support and do not require changes of the identity provider and eduroam federations RADIUS servers. Group support is fully compatible with the existing eduroam infrastucture, the both types of RADIUS servers with and without group support can operate simultaneously
This review is devoted to the history of the General situation of movements of dynamic and non-Autonomous periodic systems, as it turned out that a full and detailed description of the General situation it allows solving the problem of constructing generalized-periodic motions of dynamical and nonautonomous periodic systems. The necessity of numerical study of these systems is explained by the fact that the vast majority of models of real technical, biological, economic and other processes are described by such systems.
This article describes image retrieval using semantic features which is based on conversion from visual features to convenient form for human perception. Particularly, on these pages considered general conception of image retrieval via textual description of image features and textual retrieval via semantic features of image.
The creation of software of analyst workplace supporting the mining process large amounts of statistical data of science, education and innovation are discussed in the paper. A hybrid approach, to the integration of classical methods of mathematical correlation analysis, pattern analysis and time series, as well as the interpretation of the results is provided. Particular attention is paid to the business processes to identify trends and changes in indicators, atypical dynamics of indicators and to the definition of «Best Performance» indicators vectors.