Adam Cataldo and Edward A. Lee and Xiaojun Liu and Eleftherios Dimitrios Matsikoudis and Haiyang Zheng

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2006-4

January 24, 2006

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-4.pdf

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.

---

BibTeX citation:

@techreport{Cataldo:EECS-2006-4,
    Author= {Cataldo, Adam and Lee, Edward A. and Liu, Xiaojun and Matsikoudis, Eleftherios Dimitrios and Zheng, Haiyang},
    Title= {A Constructive Fixed-Point Theorem and the Feedback Semantics of Timed Systems},
    Year= {2006},
    Month= {Jan},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-4.html},
    Number= {UCB/EECS-2006-4},
    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.},
}

EndNote citation:

%0 Report
%A Cataldo, Adam 
%A Lee, Edward A. 
%A Liu, Xiaojun 
%A Matsikoudis, Eleftherios Dimitrios 
%A Zheng, Haiyang 
%T A Constructive Fixed-Point Theorem and the Feedback Semantics of Timed Systems
%I EECS Department, University of California, Berkeley
%D 2006
%8 January 24
%@ UCB/EECS-2006-4
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-4.html
%F Cataldo:EECS-2006-4