ANU Computer Science Technical Reports

TR-CS-07-02

Sophie Pinchinat.
Quantified mu-calculus with decision modalities for concurrent game structures.
January 2007.

[POSTSCRIPT (259867 bytes)] [PDF (289605 bytes)]

Abstract: The emerging technology of interacting systems calls for new verification methods to ensure their reliability. Concurrent Game Structures are expressive abstract models for which several logics have been studied. Yet, these logics are not sufficiently expressive to support certain strategic situation which arise naturally. We propose a second-order mu-calculus enabling a straightforward specification of complex coalition strategies, and also yields a direct synthesis procedure via automata constructions. By translating different alternating-time logics into a natural fragment of our calculus, we recover optimal complexity bounds for these logics.

Technical Reports <Technical-DOT-Reports-AT-cs-DOT-anu.edu.au>

Last modified: Tue May 31 12:56:01 EST 2011