- Tytuł:
-
Model Checking Temporal Properties of Reaction Systems
Weryfikacja temporalnych własności systemów reakcyjnych - Autorzy:
-
Męski, A.
Penczek, W.
Rozenberg, G. - Powiązania:
- https://bibliotekanauki.pl/articles/182724.pdf
- Data publikacji:
- 2014
- Wydawca:
- Polska Akademia Nauk. Instytut Podstaw Informatyki PAN
- Tematy:
-
reaction systems
model checking
temporal logic
systemy reakcyjne
weryfikacja modelowa
logika temporalna - Opis:
-
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.
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. - Źródło:
-
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk; 2014, 1028; 1-28
0138-0648 - Pojawia się w:
- Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
- Dostawca treści:
- Biblioteka Nauki
Artykuł