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 de-cidable 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.
展开▼
