Output details
11 - Computer Science and Informatics
Imperial College London
EXPTIME tableaux for the coalgebraic µ-calculus
<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.