{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,15]],"date-time":"2024-07-15T14:39:39Z","timestamp":1721054379782},"reference-count":49,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2011,3,25]],"date-time":"2011-03-25T00:00:00Z","timestamp":1301011200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2011,4]]},"abstract":"<jats:p>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 P<jats:sc>Space<\/jats:sc> decision procedures for a wide variety of structurally different logics, describing, for example, Segala systems and games with uncertain information.<\/jats:p>","DOI":"10.1017\/s0960129510000563","type":"journal-article","created":{"date-parts":[[2011,3,25]],"date-time":"2011-03-25T07:52:40Z","timestamp":1301039560000},"page":"235-266","source":"Crossref","is-referenced-by-count":12,"title":["Modular algorithms for heterogeneous modal logics via multi-sorted coalgebra"],"prefix":"10.1017","volume":"21","author":[{"given":"LUTZ","family":"SCHR\u00d6DER","sequence":"first","affiliation":[]},{"given":"DIRK","family":"PATTINSON","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2011,3,25]]},"reference":[{"key":"S0960129510000563_ref48","first-page":"243","volume-title":"Logic in Computer Science, LICS 89","author":"Vardi","year":"1989"},{"key":"S0960129510000563_ref47","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/11.1.85"},{"key":"S0960129510000563_ref46","first-page":"93","article-title":"Coalgebraic weak bisimulation for action-type systems.","volume":"19","author":"Sokolova","year":"2009","journal-title":"Scientific Annals of Computer Science"},{"key":"S0960129510000563_ref43","unstructured":"Segala R. (1995) Modelling and Verification of Randomized Distributed Real-Time Systems, Ph.D. thesis, Massachusetts Institute of Technology."},{"key":"S0960129510000563_ref41","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn096"},{"key":"S0960129510000563_ref40","doi-asserted-by":"publisher","DOI":"10.1145\/1462179.1462185"},{"key":"S0960129510000563_ref39","first-page":"324","article-title":"Shallow models for non-iterative modal logics","volume":"5243","author":"Schr\u00f6der","year":"2008","journal-title":"Springer-Verlag Lecture Notes in Artificial Intelligence"},{"key":"S0960129510000563_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73420-8_41"},{"key":"S0960129510000563_ref35","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2006.11.004"},{"key":"S0960129510000563_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_6"},{"key":"S0960129510000563_ref30","doi-asserted-by":"publisher","DOI":"10.1145\/1276920.1276924"},{"key":"S0960129510000563_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00596-1_11"},{"key":"S0960129510000563_ref28","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2005.09.006"},{"key":"S0960129510000563_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(98)00042-6"},{"key":"S0960129510000563_ref26","first-page":"457","article-title":"Intensional logics without iterative axioms.","volume":"3","author":"Lewis","year":"1975","journal-title":"Journal of Philosophical Logic"},{"key":"S0960129510000563_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"S0960129510000563_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2004.02.002"},{"key":"S0960129510000563_ref21","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2001108"},{"key":"S0960129510000563_ref19","doi-asserted-by":"publisher","DOI":"10.1006\/game.1999.0788"},{"key":"S0960129510000563_ref18","volume-title":"Time and Probability in Formal Design of Distributed Systems","author":"Hansson","year":"1994"},{"key":"S0960129510000563_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_5"},{"key":"S0960129510000563_ref13","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093890715"},{"key":"S0960129510000563_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00035-3"},{"key":"S0960129510000563_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/s001530100110"},{"key":"S0960129510000563_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.06.002"},{"key":"S0960129510000563_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.02.028"},{"key":"S0960129510000563_ref6","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107050884"},{"key":"S0960129510000563_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_3"},{"key":"S0960129510000563_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/585265.585270"},{"key":"S0960129510000563_ref1","volume-title":"Abstract and Concrete Categories","author":"Ad\u00e1mek","year":"1990"},{"key":"S0960129510000563_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80632-7"},{"key":"S0960129510000563_ref23","volume-title":"Handbook of Modal Logic","author":"Kurucz","year":"2006"},{"key":"S0960129510000563_ref49","first-page":"361","article-title":"Fusions of modal logics revisited","volume":"1","author":"Wolter","year":"1998","journal-title":"CSLI Lecture Notes"},{"key":"S0960129510000563_ref42","first-page":"917","volume-title":"International Joint Conferences on Artificial Intelligence, IJCAI 09","author":"Schr\u00f6der","year":"2009"},{"key":"S0960129510000563_ref31","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1094155277"},{"key":"S0960129510000563_ref36","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.09.023"},{"key":"S0960129510000563_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"key":"S0960129510000563_ref20","first-page":"164","volume-title":"Logic in Computer Science, LICS 94","author":"Hemaspaandra","year":"1994"},{"key":"S0960129510000563_ref38","first-page":"307","volume-title":"Principles of Knowledge Representation and Reasoning, KR 2008","author":"Schr\u00f6der","year":"2008"},{"key":"S0960129510000563_ref22","volume-title":"Handbook of Process Algebra","author":"Jonsson","year":"2001"},{"key":"S0960129510000563_ref17","first-page":"278","volume-title":"Real-Time Systems, RTSS 90","author":"Hansson","year":"1990"},{"key":"S0960129510000563_ref9","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511621192"},{"key":"S0960129510000563_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_9"},{"key":"S0960129510000563_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90076-6"},{"key":"S0960129510000563_ref44","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_5"},{"key":"S0960129510000563_ref34","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"S0960129510000563_ref33","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/12.1.149"},{"key":"S0960129510000563_ref45","first-page":"44","volume-title":"Quantitative Evaluation of Systems, QEST 2005","author":"Segala","year":"2005"},{"key":"S0960129510000563_ref16","volume-title":"Reasoning About Uncertainty","author":"Halpern","year":"2003"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129510000563","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T15:04:25Z","timestamp":1556377465000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129510000563\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,3,25]]},"references-count":49,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,4]]}},"alternative-id":["S0960129510000563"],"URL":"https:\/\/doi.org\/10.1017\/s0960129510000563","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,3,25]]}}}