TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 99411

Temporal Logics for Distributed Systems – Paradigms and Algorithms

( Oct 10 – Oct 15, 1999 )

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/99411

Organizers
  • E. Clarke (Pittsburgh)
  • P. Niebert (VERIMAG Grenoble)
  • U. Goltz (Hildesheim)
  • W. Penczek (Warszawa)



Motivation

Distributed systems, i.e. systems characterized by the concurrent operation and interaction of several components, occur throughout information technology; from microprocessors to computer networks. Since the design and development process of distributed systems is very sensitive to errors, it is an accepted fact in both science and industry that formal approaches to specification and automatic verification and debugging are needed. An important formal framework in this line is the family of temporal logics.

Originally, temporal logics were directed to describe a sequentialised (interleaved) and global view of the behavior of distributed systems. Several problems resulting from this approach have been identified. On the specification level, the global view of the system makes it difficult or impossible to intuitively specify behavioral aspects of selected parts of the whole system. On the algorithmic front, this sequentialised semantics leads to the well known state explosion problem, which is often the reason for automatic verification to fail and makes it necessary to develop heuristic workarounds. These problems have led to the following investigations:

  • On the one hand, various semantic models capturing aspects of distribution and causality of the behavior of distributed systems have been developed, in particular partial order models and event structures. On some of these models, several extensions of standard temporal logics with differing modes of expressiveness have been defined. The logics have been investigated under several aspects: Axiomatisations, theoretic and pragmatic expressiveness, complexity of the satisfiability and satisfaction problems.
  • On the other hand, research directed towards efficient model checking has focussed on heuristic improvements of model checking algorithms for interleaving logics, which are based on state space exploration. Techniques, which have been evolving in this domain include modular model checking, symbolic model checking (BDDs), partial order reductions, abstraction, and others. Many of these approaches heavily exploit the distributed structure of the system, but do not explicitly rely on a distributed logical framework.

While a lot of research in both directions has happened separately, the natural connection between them has not gone unnoticed: some logics tailored towards distribution allow new verification algorithms, and conversely the heuristics discovered in model checking algorithms influence the design of logics. However, dedicated research is needed in order to achieve practically useful results here.

The goal of this workshop thus is to bring people from these areas of research together. In particular, we would like the following topics to be addressed:

  • The comparison of specification paradigms. How logics address the characteristic aspects of distributed behavior, in particular causality and locality. Specification with distributed knowledge. How to add application oriented features.
  • The evaluation of various behavioral models for distributed systems as frames for temporal logics. For example, using event oriented or configuration oriented approaches for prime event structure semantics of logics.
  • Decidability and worst case complexity of satisfiability and model checking for distributed specification {formalisms}, e.g. automata theoretic methods and tableau methods, modular model checking.
  • The applicability of heuristic model checking methods and tools (e.g. partial order reduction methods, BDDs, Petri net unfoldings) to distributed logics. New model checking methods arising from logics with distribution.

The discussion of these and other points between experts from the research fields outlined above will lead to a better understanding of the prospects of logics for distributed systems and their verification algorithms.


Participants
  • E. Clarke (Pittsburgh)
  • P. Niebert (VERIMAG Grenoble)
  • U. Goltz (Hildesheim)
  • W. Penczek (Warszawa)