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

Znaleziono wyników: 13

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 Controlling Petri Net Behavior using Priorities for Transitions
Lomazova I. A., Popova-Zeugmann L.
Fundamenta Informaticae
|
2016
|
Vol. 143, nr 1/2
101--112
EN
In this paper we examine how it is possible to control Petri net behavior with the help of transition priorities. Controlling here means forcing a process to behave in a stable way by ascribing priorities to transitions and hence transforming a classic Petri net into a Priority Petri net. For Petri net models stability is often ensured by liveness and boundedness. These properties are crucial in many application areas, e.g. workflow modeling, embedded systems design, and bioinformatics. In this paper we study the problem of transforming a given live, but unbounded Petri net into a live and bounded one by adding priority constraints. We specify necessary conditions for the solvability of this problem and present an algorithm for ascribing priorities to net transitions in such a way that the resulting net becomes bounded while staying live.
2
Content available remote Discovery of Cancellation Regions within Process Mining Techniques
Kalenkova A. A., Lomazova I. A.
Fundamenta Informaticae
|
2014
|
Vol. 133, nr 2/3
197--209
EN
Process mining is a relatively new field of computer science which deals with process discovery and analysis based on event logs. In this work we consider the problem of discovering workflow nets with cancellation regions from event logs. Cancellations occur in the majority of real-life event logs. In spite of huge amount of process mining techniques little has been done on cancellation regions discovery. We show that the state-based region algorithm gives labeled Petri nets with overcomplicated control flow structure for logs with cancellations. We propose a novel method to discover cancellation regions from the transition systems built on event logs and show the way to construct equivalent workflow net with reset arcs to simplify the control flow structure.
3
Content available remote Analyzing Compatibility of Services via Resource Conformance
Lomazova I.A., Romanov I. V.
Fundamenta Informaticae
|
2013
|
Vol. 128, nr 1-2
129--141
EN
In this work we consider modeling of services with workflow modules, which form a Petri net subclass. The service compatibility problem is to answer the question, whether two services fit together, i.e. whether the composed system is correct. We study complementarity of resources, produced/consumed by two services-a necessary condition for the service compatibility. Resources, which are produced/consumed by a service, are represented as a multiset language. We define an algebra of multiset languages and present algorithms for checking conformance of resources for two given well-structured workflow modules.
4
Content available remote On Compositionality of Boundedness and Liveness for Nested Petri Nets
Dworzański L. W., Lomazova I.A.
Fundamenta Informaticae
|
2012
|
Vol. 120, nr 3/4
275-293
EN
Nested Petri nets (NP-nets) are Petri nets with net tokens. The liveness and boundedness problems are undecidable for two-level NP-nets [14]. Boundedness is in EXPSPACE and liveness is in EXPSPACE or worse for plain Petri nets [6]. However, for some restricted classes, e.g. for plain free-choice Petri nets, problems become more amenable to analysis. There is a polynomial time algorithm to check if a free-choice Petri net is live and bounded [4]. In this paper we prove, that for NP-nets boundedness can be checked in a compositional way, and define restrictions, under which liveness is also compositional. These results give a base to establish boundedness and liveness for NP-nets by checking these properties for separate plain components, which can belong to tractable Petri net subclasses, or be small enough for model checking.
5
Content available remote Cellular Resource-Driven Automata
Bashkin V.A., Lomazova I.A.
Fundamenta Informaticae
|
2012
|
Vol. 120, nr 3/4
243-257
EN
Resource-driven automata (RDA) are finite automata, sitting in the nodes of a finite system net and asynchronously consuming/producing shared resources through input/output system ports (arcs of the system net). RDAs themselves may be resources for each other, thus allowing the highly flexible structure of the model. It was proved earlier, that RDA-nets are expressively equivalent to Petri nets [2]. In this paper the new formalism of cellular RDAs is introduced. Cellular RDAs are RDA-nets with an infinite regularly structured system net. We build a hierarchy of cellular RDA classes on the basis of restrictions on the underlying grid. The expressive power of several major classes of 1-dimensional grids is studied.
6
Content available remote Resource Driven Automata Nets
Bashkin V.A., Lomazova I.A.
Fundamenta Informaticae
|
2011
|
Vol. 109, nr 3
223-236
EN
A new formalism of Resource Driven Automata Nets (RDA-nets) is presented. A RDAnet has two levels: a system level is represented by a net of active resources, describing distribution of agents/resources and their interactions; agents in an object level are finite automata, communicating via ports and shared resources of a system level. RDA-nets are assigned for modeling mobility in multi-agent systems from the resource dependence perspective. We prove that RDA-nets have the same expressive power as Petri nets and give examples of modeling agent communications, dynamics and mobility.
7
Content available remote Interacting Workflow Nets for Workflow Process Re-Engineering
Lomazova I.A.
Fundamenta Informaticae
|
2010
|
Vol. 101, nr 1/2
59-70
EN
In this work we consider modeling of workflow systems with Petri nets. To increase flexibility and give tools for workflow models re-engineering we extend the formalism of workflow nets by considering systems of interacting nets. Then we study soundness – the main correctness property of workflow processes – and show, that for a special class of structured workflow system soundness can be proved in compositional way.
8
Content available remote Checking Properties of Adaptive Workflow Nets
van Hee K., Oanea O., Serebrenik A., Sidorova N., Voorhoeve M., Lomazova I.A.
Fundamenta Informaticae
|
2007
|
Vol. 79, nr 3-4
347-362
EN
In this paper we consider adaptive workflow nets, a class of nested nets that allows more comfort and expressive power for modeling adaptability and exception handling in workflow nets. We define two important behavioural properties of adaptive workflow nets: soundness and circumspectness. Soundness means that a proper final marking (state) can be reached from any marking which is reachable from the initial marking, and no garbage will be left. Circumspectness means that the upper layer is always ready to handle any exception that can happen in a lower layer. We define a finite state abstraction for adaptive workflow nets and show that soundness and circumspectness can be verified on this abstraction.
9
Content available remote Communities of Interacting Automata for Modelling Distributed Systems with Dynamic Structure
Lomazova I.A.
Fundamenta Informaticae
|
2004
|
Vol. 60, nr 1-4
225--235
EN
A community of interacting automata is a set of nondeterministic finite automata which can execute actions autonomously, synchronize with each other, or generate new members of the community. Thus interacting automata allow to model distributed systems with nonlimited number of distributed agents. We show that the formalism of interacting automata has a clear semantics and nice semantic properties.
10
Content available remote Petri nets and resource bisimulation
Bashkin V.A., Lomazova I.A.
Fundamenta Informaticae
|
2003
|
Vol. 55, nr 2
101-114
EN
Resources are defined as submultisets of Petri net markings. Two resources are called similar if replacing one of them by another in any marking doesn't change the Petri net's behavior. We define the relations of resource similarity and resource bisimulation and show that they are finitely based. In this paper the resource bisimulation is studied for different classes of Petri nets: ordinary Petri nets, high-level Petri nets and nested Petri nets - Petri nets with Petri nets as tokens.
11
Content available remote Modeling Dynamic Objects in Distributed Systems with Nested Petri Nets
Lomazova I.A.
Fundamenta Informaticae
|
2002
|
Vol. 51, nr 1,2
121-133
EN
Nested Petri nets (NP-nets) is a Petri net extension, allowing tokens in a net marking to be represented by marked nets themselves. The paper discusses applicability of NP-nets for modeling task planning systems, multi-agent systems and recursive-parallel systems. A comparison of NP-nets with some other formalisms, such as OPNs of R. Valk, recursive parallel programs of O. Kushnarenko and Ph. Schnoebelen and process algebras is given. Some aspects of decidability for object-oriented Petri net extensions are also discussed.
12
Content available remote Nested Petri Nets: Multi-level and Recursive Systems
Lomazova I.A.
Fundamenta Informaticae
|
2001
|
Vol. 47, nr 3,4
283-293
EN
Nested Petri nets (NP-nets) is a formalism for modeling hierarchical multi-agent systems. Tokens in nested Petri nets are elements represented by nets themselves. The paper continues investigating semantic properties of NP-nets, started in [10], where two-level NP-nets were studied. Here we consider multi-level and recursive NP-nets, for which decidability of termination and some other properties are proved. A comparison of NP-nets with other Petri net models is given.
13
Content available remote Nested Petri nets - a formalism for specification and verification of multi-agent distributed systems
Lomazova I.A.
Fundamenta Informaticae
|
2000
|
Vol. 43, Nr 1-4
195-214
EN
Nested Petri nets is a formalism for modeling hierarchical multi-agent systems. Tokens in nested Petri nets are elements represented by nets themselves. Decidability of some crucial for verification problems shows that, in spite of their "unflat" structure, nested Petri nets maintain significant properties of ordinary Petri nets. A comparison with some other Petri net models is given. The formalism allows generalization to a recursive case, when a nested Petri net may generate its own copy as its element. Two simple examples illustrate the approach.
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ć.