Branching vs Linear Time: Semantical Perspective

Add to your list(s) Download to your calendar using vCal

• Moshe Y. Vardi, Rice University
• Friday 13 November 2009, 14:00-15:00
• UG40 Computer Science.

If you have a question about this talk, please contact Paul Levy.

The discussion of the relative merits of linear- versus branching-time frameworks goes back to early 1980s. One of the beliefs dominating this discussion has been that the linear-time framework is not expressive enough semantically, making linear-time logics lacking in expressiveness. In this talk we examine the branching-linear issue from the perpsective of process equivalence, which is one of the most fundamental notions in concurrency theory. Defining a notion of process equivalence essentially amounts to defining semantics for processes. Over the last three decades numerous notions of process equivalence have been proposed. Researchers in this area do not anymore try to identify the “right” notion of equivalence. Rather, focus has shifted to providing taxonomic frameworks, such as “the linear-branching spectrum”, for the many proposed notions and trying to determine suitability for different applications.

We revisit here this issue from a fresh perspective. We postulate three principles that we view as fundamental to any discussion of process equivalence. First, we borrow from research in denotational semantics and take contextual equivalence as the primary notion of equivalence. This eliminates many testing scenarios as either too strong or too weak. Second, we require the description of a process to specify all relevant behavioral aspects of the process. Finally, we require the observable behavior of a process to be reflected in its input/output behavior. Under these principles, linear-time semantics emerges as the right approach. As an example, we apply these principles to the framework of transducers, a classical notion of state-based process that dates back to the 1950s and is well suited to reactive systems. We show that our principles yield a unique notion of process equivalence, which is trace based, rather than tree based.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• UG40 Computer Science
• computer sience

Note that ex-directory lists are not shown.