Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

TSE

2011

2011

— We propose a new probabilistic temporal logic iLTL which captures properties of systems whose state can be represented by probability mass functions (pmf’s). Using iLTL, we can specify reachability to a state (i.e., a pmf), as well as properties representing the aggregate (expected) behavior of a system. We then consider a class of systems whose transitions are governed by a Markov Chain–in this case, the set of states a system may be in is speciﬁed by the transitions of pmf’s from all potential initial states to the ﬁnal state. We then provide a model checking algorithm to check iLTL properties of such systems. Unlike existing model checking techniques, which either compute the portions of the computational paths that satisfy a speciﬁcation, or evaluate properties along a single path of pmf transitions, our model checking technique enables us to do a complete analysis on the expected behaviors of large scale systems. Desirable system parameters may also be found as a c...

Added |
15 May 2011 |

Updated |
15 May 2011 |

Type |
Journal |

Year |
2011 |

Where |
TSE |

Authors |
YoungMin Kwon, Gul A. Agha |

Comments (0)