*banner
 

A Constructive Fixed-Point Theorem and the Feedback Semantics of Timed Systems
Adam Cataldo, Edward A. Lee, Xiaojun Liu, Eleftherios Matsikoudis, Haiyang Zheng

Citation
Adam Cataldo, Edward A. Lee, Xiaojun Liu, Eleftherios Matsikoudis, Haiyang Zheng. "A Constructive Fixed-Point Theorem and the Feedback Semantics of Timed Systems". Technical report, EECS Dept. University of California, Berkeley, 4, 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

Citation formats  
  • HTML
    Adam Cataldo, Edward A. Lee, Xiaojun Liu, Eleftherios
    Matsikoudis, Haiyang Zheng. <a
    href="http://chess.eecs.berkeley.edu/pubs/52.html"
    ><i>A Constructive Fixed-Point Theorem and the
    Feedback Semantics of Timed Systems</i></a>,
    Technical report,  EECS Dept. University of California,
    Berkeley, 4, 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".
    Technical report,  EECS Dept. University of California,
    Berkeley, 4, 2006.
  • BibTeX
    @techreport{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},
        institution = {EECS Dept. University of California, Berkeley},
        number = {4},
        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/52.html}
    }
    

Posted by Mary Stewart on 4 May 2006.
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