Wyniki wyszukiwania - Biblioteka Nauki

1

Extensions of Elementary Cause-Effect Structures

100%

Czaja L.

Fundamenta Informaticae

|

2021

|

tom Vol. 179, nr 2

93--111

EN

Cause-effect structures are objects of a formal system devised for modeling, testing and verifying properties of tasks, where parallel execution of actions is the most characteristic feature. This is an algebraic system called a quasi-semiring. In this paper elementary cause-effect structures, a system behaviourally equivalent to 1-safe Petri nets, are extended by the following features: weighted edges, multi-valued nodes having capacities (counterpart of place/transition Petri nets), inhibitors and a model of time. The extensions are accomplished by modifying the notion of state and semantics, but leaving unchanged structure of the quasi-semiring expressions.

2

A net presentation of Lithuanian sentences containing verbal forms with the grammatical suffix -dav-

80%

Roszko D. , Roszko R.

Cognitive Studies

|

2014

|

nr 14

173-182

EN

In the article the authors make an attempt to present the meaning of Lithuanian sentences containing verbal forms with the grammatical suffix -dav- (the so-called iterative past tense forms) by means of Petri nets. The authors gradually develop the net to such complexity that it makes it possible to avoid interpretative similarities to other Lithuanian verbal forms.

3

Target-oriented Petri Net Synthesis

80%

Best E. , Devillers R. , Erofeev E. , Wimmel H.

Fundamenta Informaticae

|

2020

|

tom Vol. 175, nr 1-4

97--122

EN

When a Petri net is synthesised from a labelled transition system, it is frequently desirable that certain additional constraints are fulfilled. For example, in circuit design, one is often interested in constructing safe Petri nets. Targeting such subclasses of Petri nets is not necessarily computationally more efficient than targeting the whole class. For example, targeting safe nets is known to be NP-complete while targeting the full class of place/transition nets is polynomial, in the size of the transition system. In this paper, several classes of Petri nets are examined, and their suitability for being targeted through efficient synthesis from labelled transition systems is studied and assessed. The focus is on choice-free Petri nets and some of their subclasses. It is described how they can be synthesised efficiently from persistent transition systems, summarising and streamlining in tutorial style some of the authors’ and their groups’ work over the past few years.

4

A Petri Net Interpretation of Open Reconfigurable Systems

80%

Peschanski F. , Klaudel H. , Devillers R.

Fundamenta Informaticae

|

2013

|

tom Vol. 122, nr 1-2

85--117

EN

We present a Petri net interpretation of the pi-graphs - a graphical variant of the picalculus where recursion and replication are replaced by iteration. The concise and syntax-driven translation can be used to reason in Petri net terms about open reconfigurable systems. We demonstrate that the pi-graphs and their translated high-level Petri nets agree at the semantic level. In consequence, existing results on pi-graphs naturally extend to the translated Petri nets, most notably a guarantee of finiteness by construction.

5

Full Axiomatisation of Timed Processes of Interval-Timed Petri Nets

80%

Pelz E.

Fundamenta Informaticae

|

2018

|

tom Vol. 157, nr 4

427--442

EN

In this paper we use partial order semantics to express the truly concurrent behaviour of Interval-Timed Petri nets (ITPNs) in their most general setting, i.e. with autoconcurrency and zero duration, as studied with its standard maximal step semantics in [1]. First we introduce the notion of timed processes for ITPNs inductively. Then we investigate if the equivalence of inductive and axiomatic process semantics - true for classical Petri nets - could hold for ITPNs too. We will see that the notions of independence and immediate firing obligation seem to be antagonistic ones, and that local axioms, adequate to define processes of classical Petri nets, are not sufficient to caracterize timed processes of ITPNs. We propose several original “global” axioms which reveal to be an effective solution. Thus we yield finally a full axiomatic definition of timed processes for ITPNs.

6

Integrating Petri Nets and Flux Balance Methods in Computational Biology Models : a Methodological and Computational Practice

80%

Pernice S. , Follia L. , Balbo G. , Milanesi L. , Sartini G. , Totis N. , Lió P. , Merelli I. , Cordero F. , Beccuti M.

Fundamenta Informaticae

|

2020

|

tom Vol. 171, nr 1-4

367--392

EN

Computational Biology is a fast-growing field that is enriched by different data-driven methodological approaches and by findings and applications in a broad range of biological areas. Fundamental to these approaches are the mathematical and computational models used to describe the different states at microscopic (for example a biochemical reaction), mesoscopic (the signalling effects at tissue level), and macroscopic levels (physiological and pathological effects) of biological processes. In this paper we address the problem of combining two powerful classes of methodologies: Flux Balance Analysis (FBA) methods which are now producing a revolution in biotechnology and medicine, and Petri Nets (PNs) which allow system generalisation and are central to various mathematical treatments, for example Ordinary Differential Equation (ODE) specification of the biosystem under study. While the former is limited to modelling metabolic networks, i.e. does not account for intermittent dynamical signalling events, the latter is hampered by the need for a large amount of metabolic data. A first result presented in this paper is the identification of three types of cross-talks between PNs and FBA methods and their dependencies on available data. We exemplify our insights with the analysis of a pancreatic cancer model. We discuss how our reasoning framework provides a biologically and mathematically grounded decision making setting for the integration of regulatory, signalling, and metabolic networks and greatly increases model interpretability and reusability. We discuss how the parameters of PN and FBA models can be tuned and combined together so to highlight the computational effort needed to perform this task. We conclude with speculations and suggestions on this new promising research direction.

7

Petri nets and power graphs - comparison of two concurrence-models

80%

Korczyński W.

Demonstratio Mathematica

|

1998

|

tom Vol. 31, nr 1

179-192

EN

In the paper some relation

8

Analysis of Parallel Discrete Systems: Persistent Sets vs. Concurrent Simulation

80%

Karatkevich A.

Przegląd Elektrotechniczny

|

2009

|

tom R. 85, nr 7

182-184

EN

Formal verification is one of the necessary steps of the process of digital system design. Full exploration of state space presents a complete picture of system behaviour, but it is not practically possible for the large systems because of the so-called state explosion problem. That is the reason, why algorithms of partial state space exploration are important in practice. In this paper two basic methods of such exploration are described and compared: persistent set approach and concurrent simulation approach.

PL

Niezbędnym elementem procesu projektowania systemów cyfrowych jest formalna weryfikacja projektów. Ale pełna eksploracja przestrzeni stanów, dająca pełny obraz zachowania systemu, nie jest możliwa dla dużych współbieżnych systemów z powodu problemu eksplozji stanów. Dlatego ważne są algorytmy częściowej eksploracji przestrzeni stanów. Tematem artykułu jest opis i porównanie dwóch podstawowych metod takiej eksploracji: podejścia zbiorów uporczywych i współbieżnej symulacji.

9

Graficzne środowisko do modelowania i symulacji rozmytej sieci Petriego

80%

Dec G.

Pomiary Automatyka Kontrola

|

2006

|

tom R. 52, nr 7 bis

37--39

PL

Artykuł przedstawia środowisko graficzne służące do modelowania i symulacji rozmytej sieci Petriego (FPN) [6]. Metody syntezy logicznej tej sieci [2, 6] wymagają znajomości języków opisu sprzętu i nie kładą nacisku na weryfikację projektu za pomocą FPN. W celu usunięcia tych niedogodności opracowano graficzny edytor, który pozwala na projektowanie i symulację na poziomie FPN. Edytor, bazujący na oprogramowaniu Petri Net Kernel [7], cechuje niezależność od systemu operacyjnego, obsługa różnych typów sieci Petriego, format danych oparty na XML, możliwość symulacji FPN. Pokazano przykład zastosowania opracowanego środowiska w procesie projektowania cyfrowego układu sterowania.

EN

The paper presents a graphics environment for modelling and simulation of a fuzzy Petri net (FPN) [6]. Logic synthesis methods developed for the FPN [2, 6] require knowledge of hardware description languages and do not lay stress on the project verification by the FPN. In order to remove these inconveniences, a graphics editor was developed, which allows to design and simulate the system on the FPN level. The editor, which is based on the software tool Petri Net Kernel [7], is operating system independent, handles different kinds of Petri nets, uses XML as a data format, can simulate the FPN. The article shows an example of the use of the software environment for the design of a digital control system.

10

Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction

80%

Cassez F. , Jensen P. G. , Guldstrand Larsen K.

Fundamenta Informaticae

|

2021

|

tom Vol. 178, nr 1/2

31--57

EN

We address the safety verification and synthesis problems for real-time systems. We introduce real-time programs that are made of instructions that can perform assignments to discrete and real-valued variables. They are general enough to capture interesting classes of timed systems such as timed automata, stopwatch automata, time(d) Petri nets and hybrid automata. We propose a semi-algorithm using refinement of trace abstractions to solve both the reachability verification problem and the parameter synthesis problem for real-time programs. All of the algorithms proposed have been implemented and we have conducted a series of experiments, comparing the performance of our new approach to state-of-the-art tools in classical reachability, robustness analysis and parameter synthesis for timed systems. We show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools.

11

Semi-quantitative Modelling of Gene Regulatory Processes with Unknown Parameter Values Using Fuzzy Logic and Petri Nets

80%

Bordon J. , Moškon M. , Zimic N. , Mraz M.

Fundamenta Informaticae

|

2018

|

tom Vol. 160, nr 1/2

81--100

EN

Petri nets are a well-established modelling framework in life sciences and have been widely applied to systems and synthetic biology in recent years. With the various extensions they serve as graphical and simulation interface for both qualitative and quantitative modelling approaches. In terms of quantitative approaches, Stochastic and Continuous Petri nets are extensively used for modelling biological system’s dynamics if underlying kinetic data are known. However, these are often only vaguely defined or even missing. In this paper we present a fuzzy approach, which can be used to model biological processes with unknown kinetic data in order to still obtain quantitatively relevant simulation results. We define fuzzy firing rate functions, which can be used in Continuous Petri nets and are able to describe different processes that govern the dynamics of gene expression networks. They can be used in combination with the conventional firing rate functions and applied only in the parts of the system for which the kinetic data are missing. The case study of the proposed approach is performed on models of a hypothetical repressilator and Neurospora circadian rhythm.

12

Transformacja diagramów aktywności UML 2.0 do sieci Petriego w systemach sterowania binarnego

80%

Grobelny M.

Pomiary Automatyka Kontrola

|

2009

|

tom R. 55, nr 7

498-500

PL

Artykuł zawiera omówienie oraz porównanie dwóch formalnych metod specyfikacji behawioralnej systemów osadzonych - diagramów aktywności języka UML 2.0 oraz sieci Petriego. Przedstawione są podobieństwa oraz różnice pomiędzy nimi. Poruszone jest zagadnienie transformacji pomiędzy dwoma wymienionymi technikami specyfikacji wraz z obrazującym ten proces przykładem. Uwzględniono także problem nadmiarowości sieci Petriego po bezpośredniej transformacji i wynikającą z tego konieczność redukcji miejsc i tranzycji przy zachowaniu jednoznaczności obu diagramów. Artykuł podzielony jest następująco. Rozdział 2 zawiera wprowa-dzenie do diagramów aktywności w UML 2.0. Rozdział 3 przedstawia sieci Petriego. Rozdział 4 porównuje obie metody specyfikacji - diagramy aktywności oraz sieci Petriego. Rozdział 5 porusza zagadnienie transformacji pomiędzy dwoma omawianymi technikami. Rozdział 6 zawiera podsumowanie wcześniejszych rozdziałów oraz wnioski.

EN

The paper presents and compares two formal behavioural specification methods of embedded systems [1] - activity diagrams of UML specification language [2, 3, 4, 13, 14] and Petri nets [9, 15]. Similarities and differences as well as the aspect of transformation between both specification techniques are concerned. The transformation is explained on the example of a sample control process shown in Fig. 1. Fig. 2 presents the specification using UML activity diagram. The problem of redundant places and transitions after direct transformation from the activity diagram into the Petri net is dealt with. The Petri net after transformation is shown in Fig. 3 (a), while the reduced diagram - in Fig. 3 (b). The paper is divided into sections. Section 1 contains introduction to the topic of embedded system specification techniques. Section 2 presents UML 2.0 activity diagrams with their basic elements. Petri nets and their syntactic are described in Section 3. Section 4 focuses on comparison of both techniques by means of embedded control systems (see [12] for more details). The transformation problem is considered in Section 5. Section 6 summarises and concludes the paper.

13

Petri Nets for Modelling and Analysing Trophic Networks

80%

Baldan P. , Bocci M. , Brigolin D. , Cocco N. , Heiner M. , Simeoni M.

Fundamenta Informaticae

|

2018

|

tom Vol. 160, nr 1/2

27--52

EN

We consider trophic networks, a kind of networks used in ecology to represent feeding interactions (what-eats-what) in an ecosystem. Starting from the observation that trophic networks can be naturally modelled as Petri nets, we explore the possibility of using Petri nets for the analysis and simulation of trophic networks. We define and discuss different continuous Petri net models, whose level of accuracy depends on the information available for the modelled trophic network. The simplest Petri net model we construct just relies on the topology of the network. We also propose a technique for deriving a more refined model that embeds into the Petri net the known constraints on the transition rates that represent the knowledge on metabolism and diet of the species in the network. Finally, if the information of the biomass amounts for each species at steady state is available, we discuss a way of further refining the Petri net model in order to represent dynamic behaviour. We apply our Petri net technology to a case study of the Venice lagoon and analyse the results.

14

Image generation by Petri nets

80%

Lumini A. , Maio D.

Machine Graphics and Vision

|

1998

|

tom Vol. 7, No. 1/2

221-232

EN

This paper presents a new approach to computer image generation. The basic idea is to translate the evolution of a Petri net into a graphic output. In particular, we focus on three methods for image generation which exhibit a certain analogy whit fractals. Some experimental results are reported together whit a brief investigation on the relationships between generated images and thier corresponding Petri nets.

15

Coupling iterate function systems and petri nets for image representation and generation

80%

Lumini A.

Machine Graphics and Vision

|

2000

|

tom Vol. 9, No. 1/2

139-147

EN

Image generation has been proposed for many different tasks in the literature, from physics events visualization to the purpose of "art for art's sake". In this paper a new approach to computer image generation is presented: the method creates new images by randomizing the decompression process, starting from a compressed representation of an image by Iterate Function Systems. Petri Nets are employed both for modeling the decompression process and for inserting a randomization component in it. A second method proposed in this work directly translates the evolution of a Petri Net into a graphic output. Experimental results are given, showing different class of images generated by the two methods.

16

Activity Networks with Delays an Application to Toxicity Analysis

80%

Delaplace F. , Di Giusto C. , Giavitto J. L. , Klaudel H. , Spicher A.

Fundamenta Informaticae

|

2018

|

tom Vol. 160, nr 1/2

119--142

EN

ANDy, Activity Networks with Delays, is a discrete framework aiming at the qualitative modeling of time-dependent activities. The modular and expressive syntax makes ANDy suitable for a concise and natural modeling of time-dependent biological systems (i.e., regulatory pathways). Activities involve entities playing the role of activators, inhibitors or products of biochemical network operation. Activities may have a given duration, i.e., the time required to obtain results. An entity may represent an object (e.g., an agent, a biochemical species or a family of thereof) with a local attribute, a state denoting its level (e.g., concentration, strength). Entity levels may change as a result of an activity or may decay gradually as time passes by. The semantics of ANDy is formally given via high-level Petri nets ensuring this way some modularity. As main results we show that ANDy systems have finite state representations even for potentially infinite processes and it well adapts to the modeling of toxic behaviors. As an illustration, we present a classification of toxicity properties and give some hints on how they can be verified on ANDy systems with existing tools. A case study on blood glucose regulation is provided to exemplify the ANDy framework and the toxicity properties.

17

Free-choice Nets with Home Clusters are Lucent

80%

van der Aalst W. M. P.

Fundamenta Informaticae

|

2021

|

tom Vol. 181, nr 4

273--302

EN

A marked Petri net is lucent if there are no two different reachable markings enabling the same set of transitions, i.e., states are fully characterized by the transitions they enable. Characterizing the class of systems that are lucent is a foundational and also challenging question. However, little research has been done on the topic. In this paper, it is shown that all free-choice nets having a home cluster are lucent. These nets have a so-called home marking such that it is always possible to reach this marking again. Such a home marking can serve as a regeneration point or as an end-point. The result is highly relevant because in many applications, we want the system to be lucent and many “well-behaved” process models fall into the class identified in this paper. Unlike previous work, we do not require the marked Petri net to be live and strongly-connected. Most of the analysis techniques for free-choice nets are tailored towards well-formed nets. The approach presented in this paper provides a novel perspective enabling new analysis techniques for free-choice nets that do not need to be well-formed. Therefore, we can also model systems and processes that are terminating and/or have an initialization phase.

18

Discovering Object-centric Petri Nets

80%

van der Aalst W. M. P. , Berti A.

Fundamenta Informaticae

|

2020

|

tom Vol. 175, nr 1-4

1--40

EN

Techniques to discover Petri nets from event data assume precisely one case identifier per event. These case identifiers are used to correlate events, and the resulting discovered Petri net aims to describe the life-cycle of individual cases. In reality, there is not one possible case notion, but multiple intertwined case notions. For example, events may refer to mixtures of orders, items, packages, customers, and products. A package may refer to multiple items, multiple products, one order, and one customer. Therefore, we need to assume that each event refers to a collection of objects, each having a type (instead of a single case identifier). Such object-centric event logs are closer to data in real-life information systems. From an object-centric event log, we want to discover an object-centric Petri net with places that correspond to object types and transitions that may consume and produce collections of objects of different types. Object-centric Petri nets visualize the complex relationships among objects from different types. This paper discusses a novel process discovery approach implemented in PM4Py. As will be demonstrated, it is indeed feasible to discover holistic process models that can be used to drill-down into specific viewpoints if needed.

19

Decentralized structural control approach for Petri nets

80%

Aybar A.

Control and Cybernetics

|

2007

|

tom Vol. 36, no 1

143-159

EN

The structural controller, described by adding the control places to the Petri nets, is introduced in this work to lead the Petri net to the desired marking vectors. An algorithm (Algorithm I) is developed to determine the control places for the given Petri net. The connections and the initial marking of each control place are determined in this algorithm. Moreover, a decentralized structural control approach, based on overlapping decompositions, is introduced in this work. In this decentralized approach, all disjoint Petri subnets, which are obtained by using overlapping decompositions, are determined. The control places for each Petri subnet are determined by using the given algorithm. Then, the control places for the orginal Petri net are obtained by the control places of each PSN by another algorithm (Algorithm II) and these places are added to the orginal Petri net. Therefore, a decentralized structural controller which guarantees to lead the Petri net to the desired marking vectors is obtained.

20

ROSECON: a Computer Tool for Synthesis and Verification of Concurrent Systems Specified by Information Systems

80%

Suraj Z. , Pancerz K.

Fundamenta Informaticae

|

2013

|

tom Vol. 126, nr 4

335--351

EN

In the paper, a computer tool called ROSECON, used for modeling and analyzing systems of concurrent processes, is described. A special attention is focused on synthesis and verification of concurrent systems specified by information systems. Two kinds of models, synchronous and asynchronous, are considered. In the first approach, all processes included in the modeled system are synchronized globally whereas in the second one, each process is synchronized individually. The presented tool allows generating automatically an appropriate model of a system of concurrent processes, in the form of colored Petri nets, from the specification given by an information system. Analysis of the model behaviors enables users to verify the correctness and/or optimality of the obtained models and to provide some modification procedures to get correct and/or more optimal solutions. Examples of selected well known problems in concurrency, in the paper, emphasize usefulness of the tool in the designing systems of concurrent processes.