Annotated Probabilistic Temporal logic

Approximate fixpoint implementation

Paulo Shakarian, Gerardo I. Simari, V. S. Subrahmanian

Research output: Contribution to journalArticle

11 Citations (Scopus)

Abstract

Annotated Probabilistic Temporal (APT) logic programs support building applications where we wish to reason about statements of the form "Formula G becomes true with a probability in the range [L, U] within (or in exactly) At time units after formula F became true." In this paper, we present a sound, but incomplete fixpoint operator that can be used to check consistency and entailment in APT logic programs. We present the first implementation of APT-logic programs and evaluate both its compute time and convergence on a suite of 23 ground APT-logic programs that were automatically learned from two real-world data sets. In both cases, the APT-logic programs contained up to 1,000 ground rules. In one data set, entailment problems were solved on average in under 0.1 seconds per ground rule, while in the other, it took up to 1.3 seconds per ground rule. Consistency was also checked in a reasonable amount of time. When discussing entailment of APT-logic formulas, convergence of the fixpoint operator refers to (U - L) being below a certain threshold. We show that on virtually all of the 23 automatically generated APT-logic programs, convergence was quick-often in just 2-3 iterations of the fixpoint operator. Thus, our implementation is a practical first step towards checking consistency and entailment in temporal probabilistic logics without independence or Markovian assumptions.

Original languageEnglish (US)
Article numbera13
JournalACM Transactions on Computational Logic
Volume13
Issue number2
DOIs
StatePublished - Apr 2012
Externally publishedYes

Fingerprint

Probabilistic Logic
Temporal logic
Fixpoint
Temporal Logic
Logic Programs
Probabilistic logics
Operator
Acoustic waves
Iteration
Unit
Evaluate

Keywords

  • Frequency functions
  • Imprecise probabilities
  • Probabilistic and temporal reasoning
  • Threads

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science
  • Computational Mathematics
  • Logic

Cite this

Annotated Probabilistic Temporal logic : Approximate fixpoint implementation. / Shakarian, Paulo; Simari, Gerardo I.; Subrahmanian, V. S.

In: ACM Transactions on Computational Logic, Vol. 13, No. 2, a13, 04.2012.

Research output: Contribution to journalArticle

@article{c4bb2cb50944420cb7a01a3ea109303a,
title = "Annotated Probabilistic Temporal logic: Approximate fixpoint implementation",
abstract = "Annotated Probabilistic Temporal (APT) logic programs support building applications where we wish to reason about statements of the form {"}Formula G becomes true with a probability in the range [L, U] within (or in exactly) At time units after formula F became true.{"} In this paper, we present a sound, but incomplete fixpoint operator that can be used to check consistency and entailment in APT logic programs. We present the first implementation of APT-logic programs and evaluate both its compute time and convergence on a suite of 23 ground APT-logic programs that were automatically learned from two real-world data sets. In both cases, the APT-logic programs contained up to 1,000 ground rules. In one data set, entailment problems were solved on average in under 0.1 seconds per ground rule, while in the other, it took up to 1.3 seconds per ground rule. Consistency was also checked in a reasonable amount of time. When discussing entailment of APT-logic formulas, convergence of the fixpoint operator refers to (U - L) being below a certain threshold. We show that on virtually all of the 23 automatically generated APT-logic programs, convergence was quick-often in just 2-3 iterations of the fixpoint operator. Thus, our implementation is a practical first step towards checking consistency and entailment in temporal probabilistic logics without independence or Markovian assumptions.",
keywords = "Frequency functions, Imprecise probabilities, Probabilistic and temporal reasoning, Threads",
author = "Paulo Shakarian and Simari, {Gerardo I.} and Subrahmanian, {V. S.}",
year = "2012",
month = "4",
doi = "10.1145/2159531.2159535",
language = "English (US)",
volume = "13",
journal = "ACM Transactions on Computational Logic",
issn = "1529-3785",
publisher = "Association for Computing Machinery (ACM)",
number = "2",

}

TY - JOUR

T1 - Annotated Probabilistic Temporal logic

T2 - Approximate fixpoint implementation

AU - Shakarian, Paulo

AU - Simari, Gerardo I.

AU - Subrahmanian, V. S.

PY - 2012/4

Y1 - 2012/4

N2 - Annotated Probabilistic Temporal (APT) logic programs support building applications where we wish to reason about statements of the form "Formula G becomes true with a probability in the range [L, U] within (or in exactly) At time units after formula F became true." In this paper, we present a sound, but incomplete fixpoint operator that can be used to check consistency and entailment in APT logic programs. We present the first implementation of APT-logic programs and evaluate both its compute time and convergence on a suite of 23 ground APT-logic programs that were automatically learned from two real-world data sets. In both cases, the APT-logic programs contained up to 1,000 ground rules. In one data set, entailment problems were solved on average in under 0.1 seconds per ground rule, while in the other, it took up to 1.3 seconds per ground rule. Consistency was also checked in a reasonable amount of time. When discussing entailment of APT-logic formulas, convergence of the fixpoint operator refers to (U - L) being below a certain threshold. We show that on virtually all of the 23 automatically generated APT-logic programs, convergence was quick-often in just 2-3 iterations of the fixpoint operator. Thus, our implementation is a practical first step towards checking consistency and entailment in temporal probabilistic logics without independence or Markovian assumptions.

AB - Annotated Probabilistic Temporal (APT) logic programs support building applications where we wish to reason about statements of the form "Formula G becomes true with a probability in the range [L, U] within (or in exactly) At time units after formula F became true." In this paper, we present a sound, but incomplete fixpoint operator that can be used to check consistency and entailment in APT logic programs. We present the first implementation of APT-logic programs and evaluate both its compute time and convergence on a suite of 23 ground APT-logic programs that were automatically learned from two real-world data sets. In both cases, the APT-logic programs contained up to 1,000 ground rules. In one data set, entailment problems were solved on average in under 0.1 seconds per ground rule, while in the other, it took up to 1.3 seconds per ground rule. Consistency was also checked in a reasonable amount of time. When discussing entailment of APT-logic formulas, convergence of the fixpoint operator refers to (U - L) being below a certain threshold. We show that on virtually all of the 23 automatically generated APT-logic programs, convergence was quick-often in just 2-3 iterations of the fixpoint operator. Thus, our implementation is a practical first step towards checking consistency and entailment in temporal probabilistic logics without independence or Markovian assumptions.

KW - Frequency functions

KW - Imprecise probabilities

KW - Probabilistic and temporal reasoning

KW - Threads

UR - http://www.scopus.com/inward/record.url?scp=84860278712&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84860278712&partnerID=8YFLogxK

U2 - 10.1145/2159531.2159535

DO - 10.1145/2159531.2159535

M3 - Article

VL - 13

JO - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

SN - 1529-3785

IS - 2

M1 - a13

ER -