by Lutz Schröder and Dirk Pattinson
Abstract:
State-based systems and modal logics for reasoning about them often heterogeneously combine a number of features such as non-determinism and probabilities. Here, we show that the combination of features can be reflected algorithmically and develop modular decision procedures for heterogeneous modal logics. The modularity is achieved by formalizing the underlying state-based systems as multi-sorted coalgebras and associating both a logical and an algorithmic description to 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 that this is 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 e.g. Segala systems and games with uncertain information.
Reference:
Lutz Schröder and Dirk Pattinson: Modular Algorithms for Heterogeneous Modal Logics via Multi-Sorted Coalgebra, In Math. Struct. Comput. Sci., 21(2), pp. 235–266, 2011. Copyright Cambridge University Press [preprint]
Bibtex Entry:
@Article{SchroderPattinson10c,
author = {Lutz Schr{\"o}der and Dirk Pattinson},
title = {Modular Algorithms for Heterogeneous Modal Logics via Multi-Sorted Coalgebra},
year = {2011},
journal = {Math. Struct. Comput. Sci.},
volume = {21},
pages = {235-266},
number = {2},
keywords = {multisorted coalgebra modal logic complexity pspace shallow models features},
url = {http://journals.cambridge.org/action/displayAbstract?aid=8238956},
comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/ModAlg-Ext.pdf"> [preprint] </a>},
abstract = {State-based systems and modal logics for reasoning about them often heterogeneously combine a number of features such as non-determinism and probabilities. Here, we show that the combination of features can be reflected algorithmically and develop modular decision procedures for heterogeneous modal logics. The modularity is achieved by formalizing the underlying state-based systems as multi-sorted coalgebras and associating both a logical and an algorithmic description to 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 that this is 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 e.g. Segala systems and games with uncertain information.},
note = {Copyright Cambridge University Press},
}