Switches and Jumps in Hybrid Action Systems

Mauno Rönnkö, Anders P. Ravn

    Research output: Contribution to journalJournal articleResearchpeer-review


    An action system framework is a predicate transformer based method for modelling and analysing distributed and reactive systems. The actions are statements in Dijkstra's guarded command language, and their semantics is given by predicate transformers. We extend conventional action systems with a {\em differential action} consisting of a differential equation and an evolution guard. The semantics is given by a weakest liberal precondition transformer, because it is not always desirable that differential actions terminate. It is shown that the proposed differential action has a semantics which corresponds to a discrete approximation when the discrete step size goes to zero. The extension gives action systems the power to model real-time clocks and continuous evolutions within hybrid systems. In this paper we give a standard form for such a hybrid action system. We also extend parallel composition to hybrid action systems. This does not change the original meaning of the parallel composition, and therefore ordinary action systems compose in parallel with hybrid action systems.
    Original languageEnglish
    JournalProceedings of the Estonian Academy of Sciences
    Issue number2
    Pages (from-to)106-118
    Publication statusPublished - 1998

    Cite this