## Proving ATL* Properties of Infinite-State Systems

*
Matteo Slanina,
Henny B. Sipma,
Zohar Manna,
*
Alternating temporal logic (ATL*) was introduced to prove
properties of multi-agent systems in which the agents have different
objectives and may collaborate to achieve them. Examples include
(distributed) controlled systems, security protocols, and
contract-signing protocols. Proving ATL* properties over
finite-state systems was shown decidable by Alur et al., and a model
checker for the sublanguage ATL implemented in MOCHA.

In this paper we present a sound and complete proof system for
proving ATL* properties over infinite-state systems. The proof
system reduces proofs of ATL* properties over systems to
first-order verification conditions in the underlying assertion
language. The verification conditions make use of predicate
transformers that depend on the system structure, so that proofs
over systems with a simpler structure, e.g., turn-based systems,
directly result in simpler verification conditions. We illustrate
the use of the proof system on a small example.

To appear in *ICTAC'06*

© Henny Sipma /
sipma@cs.stanford.edu
Last modified: Thu Jan 12 14:40:50 PDT 2004