Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences

COLLEGE OF ENGINEERING

UC Berkeley

CPO Semantics of Timed Interactive Actor Networks

Xiaojun Liu and Edward A. Lee

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2007-131
November 5, 2007

http://www.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-131.pdf

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.

Author Comments: Accepted for publication in Theoretical Computer Science, 2008. See http://dx.doi.org/10.1016/j.tcs.2008.08.044.


BibTeX citation:

@techreport{Liu:EECS-2007-131,
    Author = {Liu, Xiaojun and Lee, Edward A.},
    Title = {CPO Semantics of Timed Interactive Actor Networks},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2007},
    Month = {Nov},
    URL = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-131.html},
    Number = {UCB/EECS-2007-131},
    Note = {Accepted for publication in Theoretical Computer Science, 2008. See <a href="http://dx.doi.org/10.1016/j.tcs.2008.08.044">http://dx.doi.org/10.1016/j.tcs.2008.08.044</a>.},
    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.}
}

EndNote citation:

%0 Report
%A Liu, Xiaojun
%A Lee, Edward A.
%T CPO Semantics of Timed Interactive Actor Networks
%I EECS Department, University of California, Berkeley
%D 2007
%8 November 5
%@ UCB/EECS-2007-131
%U http://www.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-131.html
%F Liu:EECS-2007-131