Studia Informatica. System and information technology <p><strong>ISSN:</strong> 1731-2264</p> <p><strong>DOI:</strong> 10.34739</p> <p><strong>Points:</strong> 20</p> en-US (Jerzy Tchórzewski) (Piotr Świtalski) Thu, 23 Dec 2021 00:00:00 +0000 OJS 60 Unbounded Model Checking for ATL <p>In this paper, we deal with verification of multi-agent systems represented as concurrent game structures. To express properties to be verified, we use Alternating-Time Temporal Logic (ATL) formulas. We provide an implementation of symbolic model checking for ATL and preliminary, but encouraging experimental results.</p> Michał Kański, Artur Niewiadomski, Magdalena Kacprzak, Wojciech Penczek, Wojciech Nabiałek Copyright (c) 0 Thu, 23 Dec 2021 00:00:00 +0000 Quantum inspiration to build a neural model based on the Day-Ahead Market of the Polish Power Exchange <p>The article is an attempt of the methodological approach to the proposed quantum-inspired method of neural modeling of prices quoted on the Day-Ahead Market operating at TGE S.A. In the proposed quantum-inspired neural model it was assumed, inter alia, that it is composed of 12 parallel Perceptron ANNs with one hidden layer. Moreover, it was assumed that weights and biases as processing elements are described by density matrices, and the values flowing through the Artificial Neural Network of Signals are represented by qubits. Calculations checking the correctness of the adopted method and model were carried out with the use of linear algebra and vector-matrix calculus in MATLAB and<br>Simulink environments. The obtained research results were compared to the results obtained from the neural model with the use of a comparative model.</p> Dariusz Ruciński Copyright (c) 0 Thu, 23 Dec 2021 00:00:00 +0000 Neural model of human gait and its implementation in MATLAB and Simulink Environment using Deep Learning Toolbox <p>The article presents selected results of research on the modeling of humanoid robots, including the results of neural modeling of human gait and its implementation in the environment MATLAB and Simulink with the use of Deep Learning Toolbox. The subject of the research was placed within the scope of the available literature on the subject. Then, appropriate research experiments on human movement along a given trajectory were developed. First, the method of measuring the parameters present in the experiment was established, i.e. input quantities (displacement of the left heel, displacement of the right heel) and output quantities (displacement of the measurement point of the human body in space). Then, research experiments were carried out, as a result of which numerical data were measured in order to use them for teaching and testing the Artificial Neural Network. The Perceptron Artificial Neural Network architecture was used to build a model of a neural human walk along a given trajectory. The obtained results were discussed and interpreted, drawing a number of important conclusions.</p> Jerzy Tchórzewski, Arkadiusz Wielgo Copyright (c) 0 Thu, 23 Dec 2021 00:00:00 +0000 Comparative Study of the Identification Methods of the Management System of the Day-Ahead Market of Polish Energy Market S.A. <p>Nowadays, identification and neural methods are used more and more often in modeling IT forecasting systems in addition to analytical methods. Six characteristic models used to forecast the Day-Ahead Market system functioning as a transaction management system at the Polish Power Exchange (POLPX) and the Nord Pool Spot market have been selected for comparative analysis. The research was preceded by a detailed discussion of modern criteria used to assess the quality of model fitting to the system, namely: effectiveness, efficiency, and robustness. In the literature, there are two main groups of system modeling methods, namely time series modeling methods and identification modeling methods, including neural modeling methods. Modeling usually results in such models as parametric models and artificial neural networks learned neural models of the Day-Ahead Market, as well as time series models, among others. In the comparative analysis, special attention was paid to the accuracy of the obtained models concerning the system. It has been pointed out that the studied solutions used to measure the accuracy of modeling criteria such as accuracy of fit or efficiency, and did not use the modeling efficiency, which is very important in IT forecasting systems for such large markets as the Day-Ahead Market of POLPX. The search for the best market models, including identification models of the Day-Ahead Market operation that can be used in electricity price forecasting is a very important issue both from the point of view of algorithmic solutions and economical solutions.</p> Radosław Marlęga Copyright (c) 0 Thu, 23 Dec 2021 00:00:00 +0000 Firefly algorithm applied to the job-shop scheduling problem <p>The job shop scheduling problem (JSSP) is one of the most researched scheduling problems. This problem belongs to the NP-hard class. An optimal solution for this category of problems is rarely possible. We try to find suboptimal solutions using heuristics or metaheuristics. The firefly algorithm is a great example of a metaheuristic. In this paper, this algorithm is used to solve JSSP. We used some benchmarking JSSP datasets for experiments. The experimental program was implemented in the aitoa library. We investigated the optimal parameter settings of this algorithm in terms of JSSP. Analysis of the experimental results shows that the algorithm is useful to solve scheduling problems.</p> Piotr Świtalski, Arkadiusz Bolesta Copyright (c) 0 Thu, 23 Dec 2021 00:00:00 +0000 ICT security in tax administration - AV protection systems <p>The article discusses the topic of ICT security in tax administration. This paper presents a study of the security level of endpoints8, servers using three antivirus protection systems. It discusses three independent solutions used to ensure the protection of ICT equipment in public administration.</p> Tomasz Muliński Copyright (c) 0 Thu, 23 Dec 2021 00:00:00 +0000