Complexity of ITL Model Checking: Some Well-Behaved Fragments of the Interval Logic HS

Model checking has been successfully used in many computer science fields, including artificial intelligence, theoretical computer science, and databases. Most of the proposed solutions make use of classical, point-based temporal logics, while little work has been done in the interval temporal logic...

Full description

Saved in:
Bibliographic Details
Main Authors: Molinari, Alberto, Montanari, Angelo, Peron, Adriano
Format: Conference Proceeding
Language:English
Subjects:
Artificial intelligence
Bismuth
Cognition
Complexity
Computer science
Interval Temporal Logic
Labeling
Model checking
Semantics
Citations: Items that cite this one
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Model checking has been successfully used in many computer science fields, including artificial intelligence, theoretical computer science, and databases. Most of the proposed solutions make use of classical, point-based temporal logics, while little work has been done in the interval temporal logic setting. Recently, a non-elementary model checking algorithm for Halpern and Shoham's modal logic of time intervals HS over finite Kripke structures (under the homogeneity assumption) and an EXPSPACE model checking procedure for two meaningful fragments of it have been proposed. In this paper, we show that more efficient model checking procedures can be developed for some expressive enough fragments of HS.
ISSN:1530-1311
2332-6468
DOI:10.1109/TIME.2015.12