Algorithmic Aspects of Model Theory in a Modal Scenario

Modal logics (as characterised by bisimulation invariance) and their first-order companions in the form of two-variable logics play an important role in areas as diverse as specification/verification, temporal and causal reasoning, or uses as description logics in database theory or knowledge representation. Model theoretic issues of an algorithmic flavour, in particlar, contribute to the more systematic and comparative investigation of these semantic domains. In this talk I will concentrate on the modal domain and discuss two types of results closely related to the study of the modal mu-calculus. The first belongs to the research programme of descriptive complexity and characterizes a logical language, in fact a natural extension of the mu-calculus, as complete for the class of all modal Ptime properties. The second theme concerns boundedness issues, or the issue to decide whether least fixed point recursion is actually necessary for the formalisation of a given property.

LS Home page or Talks in 1998/99