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. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
De Alfaro, L. (2003). Quantitative verification and control via the mu-calculus. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2761, 103–127. https://doi.org/10.1007/978-3-540-45187-7_7
Mendeley helps you to discover research relevant for your work.