Model Checking Games for the Quantitative mu-Calculus

Details Model Checking Games for the Quantitative mu-Calculus Model Checking Games for the Quantitative mu-Calculus

2008-02-20

arxiv.org/abs/0802.2871v1

Dans Proceedings of the 25th Annual Symposium on the Theoretical Aspects of Computer Science - STACS 2008, Bordeaux : France (

Computer Science

Logic in Computer Science

Scientific paper

We investigate quantitative extensions of modal logic and the modal mu-calculus, and study the question whether the tight connection between logic and games can be lifted from the qualitative logics to their quantitative counterparts. It turns out that, if the quantitative mu-calculus is defined in an appropriate way respecting the duality properties between the logical operators, then its model checking problem can indeed be characterised by a quantitative variant of parity games. However, these quantitative games have quite different properties than their classical counterparts, in particular they are, in general, not positionally determined. The correspondence between the logic and the games goes both ways: the value of a formula on a quantitative transition system coincides with the value of the associated quantitative game, and conversely, the values of quantitative parity games are definable in the quantitative mu-calculus.

Affiliated with

Also associated with

No associations

Rating

Model Checking Games for the Quantitative mu-Calculus does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Model Checking Games for the Quantitative mu-Calculus, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Model Checking Games for the Quantitative mu-Calculus will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-647948