Citation
Xiaojun Liu. "Semantic Foundation of the Tagged Signal Model". PhD thesis, University of California, Berkeley, December, 2005.

Abstract
The tagged signal model provides a denotational framework to study properties of various models of computation. It is a generalization of the Signals and Systems approach to system modeling and specification. Having different models of computation or aspects of them specified in the tagged signal model framework provides the following opportunities. First, one can compare certain properties of the models of computation, such as their notion of synchrony. Such comparisons highlight both the differences and the commonalities among the models of computation. Second, one can define formal relations among signals and process behaviors from different models of computation. These relations have important applications in the specification and design of heterogeneous embedded systems. Third, it facilitates the cross-fertilization of results and proof techniques among models of computation. This opportunity is exploited extensively in this dissertation. The main goal of this dissertation is to establish a semantic foundation for the tagged signal model. Both order-theoretic and metric-theoretic concepts and approaches are used. The fundamental concepts of the tagged signal model--signals, processes, and networks of processes--are formally defined. From few assumptions on the tag sets of signals, it is shown that the set of all signals with the same partially ordered tag set and the same value set is a complete partial order. This leads to a direct generalization of Kahn process networks to tagged process networks. Building on this result, the order-theoretic approach is further applied to study timed process networks, in which all signals share the same totally ordered tag set. The order structure of timed signals provides new characterizations of the common notion of causality and the discreteness of timed signals. Combining the causality and the discreteness conditions is proved to guarantee the non-Zenoness of timed process networks. The metric structure of tagged signals is studied from the very specific--the Cantor metric and its properties. A generalized ultrametric on tagged signals is proposed, which provides a framework for defining more specialized metrics, such as the extension of the Cantor metric to super-dense time. The tagged signal model provides not only a framework for studying the denotational semantics of models of computation, but also useful constructs for studying implementations or simulations of tagged processes. This is demonstrated by deriving certain properties of two discrete event simulation strategies from the behavioral specifications of discrete event processes. A formulation of tagged processes as labeled transition systems provides yet another framework for comparing different implementation or simulation strategies for tagged processes. This formulation lays the foundation to future research in polymorphic implementations of tagged processes.

Electronic downloads

• http://ptolemy.eecs.berkeley.edu/publications/papers/05/Xiaojun_Thesis/index.htm

• HTML

  Xiaojun Liu. <a
  href="http://chess.eecs.berkeley.edu/pubs/55.html"
  ><i>Semantic Foundation of the Tagged Signal
  Model</i></a>, PhD thesis,  University of
  California, Berkeley, December, 2005.

• Plain text

  Xiaojun Liu. "Semantic Foundation of the Tagged Signal
  Model". PhD thesis,  University of California,
  Berkeley, December, 2005.

• BibTeX

  @phdthesis{Liu05_SemanticFoundationOfTaggedSignalModel,
      author = {Xiaojun Liu},
      title = {Semantic Foundation of the Tagged Signal Model},
      school = {University of California, Berkeley},
      month = {December},
      year = {2005},
      abstract = {The tagged signal model provides a denotational
                framework to study properties of various models of
                computation. It is a generalization of the Signals
                and Systems approach to system modeling and
                specification. Having different models of
                computation or aspects of them specified in the
                tagged signal model framework provides the
                following opportunities. First, one can compare
                certain properties of the models of computation,
                such as their notion of synchrony. Such
                comparisons highlight both the differences and the
                commonalities among the models of computation.
                Second, one can define formal relations among
                signals and process behaviors from different
                models of computation. These relations have
                important applications in the specification and
                design of heterogeneous embedded systems. Third,
                it facilitates the cross-fertilization of results
                and proof techniques among models of computation.
                This opportunity is exploited extensively in this
                dissertation. The main goal of this dissertation
                is to establish a semantic foundation for the
                tagged signal model. Both order-theoretic and
                metric-theoretic concepts and approaches are used.
                The fundamental concepts of the tagged signal
                model--signals, processes, and networks of
                processes--are formally defined. From few
                assumptions on the tag sets of signals, it is
                shown that the set of all signals with the same
                partially ordered tag set and the same value set
                is a complete partial order. This leads to a
                direct generalization of Kahn process networks to
                tagged process networks. Building on this result,
                the order-theoretic approach is further applied to
                study timed process networks, in which all signals
                share the same totally ordered tag set. The order
                structure of timed signals provides new
                characterizations of the common notion of
                causality and the discreteness of timed signals.
                Combining the causality and the discreteness
                conditions is proved to guarantee the non-Zenoness
                of timed process networks. The metric structure of
                tagged signals is studied from the very
                specific--the Cantor metric and its properties. A
                generalized ultrametric on tagged signals is
                proposed, which provides a framework for defining
                more specialized metrics, such as the extension of
                the Cantor metric to super-dense time. The tagged
                signal model provides not only a framework for
                studying the denotational semantics of models of
                computation, but also useful constructs for
                studying implementations or simulations of tagged
                processes. This is demonstrated by deriving
                certain properties of two discrete event
                simulation strategies from the behavioral
                specifications of discrete event processes. A
                formulation of tagged processes as labeled
                transition systems provides yet another framework
                for comparing different implementation or
                simulation strategies for tagged processes. This
                formulation lays the foundation to future research
                in polymorphic implementations of tagged
                processes. },
      URL = {http://chess.eecs.berkeley.edu/pubs/55.html}
  }
  

Posted by Mary Stewart on 4 May 2006.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.