Wyniki wyszukiwania - BazTech

1

Visualisation of concurrent processes

Mikulski Ł, Piątkowski M.

Control and Cybernetics

|

2013

|

Vol. 42, no. 3

699-725

EN

Mazurkiewicz traces are a widely used model for describing the languages of concurrent systems computations. The causal structure of atomic actions occurring in a process modeled as a trace generates a partial order. Hasse diagrams of such order are very common structures used for presentation and investigation in the concurrency theory, especially from the behavioural perspective. We present effective algorithms for Hasse diagrams construction and transformation. Later on, we use them for enumeration of all linearisations of the partial order that represents a concurrent process. Additionally, we attach the flexible visual implementation of all considered Algorithms.

2

Projection Representation of Mazurkiewicz Traces

Mikulski Ł

Fundamenta Informaticae

|

2008

|

Vol. 85, nr 1-4

399-408

EN

The behavior of infinite traces is an interesting field for studies. Infinite traces can be described using projections to word monoids. Such projection representations can be generalized to projection sets. To complete simple descriptions, the binary operation from projection sets to traces has been defined. After such preparations some properties of infinite traces are discussed.

3

Uniform Satisfiability in PSPACE for Local Temporal Logics Over Mazurkiewicz Traces

Gastin P., Kuske D.

Fundamenta Informaticae

|

2007

|

Vol. 80, nr 1-3

169-197

EN

We study the complexity of temporal logics over concurrent systems that can be described by Mazurkiewicz traces. We develop a general method to prove that the uniform satisfiability problem of local temporal logics is in PSPACE. We also demonstrate that this method applies to all known local temporal logics.

4

On First-Order Fragments for Mazurkiewicz Traces

Diekert V., Horsch M., Kufleitner M.

Fundamenta Informaticae

|

2007

|

Vol. 80, nr 1-3

1-29

EN

Mazurkiewicz traces form a model for concurrency. Temporal logic and first-order logic are important tools in order to deal with the abstract behavior of such systems. Since typical properties can be described by rather simple logical formulas one is interested in logical fragments. One focus of this paper is unary temporal logic and first-order logic in two variables. Over words, this corresponds to the variety of finite monoids called DA. However, over Mazurkiewicz traces it is crucial whether traces are given as dependence graphs or as partial orders (over words these notions coincide). The main technical contribution is a generalization of important characterizations of DA from words to dependence graphs, whereas the use of partial orders leads to strictly larger classes. As a consequence we can decide whether a first-order formula over dependence graphs is equivalent to a first-order formula in two variables. The corresponding result for partial orders is not known. This difference between dependence graphs and partial orders also affects the complexity of the satisfiability problems for the fragments under consideration: for first-order formulas in two variables we prove an NEXPTIME upper bound, whereas the corresponding problem for partial orders leads to EXPSPACE. Furthermore, we give several separation results for the alternation hierarchy for first-order logic. It turns out that even for those levels at which one can express the partial order relation in terms of dependence graphs, the fragments over partial orders have more expressive power.

5

On Communicating Automata with Bounded Channels

Genest B., Kuske D., Muscholl A.

Fundamenta Informaticae

|

2007

|

Vol. 80, nr 1-3

147-167

EN

We review the characterization of communicating finite-state machines whose behaviors have universally or existentially bounded channels. These results rely on the theory of Mazurkiewicz traces. We investigate the question whether channel bound conditions are decidable for a given communicating finite-state machine.

6

Limits of Modularity

Bednarczyk M.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

|

2006

|

Nr 989

1-21

EN

It has been observed that various synchronisation operators that underly modular design of concurrent systems can be explained as {\em pullbacks in suitable categories of concurrent systems. Here, the boundaries of such approach are investigated. For this purpose we study the issue of completeness in categories of trace monoids. It turns out that (finite) completeness is achieved if trace monoids with concurrency preserving homomorphisms are considered. Taking arbitrary monoid homomorphisms leads, in general, to incompleteness. In terms of code problem for trace monoids.

PL

Wcześnie zauważono, że modularne techniki konstruowania systemów współbieżnych oparte o mechanizmy synchronizacji można opisać jako (zmodyfikowane) produkty lub wręcz jako produkty włókniste w stosownych kategoriach systemów współbieżnych. Celem niniejszej pracy jest wyznaczenie granic stosowalności tego teorio-kategoryjnego podejścia. W tym celu w pracy rozważa się problem (skończonej) zupełności kategorii monoidów śladów Mazurkiewicza dla różnych klas morfizmów formalizującej pojęcie symulacji systemów. Okazuje się, że skończoną zupełność gwarantuje przyjęcie, iż obiektem badań są reprezentacje monoidów śladów postaci alfabet i relacja niezależności, zaś morfizmy to funkcje z alfabetu do monoidu śladów zachowujące niezależność. Z kolei akceptacja dowolnych homomorfizmów, niekoniecznie zachowujących niezależność, prowadzi na ogół do braku zupełności kategorii. Osiągnięte wyniki rozszerzają też obszar, w którym problem kodu dla monoidów śladów jest rozstrzygalny w sposób pozytywny.

7

Limits of Modularity

Bednarczyk M.A.

Fundamenta Informaticae

|

2006

|

Vol. 74, nr 2,3

167-187

EN

It has been observed that various synchronisation operators underlying the modular design of concurrent systems can be explained as pullbacks in suitable categories of concurrent systems. Here, the boundaries of such approach are investigated. For this purpose we study the issue of completeness in categories of trace monoids. It turns out that (finite) completeness is achieved if trace monoids with concurrency preserving homomorphisms are considered. Taking arbitrary monoid homomorphisms leads, in general, to incompleteness. The results obtained are used to reveal an area in which the code problem for trace monoids, undecidable in general, has always a positive answer.