Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
The fixed-point theory of strictly causal functions
Matsikoudis E., Lee E. Theoretical Computer Science574 (C):39-77,2015.Type:Article
Date Reviewed: Oct 12 2015

Consider this problem of working with timed systems. Suppose that we are to model a ball bouncing under gravity, with air resistance. The ball will bounce less high each time, with the time gaps between bounces reducing, too. In fact, bouncing will stop after a finite time, but after an infinite number of bounces: this is called a Zeno phenomenon, after Zeno’s parable of the tortoise and the hare. As this example shows, Zeno phenomena are perfectly natural, albeit in the idealized world of Newtonian physics. The point is, though, that such systems can be realized, and should be susceptible to modeling as cyber-physical systems. But can this be done with the existing semantic frameworks for these systems?

Matsikoudis and Lee show in their paper that they can go beyond the previous state of the art of modeling for timed systems--which explicitly prevented Zeno phenomena (and “instant” reactions) by requiring a defined lower bound on reaction time--to model such phenomena. They also establish through a set of counter-examples that their results are the best possible for the systems that they study, and they also point out directions for future work, including models with recursion and higher-order operations.

What are the results that the authors prove? Using motivation from pioneers in the field Cousot and Cousot, they search for a constructive fixed-point theorem establishing that a particular class of functions has unique fixed points characterized as the limits of transfinite sequences of post-fixed points. This latter characterization allows proof by induction, the workhorse for making effective proofs in this area of semantics.

The class of functions in question is that of strictly contracting functions, which they show is a strict subset of the strictly causal functions possessing a unique fixed point (which is itself a subset of the strictly causal functions). The strictly contracting components are characterized by the requirement that differences in outputs happen no sooner than differences in inputs. Of course, the formal definition relies on an infrastructure laid out by the authors, but this is the nub of (the motivation for the) definition that they give.

Their definitions are set out in the context of the literature, and the formal parts of the paper are framed by informal evaluation in the introduction and the discussion sections. Taken with the conclusion, these make this a model of exposition of technical material: theorems are proved and counterexamples defined, but with the reader able to relate these to the wider context of the semantics of cyber-physical systems. In short, this is a very good piece of work.

Reviewer:  Simon Thompson Review #: CR143846 (1512-1068)
Bookmark and Share
  Featured Reviewer  
Deduction And Theorem Proving (I.2.3 )
Would you recommend this review?
Other reviews under "Deduction And Theorem Proving": Date
Noninteractive zero-knowledge
Blum M., De Santis A., Micali S., Persiano G. SIAM Journal on Computing 20(6): 1084-1118, 1991. Type: Article
Jan 1 1993
Cut elimination and automatic proof procedures
Zhang W. Theoretical Computer Science 91(2): 265-284, 1991. Type: Article
Apr 1 1993
A non-reified temporal logic
Bacchus F., Tenenberg J., Koomen J. Artificial Intelligence 52(1): 87-108, 1991. Type: Article
Oct 1 1992

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 2004™
Terms of Use
| Privacy Policy