BazTech - Yadda

1

Generation of synchronizing state machines from a transition system: A region-based approach

Teren Viktor, Cortadella Jordi, Villa Tiziano

International Journal of Applied Mathematics and Computer Science

|

2023

|

Vol. 33, no. 1

133--149

EN

Transition systems (TSs) and Petri nets (PNs) are important models of computation ubiquitous in formal methods for modeling systems. A crucial problem is how to extract, from a given TS, a PN whose reachability graph is equivalent (with a suitable notion of equivalence) to the original TS. This paper addresses the decomposition of transition systems into synchronizing state machines (SMs), which are a class of Petri nets where each transition has one incoming and one outgoing arc. Furthermore, all reachable markings (non-negative vectors representing the number of tokens for each place) of an SM have only one marked place with only one token. This is a significant case of the general problem of extracting a PN from a TS. The decomposition is based on the theory of regions, and it is shown that a property of regions called excitation-closure is a sufficient condition to guarantee the equivalence between the original TS and a decomposition into SMs. An efficient algorithm is provided which solves the problem by reducing its critical steps to the maximal independent set problem (to compute a minimal set of irredundant SMs) or to satisfiability (to merge the SMs). We report experimental results that show a good trade-off between quality of results vs. computation time.

2

Analysis of the performance of an aircraft powered by hybrid propulsion

Majka Andrzej, Muszyńska-Pałys Jagoda

Combustion Engines

|

2023

|

R. 62, nr 2

45--51

EN

Travel is an inseparable part of human life. It is connected not only with private life but also with business life. People want to travel more, farther and faster. That is why air transport is currently one of the fastest-growing areas of passenger transport, and airlines carry more and more passengers from year to year. Due to the growing negative impact of air transport on the natural environment, research aimed at the development of technologies to reduce the negative impact of air transport is becoming more and more important. One of the possibilities for improving the situation is the use of alternative energy sources, limiting the emission of greenhouse gases into the atmosphere. The paper aimed to analyze the meaningfulness of replacing the classic power unit in a light transport aircraft with a hybrid, combustion-electric power unit. Analyzes were made with the use of simulation methods for the PZL M-28 aircraft.

3

Unbounded Model Checking for ATL

Kański Michał, Niewiadomski Artur, Kacprzak Magdalena, Penczek Wojciech, Nabiałek Wojciech

Studia Informatica : systems and information technology

|

2021

|

Vol. 1-2(25)

5--22

EN

In this paper, we deal with verification of multi-agent systems represented as concurrent game structures. To express properties to be verified, we use Alternating-Time Temporal Logic (ATL) formulas. We provide an implementation of symbolic model checking for ATL and preliminary, but encouraging experimental results.

4

Comparing sat-based bounded model checking rtectl and ectl properties

Zbrzezny A. M.

Technical Sciences / University of Warmia and Mazury in Olsztyn

|

2017

|

nr 20(2)

131--147

EN

We compare two SAT-based bounded model checking algorithms for the properties expressed in the existential fragment of a soft real-time computation tree logic (RTECTL) and in the existential fragment of computation tree logic (ECTL). To this end, we use the generic pipeline paradigm (GPP) and the train controller system (TC), the classic concurrency problems, which we formalise by means of a finite transition system. We consider several properties of the problems that can be expressed in both RTECTL and ECTL, and we present the performance evaluation of the mentioned bounded model checking methods by means of the running time and the memory used.

5

Can Machine Learning Learn a Decision Oracle for NP Problems? A Test on SAT

Grozea C., Popescu M.

Fundamenta Informaticae

|

2014

|

Vol. 131, nr 3-4

441--450

EN

This note describes our experiments aiming to empirically test the ability of machine learning models to act as decision oracles for NP problems. Focusing on satisfiability testing problems, we have generated random 3-SAT instances and found out that the correct branch prediction accuracy reached levels in excess of 99%. The branching in a simple backtracking-based SAT solver has been reduced in more than 90% of the tested cases, and the average number of branching steps has reduced to between 1/5 and 1/3 of the one without the machine learning model. The percentage of SAT instances where the machine learned heuristic-enhanced algorithm solved SAT in a single pass reached levels of 80-90%, depending on the set of features used.

6

Bridging Membrane and Reaction Systems : Further Results and Research Topics

Păun G., Pérez-Jiménez M.J., Rozenberg G.

Fundamenta Informaticae

|

2013

|

Vol. 127, nr 1-4

99--114

EN

This paper continues an investigation into bridging two research areas concerned with natural computing: membrane computing and reaction systems. More specifically, the paper considers a transfer of two assumptions/axioms of reaction systems, non-permanency and the threshold assumption, into the framework of membrane computing. It is proved that: (1) spiking neural P systems with non-permanency of spikes assumption characterize the semilinear sets of numbers, and (2) symport/antiport P systems with threshold assumption (translated as ω multiplicity of objects) can solve SAT in polynomial time. Also, several open research problems are stated.

7

Using BOINC desktop grid to solve large scale SAT problems

Posypkin M., Semenov A., Zaikin O.

Computer Science

|

2012

|

Vol. 13 (1)

25-34

EN

Many practically important combinatorial problems can be efficiently reduced to a problem of Boolean satisfiability (SAT). Therefore, the implementation of distributed algorithms for solving SAT problems is of great importance. In this article we describe a technology for organizing desktop grid, which is meant for solving SAT problems. This technology was implemented in the form of a volunteer computing project SAT@home based on a popular BOINC platform.

8

Współczesne zmiany powierzchni lodów morskich na wodach wokółantarktycznych - problemy i niejasności

Marsz A. A.

Problemy Klimatologii Polarnej

|

2011

|

nr 21

7-38

PL

Praca charakteryzuje trendy zmian powierzchni zlodzonej na wodach wokółantarktycznych w latach 1979-2010. Stwierdza się występowanie dodatniego trendu rocznego powierzchni zlodzonej (+15.6ź103 km2źrok-1) o wysokiej istotności statystycznej (p < 0.001). Dodatnie trendy występują we wszystkich miesiącach roku, z tego trendy te są statystycznie istotne w okresie od maja do października. Najsilniejsze trendy dodatnie występują w okresie rozrastania się pokrywy lodowej (marzec-lipiec). W ujęciu regionalnym w czterech z pięciu sektorów Antarktyki trendy są dodatnie, z czego tylko w jednym – sektorze Morza Rossa – trend jest istotny statystycznie, w jednym sektorze (mórz Amundsena i Bellingshausena) – występuje statystycznie istotny trend ujemny. Analiza przyczyn występowania dodatniego trendu powierzchni zlodzonej na wodach wokółantarktycznych, pozwala wskazać jako główną przyczynę rozrostu pokrywy lodowej cyrkulację atmosferyczną. Te same procesy cyrkulacyjne są przyczyną zarówno ogólnego wzrostu powierzchni lodów na wodach wokółantarktycz-nych, jak jednoczesnego jej spadku w rejonie Morza Bellingshausena i wzrostu temperatury powietrza nad Półwyspem Antarktycznym. Zmiany cyrkulacji atmosferycznej następują pod wpływem zmian zasobów ciepła w SW części subtropikalnego Pacyfiku (~30°N, 170-160°W), które wymuszają zwiększoną lub zmniejszoną powtarzalność lokowania się górnego klina na długości geograficznej Morza Rossa i górnej zatoki na pograniczu mórz Amundsena i Bellingshausena. Zmiany temperatury wody powierzchniowej w tym rejonie objaśniają około 28% międzyrocznej zmienności rocznej powierzchni zlodzonej na wodach wokółantarktycznych, występujący w niej trend dodatni, spadek powierzchni zlodzonej na Morzu Bellingshausena i wzrost temperatury powietrza w rejonie Półwyspu Antarktycznego.

EN

This work describes trends in changes in sea ice extent in the waters in the vicinity of the Antarctica in the years 1979-2010. A positive trend in the annual ice extent (+15.6ź103 km2źyear-1) with high statistical significance (p <0.001) was observed. Positive trends occur in all months of the year and statistically significant trends are noted in the period from May to October. The strongest positive trends occur in the period when ice cover grows (March-July). Regionally, in four out of the five sectors of the Antarctica, trends are positive but only in one - the Ross Sea sector - the trend is statistically significant and in one sector (the Amundsen and Bellingshausen seas) there is a statistically significant negative trend. Analysis of the causes of the positive trend in the sea ice extent indicates that the primary role in the growth of ice extent is attributed to atmospheric circulation. The same circulation processes are responsible for both an overall increase in the ice extent in the region of the Antarctica and in the simultaneous decrease in the ice extent in the Bellingshausen Sea and the growth in air temperature over the Antarctic Peninsula. Changes in atmospheric circulation are influenced by heat resources in the south-western part of the subtropical Pacific (~ 30°N, 170-160°W). These heat resources cause that the same location of the upper ridge of high pressure at the Ross Sea longitude and the upper trough on the border of the Amundsen and Bellingshausen seas is repeated more or less frequently. SST changes in this region explain about 28% of the interannual variability of annual sea ice extent in the area of the Antarctic waters. They also explain the positive trend noted there and the decline in sea ice extent in the Bellingshausen Sea and increase in the air temperature in the region of the Antarctic Peninsula.

9

Testing satisfiability of logical formulas based on FPGA

Sadowski A., Jakubski A.

Metody Informatyki Stosowanej

|

2011

|

nr 3

151-156

EN

FPGA (Field Programmable Gate Array) allows direct programming the matrix of configurable blocks and thus forming a programmable logic adapted to the problem being solved. The appearance of programmable devices on the market and their higher capacity have resulted in increase of interest in this technology in recent years. In this paper we introduce the use of programmable devices for testing satisfiability and tautological character of logical formulas. We compare the achieved results of the calculations for the architecture created by us with the general-purpose architectures.

10

SAT-based searching for k-quasi-optimal runs in weighted timed automata

Woźna-Szcześniak B., Zbrzezny A.

Scientific Issues of Jan Długosz University in Częstochowa. Mathematics

|

2010

|

Vol. 15

163--176

EN

In the paper we are concerned with an optimal cost reachability problem for weighted timed automata, and we use a translation to SAT to solve the problem. In particular, we show how to find a run of length k ∈ IN that starts at the initial state and terminates at a state containing a target location, its total cost belongs to the interval [c,c+1), for some natural number c ∈ IN, and the cost of each other run of length k, which also leads from the initial state to a state containing the target location, is greater or equal to c. This kind of runs is called k-quasi-optimal. We exemplify the use of our solution to the mentioned problem by means of the air traffic control problem, and we provide some preliminary experimental results.

11

Systemy kontroli eksploatacji bloków

Rusinowski H., Szega M.

Energetyka Cieplna i Zawodowa

|

2010

|

Nr 3

7--11

PL

W artykule dokonujemy przeglądu komputerowych systemów kontroli eksploatacji zainstalowanych w elektrowniach i elektrociepłowniach w Polsce i na świecie. Przedstawiamy strukturę i funkcje Modułowego Systemu Kontroli Eksploatacji (MSKE), który dostarcza służbom korzystającym z systemu pełnej i wiarygodnej informacji o procesie oraz umożliwia eksploatację bloków w otoczeniu stanów optymalnych.

12

Diagnozowanie bezpieczeństwa systemu antropotechnicznego w ujęciu potencjałowym

Bednarek M., Będkowski L., Dąbrowski T.

Przegląd Elektrotechniczny

|

2009

|

R. 85, nr 11

87-92

PL

W artykule przedstawiono system antropotechniczny (SAT) w ujęciu potencjałowym. Podano potencjałowe oraz bezpiecznościowe potencjałowe kryterium zdatności systemu antropotechnicznego. Zaadaptowano ujęcie potencjałowe do oceny ryzyka zawodowego. Całość artykułu uzupełniają przykłady.

EN

A human engineering system (HES) in a potential conception is presented in the article. The human engineering potential fitness criterion and potential fitness criterion in safety perspective are given. Furthermore the potential approach was adopted to a risk assessment. The article is complemented with examples.

13

Doświadczenia związane z uruchomieniem Systemu Alarmowo Telefonicznego SAT w JSW S.A. KWK Dniówek

Lojza H.

Mechanizacja i Automatyzacja Górnictwa

|

2006

|

R. 44, nr 6

25-28

PL

W referacie przedstawiono doświadczenia zebrane w trakcie uruchomienia oraz wdrożenia w JSW S.A. KWK Pniówek Zintegrowanego systemu łączności telefonicznej, dyspozytorskiej i alarmowo-rozgłoszeniowej typu SAT o pojemności 2x192 NN. Omówiono możliwość współpracy systemu SAT z innymi urządzeniami i systemami wchodzącymi w skład systemu ogólnozakładowej łączności telefonicznej i systemu dyspozytorskiego KWK Pniówek. Ponadto w referacie zaprezentowano zmiany wprowadzone w systemie SAT, których celem było poprawienie funkcjonalności oraz niezawodności jego działania.

EN

The experiences gained during startup and implementation of the Integrated Telephone Communication, Mine Control and Alarm-broadcasting System with a capacity of 2xy192 NN in the JSW S.A. KWK "Pniówek" colliery have been presented in the paper. A usability of the SAT system together with other devices and systems included in the minewide telephone communication and mine control system of the .Pniówek. colliery has been discussed. Furthermore the paper presents the changes made within the SAT system aiming at improvement in its functionality and reliability of operation.