Affordable Access

Publisher Website

Abstract interpretation of programs as Markov decision processes

Authors
Journal
Science of Computer Programming
0167-6423
Publisher
Elsevier
Publication Date
Volume
58
Identifiers
DOI: 10.1016/j.scico.2005.02.008
Keywords
  • Abstract Interpretation
  • Probabilistic Semantics
  • Program Semantics
  • Probabilities
  • Measure Theory
Disciplines
  • Linguistics
  • Logic
  • Mathematics

Abstract

Abstract We propose a formal language for the specification of trace properties of probabilistic, nondeterministic transition systems, encompassing the properties expressible in Linear Time Logic. Those formulas are in general undecidable on infinite deterministic transition systems and thus on infinite Markov decision processes. This language has both a semantics in terms of sets of traces, as well as another semantics in terms of measurable functions; we give and prove theorems linking the two semantics. We then apply abstract interpretation-based techniques to give upper bounds on the worst-case probability of the studied property. We propose an enhancement of this technique when the state space is partitioned — for instance along the program points — allowing the use of faster iteration methods.

There are no comments yet on this publication. Be the first to share your thoughts.