Wyznaczanie SM - pokrycia bezpiecznej sieci Petriego metodą komputerowego wnioskowania

• Autorzy: Tkacz J. , Adamski M.

Warianty tytułu

EN

Calculation of State Machine cover of safe Petri net by means of computer based reasoning

• Języki publikacji: PL

Abstrakty

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.

Słowa kluczowe

PL

przestrzeń stanów lokalnych i globalnych sieci Petriego; transwersale; podsieci automatowe SM; logika sekwentów Gentzena

EN

Petri net state space; transversal; formal reasoning; State Machine subnets; configurable logic controllers

• Wydawca: Wydawnictwo PAK
• Czasopismo: Pomiary Automatyka Kontrola
• Rocznik: 2011
• Tom: R. 57, nr 11
• Strony: 1397--1400
• Opis fizyczny: Bibliogr. 17 poz., rys., wzory

Twórcy

autor

Tkacz J.

autor

Adamski M.

• Uniwersytet Zielonogórski, Wydział Elektrotechniki, Informatyki i Telekomunikacji, Instytut informatyki i Elektroniki, ul. Podgórna 50, 65-246 Zielona Góra,

Bibliografia

• [1] Adamski M., Chodań M.: Modelowanie układów sterowania dyskretnego z wykorzystaniem sieci SFC, Wydawnictwo PZ, Zielona Góra, 2000.
• [2] Adamski M., Tkacz J., Wrzesińska B.: Redukcja binarnych tablic decyzyjnych z wykorzystaniem automatycznego wnioskowania, Metody Informatyki Stosowanej. - 2010, nr 3, s. 5-12.
• [3] Adamski M.: Projektowanie układów cyfrowych systematyczną metodą strukturalną. Monografie Nr 49. Wydawnictwo Wyższej Szkoły Inżynierskiej w Zielonej Górze, 1990, ISSN 0239-7390.
• [4] Adamski M., Węgrzyn M.: Petri nets mapping into reconfigurable logic controllers. Electronics and Telecommunications Quarterly, 2009, Vol. 55, no. 2, s. 157-182.
• [5] David R., Alla H. D. R.: Petri Nets and Grafcet. Tools for modeling discrete event system. London: Prentice Hall, 1992.
• [6] Atserias, A., Galesi, N., and Pudlák, P.: Monotone simulations of non-monotone proofs. J. Comput. Syst. Sci. 65, 4 (Dec. 2002), 626-638.
• [7] Adamski M., Karatkevich A., Węgrzyn M.: Design of embedded control systems, New York : Springer, 2005, 267 s.
• [8] Eiter T., Gottlob G. and Makino K.: New results on monotone dualization and generating hypergraph transversals. Proc. of the 32th ACM Symp. STOC’02, 14-22, 2002.
• [9] Gallier J. H.: Logic for computer science, Foundations of Automatic Theorem Proving. Harper & Row, (1986).
• [10] Murata T.: Petri Nets: Properties, Analysis and Applications, Proceedings of the IEEE, Vol. 77, No. 4, 1989.
• [11] Tkacz J.: Projektowanie układów sterowania binarnego wspomagane automatycznym wnioskowaniem Gentzena, Rozprawa doktorska. Uniwersytet Zielonogórski, Wydział Elektrotechniki, Informatyki i Telekomunikacji, Zielona Góra, 2008.
• [12] Tkacz J., Adamski M.: Projektowanie sekwencyjnych układów cyfrowych z wykorzystaniem logiki sekwentów Gentzena, Przegląd Elektrotechnicz. 2009, R. 85, nr 7, s. 196-199.
• [13] Valette R.: Etude comparative de deux outils de representation: Grafcet et reseau de Petri, Le Nouvel Automatisme, Decembre 1978, str. 337-382.
• [14] Węgrzyn M., Adamski M.: Wykorzystanie standardowych kompilatorów FPLD do syntezy sterowników logicznych, Kwartalnik Elektroniki i Telekomunikacji - 1997, T. 43, z. 3, s. 353-372.
• [15] Wilson R. J.: Wprowadzenie do teorii grafów. Wydawnictwo PWN, Warszawa 1998.
• [16] Wiśniewska M., Adamski M.: Zastosowanie dualizmu hipergrafów w dekompozycji równoległej automatów współbieżnych, Przegląd Telekomunikacyjny 6/2008.
• [17] Karatkevich A.: Dynamic Analysis of Petri Net Based Discrete Systems. LNCiS, vol. 356, Springer-vErlag, Berlin 2007.