Probabilistic Interval Temporal Logic and Duration Calculus with Infinite Intervals: Complete Proof Systems

TL;DR

This paper introduces probabilistic extensions of interval temporal logic and duration calculus that handle infinite intervals, providing complete proof systems and establishing their relation to existing probabilistic real-time DC and finite interval systems.

Contribution

It develops complete Hilbert-style proof systems for probabilistic ITL and DC with infinite intervals, extending prior work and establishing formal correspondence with finite interval probabilistic systems.

Findings

Established strong and relative completeness theorems.

Unified probabilistic ITL and DC frameworks with infinite intervals.

Connected infinite interval systems to finite interval probabilistic logic.

Abstract

The paper presents probabilistic extensions of interval temporal logic (ITL) and duration calculus (DC) with infinite intervals and complete Hilbert-style proof systems for them. The completeness results are a strong completeness theorem for the system of probabilistic ITL with respect to an abstract semantics and a relative completeness theorem for the system of probabilistic DC with respect to real-time semantics. The proposed systems subsume probabilistic real-time DC as known from the literature. A correspondence between the proposed systems and a system of probabilistic interval temporal logic with finite intervals and expanding modalities is established too.