Informatica

The paper deals with a simple model of the competition of two queuing systems, providing the same service. Each system may vary its service price and its service rate. The customers choose the system with less total service price, that depends on the waiting time and on the service price. The possibility for the existence of equilibrium is investigated. Simple cases are investigated analytically. It is shown that the Nash equilibrium exists in special cases only. A modification of the Stakelberg equilibrium is proposed as a model of competition with a prognosis. This prognosis helps form more stable prices and more stable strategies of competitors. The case of social economics is investigated, too. The dynamics of the competition of more realistic stochastic queuing systems is investigated by Monte Carlo simulation. The simulative analysis is realized by means of a rule-based simulation system.

An analysis of an event driven local area network protocol for special purposes in industrial applications is represented. The analysis is performed using the specification language ESTELLE/Ag and protocol analysis tool PRANAS-2. Validation was focused on the correctness media access algorithm, initialization of the protocol and recovery from error situations. The obtained simulation results can be used for comparison of the effectiveness of this protocol with other protocols.

The model of the HIV/AIDS infection spread is proposed and investigated. The paper deals with some specific features of the disease spread at the initial stage, i.e., when the infection extent is small enough. We propose a model characterizing any risk group by three differential equations. These equations describe the dynamics of active susceptible, active infected, and passive infected individuals. The evaluation of parameters from demographical and medical data is discussed. The package for the investigation of infection is presented, and possibilities to control the infection are shown. Two general directions of control may be distinguished: the HIV/AIDS blood tests and the publicity and availability of protective means. The investigations showed under what conditions the HIV/AIDS infection may be stopped.

The aggregate approach to the formal description, verification and simulation of computer network protocols is considered in the paper. With this approach, the offered design stages can be performed using a single mathematical scheme. The reachability analysis method and the program proof technique are viewed as methods for correctness analysis. The proposed approach for correctness analysis and model construction was used in creating the protocol analysis system PRANAS.