Article
Адаптивная редукция симметричных моделей в задаче верификации моделей программ для логики линейного времени
The research is carried out in accord with the main principles of communicative and paradigmatic linguistics. It is devoted to the study of lingual ways of expressing harmony as an ethetic category. Rhythm as a regular repetition of similar and commensurable units of language is considered to be the main mechanism of the harmonious organization of belle-lettres style texts. The high efficiency of rhythm as a stylistic device creates the expressiveness of the text at all the levels of language, beginning with the phonemic level and finishing with the dictemic level. The principle of repeatability of elements and their relations within the system of semantic and syntactic ties manifests internal symmetry; and the symmetry of text elements is the main indicator of its harmony.
One of the most simple models of computation which is suitable for representation of reactive systems behaviour is a finite state transducer which operates over an input alphabet of control signals and an output alphabet of basic actions. A behaviour of such a reactive system displays itself in the correspondence between flows of control signals and compositions of basic actions performed by the system. We believe that behaviour of this kind requires more suitable and expressive means for formal specifications than conventional LTL. In this paper we define some new (as far as we know) extension LP-LTL of Linear Temporal Logic specifically intended for describing the properties of transducers computations. In this extension the temporal operators are parameterized by sets of words (languages) which aANaANrepresent distinguished flows of control signals that impact on a reactive system. Basic predicates in our variant of temporal logic are also languages in the alphabet of basic actions of a transducer; they represent the expected response of a transducer to the specified environmental influences. In our earlier papers we considered model checking problem for LP-LTL and LP-CTL and showed that this problem has effective solutions. The aim of this paper is to estimate the expressive power of LP-LTL by comparing it with some well known logics widely used in computer science for specification of reactive systems behaviour. We discovered that a restricted variant LP-1 -LTL of our logic is more expressive than LTL and another restricted variant LP-n-LTL has the same expressive power as monadic second order logic S1S.
A model for organizing cargo transportation between two node stations connected by a railway line which contains a certain number of intermediate stations is considered. The movement of cargo is in one direction. Such a situation may occur, for example, if one of the node stations is located in a region which produce raw material for manufacturing industry located in another region, and there is another node station. The organization of freight traffic is performed by means of a number of technologies. These technologies determine the rules for taking on cargo at the initial node station, the rules of interaction between neighboring stations, as well as the rule of distribution of cargo to the final node stations. The process of cargo transportation is followed by the set rule of control. For such a model, one must determine possible modes of cargo transportation and describe their properties. This model is described by a finite-dimensional system of differential equations with nonlocal linear restrictions. The class of the solution satisfying nonlocal linear restrictions is extremely narrow. It results in the need for the “correct” extension of solutions of a system of differential equations to a class of quasi-solutions having the distinctive feature of gaps in a countable number of points. It was possible numerically using the Runge–Kutta method of the fourth order to build these quasi-solutions and determine their rate of growth. Let us note that in the technical plan the main complexity consisted in obtaining quasi-solutions satisfying the nonlocal linear restrictions. Furthermore, we investigated the dependence of quasi-solutions and, in particular, sizes of gaps (jumps) of solutions on a number of parameters of the model characterizing a rule of control, technologies for transportation of cargo and intensity of giving of cargo on a node station.
Event logs collected by modern information and technical systems usually contain enough data for automated process models discovery. A variety of algorithms was developed for process models discovery, conformance checking, log to model alignment, comparison of process models, etc., nevertheless a quick analysis of ad-hoc selected parts of a journal still have not get a full-fledged implementation. This paper describes an ROLAP-based method of multidimensional event logs storage for process mining. The result of the analysis of the journal is visualized as directed graph representing the union of all possible event sequences, ranked by their occurrence probability. Our implementation allows the analyst to discover process models for sublogs defined by ad-hoc selection of criteria and value of occurrence probability
Existing approaches suggest that IT strategy should be a reflection of business strategy. However, actually organisations do not often follow business strategy even if it is formally declared. In these conditions, IT strategy can be viewed not as a plan, but as an organisational shared view on the role of information systems. This approach generally reflects only a top-down perspective of IT strategy. So, it can be supplemented by a strategic behaviour pattern (i.e., more or less standard response to a changes that is formed as result of previous experience) to implement bottom-up approach. Two components that can help to establish effective reaction regarding new initiatives in IT are proposed here: model of IT-related decision making, and efficiency measurement metric to estimate maturity of business processes and appropriate IT. Usage of proposed tools is demonstrated in practical cases.