| Alternating systems are models of computer programs whose behavior is governed by the actions of multiple agents with, potentially, different goals. Examples include control systems, resource schedulers, security protocols, auctions and election mechanisms. Proving properties about such systems has emerged as an important new area of study in formal verification, with the development of logical frameworks such as the alternating temporal logic ATL*.; Techniques for model checking ATL* over finite-state systems have been well studied, but many important systems are infinite-state and thus their verification requires, either explicitly or implicitly, some form of deductive reasoning.; The first part of this thesis presents a theoretical framework for the alternating analysis of infinite-state systems. It describes models of computation, of various degrees of generality, and alternating-time logics such as ATL* and its variations. It then develops a proof system that allows to prove arbitrary ATL* properties over these infinite-state models. The proof system is shown to be complete relatively to validities in the weakest possible assertion language.; The second part focuses on applications of the theory. It starts by developing several derived and specialized proof rules and shows how to engineer verification diagrams to concisely and intuitively represent applications of the rules. It then uses proof rules and diagrams on security protocols, including a new formal proof of fairness of a multi-party contract signing protocol where the model of the protocol and of the properties contains both game-theoretic and infinite-state (parameterized) aspects. The final contribution is to apply the previous ideas to a control problem on linear discrete-time controlled systems: starting with some previously introduced proof rules, it applies abstract interpretation techniques to derive an algorithmic solution to the control synthesis problem. |
