• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Quantitative Temporal Logic Mechanized in HOL

Orieta Celiku, Quantitative Temporal Logic Mechanized in HOL. In: Theoretical Aspects of Computing - ICTAC 2005, Lecture Notes in Computer Science 3722, 439–453, Springer-Verlag, 2005.

Abstract:

We describe an implementation in the HOL theorem prover of the
quantitative Temporal Logic of Morgan and McIver, a temporal logic
suitable for reasoning about probabilistic nondeterministic systems. In
the qTL framework many laws of standard branching-time temporal logic
generalize nicely giving access to a number of logical tools for
reasoning about quantitative aspects of randomized algorithms.

BibTeX entry:

@INPROCEEDINGS{inpCeliku05b,
  title = {Quantitative Temporal Logic Mechanized in HOL},
  booktitle = {Theoretical Aspects of Computing - ICTAC 2005},
  author = {Celiku, Orieta},
  volume = {3722},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  pages = {439–453},
  year = {2005},
}

Belongs to TUCS Research Unit(s): Learning and Reasoning Lab

Publication Forum rating of this publication: level 1

Edit publication