Wyniki wyszukiwania - BazTech

1

Modeling and Verification using Different Notations for CPSs: The One-Water-Tank Case Study

Staroletov Sergey, Schulte Horst, Baar Thomas, Konyukhov Ivan, Shilov Nikolay, Rozov Andrei, Liakh Tatiana, Zyubin Vladimir

Annals of Computer Science and Information Systems

|

2021

|

Vol. 25

485--488

EN

The choice of an adequate notation and subsequent system formalization are the crucial points for the design of cyber-physical systems (CPSs). Here, an appropriate notation allows an explicit specification of the deterministic system behavior for specified initial states and inputs. We base our study on an industrial example (water tank) that comprises nominal as well as safety-critical states, and focus on the notation’s support to validate/verify crucial safety properties. Several industrial notations (e.g. Matlab/Simulink©) to design and simulate such a hybrid system have been tried based on our physical model. In addition, we remodel our example using the well-founded mathematical formalism of hybrid automata. It enables us to formally express and verify important safety properties using the theorem prover KeYmaera

2

Analiza tablic decyzyjnych z wykorzystaniem monotonicznego rachunku sekwensów

Tkacz J., Adamski M.

Przegląd Elektrotechniczny

|

2013

|

R. 89, nr 6

256--259

PL

W artykule przedstawiono nowatorski sposób analizy systemów regułowych z wykorzystaniem symbolicznego wnioskowania w monotonicznej logice sekwentów Gentzena. Badany system dyskretny jest opisywany w postaci tablicy decyzyjnej. Celem analizy systemu jest usunięcie zbytecznych kolumn w tablicy decyzyjnej oraz nieistotnych symboli zmiennych logicznych w jej poszczególnych wierszach. Efektywny aparat wnioskowania w logice formalnej umożliwia sprawne wyznaczanie transwersal krawędzi hipergrafu rozróżnialności.

EN

The paper presents a new methodology for symbolic reduction of multivalued decision tables, currently intensively used for compact behavioral specifications of logic controllers. As an example the well known problem of simplification of a set of several logic rules with many variables is chosen. As a completely new, original solution, the formal automated reasoning based on Gentzen propositional calculus together with hypergraph theory are jointly used. The clique-transversal symbolic calculation is performed by means of effective reasoning in Gentzen calculus.

3

Koncepcja i realizacja systemu wnioskującego Gentzena z wykorzystaniem RDBMS – IBM DB2

Gaczyński A., Tkacz J., Doligalski M.

Przegląd Elektrotechniczny

|

2012

|

R. 88, nr 8

148-151

PL

Poniższy artykuł przedstawia realizację systemu wnioskującego Gentzena z wykorzystaniem systemu zarządzania relacyjną bazą danych IBM DB2 w wersji 9.7. Niniejsza publikacja prezentuje zalety z używania procedur składowanych oraz w jaki sposób można wykorzystać strukturę tabel w bazie danych do zaawansowanego przetwarzania informacji. Przedstawia użycie bazy danych przy implementacji automatycznych systemów dowodzenia twierdzeń oraz w jaki sposób architektura klient-serwer znajduje zastosowanie w stosunku do tego typu aplikacji.

EN

The paper presents conception and design of Gentzen deduction system by using RDBMS – IBM DB2. It shows adds of stored procedures and method of using table structure in database for advanced information computing. Testing of the solution is based on the analysis of randomly generated not oriented graphs. The tests confirm the correctness of implementations, and also highlight the problem of high computational complexity. This unusual implementation and use of RDBMS environment opens up new areas of research on the optimization of reasoning algorithm.

4

The Procedures of the Assigvment of Tasks Distribution for Parallel Processors System

Borowik A., Piech H.

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

|

1998

|

Vol. 4

63-73

EN

In this paper one of possible optimum conditions distribution processes algorithmes with precised (limited) number of processors is described. This method accepts that realization lines of particular variavles with initial supplementary procedures application are specified earlier. Results are produced as a time-vectors of particular rules realization with determine each variable creation stages. In this algorithm criterions relavant with minimalization following rules expection of time which determine particular variable creation stages and also with conferment highest priorites lines which are characterized by langest realization time is regarded. Moreover in investigations is experimentated a simulation program of proposed algorithm.

5

A Survay of Foundational Gentzen's Systems for Finitely-Valued Logics

Borowik P.

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

|

1998

|

Vol. 4

89-120

EN

The Gentzen system for n-valued logical calculi discussed here is based on the notion of a sequent. However, this notion can be defined in at least three different ways. The first defines a sequent as a finite sequence of formulas (Kirin 1985, Saloni 1972, Orłowska 1985), the second defines it as an ordered n-tuple of finite sequences or sets of formulas (Rousseau 1967, Takahasi 1967, Borowik 1984). The third way consists in defining a sequent as an ordered pair of finite sets or sequences of formulas (Fitting 1991). The assumed definition determines then the form of the rules for eliminating or introducing propositional connectives in a given sequent, and thus also the whole formalization of the system.