SwePub - sökning: L773:9781615673346

Numrering	Referens	Omslagsbild	Hitta
1.	Cohen, M., et al. (författare) Abstraction in Model Checking Multi-agent Systems 2009 Ingår i: AAMAS '09 Proceedings of The 8th International Conference on Autonomous Agents and Multiagent Systems. - : Association for Computing Machinery (ACM). - 9781615673346 ; , s. 710-717 Konferensbidrag (refereegranskat)abstract We present an abstraction technique for multi-agent, systems preserving temporal-epistcrnic specifications. We abstract a multi-agent system, defined in the interpreted systems framework, by collapsing the local states and actions of each agent in the system. We show that the resulting abstract system simulates the concrete system, from which we obtain a preservation theorem: If a temporal-epistemic specification holds on the abstract system, the specification also holds on the concrete one. In principle this permits us to model check the abstract system rather than the concrete one, thereby saving time and space in the verification step. We illustrate the abstraction technique with two examples. The first example, a card game, illustrates the potential savings in the cost of model checking a typical MAS scenario. In the second example, the abstraction technique is used to verify a communication protocol with an arbitrarily large data domain.

Cohen, M., et al. (författare)
Abstraction in Model Checking Multi-agent Systems
2009
Ingår i: AAMAS '09 Proceedings of The 8th International Conference on Autonomous Agents and Multiagent Systems. - : Association for Computing Machinery (ACM). - 9781615673346 ; , s. 710-717
Konferensbidrag (refereegranskat)abstract
- We present an abstraction technique for multi-agent, systems preserving temporal-epistcrnic specifications. We abstract a multi-agent system, defined in the interpreted systems framework, by collapsing the local states and actions of each agent in the system. We show that the resulting abstract system simulates the concrete system, from which we obtain a preservation theorem: If a temporal-epistemic specification holds on the abstract system, the specification also holds on the concrete one. In principle this permits us to model check the abstract system rather than the concrete one, thereby saving time and space in the verification step. We illustrate the abstraction technique with two examples. The first example, a card game, illustrates the potential savings in the cost of model checking a typical MAS scenario. In the second example, the abstraction technique is used to verify a communication protocol with an arbitrarily large data domain.

Träfflista för sökning "L773:9781615673346 "