Model Checking Temporal Properties of Reaction Systems

• Autorzy: Męski A. , Penczek W. , Rozenberg G.

Warianty tytułu

PL

Weryfikacja temporalnych własności systemów reakcyjnych

• Języki publikacji: EN

Abstrakty

EN

This paper defines a temporal logic for reaction systems (RSTL). The logic is interpreted over the models for the context restricted reaction systems that generalize standard reaction systems by controlling context sequences. Moreover, a translation from the context restricted reaction systems into boolean functions is defined in order to be used for a symbolic model checking for RSTL over these systems. Finally, model checking for RSTL is proved to be PSPACE-complete.

PL

Praca wprowadza logikę temporalną dla systemów reakcyjnych (RSTL), która jest interpretowana w modelach dla systemów reakcyjnych z ograniczeniami kontekstów. Systemy te uogólniają standardowe systemy reakcyjne przez wprowadzenie ograniczeń kontrolujących dopuszczalne konteksty. Ponadto, przedstawiono translację z systemów reakcyjnych z ograniczeniami kontekstów do formuł boolowskich, która umożliwia symboliczną weryfikację modelową dla tych systemów oraz RSTL. Wykazano również, że problem weryfikacji modelowej dla RSTL jest problemem PSPACE-zupełnym.

Słowa kluczowe

EN

reaction systems; model checking; temporal logic

PL

systemy reakcyjne; weryfikacja modelowa; logika temporalna

• Wydawca: Instytut Podstaw Informatyki PAN
• Czasopismo: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
• Rocznik: 2014
• Tom: Nr 1028
• Strony: 1--28
• Opis fizyczny: Bibliogr. 11 poz., rys.

Twórcy

autor

Męski A.

• Instytut Podstaw Informatyki PAN ul. Jana Kazimierza 5, 01-248 Warszawa, Polska

autor

Penczek W.

• Instytut Podstaw Informatyki PAN ul. Jana Kazimierza 5, 01-248 Warszawa, Polska

autor

Rozenberg G.

• LIACS, Leiden University P.O. Box 9512, 2300 RA, The Netherlands

Bibliografia

• R. Alur, C. Courcoubetis, and D. Diii. Model checking in dense real-time. Information and Computation, 104(1) :2-34, 1993.
• R. Brijder, A. Ehrenfeucht, M. G. Main, and G. Rozenberg. A tour of reaction systems. Int. J. Found. Comput. Sci., 22(7):1499-1517, 2011.
• R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers, 35(8):677-691, 1986.
• E. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. ACM Transactions on Programming Languages and Systems, 8(2):244-263, 1986.
• E.Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
• A. Ehrenfeucht and G. Rozenberg. Reaction systems. Fundamenta Informaticae, 75(1-4):263-280, 2007.
• A. Ehrenfeucht, J. Kleijn, M. Koutny, and G. Rozenberg. Reaction systems: A natural computing approach to the functioning of living cells. A Computable Universe, Understanding and Exploring Nature as Computation (H. Zenil, ed.), pages 189-208, 2012.
• F.Laroussinie. N. Markey, and P. Schnoebelen. Model checking timed automata with one or two clocks. In CONCUR, pages 387-401, 2004.
• K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers. 1993.
• C. Pecheur and F. Raimondi. Symbolic model checking of logics with actions. In MoChArt, pages 113-128. 2006.
• L. J. Stockmeyer and A. R. Meyer. Word problems requiring exponential time: Preliminary report. In STOC. pages 1-9. 1973.