PL
 |
EN
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 16

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last
Wyniki wyszukiwania
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote Wyznaczanie precyzji i dokładności lokalizacji obiektu na przykładzie systemu lokalizacji wewnątrzbudynkowej Dimension4 firmy Ubisense
Eljasz D., Tkacz J., Gratkowski T., Doligalski M.
Przegląd Elektrotechniczny
|
2018
|
R. 94, nr 12
56--59
PL
Systemy umożliwiające lokalizację obiektu zdobywają coraz większą popularność. Kilka lat temu jedynym ogólnodostępnym systemem lokalizacyjnym był amerykański Navstar GPS, który niestety nie pracował w pomieszczeniach zamkniętych takich jak magazyny, czy hale produkcyjne. Postęp technologiczny i miniaturyzacja sprawiły, że systemy lokalizacyjne wkroczyły w nowy obszar. W artykule zaprezentowano wyniki testów precyzji i dokładności lokalizacji obiektów z użyciem systemu lokalizacji wewnątrzbudynkowej Dimension4 firmy Ubisense.
EN
Systems enabling the location of objects are gaining more and more popularity. A few years back, only the American localization system Navstar GPS has been available for commercial use. Unfortunately, this system does not perform well in enclosed spaces such as buildings, warehouses or production halls. Technological progress and miniaturization possibilities have made the localization systems enter the previously unavailable area. In this paper tests for determining the precision and accuracy of the Ubisense Dimension4 indoor location system are presented.
2
Content available Dual synthesis of Petri net based application specific logic controllers with increased safety
Tkacz J., Bukowiec A., Adamski M.
Bulletin of the Polish Academy of Sciences. Technical Sciences
|
2016
|
Vol. 64, nr 3
467--478
EN
In the paper, design flow of the application specific logic controllers with increased safety by means of Petri nets is proposed. The controller architecture is based on duplicated control unit and comparison results from both units. One specification of control algorithm is used by means of Petri net for both units. The hardware duplication is obtained during dual synthesis process. This process uses two different logic synthesis methods to obtain two different hardware configurations for both control units. Additionally, the dual verification is applied to increase reliability of the control algorithm. Such design flow simplifies the process of realization of control systems with increased safety.
3
Content available remote Analiza tablic decyzyjnych z wykorzystaniem monotonicznego rachunku sekwensów
Tkacz J., Adamski M.
Przegląd Elektrotechniczny
|
2013
|
R. 89, nr 6
256--259
PL
W artykule przedstawiono nowatorski sposób analizy systemów regułowych z wykorzystaniem symbolicznego wnioskowania w monotonicznej logice sekwentów Gentzena. Badany system dyskretny jest opisywany w postaci tablicy decyzyjnej. Celem analizy systemu jest usunięcie zbytecznych kolumn w tablicy decyzyjnej oraz nieistotnych symboli zmiennych logicznych w jej poszczególnych wierszach. Efektywny aparat wnioskowania w logice formalnej umożliwia sprawne wyznaczanie transwersal krawędzi hipergrafu rozróżnialności.
EN
The paper presents a new methodology for symbolic reduction of multivalued decision tables, currently intensively used for compact behavioral specifications of logic controllers. As an example the well known problem of simplification of a set of several logic rules with many variables is chosen. As a completely new, original solution, the formal automated reasoning based on Gentzen propositional calculus together with hypergraph theory are jointly used. The clique-transversal symbolic calculation is performed by means of effective reasoning in Gentzen calculus.
4
Content available Rozpoznawanie symboli języka migowego z wykorzystaniem algorytmów cyfrowego przetwarzania obrazów
Fogiel A., Tkacz J.
Pomiary Automatyka Kontrola
|
2013
|
R. 59, nr 11
1167--1170
PL
W artykule został opisany proces projektowania i realizacji aplikacji, przeznaczonej do analizy, w czasie rzeczywistym, obrazów cyfrowych zawierających symbole języka migowego. Stworzone oprogramowanie zostało napisane w języku C++. Wykorzystuje ono bibliotekę OpenCV w połączeniu z sensorem Microsoft Kinect. Oprogramowanie przetwarza około 15 klatek obrazu w ciągu sekundy i rozpoznaje gesty ze skutecznością 71% . Opracowane oprogramowanie jest odporne w znacznym stopniu na wpływ warunków oświetleniowych.
EN
The paper describes the implementation process of application that recognizes sign language symbols which are presented by a user in real time. The first part of this paper presents software and libraries used by this program. It also contains description of a Microsoft Kinect sensor with explanation of its operation. The second part of this paper is dedicated to KinectSL application. It presents the structure of the application, its algorithm and a study that led to the described method of recognizing sign language gestures. Section 5 deals with main problems that appeared while working on the project such as detecting writs and fingers. Subsection 5.4 contains the detailed explanation of parameters that are passed to a KNN classifier and formulas necessary to compute them. The presented application is multi-platform and can be run on Windows, Linux and MacOS operating systems. This software is able to recognize gestures for two hand at once that allows it to support advanced gestures. The tests carried out showed that KinectSL processed 15 frames per second and its performance of gestures recognizing was above 71 percent. The described system is a good basis to create a program that will be able to fluent translate sign language. It can also be used in industry and entertainment to control processes with user gestures.
5
Content available Structured Mapping of Petri Net States and Events for FPGA Implementations
Tkacz J., Adamski M.
International Journal of Electronics and Telecommunications
|
2013
|
Vol. 59, No. 4
331-339
EN
The paper presents a new method of structured encoding of global internal states and events in Reconfigurable Logic Controllers, which are directly mapped into Field Programmable Gate Arrays (FPGA). Modular, concurrently decomposed, colored state machine is chosen as a intermediate model, before the mapping of Petri net into an array structure of dedicated but very flexible and reliable digital system. The initial textual specification in formal Gentzen logic serves both as a design description for a rapid prototyping, as well as formal model, suitable for detailed computer-based reasoning about optimized and synthesized logic controller, implemented in configurable hardware. Only the selected linear subset from general, universal propositional Gentzen Logic is necessary to deduce several properties of the net, such as relations of nonconcurrency among structurally ordered macroplaces. The goal of this paper is to present the design methodology for modeling and synthesis of discrete controllers using related Petri net theory, rule-based theory (mathematical logic), and VHDL.
6
Content available Implementation of Algorithm of Petri Nets Distributed Synthesis into FPGA
Bukowiec A., Tkacz J., Gratkowski T., Gidlewicz T.
International Journal of Electronics and Telecommunications
|
2013
|
Vol. 59, No. 4
317-324
EN
In the paper an implementation of algorithm of Petri net array-based synthesis is presented. The method is based on decomposition of colored interpreted macro Petri net into subnets. The structured encoding of places in subnets is done of using minimal numbers of bits. Microoperations, which are assigned to places, are written into distributed and flexible memories. It leads to realization of a logic circuit in a twolevel concurrent structure, where the combinational circuit of the first level is responsible for firing transitions, and the second level memories are used for generation of microoperations. This algorithm is implemented in C# and delivered as a stand alone library.
7
Content available remote Koncepcja i realizacja systemu wnioskującego Gentzena z wykorzystaniem RDBMS – IBM DB2
Gaczyński A., Tkacz J., Doligalski M.
Przegląd Elektrotechniczny
|
2012
|
R. 88, nr 8
148-151
PL
Poniższy artykuł przedstawia realizację systemu wnioskującego Gentzena z wykorzystaniem systemu zarządzania relacyjną bazą danych IBM DB2 w wersji 9.7. Niniejsza publikacja prezentuje zalety z używania procedur składowanych oraz w jaki sposób można wykorzystać strukturę tabel w bazie danych do zaawansowanego przetwarzania informacji. Przedstawia użycie bazy danych przy implementacji automatycznych systemów dowodzenia twierdzeń oraz w jaki sposób architektura klient-serwer znajduje zastosowanie w stosunku do tego typu aplikacji.
EN
The paper presents conception and design of Gentzen deduction system by using RDBMS – IBM DB2. It shows adds of stored procedures and method of using table structure in database for advanced information computing. Testing of the solution is based on the analysis of randomly generated not oriented graphs. The tests confirm the correctness of implementations, and also highlight the problem of high computational complexity. This unusual implementation and use of RDBMS environment opens up new areas of research on the optimization of reasoning algorithm.
8
Content available remote Kodowanie makrostanów rekonfigurowalnego sterownika matrycowego na podstawie struktury topologicznej interpretowanej sieci Petriego
Tkacz J., Adamski M.
Przegląd Elektrotechniczny
|
2012
|
R. 88, nr 8
137-140
PL
W artykule przedstawiono metodę kodowania stanów lokalnych i globalnych cyfrowego sterownika matrycowego, realizowanego z wykorzystaniem struktur FPGA. Funkcjonowanie sterownika z wejściami i wyjściami opisanymi sygnałami binarnymi jest przedstawione z wykorzystaniem interpretowanej, sterującej sieci Petriego. Struktura topologiczna sieci jest odwzorowana na specyfikację logiczną w języku sekwentów Gentzena. Relacja sekwencyjności między miejscami sieci uzyskiwana jest metodą wnioskowania komputerowego.
EN
The paper presents the method of local and global states encoding for configurable logic controller, which is designed by means of Field Programmable Logic Arrays (FPGA). The desired behaviour of controller is specified as hierarchical control interpreted Petri net. The inputs and outputs of controller are described as sets of binary signals. Relationship among places of Petri net, such as concurrency and sequentiality is obtained by using symbolic deduction method and presented as hypergraphs.
9
Content available UML Modelling in Rigorous Design Methodology for Discrete Controllers
Łabiak G., Adamski M., Doligalski M., Tkacz J., Bukowiec A.
International Journal of Electronics and Telecommunications
|
2012
|
Vol, 58, No. 1
27-34
EN
The paper presents an application of UML technology in a discrete system development process. In the process at the analysis stage UML diagrams are fundamental tool. The outcome of this stage is a basis for formal models exploited at the design stage, where the design is symbolically verified and treated as a rule-based system. Two formal models of good graphical appeal are proposed: Petri nets and state machine diagrams. Both are heavily using Boolean expressions what makes that design can easily be implemented in modern programmable structures.
10
Content available Wyznaczanie SM - pokrycia bezpiecznej sieci Petriego metodą komputerowego wnioskowania
Tkacz J., Adamski M.
Pomiary Automatyka Kontrola
|
2011
|
R. 57, nr 11
1397-1400
PL
W artykule przedstawiono nowy sposób pokrywania bezpiecznej sieci Petriego minimalną liczbą podsieci automatowych. Metoda symboliczna polega na wczesnej selekcji odpowiednich transwersali, stopniowo wyznaczanych dla rodziny maksymalnych podzbiorów współbieżnych miejsc sieci. W przypadku bezpiecznej sterującej sieci Petriego, miejsca traktowane są jako stany lokalne, natomiast ich dopuszczalne konfiguracje określają jej stany globalne. Transwersale wyróżniają podzbiory miejsc niewspółbieżnych, przypisanych do odpowiednich SM-podsieci. Komputerowe wnioskowanie odbywa się w monotonicznym rachunku sekwentów Gentzena. Rezultaty wykorzystywane są podczas syntezy cyfrowych, konfigurowanych sterowników logicznych z zastosowaniem komercjalnego oprogramowania i języków opisu sprzętu.
EN
The paper presents a way of finding a suitable Petri net cover by means of a minimal number of maximal State Machine subnets (SM-components). A new symbolic method of Petri net parallel decomposition is based on early selection of proper minimal transversals, taken from family of all global Petri net states. Global states are given in advance as maximal subsets, formed from mutually concurrent places. They can be found as reachable global states of Petri net. During digital design of a logic controller, the places of the safe Petri net are treated as local internal states of Concurrent State Machine, implemented in a reconfigurable logic device (FPGA). The minimal number of selected transversals, which characterizes subsets of sequentially related places, is assigned to separate State Machine subnets. The computer based reasoning is searching a logic expression describing transversals in Gentzen sequent logic. The obtained decomposition (or cover) is used for state encoding of configurable array based embedded logic controllers, implemented as microsystems.
11
Redukcja binarnych tablic decyzyjnych z wykorzystaniem automatycznego wnioskowania
Adamski M., Tkacz J., Wrzesińska B.
Metody Informatyki Stosowanej
|
2010
|
nr 3 (24)
5-12
PL
W artykule przedstawiono sposób redukcji binarnych tablic decyzyjnych z wykorzystaniem systemu komputerowego dowodzenia twierdzeń w zdaniowym rachunku Gentzena [1, 4]. Binarna tablica decyzyjna przedstawia słabo określoną funkcję logiczną wielu zmiennych [6, 7]. Przykładową tablicę zaczerpnięto z książki [5], ze względu na zamieszczony w niej pełny i systematyczny opis wszystkich kroków minimalizacji funkcji i stopniowo uzyskiwanych rezultatów częściowych. Proponowany sposób minimalizacji symbolicznej postaci funkcji logicznej umożliwia w stosunkowo sprawny sposób otrzymywanie rezultatów dokładnych, wraz z formalnym dowodem ich gwarantowanej poprawności.
EN
The paper presents a new methodology for symbolic reduction of binary decision tables, currently intensively used for compact behavioral specifications of logic controllers. As an example the well known problem of simplification of a set of boolean relations with many variables and large sets of don’t care condition is chosen. They described also a special class of Boolean function called weakly specified or strongly unspecified. As a completely new, original solution, the formal automated reasoning based on Gentzen propositional calculus together with hypergraph theory are jointly used. The clique-transversal symbolic calculation is performed by means of effective reasoning in Gentzen calculus, giving the formal proof of all transformations.
12
Optymalizacja zapytan a kompresja danych w bazie DB2 9
Wegrzyn A., Tkacz J., Wojciechowski A.
Metody Informatyki Stosowanej
|
2010
|
nr 2 (23)
143-150
PL
Ważny nurt badań w zakresie baz danych koncentruje się wokół metod optymalizacji z jednej strony w celu zmniejszenia zajmowanej powierzchni dysków, a z drugiej w celu zwiększenia wydajności. Ma to szczególne znacznie przy coraz większych baza danych gdzie przetwarzane są miliony rekordów. W ramach tego nurtu firma IBM zaproponowała w najnowszej wersji serwera baz danych DB2 9.5 metodę kompresji danych opartą na kompresji wierszy, która oprócz znaczącego zmniejszenia przestrzeni dyskowej jednocześnie skraca czas dostępu do skompresowanych informacji. W przeprowadzonych pracach stwierdzono to oświadczalnie na różnych strukturach danych, a także stosując różne sposoby dostępu do nich.
EN
In the paper, query optimization problem in SQL language in IBM DB2 system is presented. DB2 database system in 9.5 version has possibility of data compression. Data compression is made by searching of recur data in records. For such recur data additional dictionary is prepare. Aim of research was testing of access by user to compress and non-compress data. For this problem special structure of data was prepared. In the paper result of testing compression and non-compression data is presented, too.
13
Content available remote Projektowanie sekwencyjnych układów cyfrowych z wykorzystaniem logiki sekwentów Gentzena
Tkacz J., Adamski M.
Przegląd Elektrotechniczny
|
2009
|
R. 85, nr 7
196-199
PL
Artykuł jest ilustracją możliwości zastosowania komputerowego wnioskowania symbolicznego w projektowaniu układów cyfrowych, a w tym do rozwiązywania skomplikowanych problemów logicznych. Wykorzystując przykład sieci działań zaczerpnięty z literatury, przedstawiono sposób uzyskiwania uproszczonego opisu bloku kombinacyjnego automatu cyfrowego na podstawie jego specyfikacji regułowej. Metoda polega na zastąpieniu sekwentami tablicy przejść-wyjść automatu i przeprowadzeniu syntezy logicznej metodą komputerowego wnioskowania.
EN
There is presented a new idea of an application of Gentzen logic symbolic reasoning for solving some combinational problems in the sequential circuit design. Behavioral description of combinatorial block of synchronous control unit is given as flowchart. The method is realized by a replacement of the transition table by the sequents, which describe relations between inputs and outputs of combinatorial block of sequential digital circuit in rule based format.
14
Wykorzystanie komputerowego wnioskowania w projektowaniu kombinacyjnych układów sterowania
Tkacz J., Adamski M.
Przegląd Telekomunikacyjny + Wiadomości Telekomunikacyjne
|
2008
|
R. 81, nr 6
728-730
PL
Przedstawiono możliwości zastosowania komputerowego wnioskowania symbolicznego Gentzena w projektowaniu układów cyfrowych oraz do rozwiązywania skomplikowanych problemów logicznych. Wykorzystując przykład sterownika zaczerpnięty z literatury, przedstawiono sposób uzyskiwania uproszczonego opisu układu kombinacyjnego, kilkukrotnie odwołujący się do systemu wnioskującego. Metoda polega na zastąpieniu silnie nieokreślonej klasycznej tablicy decyzyjnej sekwentami, które opisują relacje pomiędzy wejściami i wyjściami układu. W wyniku normalizacji tych sekwentów otrzymuje się zbiór reguł typu if-then, równoważny formie koniunkcyjnej lub dysjunkcyjnej funkcji boolowskich.
EN
The paper presents a new idea of an application of Gentzen logic symbolic reasoning for solving some combinational problems in the digital system design. Taking into account an example of industrial combinational logic controller, which could be alternatively described in classic way as an binary decision table, it is demonstrated how to apply a new efficient version of automated theorem prover in propositional sequent logic for a direct design from behavioural specification.
15
Content available Kolorowanie automatowe sieci Petriego metodą wnioskowania symbolicznego
Tkacz J.
Pomiary Automatyka Kontrola
|
2007
|
R. 53, nr 5
120-122
PL
W referacie przedstawiono sposób dekompozycji sieci Petriego za pomocą naturalnego wnioskowania Gentzena na podsieci typu automatowego. Normalizacja i minimalizacja zbioru reguł z zastosowaniem algorytmu wnioskującego może zostać wykorzystana w procesach wyznaczania podsieci automatowych reprezentujących zdekomponowane, niezależne fragmenty większego układu sterowania. Prezentowana metoda, w odróżnieniu od innych, znanych z literatury, nie wymaga pełnego przekształcenia równania charakterystycznego, reprezentującego listę sąsiedztwa w celu uzyskania pierwszego rozwiązania.
EN
The paper presents a concept and design methodology for decomposition of logic controllers' specification by means of using Gentzen symbolic reasoning. Specification of logic controller behaviour can be represented by Petri net, which can be decomposed into simplified subnets. These subnets directly represent smaller and independent parts of logic controller. The first result (Petri net State Machine-subnet), obtained from symbolic deduction, can be generated without complete analysis of characteristic logic expression, created from local state space description.
16
Wykrywanie zastojów w sterownikach logicznych metodą symbolicznego wnioskowania Gentzena
Tkacz J.
Pomiary Automatyka Kontrola
|
2006
|
R. 52, nr 6 bis
11-13
PL
W referacie przedstawiono koncepcję i sposób weryfikacji specyfikacji sterowników logicznych z wykorzystaniem wnioskowania Gentzena. Zastosowanie symbolicznej metody Gentzena w odróżnieniu od opisywanych w literaturze rozwiązań, pozwala na pominięcie szeregu kroków w procesie analizy symbolicznej sieci Petriego, opisującej funkcjonowanie sterownika, co prowadzi do pełnej automatyzacji procesu weryfikacji. Metoda dokładnie określa fragmenty specyfikacji, w których występują defekty (np. zastoje).
EN
The paper presents a concept and methodology for verification of logic control-lers specification by means of using Gentzen symbolic deduction. This method omits some steps of algorithm of Petri net symbolic analysis, where Petri net specifies behavior of logic controller. This concept makes possible to automate full process of verification and determines places, for which specification has errors (deadlocks).
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.