|
|
|
篇目详细内容 |
|
【篇名】 |
Abstraction for model checking multi-agent systems |
|
【刊名】 |
Frontiers of Computer Science in China |
|
【刊名缩写】 |
Front. Comput. Sci. China |
|
【ISSN】 |
1673-7350 |
|
【EISSN】 |
1673-7466 |
|
【DOI】 |
10.1007/s11704-010-0358-y |
|
【出版社】 |
Higher Education Press and Springer-Verlag Berlin
Heidelberg |
|
【出版年】 |
2011 |
|
【卷期】 |
5
卷1期 |
|
【页码】 |
14-25
页,共
12
页 |
|
【作者】 |
Conghua ZHOU;
Bo SUN;
Zhifeng LIU;
|
|
【关键词】 |
model checking; abstraction; refinement; epistemic temporal logic |
【摘要】 |
|
Model checking multi-agent systems (MAS) always suffers from the state explosion problem. In this paper we focus on an abstraction technique which is one of the major methods for overcoming this problem. For a multi-agent system, we present a novel abstraction procedure which reduces the state space by collapsing the global states in the system. The abstraction is automatically computed according to the property to be verified. The resulting abstract system simulates the concrete system, while the universal temporal epistemic properties are preserved. Our abstraction is an over-approximation. If some universal temporal epistemic property is not satisfied, then we need to identify spurious counterexamples. We further show how to reduce complex counterexamples to simple structures, i.e., paths and loops, such that the counterexamples can be checked and the abstraction can be refined efficiently. Finally, we illustrate the abstraction technique with a card game. |
|
