Weryfikacja temporalnych własności algorytmów niedeterministycznych

• Autorzy: Kacprzak M.

Warianty tytułu

EN

Verification of temporal properties of nondeterministic algorithms

• Języki publikacji: PL

Abstrakty

PL

W pracy zaprezentowany został system dowodowy dla logiki temporalnej czasu rozgałęzionego, nazwany Temporalną Logiką Procesów. Pozwala on na badanie statycznych i dynamicznych własności programów wyrażonych jako formuły temporalne rozważanego języka. Udowodniono mocne twierdzenie o pełności dla przedstawionego systemu formalnego.

EN

This paper provides one of the versions of prepositional, branching time temporal logic, called Process Temporal Logic. It allows to verify static and dynamic properties of programs, which are expressed as temporal formulas. PTL system is presented with the infinitary axiomatic system and the proof of the completeness theorem. The majority of temporal logics treats a program as a separate object and not as a language element. The system shown in this article is different. Program is a part of expression which describes its quality just as in dynamic and algorithmic logic.

Słowa kluczowe

PL

algorytmy niedeterministyczne; własności temporalne; Temporalna Logika Procesów

EN

nondeterministic algorithms; temporal properties; Process Temporal Logic

• Wydawca: Oficyna Wydawnicza Politechniki Białostockiej
• Czasopismo: Zeszyty Naukowe Politechniki Białostockiej. Matematyka, Fizyka, Chemia
• Rocznik: 2001
• Tom: Z. 20
• Strony: 37--53
• Opis fizyczny: Bibliogr. 10 poz., wykr.

Twórcy

autor

Kacprzak M.

• Politechnika Białostocka, Katedra Matematyki, ul. Wiejska 45 A, 15-351 Białystok

Bibliografia

• [1] L. Bolec, K. Dziewicki, P. Rychlik, A. Szalas, Wnioskowanie w logikach nieklasycznych. Podstawy teoretyczne, Akademicka Oficyna Wydawnicza PLJ, Warszawa, 1995
• [2] E. A. Emerson, J. Y. Halpern, Decision Procedures and Expressiveness in the Temporal Logic of Branching Time, Journal of Computer and System Sciences 30, 1985, 1-24 !
• [3] L. Fix, O. Grumberg, Verification of Temporal Properties, Journal of Logic and Computation, vol. 6 No. 3,1996, 343-361
• [4] D. Harel, Dynamic Logic, Handbookof Philosophical Logic, vol. 2, D. Reidel Pub. Co., 1984, 497-607
• [5] F. Kröger, A Generalized Nexttime Operator in Temporal Logic, Journal of Computer and System Sciences 29, 1984, 80-98 i
• [6] G. Mirkowska, A. Salwicki, Algorithmic Logic, PWN, Polish Scientific Publishers, Warszawa, 1987 |
• [7] W. Penczek, A Temporal Logic for Event Structures, Fundamenta Informaticae XI, 1988, 291-326
• [8] W. Penczek, Axiomatizations of Temporal Logic on Trace Systems, Fundamenta Informaticae 25, 1996, 183-200
• [9] H. Rasiowa, R. Sikorski, The Mathematics of Metamathematies, PWN, Warszawa, 1970
• 10] A. Szalas, U. Petermann, On Temporal Logic for Distributed Systems and Its Application to Processes Communicating by Interrupts, Fundamenta Informaticae 12, 1989, 191-204