The Complexity of Model Checking in Modal Event Calculi with Quantifiers.
Summary:
The Event Calculus
The Event Calculus, abbreviated EC, is a
simple temporal formalism designed to model and reason about scenarios
characterized by a set of events, whose occurrences have the effect of
starting or terminating the validity of determined properties. Given a
possibly incomplete description of when these events take place and of
the properties they affect, EC is able to determine the maximal
validity intervals, or MVIs, over which a property holds
uninterruptedly.
State-of-the-art
A systematic analysis of EC has recently been undertaken in order to
gain a better understanding of this calculus and determine ways of augmenting
its expressive power. The keystone of this endeavor has been the definition
of an extendible formal specification of the functionalities of this
formalism. This has had the effects of establishing a
semantic reference against which to verify the correctness of
implementations, of casting EC as a model checking
problem, and of setting the ground for studying the
complexity of this problem, which was proved
polynomial. Extensions of this model have been
designed to accommodate constructs intended to enhance the expressiveness of
EC@. In particular, modal versions of
EC, the interaction between modalities and
connectives, and preconditions
have all been investigated in this context.
Contributions
The main contributions of the present paper are the following:
- The extension of a family of modal event calculi with quantifiers.
We enhance the expressive power
of EC by considering the possibility of quantifying over events in
queries, in conjunction with boolean connectives and modal operators. We also
admit requests to check the relative order of two events. We thoroughly
analyze the representational and computational features of the resulting
formalism, that we call QCMEC@. We also consider two proper
sublanguages of it, EQCMEC, in which modalities are applied to atomic
formulas only, and CMEC, which is quantifier-free.
- The use of the proposed formalisms to encode diagnosis problems.
We consider a case study taken from the domain of hardware
fault diagnosis. We model it using EC and use the
various extensions of EC to draw conclusions about it.
- The use of the higher-order features of modern logic
programming languages in temporal reasoning.
We provide an elegant implementation in the higher-order
logic programming language lambda Prolog and
prove its soundness and completeness.
- Analyzing the complexity of model checking in the proposed extensions
of EC@.
We prove that model checking in CMEC, EQCMEC, and QCMEC is
PSPACE-complete. However, while solving an EQCMEC problem is
exponential in the size of the query, it has only polynomial cost in the
number of events, thus making EQCMEC a viable formalism for
MVI verification or computation. Since in most realistic applications
the size of databases dominates by several orders of magnitude the size
of the query, the former is asymptotically the parameter of interest.