2003 | OriginalPaper | Buchkapitel
Quantitative Verification and Control via the Mu-Calculus
verfasst von : Luca de Alfaro
Erschienen in: CONCUR 2003 - Concurrency Theory
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
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
Linear-time properties and symbolic algorithms provide a widely used framework for system specification and verification. In this framework, the verification and control questions are phrased as boolean questions: a system either satisfies (or can be made to satisfy) a property, or it does not. These questions can be answered by symbolic algorithms expressed in the μ-calculus. We illustrate how the μ-calculus also provides the basis for two quantitative extensions of this approach: a probabilistic extension, where the verification and control problems are answered in terms of the probability with which the specification holds, and a discounted extension, in which events in the near future are weighted more heavily than events in the far away future.