Model Checking Quantitative Linear Time Logic

This paper considers QLtl, a quantitative analagon of Ltl and presents algorithms for model checking QLtl over quantitative versions of Kripke structures and Markov chains.

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Marco Faella, Axel Legay, Mariëlle Stoelinga
• Keywords: ENTCS 2008, Kripke Structures, Quantitative Analagon, Quantitative Versions