*banner
 

CPO semantics of timed interactive actor Networks
Xiaojun Liu, Edward A. Lee

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

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

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