Bounded Model Cheking for Interpreted Systems

• Autorzy: Penczek W. , Lomuscio A.
• 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

EN

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

PL

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

• Wydawca: Instytut Podstaw Informatyki PAN
• Czasopismo: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
• Rocznik: 2002
• Tom: Nr 946
• Strony: 1--8
• Opis fizyczny: Bibliogr. 12 poz.

Twórcy

autor

Penczek W.

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

autor

Lomuscio A.

• Department of Computer Science King’s College London London, WC2R 2LS, United Kingdom

Bibliografia

• [BCCZ99] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. of TACAS’99, volume 1579 of LNCS, pp. 193-207. Springer-Verlag, 1999.
• [CBRZ01] E. Clarke, A. Biere, R. Raimi, and Y. Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design, 19(1):7—34, 2001.
• [CGP99] E. M. Clarke, 0. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
• [EC82] E. A. Emerson and E. M. Clarke. Using branching-time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2(3):241-266, 1982.
• [Eme90] E. A. Emerson. Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, chapter Temporal and Modal Logic, pp. 995-1067. Elsevier, 1990.
• [FHMV95] R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about Knowledge. MIT Press, Cambridge, 1995.
• [MP92] Z. Manna and A. Pnueli. Temporal Logic of Reactive and Concurrent Systems. Barnes and Noble. Springer-Verlag, 1992.
• [MMZZM01] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Proc. of the 38th Design Automation Conference (DAC01), pp. 530-535, June 2001.
• [MS99] R. van der Meyden and H. Shilov. Model checking knowledge and time in systems with perfect knowledge. In Proc. of FST&TCS, volume 1738 of LNCS, pp. 432-445, 1999.
• [PWZ02] W. Penczek, B. Wozna, and A. Zbrzezny. Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae, Vol. 51(1,2), pp. 135-156, 2002.
• [vdHW02a] W. van der Hoek and M. Wooldridge. Model checking knowledge and time. In Proc. of the 9th Int. SPIN Workshop (SPIN’02), volume 2318 of LNCS, pp. 95-111. Springer-Verlag, 2002.
• [vdHW02b] W. van der Hoek and M. Wooldridge. Tractable multiagent planning for epistemic goals. In Proc. of the 1st Int. Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS’02), July 2002. to appear.