Citation
Xiaojun Liu, Edward A. Lee. "CPO semantics of timed interactive actor Networks". Theoretical Computer Science, 409(1):110-125, 2008.

Abstract
We give a denotational framework for composing interactive components into closed or open systems and show how to adapt classical domain-theoretic approaches to open systems and to timed systems. For timed systems, prior approaches are based on temporal logics, automata theory, or metric-spaces. In this paper, we base the semantics on a CPO with a prefix order, as has been done previously for untimed systems. We show that existence and uniqueness of behaviors are ensured by continuity with respect to this prefix order. Existence and uniqueness of behaviors, however, does not imply that a composition of components yields a useful behavior. The unique behavior could be empty or smaller than expected. We define liveness and show that appropriately defined causality conditions ensure liveness and freedom from Zeno conditions. In our formulation, causality does not require a metric and can embrace a wide variety of models of time,

Electronic downloads

• http://dx.doi.org/10.1016/j.tcs.2008.08.044. (The original publication at http://www.sciencedirect.com)
• http://www.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-67.html. (EECS Memo Version)

• HTML

  Xiaojun Liu, Edward A. Lee. <a
  href="http://chess.eecs.berkeley.edu/pubs/490.html"
  >CPO semantics of timed interactive actor
  Networks</a>, <i>Theoretical Computer
  Science</i>, 409(1):110-125,  2008.

• Plain text

  Xiaojun Liu, Edward A. Lee. "CPO semantics of timed
  interactive actor Networks". <i>Theoretical
  Computer Science</i>, 409(1):110-125,  2008.

• BibTeX

  @article{LiuLee08_CPOSemanticsOfTimedInteractiveActorNetworks,
      author = {Xiaojun Liu and Edward A. Lee},
      title = {CPO semantics of timed interactive actor Networks},
      journal = {Theoretical Computer Science},
      volume = {409},
      number = {1},
      pages = {110-125},
      year = {2008},
      abstract = {We give a denotational framework for composing
                interactive components into closed or open systems
                and show how to adapt classical domain-theoretic
                approaches to open systems and to timed systems.
                For timed systems, prior approaches are based on
                temporal logics, automata theory, or
                metric-spaces. In this paper, we base the
                semantics on a CPO with a prefix order, as has
                been done previously for untimed systems. We show
                that existence and uniqueness of behaviors are
                ensured by continuity with respect to this prefix
                order. Existence and uniqueness of behaviors,
                however, does not imply that a composition of
                components yields a useful behavior. The unique
                behavior could be empty or smaller than expected.
                We define liveness and show that appropriately
                defined causality conditions ensure liveness and
                freedom from Zeno conditions. In our formulation,
                causality does not require a metric and can
                embrace a wide variety of models of time,},
      URL = {http://chess.eecs.berkeley.edu/pubs/490.html}
  }
  

Posted by Mary Stewart on 2 Oct 2008.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.