For the current REF see the REF 2021 website REF 2021 logo

Output details

11 - Computer Science and Informatics

Imperial College London

Return to search Previous output Next output
Output 0 of 0 in the submission
Output title

EXPTIME tableaux for the coalgebraic µ-calculus

Type
E - Conference contribution
Name of conference/published proceedings
18th Annual Conference on Computer Science Logic (EACSL’09)
Volume number
5771
Issue number
-
First page of article
179
ISSN of proceedings
-
Year of publication
2009
URL
-
Number of additional authors
2
Additional information

<11>The mu-calculus is one of the most widely studied formalism for the verification of reactive systems. Traditionally, the semantics of the calculus is given in terms of so-called Kripke models and the models are graph theoretic. This precludes applications of standard results to models that embody a richer structure such as probabilistic transition systems or weighted graphs. This paper abstracts the concrete shape of the system using coalgebraic techniques and gives a complexity-optimal tableau calculus that captures transition systems with structure. Our main result is that for systems with structure, the decision problem remains in the same complexity class.

Interdisciplinary
-
Cross-referral requested
-
Research group
A - Logic and Artificial Intelligence
Citation count
7
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-