文章基本信息

标题：Model Checking the Quantitative Î¼-Calculus on Linear Hybrid Systems
本地全文：下载
作者：Diana Fischer ; Lukasz Kaiser
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2012
卷号：8
期号：3
页码：1
DOI：10.2168/LMCS-8(3:21)2012
出版社：Technical University of Braunschweig
摘要：We study the model-checking problem for a quantitative extension of the modal mu-calculus on a class of hybrid systems. Qualitative model checking has been proved decidable and implemented for several classes of systems, but this is not the case for quantitative questions that arise naturally in this context. Recently, quantitative formalisms that subsume classical temporal logics and allow the measurement of interesting quantitative phenomena were introduced. We show how a powerful quantitative logic, the quantitative mu-calculus, can be model checked with arbitrary precision on initialised linear hybrid systems. To this end, we develop new techniques for the discretisation of continuous state spaces based on a special class of strategies in model-checking games and present a reduction to a class of counter parity games.
其他关键词：hybrid systems, model checking, µ-calculus, quantitative logics, games.