Verification of strategic ability under imperfect information is challenging, with complexity ranging from NP-complete to undecidable. This is partly because traditional fixpoint equivalences fail in this setting. Some years ago, an interesting idea of fixpoint approximation was proposed for model checking of ATL_ir, i.e., the logic of strategic ability for agents with imperfect information and imperfect recall. In this paper, we propose a new variant of the approximation, that uses the agent's local model rather than the global model of the system. We prove correctness of the construction, and demonstrate its effectiveness through experimental results on scalable models of voting.

Formal verification of intelligent agents is often computationally infeasible due to state-space explosion. We present a tool for reducing the impact of the explosion by means of state abstraction that is (a) easy to use and understand by non-experts, and (b) agent-based in the sense that it operates on a modular representation of the system, rather than on its huge explicit state model.

Model checking of multi-agent systems (MAS) is known to be hard, both theoretically and in practice. A smart abstraction of the state space may significantly reduce the model,and facilitate the verification. In this paper, we propose and study an intuitive agent-based abstraction scheme, based on the removal of variables in the representation of a MAS. This allows to achieve a desired reduction of a state space without generating the global model of the system. Moreover, the process is easy to understand and control even for domain experts with little knowledge of computer science. We formally prove the correctness of the approach, and evaluate the gains experimentally on a family of a postal voting models.

The effective method (based on Theorem 5.3) of classifying tubular algebras by the Cartan matrices of tilting sheaves over weighted projective lines with all indecomposable direct summands in some finite “fundamental domain” , by the reduction to the two elementary problems of discrete mathematics having algorithmic solutions is presented in details (see Problem A and B). The software package CART_TUB being an implementation of this method yields the precise classification of all up to isomorphism tubular algebras of a fixed tubular type p, by creating the complete lists of their Cartan matrices, and furnish their tilting realizations. In particular, the number of isomorphism classes of tubular algebras of the type p is determined (Theorem 2.3).