@CONFERENCE\{IMM2001-01011,
    author       = "M. Fr{\"{a}}nzle",
    title        = "What will be eventually true of polymomial hybrid automata",
    year         = "2001",
    keywords     = "Hybrid systems; State recurrence; Progress properties; Decidability; Verification procedures",
    pages        = "340-359",
    booktitle    = "Theoretical Aspects of Computer Software, {TACS} 2001",
    volume       = "2215",
    series       = "Lecture Notes in Computer Science",
    editor       = "Naoki Kobayashi and Benjamin C. Pierce",
    publisher    = "Springer-Verlag",
    organization = "",
    address      = "",
    url          = "http://www.imm.dtu.dk/~mf/HA-MC-progress.ps.gz",
    abstract     = "Hybrid automata have been introduced in both control engineering and
  computer science as a formal model for the dynamics of hybrid
  discrete-continuous systems. While computability issues
  concerning safety properties have been extensively studied, 
  liveness properties have remained largely uninvestigated.
  In this article, we investigate decidability  of state recurrence and
  of progress properties. 
  
  First, we show that state recurrence and progress are in general
  undecidable for polynomial hybrid automata. Then, we demonstrate
  that they are closely related for hybrid automata subject to a
  simple model of noise, even though these automata are infinite-state
  systems. Based on this, we augment a semi-decision procedure for
  recurrence with a semi-decision method for length-boundedness of
  paths in such a way that we obtain an automatic verification method
  for progress properties of linear and polynomial hybrid automata
  that may only fail on pathological, practically uninteresting cases.
  These cases are such that satisfaction of the desired progress
  property crucially depends on the complete absence of noise, a
  situation unlikely to occur in real hybrid systems."
}