Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
10333992 | Theoretical Computer Science | 2005 | 22 Pages |
Abstract
We generalize the familiar semantics for probabilistic computation tree logic from finite-state to infinite-state labelled Markov chains such that formulas are interpreted as measurable sets. Then we show how to synthesize finite-state abstractions which are sound for full probabilistic computation tree logic and in which measures are approximated by monotone set functions. This synthesis of sound finite-state approximants also applies to finite-state systems and is a probabilistic analogue of predicate abstraction. Sufficient and always realizable conditions are identified for obtaining optimal such abstractions for probabilistic propositional modal logic.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Michael Huth,