Verification of reactive systems and decision problems in temporal logic  Posted on:20020111  Degree:Ph.D  Type:Thesis  University:University of Pennsylvania  Candidate:La Torre, Salvatore  Full Text:PDF  GTID:2468390011498603  Subject:Computer Science  Abstract/Summary:   We study decision problems related to system analysis in automata theory and temporal logic.; First, we consider an optimalreachability problem for timed automata with respect to a general linearcost function (weighted timed automata). Our solution consists of reducing this problem to a (parametric) shortestpath 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 stateset 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 origindependent 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 twoplayer games on finite graphs with winning conditions specified by linear temporal logic (LTL) formulas, is known to be 2EXPTIMEcomplete. 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 TCTLformulas 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 TCTLformulas then the finite satisfiability is decidable. This proof is obtained by a reduction to the emptiness problem of timed tree automata.  Keywords/Search Tags:  Problem, Automata, Logic, Temporal, Satisfiability, Timed   Related items 
 
