Wyniki wyszukiwania - Biblioteka Nauki

1

Collaborative processing of XML documents in Internet

100%

Sikorski A.

Theoretical and Applied Informatics

|

2008

|

tom Vol. 20, No. 4

229-244

EN

In order to enable eective collaboration on XML documents published in Internet, we propose an indexing technique making use of nodes labeling. In particular we consider two types of locks, acquired by multiple user transactions on segments of a document. These segments correspond to paths and ranges – defined by labels, with the document subtree being a special case of a range. We put forward algorithms for consolidation of shared locks that define a continuous covering, a way of initial processing simplifying and accelerating the lock manager. Two algorithms for the lock manager are framed with the use of XML labels for both the 2PL protocol and the cooperative one. We also point to some interesting ties between the lock management and the shortest path problem. Our motivation is given in the context of the SEDNA native XML DB isolation rules, however, our technique is useful for most of the fine-granular lock protocols.

PL

Ze względu na swa elastyczność oraz poparcie formatu przez znaczące gremia standaryzacyjne XML stał się powszechnie stosowanym sposobem udostępniania i wymiany danych, popularnym zwłaszcza w Internecie. Dokument XML można postrzegać również jako instancję, co prawda dość ograniczoną funkcjonalnie, obiektowej bazy danych, na której możliwe jest współbieżnie wykonywanie operacji aktualizujących. Jeżeli aktualizacje zasobu danych mają się odbywać współbieżnie, to konieczne jest ich synchronizowanie za pomocą odpowiedniego menedżera, zarządzającego blokowaniem węzłów XML i udostępnianiem odpowiednich danych. Zaproponowane w pracy rozwiązanie oparte jest na wykorzystaniu tzw. etykiet węzłów dokumentu XML [5],[6], do celów identyfikacji blokowanych obiektów i obsługi stanu menedżera blokad. Pojawienie się etykiet związane jest z pracami [7],[8] nad efektywnym wykonywaniem zapytań XPath, mającymi na celu optymalizację algorytmu wyznaczania tzw. złączenia strukturalnego (odpowiednik złączenia relacyjnego znanego z SQL). Okazuje się, że wartości etykiety mogą w wydajny sposób definiować pewne podzbiory węzłów dokumentu XML, podlegające blokowaniu przez menedżera współbieżności, umożliwiając tym samym implementację złożonych reguł współbieżności. Kluczowe dla wydajnego zarządzania współbieżnością jest operowanie takimi podzbiorami węzłów jak: ścieżka, poddrzewo czy zakres wierzchołków (wierzchołki o etykietach mających wartości z określonego przedziału). Chociaż rozwiązanie jest prezentowane w kontekście dokumentów XML i reguł współbieżnego przetwarzania bazy XML Sedna [2], to możliwe jest jego stosowanie do celów synchronizacji współbieżnego przetwarzania hierarchicznych (drzewiastych) struktur danych (Fig.4.). Blokady zakładane na zbiorach sa są przykładami szczególnych blokad predykatowych (intensjonalnych), których obsługa jest możliwa w czasie log(n), względem liczby założonych blokad. Predykaty te są formułami o postaciach zależnych jedynie od typu zbioru (tj. drzewo, ścieżka , zakres), zawierającymi wartości etykiet. Należy też zwrócić uwagę, że liczba n od której zależy złożoność obsługi blokady, jest na ogół dużo mniejsza od liczby zablokowanych węzłów dokumentów, ponieważ blokady zakładane mogą być na całych zbiorach.

2

A Linear Logic view of object Petri Nets

100%

Farwer B.

|

1999

|

tom Vol. 37, Nr 3

225-246

EN

Linear Logic has been shown to incorporate a fragment suitable for representing P/T-nets and giving a semantics to the computations of such nets. This result is generalized to coloured nets. Furthermore a new kind of high-level nets is defined: Linear Logic Petri Nets (LLPN). These nets are used as an intuitive semantics to well-known and new high-level net concepts like object systems and agent orientation.

3

Applying techniques of asynchronous concurrency to synchronous languages

100%

Maggiolo-Schettini A. , Tini S.

|

1999

|

tom Vol. 40, Nr 2,3

221-250

EN

In synchronous programming, programs can be perceived as purely sequential, and parallelism is only a logical concept useful to develop programs in a modular way. Classical semantics for synchronous languages interpret programs as sequential input/output finite state machines (i/o FSMs) where concurrency disappears. We argue that semantics where concurrency is reflected can be useful at least for improving hardware implementation, verification, and design of model-based schedulers. So, these semantics should not ``compete'' with the classical ones but should offer different, although consistent, views of programs, each supporting a particular task in their development. In order to define semantics reflecting concurrency, well established techniques adopted to define ``truly concurrent'' semantics for asynchronous languages could be applied. In this paper, we consider as a prototype of the class of synchronous languages the language Esterel, which is gaining use in a wide variety of applications. Then, following a method proposed by Degano and Priami to give semantics for asynchronous process algebras, we develop a semantic framework in which one can define different, although consistent, semantics of Esterel programs. The idea is to define a very concrete model of the language from which more abstract models can be recovered by means of suitable abstraction functions. We define a proved transition system (PTS) as the most concrete model of Esterel. We show that the classical interpretation in FSMs can be recovered from the PTS by a suitable abstraction function, namely we show that our most concrete semantics is consistent with the classical one. Then, from proved trees obtained by unfolding parts of the PTS, we abstract locality trees and enabling trees. We show how locality trees can be used to improve the hardware implementation of the language, namely to remove redundant latches generated by the compiler. Finally, we show how enabling trees can be used to improve the verification phase, namely to isolate program parts which actually cause the violation of a certain property.

4

The synthesis problem for Elementary Net Systems with Inhibitor Arcs

100%

Pietkiewicz-Koutny M.

|

1999

|

tom Vol. 40, Nr 2,3

251-283

EN

We investigate the synthesis problem for the Elementary Net Systems with Inhibitor Arcs (ENI-systems) executed according to the a-priori semantics. We characterise transition systems generated by ENI-systems, called TSENI transition systems, by adapting the notion of a step transition system whose arcs are labelled by sets of concurrently executed events. The relationship between the ENI-systems and TSENI transition systems is established via the notion of a region. We define, and show consistency of, two behaviour preserving translations between nets and transition systems. We also discuss how to optimise the synthesis procedure by using only minimal regions and selected inhibitor arcs.

5

Occurrence net logics

100%

Haar S.

|

2000

|

tom Vol. 43, Nr 1-4

105-127

EN

This paper investigates Occurrence (Petri) Nets on two levels: their structural theory and their interpretation in branching unfolding semantics of Petri Net systems. The key issue is the decomposition of occurrence nets into substructures given by the node relations associated with causal ordering, concurrency, and conflict. In addition to lines and cuts, which have long been studied in the context of causal nets, we introduce and study branches, trails, choices, and alternatives. All finite systems will be shown to satisfy certain density properties, i.e. non-empty intersections of substructures as above. On the semantic level, we introduce partial order logics to be interpreted on two different kind of frames, given by substructures of occurrence nets: on the frame of cuts, the CTL* type logics BFC and BLC, and the ``non-branching'' logic LLC, taylored to the frame given by the lattice of choices.

6

Factored Cost-Optimal Planning Using Message Passing Algorithms

100%

Jezequel L. , Fabre E.

Fundamenta Informaticae

|

2015

|

tom Vol. 139, nr 4

369--401

EN

This paper proposes an approach to solve cost-optimal factored planning problems. Planning consists in organizing actions in order to reach some predefined goal. In factored planning one considers several interacting planning problems and has to design an action plan for each of them. But one must also guarantee that all these local plans are compatible: actions shared among several problems must be jointly performed or jointly rejected. We enrich the problem with the extra requirement that the global plan computed in this modular manner must also minimize the sum of all action costs. A solution is provided to this problem, based on classical message passing algorithms, known as belief propagation in the setting of Bayesian networks. Here, messages carry complex information under the form of weighted (or (min; +)) automata, and all computations are performed with these objects. At the time our first paper on this topic was published, this method was the only one to solve cost-optimal factored planning problems in a modular way. Since then, new approaches were proposed. Experiments on classical benchmarks show that it is a valuable alternative to existing methods.

7

Interpreted Nets

100%

Czaja L.

|

2007

|

tom Vol. 79, nr 3-4

283-293

EN

The nets considered here are an extension of Petri nets in two aspects. In the semantic aspect, there is no one firing rule common to all transitions, but every transition is treated as an operator on data stored in its entry places and return results in its exit places. A state (marking) is a mapping of places (variables) into a given data structure, while interpretation is a mapping of transitions into a set of state transformers. Locality of transition's activity is like in Petri nets. In the structural aspect, entry and exit places to a transition are ordered. A concatenation of such nets is defined, hence their calculus (a monoid). This allows for combining small nets into large ones, in particular designing a computation and control parts separately, then putting them together into one. Such extended nets may produce, in particular, other nets. A number of properties of the operation on nets and their decomposition are demonstrated.

8

Process algebras for network communication

100%

Gruska D. P. , Maggiolo-Schettini A.

|

2001

|

tom Vol. 45, nr 4

359-378

EN

Critical issues that arise when process algebras are used for protocol specifications are discussed. To overcome some of these problems, a process algebra for protocol specifications is presented. It is based on Milner's Calculus of Communicating Systems, which is enriched by time and network reasoning. Several bisimulation based semantics for the calculus are defined and their properties are discussed.

9

Type-driven development of concurrent communicating systems

100%

Brady E.

|

tom Vol. 18 (3)

219--240

EN

Modern software systems rely on communication, for example mobile applcations communicating with a central server, distributed systems coordinaing a telecommunications network, or concurrent systems handling events and processes in a desktop application. However, reasoning about concurrent prgrams is hard, since we must reason about each process and the order in which communication might happen between processes. In this paper, I describe a type-driven approach to implementing communicating concurrent programs, using the dependently typed programming language Idris. I show how the type system can be used to describe resource access protocols (such as controlling access to a file handle) and verify that programs correctly follow those prtools. Finally, I show how to use the type system to reason about the order of communication between concurrent processes, ensuring that each end of a communication channel follows a defined protocol.

10

Concurrency in Mobile Object Net Systems

100%

Köhler M. , Rölke H.

|

2003

|

tom Vol. 54, nr 2,3

221-235

EN

In this work we present the model of ``mobile object net systems'' - an algebraic formalisation of the ``nets within nets''-paradigm. The formalism of ``mobile object nets'' is well suited to express the dynamics of open, mobile systems, since it allows tokens to be active. The algebraic theory of ``mobile object net systems'' covers an integrated view of the two major topics concurrency and locality, which are central in the area of mobile computing. As a main result of this contribution, we derive an algebraic model in the ``Petri nets are monoids'' style. It is shown, that mobile object net systems are a conservative extension of the Petri net formalism.

11

Graph Transformation with Time

100%

Gyapay S. , Varró D. , Heckel R.

|

2003

|

tom Vol. 58, nr 1

1--22

EN

Following TER nets, an approach to the modeling of time in high-level Petri nets, we propose a model of time within (attributed) graph transformation systems where logical clocks are represented as distinguished node attributes. Corresponding axioms for the time model in TER nets are generalized to graph transformation systems and semantic variations are discussed. They are summarized by a general theorem ensuring the consistency of temporal order and casual dependencies. The resulting notions of typed graph transformation with time specialize the algebraic double-pushout (DPO) approach to typed graph transformation. In particular, the concurrency theory of the DPO approach can be used in the transfer of the basic theory of TER nets.

12

The BDD Space Complexity of Different Forms of Concurrency

100%

Baldamus M. , Schneider K.

|

2002

|

tom Vol. 50, nr 2

111-133

EN

The automated verification of concurrent systems by model checking is often confronted with the state space explosion problem. A widely adopted method to tackle this problem is to use binary decision diagrams (BDDs) for representing systems and state spaces implicitly. However, it may be that even the system representation itself is prohibitively large. It is therefore interesting to study which factors influence the size of a BDD that represents the transition relation of a system. In this article, we consider the BDD representations of synchronous, asynchronous, and interleaved processes with communication via shared variables and present upper bounds for their sizes. To this end, we introduce a general representation strategy where catastrophic exponential growth of the BDD can only be due to the specifics of communication and/or write conflict resolution; it is neither due to the number of processes nor to the concurrency discipline. Moreover, conditions on communication and write conflict resolution are presented that are sufficient for polynomial sized BDD representations.

13

An acceptance vector semantics for path programs

88%

Shields M. W.

|

1999

|

tom Vol. 40, Nr 2,3

285-316

EN

In this paper, we consider two formal semantics for path programs. The first is a version of the net semantics introduced in [8] and further described in [7], and the second is an extension of the vector semantics of [15]. The extension involves the idea of tagging vectors with sets of sets of action names as with acceptance sets [3, 5] or refusal sets [1, 6] as used in the semantics of certain process algebras. The net semantics of [8, 7] associates a path program with an isomorphism class of labelled, marked nets - two such nets being isomorphic if they have identical pictorial representations and consequently describe the same system. A behaviour of such a class is an isomorphism class of cycle-free labeled nets showing the (partial) order in which conditions have held and events have occurred. We review these basic ideas and then present a version of the [7] semantics. We next present an acceptance vector semantics for path programs. An acceptance vector consists of a collection of sequences, one for each component path, describing the sequence of actions associated with the path in question during some period of activity, together with a set of actions which are available to continue the behaviour represented by the collection. Finally, we show that the two semantics are related in the sense that every net based behaviour may be transformed into an accceptance vector.

14

Types for Active Objects with Static Deadlock Prevention

88%

Puntigam F. , Peter C.

|

2001

|

tom Vol. 48, nr 4

315-341

EN

Process types statically ensure the acceptability of all messages sent to an object even if the set of acceptable messages changes dynamically. As proposed so far, process types do not ensure the return of answers; deadlocks may prevent objects from behaving as expected. In this article we propose an object calculus with types distinguishing between obligatory messages (that must be sent, for example, as answer to a question) and optional messages (that can, but need not be sent). A type checker enforces the sending of obligatory messages and ensures that obligatory messages are not suppressed by deadlocks. The proposed type concept supports subtyping.

15

Clusters, Confusion and Unfoldings

88%

Haar S.

|

2001

|

tom Vol. 47, nr 3,4

259-270

EN

We study independence of events in the unfoldings of Petri nets, in particular indirect influences between concurrent events: Confusion in the sense of Smith [11] and weak interference. The role of structural (conflict) clusters is investigated, and a new unfolding semantics based on clusters motivated and introduced.

16

Petri nets with weak conflicts : a proposal of classification

88%

Ochmański E.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

|

1998

|

tom nr 866

3-22

EN

The paper deals with theoretical aspects of some practical problems about Petri nets: how to avoid conflicts and when is it possible? We are studying the class of Petri nets, which can be implemented without an external conflict resolving supervisor. Such nets are named weakly conflicting, and conflicts appearing in them are said to be weak. We investigate properties of nets, with respect to conflicts, and propose a classification of them. Then we prove the proposed classes of nets form a partially ordered hierarchy.

PL

Praca zajmuje się teoretycznymi aspektami pewnych praktycznych problemów dotyczących sieci Petriego: jak unikać konfliktów i kiedy jest to możliwe? Badamy klasę sieci, które mogą być implementowane bez mechanizmu rozstrzygającego konflikty. Sieci takie nazywamy słabo konfliktowymi, a konflikty w nich występujące słabymi konfliktami. Badamy własności sieci względem konfliktów i proponujemy pewną ich klasyfikację. Dowodzimy, że zdefiniowane klasy sieci tworzą częściowo uporządkowaną hierarchię.

17

Adding parallelism to sequential programs : a combined method

88%

Daszczuk W. B. , Czejdo D. B. , Grześkowiak W.

International Journal of Electronics and Telecommunications

|

2024

|

tom Vol. 70, No. 1

135--144

EN

The article outlines a contemporary method for creating software for multi-processor computers. It describes the identification of parallelizable sequential code structures. Three structures were found and then carefully examined. The algorithms used to determine whether or not certain parts of code may be parallelized result from static analysis. The techniques demonstrate how, if possible, existing sequential structures might be transformed into parallel-running programs. A dynamic evaluation is also a part of our process, and it can be used to assess the efficiency of the parallel programs that are developed. As a tool for sequential programs, the algorithms have been implemented in C#. All proposed methods were discussed using a common benchmark.

18

A Kleene-Schützenberger Theorem for Trace Series over Bounded Lattices

88%

Huschenbett M.

|

tom Vol. 112, nr 2/3

171-191

EN

We study weighted trace automata with weights in strong bimonoids. Traces form a generalization of words that allow to model concurrency; strong bimonoids are algebraic structures that can be regarded as "semirings without distributivity". A very important example for the latter are bounded lattices, especially non-distributive ones. We show that if both operations of the bimonoid are locally finite, then the classes of recognizable and mc-rational trace series coincide and, in general, are properly contained in the class of c-rational series. Moreover, if, in addition, in the bimonoid the addition is idempotent and the multiplication is commutative, then all three classes coincide.

19

Discovery of Asynchronous Concurrent Models from Experimental Tables

88%

Pancerz K. , Suraj Z.

|

2004

|

tom Vol. 61, nr 2

97--116

EN

The synthesis problem of concurrent systems has earlier been discussed in the literature using different types of formalisms. This paper presents a new method for discovery of asynchronous concurrent models from experimental tables by using a rough set approach. The proposed method can be applied to the automatic data model discovery. The algorithm for constructing asynchronous concurrent models is described in detail. As a model for concurrency the Coloured Petri Nets are used. Constructed asynchronous models can be helpful to solving some problems arising in design of asynchronous digital systems or addressing of nodes in parallel systems. An example illustrates an application of the proposed approach in such problems.

20

Synthesis of Petri Net Models: A Rough Set Approach

88%

Pancerz K. , Suraj Z.

|

2003

|

tom Vol. 55, nr 2

149-165

EN

The synthesis problem of concurrent data models from experimental tables based on rough set approach has earlier been discussed [14], [15]. Classical Petri nets have been used as a model for concurrency. In this paper we propose the nets with inhibitor expressions and Coloured Petri Nets as models for concurrency. The nets with inhibitor expressions are defined on the base of so called inhibitor rules extracted from modelled systems. The approach presented in this paper enables to implement the algorithms for easier construction of Petri net models. The proposed approach can be applied to discover data models in semi-automatic way. The obtained models enable us to determine all global states of a modelled system represented by an information system, consistent with all rules extracted from the given information system.