*banner
 

On the Verification of Timed Discrete-Event Models
Christos Stergiou, Stavros Tripakis, Eleftherios Matsikoudis, Edward A. Lee

Citation
Christos Stergiou, Stavros Tripakis, Eleftherios Matsikoudis, Edward A. Lee. "On the Verification of Timed Discrete-Event Models". 11th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), 29, August, 2013; Buenos Aires, Argentina.

Abstract
Timed discrete-event (DE) is an actor-oriented formalism for modeling timed systems. A DE model is a network of actors consuming/producing timed events from/to a set of input/output channels. In this paper we study a basic DE model, called deterministic DE (DDE), where actors are simple constant-delay components, and two extensions of DDE: NDE, where actors are non-deterministic delays, and DETA, where actors are either deterministic delays or timed automata. We investigate verification questions on DE models and examine expressiveness relationships between the DE models and timed automata.

Electronic downloads

Citation formats  
  • HTML
    Christos Stergiou, Stavros Tripakis, Eleftherios
    Matsikoudis, Edward A. Lee. <a
    href="http://chess.eecs.berkeley.edu/pubs/992.html"
    >On the Verification of Timed Discrete-Event
    Models</a>, 11th International Conference on  Formal
    Modeling and Analysis of Timed Systems (FORMATS), 29,
    August, 2013; Buenos Aires, Argentina.
  • Plain text
    Christos Stergiou, Stavros Tripakis, Eleftherios
    Matsikoudis, Edward A. Lee. "On the Verification of
    Timed Discrete-Event Models". 11th International
    Conference on  Formal Modeling and Analysis of Timed Systems
    (FORMATS), 29, August, 2013; Buenos Aires, Argentina.
  • BibTeX
    @inproceedings{StergiouTripakisMatsikoudisLee13_OnVerificationOfTimedDiscreteEventModels,
        author = {Christos Stergiou and Stavros Tripakis and
                  Eleftherios Matsikoudis and Edward A. Lee},
        title = {On the Verification of Timed Discrete-Event Models},
        booktitle = {11th International Conference on  Formal Modeling
                  and Analysis of Timed Systems (FORMATS)},
        day = {29},
        month = {August},
        year = {2013},
        note = {Buenos Aires, Argentina},
        abstract = {Timed discrete-event (DE) is an actor-oriented
                  formalism for modeling timed systems. A DE model
                  is a network of actors consuming/producing timed
                  events from/to a set of input/output channels. In
                  this paper we study a basic DE model, called
                  deterministic DE (DDE), where actors are simple
                  constant-delay components, and two extensions of
                  DDE: NDE, where actors are non-deterministic
                  delays, and DETA, where actors are either
                  deterministic delays or timed automata. We
                  investigate verification questions on DE models
                  and examine expressiveness relationships between
                  the DE models and timed automata. },
        URL = {http://chess.eecs.berkeley.edu/pubs/992.html}
    }
    

Posted by Christos Stergiou on 3 Jun 2013.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.

©2002-2018 Chess