Repositorium | Zeitschrift | Band | Zeitschriftartikel
(2004) Synthese 142 (2).
A sat-based approach to unbounded model checking for alternating-time temporal epistemic logic
M. Kacprzak, W. Penczek
pp. 203-227
This paper deals with the problem of verification of game-like structures by means of symbolic model checking. Alternating-time Temporal Epistemic Logic (ATEL) is used for expressing properties of multi-agent systems represented by alternating epistemic temporal systems as well as concurrent epistemic game structures. Unbounded model checking (a SAT based technique) is applied for the first time to verification of ATEL. An example is given to show an application of the technique.
Publikationsangaben
DOI: 10.1007/s11229-004-2446-8
Quellenangabe:
Kacprzak, M. , Penczek, W. (2004). A sat-based approach to unbounded model checking for alternating-time temporal epistemic logic. Synthese 142 (2), pp. 203-227.
Dieses Dokument ist derzeit leider nicht zum Runterladen verfügbar.