Bounded Model Cheking for Interpreted Systems

• Autorzy: Penczek, W.
• Języki publikacji: EN

Abstrakty

EN

We present an extension of a bounded model checking algorithm to deal with temporal epistemic formulas. We use the algorithm to solve a variant of the bit transmission problem

PL

W pracy przedstawiamy rozszerzenie algorytmu ograniczonej weryfikacji modelowej do temporalnych formuł epistemicznych. Algorytm jest zastosowany do weryfikacji pewnego wariantu problemu transmisji bitów.

Słowa kluczowe

PL

logiki temporalne; interpretowane systemy; logika wiedzy; ograniczona weryfikacja modelowa; translacja do SAT; weryfikacja systemów

EN

interpreted systems; temporal logics; logic for knowledge; bounded model checking; translation to SAT; system verification

• Czasopismo: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
• Rocznik: 2002
• Tom: Nr 946
• Strony: 1-8

Twórcy

autor

Penczek, W.

• Institute of Computer Science, PAS, Ordona 21, 01-237 Warsaw, Poland,