Model Checking for Branching-Time Temporal Logics ------------------------------------------------- The thesis considers formal verification of computerized systems. In formal verification, we verify that a system meets a desired behavior by checking that a mathematical model of the system satisfies a formal specification that describes the behavior. The special method of formal verification that we consider is branching-time model checking. In this method, formal verification means determining whether a Kripke structure satisfies a branching temporal logic formula. Translating linear temporal logic formulas to automata on infinite words has proven to be an effective approach for implementing linear-time model-checking and for obtaining many extensions and improvements to this verification method. On the other hand, for branching temporal logics, automata-theoretic techniques have long been thought to introduce an exponential penalty, making them essentially useless for model-checking. Efforts to employ the theory of automata on infinite trees for the benefit of branching-time model checking started at the 80's, but with no success. In this thesis we show that alternating tree automata are the key to a comprehensive automata-theoretic framework for branching temporal logics. Using the automata-theoretic framework we are able to improved the space complexity of branching-time model-checking. In particular, we show that alternating tree automata provide a PSPACE procedure for CTL* model checking of concurrent programs, and provide an explanation why this bound can not be achieved for Mu-calculus model checking and even for its alternation-free fragment. We show that the efficient bounds hold also for fair model-checking, where a system is checked to be correct under certain fairness constraints, and for modular model checking, where a system is checked to be correct by checking its components. Improving branching-time model-checking complexity is only one way to make this method practical. Naturally, there is a trade-off between the expressive power of a temporal logic and the complexity of its model-checking problem: the more a logic is expressive, the higher its model-checking complexity is. A wise model checker should enable the maximal expressive power and ease of use within the complexity limits enforced by the user. In the second part of the thesis, we consider three different ways of extending conventional branching temporal logics: more liberal syntax, existential quantification over atomic propositions, and temporal modalities that refer to the past. Each of the three ways makes branching temporal logic a more convenient specification language. We examine their both theoretical and practical~aspects.