Citation
Adam Cataldo, Edward A. Lee, Xiaojun Liu, Eleftherios Matsikoudis, Haiyang Zheng. "A Constructive Fixed-Point Theorem and the Feedback Semantics of Timed Systems". Workshop on Discrete Event Systems, July, 2006.

Abstract
Deterministic timed systems can be modeled as fixed point problems. In particular, any connected network of timed systems can be modeled as a single system with feedback, and the system behavior is the fixed point of the corresponding system equation, when it exists. For delta-causal systems, we can use the Cantor metric to measure the distance between signals and the Banach fixed-point theorem to prove the existence and uniqueness of a system behavior. Moreover, the Banach fixed-point theorem is constructive: it provides a method to construct the unique fixed point through iteration. In this paper, we extend this result to systems modeled with the superdense model of time used in hybrid systems. We call the systems we consider eventually delta-causal, a strict generalization of delta-causal in which multiple events may be generated on a signal in zero time. With this model of time, we can use a generalized ultrametric instead of a metric to model the distance between signals. The existence and uniqueness of behaviors for such systems comes from the fixed-point theorem of Priess-Crampe, but this theorem gives no constructive method to compute the fixed point. This leads us to define petrics, a generalization of metrics, which we use to generalize the Banach fixed-point theorem to provide a constructive fixed-point theorem. This new fixed-point theorem allows us to construct the unique behavior of eventually delta-causal systems

Electronic downloads

• http://ptolemy.eecs.berkeley.edu/publications/papers/06/constructive/

• HTML

  Adam Cataldo, Edward A. Lee, Xiaojun Liu, Eleftherios
  Matsikoudis, Haiyang Zheng. <a
  href="http://chess.eecs.berkeley.edu/pubs/256.html"
  >A Constructive Fixed-Point Theorem and the Feedback
  Semantics of Timed Systems</a>, Workshop on Discrete
  Event Systems, July, 2006.

• Plain text

  Adam Cataldo, Edward A. Lee, Xiaojun Liu, Eleftherios
  Matsikoudis, Haiyang Zheng. "A Constructive Fixed-Point
  Theorem and the Feedback Semantics of Timed Systems".
  Workshop on Discrete Event Systems, July, 2006.

• BibTeX

  @inproceedings{CataldoLeeLiuMatsikoudisZheng06_ConstructiveFixedPointTheoremFeedbackSemanticsOfTimed,
      author = {Adam Cataldo and Edward A. Lee and Xiaojun Liu and
                Eleftherios Matsikoudis and Haiyang Zheng},
      title = {A Constructive Fixed-Point Theorem and the
                Feedback Semantics of Timed Systems},
      booktitle = {Workshop on Discrete Event Systems},
      month = {July},
      year = {2006},
      abstract = {Deterministic timed systems can be modeled as
                fixed point problems. In particular, any connected
                network of timed systems can be modeled as a
                single system with feedback, and the system
                behavior is the fixed point of the corresponding
                system equation, when it exists. For delta-causal
                systems, we can use the Cantor metric to measure
                the distance between signals and the Banach
                fixed-point theorem to prove the existence and
                uniqueness of a system behavior. Moreover, the
                Banach fixed-point theorem is constructive: it
                provides a method to construct the unique fixed
                point through iteration. In this paper, we extend
                this result to systems modeled with the superdense
                model of time used in hybrid systems. We call the
                systems we consider eventually delta-causal, a
                strict generalization of delta-causal in which
                multiple events may be generated on a signal in
                zero time. With this model of time, we can use a
                generalized ultrametric instead of a metric to
                model the distance between signals. The existence
                and uniqueness of behaviors for such systems comes
                from the fixed-point theorem of Priess-Crampe, but
                this theorem gives no constructive method to
                compute the fixed point. This leads us to define
                petrics, a generalization of metrics, which we use
                to generalize the Banach fixed-point theorem to
                provide a constructive fixed-point theorem. This
                new fixed-point theorem allows us to construct the
                unique behavior of eventually delta-causal systems },
      URL = {http://chess.eecs.berkeley.edu/pubs/256.html}
  }
  

Posted by Eleftherios Matsikoudis on 15 May 2007.
Groups: ptolemy
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.