Wyniki wyszukiwania - BazTech

1

Coverability, Termination, and Finiteness in Recursive Petri Nets

Finkel Alaina, Haddad Sergeb, Khmelnitsky Igor

Fundamenta Informaticae

|

2021

|

Vol. 183, nr 1-2

33--66

EN

In the early two-thousands, Recursive Petri nets have been introduced in order to model distributed planning of multi-agent systems for which counters and recursivity were necessary. Although Recursive Petri nets strictly extend Petri nets and context-free grammars, most of the usual problems (reachability, coverability, finiteness, boundedness and termination) were known to be solvable by using non-primitive recursive algorithms. For almost all other extended Petri nets models containing a stack, the complexity of coverability and termination are unknown or strictly larger than EXPSPACE. In contrast, we establish here that for Recursive Petri nets, the coverability, termination, boundedness and finiteness problems are EXPSPACE-complete as for Petri nets. From an expressiveness point of view, we show that coverability languages of Recursive Petri nets strictly include the union of coverability languages of Petri nets and context-free languages. Thus we get a more powerful model than Petri net for free.

2

Cooperation of multiple autonomous robots and analysis of their swarm behawior

Czejdo B., Daszczuk W. B., Grabski W., Bhattacharya S.

Autobusy : technika, eksploatacja, systemy transportowe

|

2018

|

R. 19, nr 12

872--879

EN

In this paper, we extended previous studies of cooperating autonomous robots to include situations when environmental changes and changes in the number of robots in the swarm can affect the efficiency to execute tasks assigned to the swarm of robots. We have presented a novel approach based on partition of the robot behavior. The sub-diagrams describing sub-routs allowed us to model advanced interactions between autonomous robots using limited number of state combinations avoiding combinatorial explosion of reachability. We identified the systems for which we can ensure the correctness of robots interactions. New techniques were presented to verify and analyze combined robots’ behavior. The partitioned diagrams allowed us to model advanced interactions between autonomous robots and detect irregularities such as deadlocks, lack of termination etc. The techniques were presented to verify and analyze combined robots’ behavior using model checking approach. The described system, Dedan verifier, is still under development. In the near future, timed and probabilistic verification are planned.

PL

W artykule opisano kontynuację wcześniejszych badań dotyczących współpracy autonomicznych robotów wewnątrz budynku. Obejmują one obejmują sytuacje, w których zmiany środowiska i zmiana liczby robotów w roju mogą poprawić lub pogorszyć efektywność wykonywania zadań przypisanych do roju robotów. Zaprezentowaliśmy nowatorskie podejście z wykorzystaniem dzielenia zachowań robota na zachowania składowe. Poddiagramy opisujące kładowe podmarszruty pozwoliły nam modelować zaawansowane interakcje między autonomicznymi robotami w oparciu o ograniczoną liczbę kombinacji zachowań, unikając eksplozji kombinatorycznej przestrzeni osiągalności. Opisano systemy, dla których możemy zapewnić poprawność interakcji robotów i zaprezentowano techniki weryfikacji i analizy zachowań połączonych robotów. Diagramy podzielone na partycje pozwoliły nam modelować zaawansowane interakcje pomiędzy autonomicznymi robotami i wykrywać nieprawidłowości, takie jak zakleszczenia, brak terminacji itp. Przedstawiono techniki weryfikacji i analizy złożonych zachowań robotów za pomocą techniki weryfikacji modelowej. Opisany system weryfikacji, Dedan, jest wciąż rozwijany. W niedalekiej przyszłości planowana jest weryfikacja z czasem rzeczywistym i probabilistyczna.

3

Nawiązanie i rozwiązanie stosunku pracy - prawo pracy w laboratorium

Paszkowska M.

Laboratorium - Przegląd Ogólnopolski

|

2016

|

nr 3-4

80--84

PL

Prawo pracy reguluje prawa i obowiązki stron stosunku pracy. Od 22 lutego 2016 r. obowiązują ważne zmiany Kodeksu pracy dotyczące umów o pracę. Celem artykułu jest przybliżenie podstawowych regulacji prawa pracy dotyczących nawiązania i rozwiązania umowy o pracę.

EN

Labor law regulates the rights and obligations of the employment relationship parties. Important changes to The Labour Code concerning employment contracts have applied from 22 February 2016. The aim of the article is to present the basic regulations of the labor law relating to the establishment and termination of the employment contract.

4

On One-Rule Grid Semi-Thue Systems

Latteux M., Roos Y.

Fundamenta Informaticae

|

2012

|

Vol. 116, nr 1-4

189-204

EN

The family of one-rule grid semi-Thue systems, introduced by Alfons Geser, is the family of one-rule semi-Thue systems such that there exists a letter c that occurs as often in the left-hand side as the right-hand side of the rewriting rule. We prove that for any one-rule grid semi-Thue system S, the set S(w) of all words obtainable from w using repeatedly the rewriting rule of S is a constructible context-free language. We also prove the regularity of the set Loop(S) of all words that start a loop in a one-rule grid semi-Thue systems S.

5

Gained and Excluded Private Actions by Process Observations

Gruska D.P.

Fundamenta Informaticae

|

2011

|

Vol. 109, nr 3

281-295

EN

Formalisms for description how much information on private actions can be obtained by observing public ones are presented. Two sets of private actions are considered. The set of actions which execution is guaranteed according to observations and the set of actions which execution is excluded according to observations. Since information flows could be realized also by means of different covert channels as time, termination and divergence this possibility is considered as well. Both qualitative and quantitative dimensions of the flow are considered.

6

Higher Order Deforestation

Hamilton G.W.

Fundamenta Informaticae

|

2006

|

Vol. 69, nr 1,2

39-61

EN

Deforestation is a well known transformation algorithm which can eliminate intermediate structures from functional programs. In previous work, we have shown how the deforestation algorithm can be extended to handle higher order programs. A higher order treeless form of expression was defined to ensure the termination of this algorithm. Our higher order algorithm was further extended by Seidl and S?rensen, and this extension was shown to remove some intermediate structures not removed by our algorithm (although our original algorithm can also remove some intermediate structures not removed by their technique). In this paper, we show how our original definition of higher order treeless form can be extended to allow the intermediate structures in the examples given by Seidl and S?rensen to be removed. We argue that, because our extended algorithm uses an easy to recognise treeless form, there is more transparency for the programmer in terms of the improvements which will be made. We prove that our new algorithm terminates, and we conjecture that it ensures that there is no efficiency loss, which we argue is essential for any optimisation.

7

Event Structures for Arbitrary Disruption

Fecher H., Majster-Cederbaum M.

Fundamenta Informaticae

|

2005

|

Vol. 68, nr 1/2

103--130

EN

In process algebras that allow for some form of disruption, it is important to state when a process terminates. One option is to include a termination action Ö. Another approach is that the `final' executed action of a process terminates the process. The semantics of the former approach has been investigated in the literature in detail, e.g. by providing consistent true-concurrency and operational descriptions. The `final' executed action termination approach, which is more adequate for modelling, still lacks the existence of a detailed true concurrent description. In order to give a true concurrency model of such a termination view, we introduce a new class of event structures. This type of event structures models disabling by indicating sets of precursor events. We show that the introduced class of event structures has more expressive power with respect to event traces than the common event structures. We also give a classification of the expressive power in terms of sets of event traces. A consistency result of an operational and a denotational semantics is shown.

8

Termination of graph rewriting is undecidable

Plump D.

Fundamenta Informaticae

|

1998

|

Vol. 33, nr 2

201-209

EN

It is shown that it is undecidable in general whether a graph rewriting system (in the 'double pushout approach') is terminating. The proof is by a reduction of the Post Correspondence Problem. It is also argued that there is no straightforward reduction of the halting problem for Turing machines or of the termination problem for string rewriting systems to the present problem.