Title: HIOA - A Specification Language for Hybrid I/O Automata

Speaker: Sayan Mitra

Abstract

This paper introduces the HIOA language ~---~ a specification language for hybrid systems based on the Hybrid Input/Output Automaton model of Lynch, Segala, and Vaandrager. In HIOA the discrete transitions of an automaton's state are specified in the precondition-effect style. The continuous evolution is specified by a set of activities which partition the state space of the automaton into (possibly overlapping) regions and define state models that govern the state evolution within each such region. The language includes features for specifying composite automata and the composition transformations for actions and activities have been defined. The HIOA language provides a consistent and natural means to specify hybrid I/O automata and is amenable to syntactic and semantic checking. A prototype front end tool for the language has been implemented as a first step towards building a framework for automated verification of hybrid systems using deductive techniques.