Searcharxiv⌕ Search

arXiv subjects

Wiktor B. Daszczuk

Publications and source records attributed to Wiktor B. Daszczuk.

At least 19 recordsLinked to original sources
arXiv2018

Cooperation of Multiple Autonomous Robots and Analysis of their Swarm Behavior

In this paper, we extended previous studies of cooperating autonomous robots to include situations when environmental changes and changes in the number of robots in the swarm can affect the efficiency to execute tasks assigned to the swarm of robots. We have presented a novel approach based on partition of the robot behavior. The sub-diagrams describing sub-routs allowed us to model advanced interactions between autonomous robots using limited number of state combinations avoiding combinatorial explosion of reachability. We identified the systems for which we can ensure the correctness of robots interactions. New techniques were presented to verify and analyze combined robots' behavior. The partitioned diagrams allowed us to model advanced interactions between autonomous robots and detect irregularities such as deadlocks, lack of termination etc. The techniques were presented to verify and analyze combined robots' behavior using model checking approach. The described system, Dedan verifier, is still under development. In the near future, timed and probabilistic verification are planned.

cs.RO↗
arXiv2017

Priority Rules on ATN (PRT) Intersections

In Autonomous Transit Networks some basic elements influence the throughput: network structure, maximum velocity, number of vehicles etc. Other parameters like station structure, dynamic routing or vehicle behavior on intersections play minor role. Yet in highly congested nets, when vehicles interfere in the traffic, some subtle decisions may influence overall system ridership. We tested the impact of intersection priority rules on passenger waiting time, which measures the throughput. The dependence occurred its relevance in a crowded network.

cs.MA↗
arXiv2017

Using Machine Learning to Enhance Vehicles Traffic in ATN (PRT) Systems

This paper discusses new techniques to enhance Automated Transit Networks (ATN, previously called Personal Rapid Transit - PRT) based on Artificial Intelligence tools. The main direction is improvement of the cooperation of autonomous modules that use negotiation protocols, following the IoT paradigm. One of the goals is to increase ATN system throughput by tuning up autonomous vehicles cooperation. Machine learning (ML) was used to improve algorithms designed by human programmers. We used "existing controls" corresponding to near-optimal solutions and built refinement models to more accurately relate a system's dynamics to its performance. A mechanism that mostly influences ATN performance is Empty Vehicle Management (EVM). The algorithms designed by human programmers was used: calls to empty vehicles for waiting passengers and balancing based on reallocation of empty vehicles to achieve better regularity of their settlement. In this paper we discuss how we can improve these algorithms (and tune them to current conditions) by using ML to tailor individual behavioral policies. Using ML techniques was possible because our algorithm is based on a set of parameters. A number of weights and thresholds could be tuned up to give better decisions on moving empty vehicles across the track.

cs.MA↗
arXiv2017

Critical trees: counterexamples in model checking of CSM systems using CBS algorithm

The important feature of temporal model checking is the generation of counterexamples. In the report, the requirements for generation of counterexample (called critical tree) in model checking of CSM systems are described. The output of TempoRG model checker for QsCTL logic (a version of CTL) is presented. A contradiction between counterexample generation and state space reduction is commented.

cs.SE↗
arXiv2017

State Space Reduction for Reachability Graph of CSM Automata

Classical CTL temporal logics are built over systems with interleaving model concurrency. Many attempts are made to fight a state space explosion problem (for instance, compositional model checking). There are some methods of reduction of a state space based on independence of actions. However, in CSM model, which is based on coincidences rather than on interleaving, independence of actions cannot be defined. Therefore a state space reduction basing on identical temporal consequences rather than on independence of action is proposed. The new reduction is not as good as for interleaving systems, because all successors of a state (in depth of two levels) must be obtained before a reduction may be applied. This leads to reduction of space required for representation of a state space, but not in time of state space construction. Yet much savings may occur in regular state spaces for CSM systems.

cs.SE↗
arXiv2017

Deadlock and Termination Detection using IMDS Formalism and Model Checking. Version 2

Modern model checking techniques concentrate on global properties of verified systems, because the methods base on global state space. Local features like partial deadlock or process termination are not easy to express and check. In the paper a description of distributed system in an Integrated Model of Distributed Systems (IMDS) combined with model checking is presented. IMDS expresses a dualism in distributed systems: server view and agent view. The formalism uses server states and messages. A progress in computations is defined in terms of actions consuming and producing states and messages. Distributed actions are totally independent and they do not depend on global state. Therefore, IMDS allows the designer to express local features of subsystems. In this model it is easy to describe various kinds of deadlock (including partial deadlock) and to differentiate deadlock from termination. The integration of IMDS with model checking is presented. Temporal formulas testing various kinds of deadlock (in communication or over resources) and termination are proposed.

cs.DC↗
arXiv2017

Macrogeneration and Automata Libraries For COSMA design environment

In ICS, WUT a COSMA design environment is being developed. COSMA is based on Concurrent State Machines (CSM) formalism of system specification. It contains a graphical tool for system design, various tools for the analysis (including a temporal model checker), simulator and code generator. In many projects, some common susbsystems take place. This concerns both complicated modules and simple counters. In the report, a concept of macrogeneration technique for building of libraries of automata is presented. The new technique will support a compactness of projects and reusability of modules.

cs.SE↗
arXiv2017

JADE - A Platform for Research on Cooperation of Physical and Virtual Agents

In the ICS, WUT a platform for simulation of cooperation of physical and virtual mobile agents is under development. The paper describes the motivation of the research, an organization of the platform, a model of agent, and the principles of design of the platform. Several experimental simulations are briefly described.

cs.MA↗
arXiv2017

Communication Dualism in Distributed Systems with Petri Net Interpretation

In the paper notion of communication dualism id formalized and explained in Petri net interpretation. We consider communication dualism a basic property of communication in distributed systems. The formalization is done in the Integrated Model of Distributed Systems (IMDS) where synchronous communication, as well as asynchronous message-passing and variable-sharing are modeled in a common framework. In the light of this property, communication in distributed systems can be seen as a two-dimensional phenomenon with passing being its spatial dimension and sharing its temporal dimension. Any distributed system can be modeled as a composition of message-passes asynchronous processes or as a composition of variable-sharing asynchronous processes. A method of automatic process extraction in Petri net interpretation of IMDS is presented.

cs.DC↗
arXiv2017

Timed Concurrent State Machines

Timed Concurrent State Machines are an application of Alur's Timed Automata concept to coincidence-based (rather than interleaving) CSM modeling technique. TCSM support the idea of testing automata, allowing to specify time properties easier than temporal formulas. Also, calculation of a global state space in real-time domain (Region Concurrent State Machines) is defined, allowing to store a verified system in ready-to-verification form, and to multiply it by various testing automata.

cs.LO↗
arXiv2017

Distributed algorithm for empty vehicles management in personal rapid transit (PRT) network

In this paper, an original heuristic algorithm of empty vehicles management in personal rapid transit network is presented. The algorithm is used for the delivery of empty vehicles for waiting passengers, for balancing the distribution of empty vehicles within the network, and for providing an empty space for vehicles approaching a station. Each of these tasks involves a decision on the trip that has to be done by a selected empty vehicle from its actual location to some determined destination. The decisions are based on a multi-parameter function involving a set of factors and thresholds. An important feature of the algorithm is that it does not use any central database of passenger input (demand) and locations of free vehicles. Instead, it is based on the local exchange of data between stations: on their states and on the vehicles they expect. Therefore, it seems well-tailored for a distributed implementation. The algorithm is uniform, meaning that the same basic procedure is used for multiple tasks using a task-specific set of parameters.

cs.DC↗
arXiv2017

Proposed benchmarks for PRT networks simulation

Personal Rapid Transit (PRT) is a promising form of urban transport. Its operation consists in the use of small unmanned vehicles which convey the passengers among stations within a dedicated network. Various aspects of the PRT network performance are frequently evaluated using the discrete-event simulation. The paper supports the need of establishing some reference models for the simulation of PRT networks, targeted mainly towards the needs of the research on network management algorithms. Three models of such PRT network models are proposed and discussed. The presented models can play the role of benchmarks which would be very useful for comparative evaluation of heuristic control algorithms, developed by different research groups.

physics.soc-ph↗
arXiv2017

Threefold Analysis of Distributed Systems: IMDS, Petri Net and Distributed Automata DA3

Integrated Model of Distributed Systems is used for specification and verification of distributed systems. In the formalism, a system is modeled as a set of servers' states and agents' messages. The operation of a system is modeled as actions converting global system configuration (a set of states and messages) to a new configuration. The formalism is used in Dedan verification environment, in which specification and verification of distributed systems is performed. Equivalent Petri nets are used for structural analysis. For the graphical specification and simulation of distributed systems, Distributed Autonomous and Asynchronous Automata (DA3) are invented. Such simulation does not require calculation of global configuration space of a system. Two forms of DA3 are shown: Server-DA3 (SDA3) for the server view and Agent-DA3 (ADA3) for the agent view.

cs.SE↗
arXiv2017

Rybu: Imperative-style Preprocessor for Verification of Distributed Systems in the Dedan Environment

Integrated Model of Distributed Systems (IMDS) is developed for specification and verification of distributed systems, and verification against deadlocks. On the basis of IMDS, Dedan verification environment was prepared. Universal deadlock detection formulas allow for automatic verification, without any knowledge of a temporal logic, which simplifies the verification process. However, the input language, following the rules of IMDS, seems to be exotic for many users. For this reason Rybu preprocessor was created. Its purpose is to build large models in imperative-style language, on much higher abstraction level.

cs.DC↗
arXiv2017

Practical Approach to Distributed Systems' Design

The paper, based on authors' experience from several distributed systems integration projects, summarizes briefly practical designer's view on methodological requirements and overall system organization, including clues as to the organization of the application layer, use of operating system and preferred communication protocols.

cs.DC↗
arXiv2017

Distributed management of Personal Rapid Transit (PRT) vehicles under unusual transport conditions

The paper presents a flexibility of management of vehicles in Personal Rapid Transit (PRT) network. The algorithm used for delivering empty vehicles for waiting passengers is based on multiparameter analysis. Due to its distributed construction, the algorithm has a horizon parameter, which specifies the maximum distance between stations the communications is performed. Every decision is made basing on an information about situation (number of vehicles standing at a station, number of vehicles travelling to a station, number of passengers waiting) sent between stations, without any central data base containing traffic conditions. The simulation of the traffic in random case (typical) and in unusual case of delivering people to a social event occurring at single place is presented. It is shown that simple manipulation with horizon parameter allows to adapt the network to extremely uneven demand and destination choice.

eess.SY↗
arXiv2017

Model Checking in The COSMA Environment as a Support for The Design of Pipelined Processing

The case study analyzed in the report involves the behavioral specification and verification of a three-stage pipeline consisting of mutually concurrent modules which also compete for a shared resource. The system components are specified in terms of Concurrent State Machines (CSM) and the verification technique used is the temporal model checking in the COSMA environment.

cs.SE↗