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 /
Last modified: Thu Jan 12 14:40:50 PDT 2004