Files: Description File size Format
Fulltext PDF (requires Acrobat Reader)
Fulltext PostScript (requires a PostScript Reader)
   
Authors: Iliano Cervesato, Massimo Franceschet, and Angelo Montanari
Article title: The Complexity of Model Checking in Modal Event Calculi with Quantifiers
Publ. type: Article
Volume: 3
Article No: 21
Language: English
Abstract [en]: Kowalski and Sergot's Event Calculus (EC) is a simple temporal formalism that, given a set of event occurrences, derives the maximal validity intervals (MVIs) over which properties initiated or terminated by these events hold. It does so in polynomial time with respect to the number of events. Extensions of its query language with Boolean connectives and operators from modal logical have been shown to improve substantially its scarce expressiveness, although at the cost of an increase computational complexity. However, significant sublanguages are still tractable. In this paper, we further extend EC queries by admitting arbitrary event quantification. We demonstrate the added expressive power by encoding a hardware diagnosis problem in the resulting calculus. We conduct a detailed complexity analysis of this formalism and several sublanguages that restrict the way modalities, connectives, and quantifiers can be interleaved. We also describe an implementation in the higher-order logic programming language  lambda  Prolog.
PDF
Publisher: Linköping University Electronic Press
Year: 1998
Available: 1997-12-19, 1st Revised 1998-03-28, 2nd Revised 1998-07-29
No. of pages: 21, 1st and 2nd Revised 19
Series: Linköping Electronic Articles in Computer and Information Science
ISSN: 1401-9841
REFERENCE TO THIS PAGE:
Cervesato, Iliano ; Franceschet, Massimo and Montanari, Angelo (1998). The Complexity of Model Checking in Modal Event Calculi with Quantifiers in Linköping Electronic Articles in Computer and Information Science, Vol. 3. http://www.ep.liu.se/ea/cis/1998/021/. ()