| Título: | Calculating the probability of an LTL formula over a labeled Markov chain |
| Autores: | Eliosoff, Jacob |
| Fecha: | 2003 |
| Publicador: | McGill University - MCGILL |
| Fuente: |
 |
| Tipo: | Electronic Thesis or Dissertation |
| Tema: | Computer Science. |
| Descripción: | This thesis presents a new algorithm to compute the probability that a state in a labeled Markov chain model satisfies an LTL specification. A solution to this problem was given by Courcoubetis & Yannakakis in 1995, but unlike their solution the algorithm presented here requires no transformations of the input model. This advantage may be significant because of the large models which occur in most practical verification problems. The new algorithm is proved correct and shown to be not worse than doubly exponential in the size of the formula and cubic in the size of the model. However limited experimental results suggest that these bounds are pessimistic and that with further optimization the algorithm might approach the efficiency of current model checkers, which compute only true or false rather than an exact probability. I also include a working Java implementation, MCMC, and a proof that for any plausible path P followed by a Markov chain and any LTL formula Φ, some finite prefix of P determines whether P satisfies Φ. |
| Idioma: | en |
1 Investigations on the form-genera Beauveria and Tritirachium por MacLeod, Donald Murdock | 6 Treatment and recovery in first-episode psychosis : a qualitative analysis of client experiences por Windell, Deborah L. |
2 Seismic sensitivity of tall guyed telecommunication towers. por Ghodrati Amiri, Gholamreza. | 7 |
3 Exploring the Relationship Between Assets and Family Stress Among Low-Income Families por Rothwell, David W.,Han, Chang-Keun | 8 |
4 The case for asset-based interventions with indigenous peoples: Evidence from Hawai‘i por Rothwell, David W. | 9 |
5 Second Thoughts: Who Almost Participates in an IDA Program? por Rothwell, David W.,Han, Chang-Keun | 10 Recent contributions to the phenomenology of musical time : a critical survey por Beaudreau, Pierre |