A Sat-Based Approach to Unbounded Model Checking for Alternating-Time Temporal Epistemic Logic期刊界 All Journals 搜尽天下杂志传播学术成果专业期刊搜索期刊信息化学术搜索

A Sat-Based Approach to Unbounded Model Checking for Alternating-Time Temporal Epistemic Logic

Authors:	M.?Kacprzak author-information" > author-information__contact u-icon-before" > mailto:mdkacprzak@wp.pl" title=" mdkacprzak@wp.pl" itemprop=" email" data-track=" click" data-track-action=" Email author" data-track-label=" " >Email author,W.?Penczek

Affiliation:	(1) Institute of Mathematics and Physics, Bialystok University of Technology, ul. Wiejska 45A, Bialystok, 15-351, Poland;(2) PAS, Institute of Computer Science, ul. Ordona 21, Warsaw, 01-237, Poland;(3) Institute of Informatics, Podlasie Academy, Siedlce, Poland

Abstract:	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.

Keywords:
本文献已被 SpringerLink 等数据库收录！