TY - JOUR
T1 - Modular algorithms for heterogeneous modal logics via multi-sorted coalgebra
AU - Schröder, Lutz
AU - Pattinson, Dirk
PY - 2011/4
Y1 - 2011/4
N2 - State-based systems and modal logics for reasoning about them often heterogeneously combine a number of features such as non-determinism and probabilities. In this paper, we show that the combination of features can be reflected algorithmically, and we develop modular decision procedures for heterogeneous modal logics. The modularity is achieved by formalising the underlying state-based systems as multi-sorted coalgebras and associating both a logical and algorithmic description with a number of basic building blocks. Our main result is that logics arising as combinations of these building blocks can be decided in polynomial space provided this is also the case for the components. By instantiating the general framework to concrete cases, we obtain PSpace decision procedures for a wide variety of structurally different logics, describing, for example, Segala systems and games with uncertain information.
AB - State-based systems and modal logics for reasoning about them often heterogeneously combine a number of features such as non-determinism and probabilities. In this paper, we show that the combination of features can be reflected algorithmically, and we develop modular decision procedures for heterogeneous modal logics. The modularity is achieved by formalising the underlying state-based systems as multi-sorted coalgebras and associating both a logical and algorithmic description with a number of basic building blocks. Our main result is that logics arising as combinations of these building blocks can be decided in polynomial space provided this is also the case for the components. By instantiating the general framework to concrete cases, we obtain PSpace decision procedures for a wide variety of structurally different logics, describing, for example, Segala systems and games with uncertain information.
UR - http://www.scopus.com/inward/record.url?scp=80053000863&partnerID=8YFLogxK
U2 - 10.1017/S0960129510000563
DO - 10.1017/S0960129510000563
M3 - Article
SN - 0960-1295
VL - 21
SP - 235
EP - 266
JO - Mathematical Structures in Computer Science
JF - Mathematical Structures in Computer Science
IS - 2
ER -