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

• model_checking.pdf · application/pdf · 347 kbytes
• http://dl.acm.org/citation.cfm?id=2529517. (In Proceedings of the 11th international conference on Formal Modeling and Analysis of Timed Systems , pp 213-227.)

• 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.