What will be eventually true of polymomial hybrid automata

Martin Fränzle, Naoki Kobayashi et al. (Editor)

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    12 Downloads (Pure)

    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.
    Original languageEnglish
    Title of host publicationTheoretical Aspects of Computer Software, TACS 2001
    PublisherSpringer
    Publication date2001
    Pages340-359
    Publication statusPublished - 2001

    Cite this