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 2013), 29, August, 2013; Accepted.

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. This paper studies 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. This work investigates verification questions on DE models and examines expressiveness relationships between the DE models and timed automata.

Electronic downloads

Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.

Citation formats

• HTML

  Christos Stergiou, Stavros Tripakis, Eleftherios
  Matsikoudis, Edward A. Lee. <a
  href="http://www.terraswarm.org/pubs/71.html"
  >On the Verification of Timed Discrete-Event
  Models</a>, 11th International Conference on Formal
  Modeling and Analysis of Timed Systems (FORMATS 2013), 29,
  August, 2013; Accepted.

• 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 2013), 29, August, 2013; Accepted.

• 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 2013)},
      day = {29},
      month = {August},
      year = {2013},
      note = {Accepted.},
      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.
                This paper studies 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. This work
                investigates verification questions on DE models
                and examines expressiveness relationships between
                the DE models and timed automata.},
      URL = {http://terraswarm.org/pubs/71.html}
  }
  

Posted by Christopher Brooks on 22 May 2013.
Groups: tools