Informatica

In this paper, we consider piecewise linear aggregates (PLA) and a possibility to use a linear temporal logic for analysis of their performance over finite structures (finite linear temporal logic (LTL)). We describe a calculus where the search is performed with respect to a context of the formula. An important aspect of finite LTL is the simplicity of its model of time and actions. PLA is used for description of numerous complex systems. The answers about the behavior of the aggregate are got by finding an interpretation in which all the formulas describing the work of the aggregate are true. This is illustrated by formalizing alternative bit protocol (ABP) task. We describe the ABP by putting it in the form of a planning problem. From the obtained model, we can find a finite sequence of actions to be executed in order to achieve the goal. In addition, an alternative bit protocol problem is described using the planning domain description language (PDDL). We report the results of experiments conducted using the LPG-TD planner.

In stochastic programming and decision analysis, an important issue consists in the approximate representation of the multidimensional stochastic underlying process in the form of scenario tree. This paper presents the approach to generate the multistage multidimensional scenario tree out of a set of scenario fans. For this purpose, the multistage K-means clustering algorithm is developed. The presented scenario tree generation algorithm is motivated by the stability results for optimal values of a multistage stochastic program. The time complexity of developed multistage K-means clustering algorithm is proved to be linear in regard to the number of scenarios in the fan. The algorithm to determine the branches with nonduplicate information in the multistage scenario tree is also presented as an intermediate result of research.

The paper presents a technique that defines creation of ESTELLE/Ag specifications using knowledge bases (KB). Application KB is created using the knowledge acquisition technique joined with a piece‐linear aggregate model. The production rules of the application KB are transformed to decision tables, and the static properties of the KB are checked in PROLOGA system. Further, the application KB is combined with the defined KB of validated properties and validation method, and application KB dynamic properties are checked in the expert system in CLIPS. A validated application KB is used defining a framework of ESTELLE/Ag specification using PRAXIS editor and supplementing PRAXIS generated framework with the application functional description. The technique is illustrated with an example of a single channel queuing system.