Syntetyczne omówienie wyników poznawczych projektu 8 T11C 037 16 :
‹‹Dedukcyjne systemy specyfikowania, weryfikowania i konstruowania››

Marek A. Bednarczyk

m.bednarczyk@ipipan.gda.pl

Instytut Podstaw Informatyki PAN, filia Gdańska

Badania teoretyczne prowadzone w ramach realizacji projektu dotyczyły zarówno matematyczno-logicznych podstaw meta-teorii systemów specyfikowania, weryfikowania i konstruowania systemów obliczeniowych. Studiowaliśmy również zagadnienia dotyczące konkretnych klas takich systemów: programów imperatywnych, procesów i programów współbieżnych i reaktywnych, systemów typowania, itd.

Do prac z obszaru badań meta-teorii zaliczyć należy między innymi [6,8,9,16,18,19]. Większość z nich prezentuje teorio-kategoryjne podejście do opisu pojęć podstawowych: co to jest system dedukcyjny, model, specyfikacja, związki między procesami/programami a specyfikacjami, itp. Na podkreślenie zasługują należące do tej kategorii prace doktorskie T. Borzyszkowskiego ([18]) i W. Pawłowskiego ([19]) ukończone i obronione przez obu realizatorów w czasie trwania projektu.

Największe sukcesy poznawcze osiągnęliśmy, w moim przekonaniu, w badaniach dotyczących specyfikowania i konstruowania procesów i systemów współbieżnych [1-2,4-5,7,10-11,13-14,17,21-29]. Dotyczy to zarówno matematycznych podstawi teorii systemów współbieżnych: zarówno w ujęciu tradycyjnym ([1-2,7,10,14,21]), jak i w nowatorskim podejściu nawiązującym do metod topologii algebraicznej ([11,26,27-28]). Z punktu widzenia tematyki projektu powyższe stanowią jednak rezultaty wspierające—zasadnicze efekty naszych badań dotyczą zasad automatycznego konstruowania systemów współbieżnych spełniających zadane specyfikacje ([1,2,4]). Wkład realizatorów w rozwój tej dziedziny został doceniony przez społeczność międzynarodową co znalazło odzwierciedlenie w zaproszeniu do współtworzenia monografii [1] poświeconej udokumentowaniu najnowszych osiągnięć w dziedzinie. W monografii tej znalazł się również rozdział [2] będący wynikiem współpracy z ośrodkiem w Rennes, Francja, nawiązanej w trakcie realizowania projektu.

Rozwinięciem pomysłu wykorzystania do specyfikowania programów imperatywnych formułami logiki predykatów z jawnymi zastąpieniami na grunt sztucznej inteligencji ([12,20]). Zasadniczą zaletą proponowanego tu podejścia jest uniknięcie problemów zwanych w dziedzinie wnioskowania o skutkach akcji, np. w robotyce, z tak zwanym ,,problemem framki’’. Problem ten prowadza się do nieadekwatności zwyczajnych logik, np., logiki pierwszego rzędu, jako języka opisu skutków akcji. W prezentowanej pracy rozwiązanie zapewniają jawne zastąpienia jako nowa klasa formuł atomowych.

Jedną z istotnych składowych projektu były eksperymenty związane z kodowanie systemów formalnych, w tym logik, w systemie Isabelle — popularnym środowisku komputerowym do kodowania logik i systemów formalnych oraz dowodzenia twierdzeń. Natknęliśmy się jednak na istotne problemy. Kłopoty pojawiły się wówczas, gdy próbowaliśmy zmusić Isabelle do akceptacji musików dowodowych generowanych przez zaproponowany przez Stefana Sokołowskiego system dynamicznego typowania termów języka programowania. Nasz problem sprowadzał się do nieumiejętności przekonania systemu Isabelle by ten, zgodnie z opisem, akceptował w trybie on-line musiki wygenerowane przez zakodowany formalny system typowania i przekazywał je, dzięki mechanizmowi wyjątków, do obróbki innemu systemowi wnioskowania również zakodowanemu w Isabelle. Ostatecznie dr Sokołowski zaprogramował całość w SML.

W zaawansowanym stadium znajduje się przygotowywany skrypt [3], którego powstanie wiąże się z prowadzonym na Uniwersytecie Gdańskim wykładzie poświęconym komputerowo-wspomaganemu wnioskowaniu logicznemu. W związku z realizacją projektu i w ramach prowadzonych na Uniwersytecie Gdańskim seminariów przygotowanych zostało kilkanaście prac magisterskich, z których większość została już obroniona.

Większość prac powstałych w trakcie projektu dostępnych jest w wersji elektronicznej, format PostScript, z internetowych stron realizatorów projektu: http://www.ipipan.gda.pl/ lub poprzez podane tam linki.

Książki i Rozdziały monografii

1	M. A. Bednarczyk, A. M. Borzyszkowski	On Concurrent Realizations of Reactive Systems and Their Morphisms. H. Ehrig et al. (Eds.): Unifying Petri Nets,. LNCS 2128, 346-379. Springer-Verlag, 2001.
2	E. Badouel, M. A. Bednarczyk, Ph. Darondeau	Generalized automata and their net representations. H. Ehrig et al. (Eds.): Unifying Petri Nets, Advances in Petri Nets. LNCS 2128, 304-345. Springer-Verlag, 2001.
3	M. A. Bednarczyk, T. Borzyszkowski, W. Pawłowski, P. Pączkowski, S. Sokołowski	Komputerowe wspomaganie dowodzenia. Skrypt do wykładu prowadzonego na Uniwersytecie Gdańskim, str. 77 w przygotowaniu, 2002.

Prace w czasopismach o zasięgu międzynarodowym

4	M. A. Bednarczyk	Towards automatic synthesis of concurrent, asynchronous and distributed programs. Annual Report of the Polish Academy of Sciences, 2002, w druku.
5	M. A. Bednarczyk, A. Borzyszkowski	Concurrent Realizations of Reactive Systems. M. Hoffmann, et al (Eds). 8th Category Theory in Computer Science, Edinburgh, Electronic Notes in Theoretical Computer Science, Vol. 29, 1-19, Elsevir, 1999
6	M. A. Bednarczyk, A. Borzyszkowski, W. Pawłowski	Generalised Congruencies – Epimorphisms in CAT. Theory and Applications of Categories, 1999
7	M. A. Bednarczyk, A. Borzyszkowski, R. Somla	Finite Completeness of Categories of Petri Nets. Fundamenta Informaticae, Vol. 43, No 1-4, 21-48, 2000.
8	T. Borzyszkowski	Logical systems for structured specifications, Przyjęte do Theoretical Computer Science, 1999. W druku.
9	T. Borzyszkowski	Generalized interpolation in CASL. Information Processing Letters, Vol. 76, No1-2, 19-24, 2000
10	J. Skurczyński	A characterization of Buechi tree automata. Information Processing Letters, Vol 81, 29-33, 2002.
11	S. Sokołowski	Investigation of concurrent processes by means of homotopy functors. Przyjęta do Mathematical Structures in Computer Science, 2000. W druku.

doniesienia konferencyjne w materiałach o zasięgu międzynarodowym

12	M. A. Bednarczyk	A non-monotone logic for reasoning about action. Proc. Inteligent Information Systems'02, Advances in Soft Computing, Physica-Verlag, 2002, w druku.
13	M. A. Bednarczyk, A. Borzyszkowski	General Morphisms of Petri nets. J. Wiedermann, P. van Emde Boas, M. Nielsen (Eds). Proc. 26th Intn'l Coll. in Automata, Languages & Programming, Prague, 1999,Springer Lecture Notes in Computer Science, vol 1644, 190-199, 1999
14	M. A. Bednarczyk, A. Borzyszkowski, R. Somla	Equalizing Morphisms of Petri Nets. Proceedings. International Workshop on Concurrency, Specification and Programming, Warsaw, pp.: 24-35, 1999.
15	T. Borzyszkowski	Higher-order logic and theorem proving for structured specifications. Proc. Work. on Abstract Data Types'99, Springer LNCS 1827, 401-418, 2000
16	W. Pawłowski	Presentations for Abstract Context Institutions M.Cerioli, G. Reggio (Eds), 15th International Workshop on Algebraic Development Techniques joint with the CoFI WG Meeting Genova, April 2001 - Selected Papers LNCS vol. 2267, Springer-Verlag 2001
17	S. Sokołowski	Categories of dimaps and their dihomotopies in po-spaces and local po-spaces. Proc. Workshop on Geometry and Topology in Concurrency Theory GETCO'01 (Aalborg, Denmark), BRICS Notes Series 01-7, pp.77-97, 2001.

rozprawy doktorskie

18	T. Borzyszkowski	Systemy logiczne dla specyfikacji strukturalnych. Uniwersytet Warszawski, 2000
19	W. Pawłowski	Kontekstowe systemy logiczne w podstawach specyfikowania i konstruowania oprogramowania., IPI PAN, 2000

raporty techniczne i manuskrypty

20	M. A. Bednarczyk	Explicit Substitution into Action. A non-monotone logic for reasoning about action and change. Raport IPI PAN, nr 942, 2002
21	M. A. Bednarczyk, A. Borzyszkowski	General Morphisms of Petri nets. Prace IPI PAN 874,1999.
22	M. A. Bednarczyk, A. Borzyszkowski	Concurrent Realizations of Reactive Systems Prace IPI PAN 881,1999.
23	M. A. Bednarczyk, B. Caillaud	On Concurrency preserving distributed implementation of asynchronous automata. Manuskrypt, 2001
24	P. Pączkowski	Bisimilarity assertions for value-passing BPA-processes. Manuskrypt, 1999.
25	P. Pączkowski	Bisimilarity assertions for normed value-passing BPA-processes. Preprint 146, 2002.
26	J. Skurczyński	A characterization of Buechi tree automata. Manuskrypt, 1999.
27	S. Sokołowski	Classifying holes of arbitrary dimensions in partially ordered cubes. Kansas State University, Report 2000-1, 2000.
28	S. Sokołowski	A new notion of dimap, and the functoriality of the fundamental po-set Ω1. Manuskrypt, 2001.
29	R. Somla	Temporalna logika procesów. Manuskrypt, 1999.