Model checking by abstraction for proving liveness properties of hybrid dynamical systems

Eva Navarro Lopez, Renate Schmidt (Editor)

    Research output: Chapter in Book/Conference proceedingConference contributionpeer-review

    Abstract

    We consider a method for model checking certain properties of continuous dynamical systems, by adapting an abstraction method previously proposed so that it will work with the timed automata model checker UPPAAL. We also describe our ongoing work to extend this method to verify liveness (reachability) properties of hybrid dynamical systems
    Original languageEnglish
    Title of host publicationAutomated Reasoning Workshop, ARW 2012
    EditorsRenate Schmidt
    Place of PublicationUK
    Pages29-30
    Number of pages2
    Publication statusPublished - Apr 2012
    EventAutomated Reasoning Workshop, ARW 2012 - Manchester, UK
    Duration: 2 Apr 20124 Apr 2012

    Conference

    ConferenceAutomated Reasoning Workshop, ARW 2012
    CityManchester, UK
    Period2/04/124/04/12

    Keywords

    • Hybrid dynamical systems
    • Liveness
    • Formal verification

    Fingerprint

    Dive into the research topics of 'Model checking by abstraction for proving liveness properties of hybrid dynamical systems'. Together they form a unique fingerprint.

    Cite this