Verification of reactive systems and decision problems in temporal logic

We study decision problems related to system analysis in automata theory and temporal logic. First, we consider an optimal-reachability problem for timed automata with respect to a general linear-cost function (weighted timed automata). Our solution consists of reducing this problem to a (parametric) shortest-path problem for directed graphs. The corresponding algorithm takes doubly exponential time when a general source zone of the state space is considered, and exponential time in the case of a single source state. Then, we study if we can generalize the syntax of linear hybrid automata for describing flows without sacrificing the polyhedral property: given a state-set described by a polyhedron, the set of states that can be reached, as time elapses, is also a polyhedron. We extend linear hybrid automata by allowing flows described by origin-dependent rate polytopes, in which the allowed rates depend, not only on the current control mode, but also on the specific state at which the mode was entered. Deciding infinite two-player games on finite graphs with winning conditions specified by linear temporal logic (LTL) formulas, is known to be 2EXPTIME-complete. We identify LTL fragments of lower complexity, and solve the corresponding games by reducing them to Büchi games. The key step of this reduction consists of translating formulas from these fragments into Büchi deterministic generators. We prove our constructions to be optimal with respect to both the size and the longest distance. Then we give an O(dlog n)-space procedure to solve Büchi games with n vertices and longest distance d. The last contribution of this thesis concerns the satisfiability of formulas in the logic TCTL. TCTL semantics is defined on dense trees and the satisfiability of TCTL-formulas is undecidable even if we restrict the semantics to dense trees obtained from timed graphs (finite satisfiability). There are two possible causes of such undecidability: the denseness of the underlying structure and the equality in the timing constraints. We prove that if the equality is not allowed in the timing constraints of TCTL-formulas then the finite satisfiability is decidable. This proof is obtained by a reduction to the emptiness problem of timed tree automata