Anzeige
Erschienen in:
2010 | OriginalPaper | Buchkapitel
A Formal Language toward the Unification of Model Checking and Performance Evaluation
verfasst von : Andrew S. Miner, Yaping Jing
Erschienen in: Analytical and Stochastic Modeling Techniques and Applications
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
There are currently a variety of logics used to describe properties of discrete–state systems, such as linear temporal logic (LTL) and computation tree logic (CTL), and of discrete–state stochastic systems, such as probabilistic CTL (PCTL) and continuous stochastic logic (CSL). While powerful, these logics are by definition limited to producing only true or false responses. In this work, we introduce a query language, CTML, that operates on real–valued quantities to reason over probabilistic systems. CTML is inspired by, and evolves from stochastic logic. It extends until and weak until with arithmetic operations on real values, while still preserving their conventional semantics of temporal logic. We derive mathematical algorithms for computing each of the operators, show how any PCTL property can be expressed in CTML, and illustrate the expressiveness of CTML with some example performance–related queries.