DC Field | Value | Language |
---|---|---|
dc.contributor.author | Shilov, NV | ko |
dc.contributor.author | Garanina, NO | ko |
dc.contributor.author | Choe, Kwang-Moo | ko |
dc.date.accessioned | 2013-03-08T07:28:45Z | - |
dc.date.available | 2013-03-08T07:28:45Z | - |
dc.date.created | 2012-02-06 | - |
dc.date.created | 2012-02-06 | - |
dc.date.issued | 2006-07 | - |
dc.identifier.citation | FUNDAMENTA INFORMATICAE, v.72, no.1-3, pp.347 - 361 | - |
dc.identifier.issn | 0169-2968 | - |
dc.identifier.uri | http://hdl.handle.net/10203/92473 | - |
dc.description.abstract | We present (update+abstraction) algorithm for model checking a fusion of Computation Tree Logic and Propositional Logic of Knowledge in systems with the perfect recall synchronous semantics. It has been already known that the problem is decidable with a non-elementary lower bound. The decidability follows from interpretation of the problem in a so-called Chain Logic and then in the Second Order Logic of Monadic Successors. This time we give a direct algorithm for model checking and detailed time upper bound where a number of different parameters are taken into count (i.e. a number of agents, a number of states, knowledge depth, formula size). We present a toy experiment with this algorithm that encourages our hope that the algorithm can be used in practice. | - |
dc.language | English | - |
dc.publisher | IOS PRESS | - |
dc.subject | INFINITE-TREES | - |
dc.title | Update and abstraction in model checking of knowledge and branching time | - |
dc.type | Article | - |
dc.identifier.wosid | 000240603000026 | - |
dc.identifier.scopusid | 2-s2.0-33747077449 | - |
dc.type.rims | ART | - |
dc.citation.volume | 72 | - |
dc.citation.issue | 1-3 | - |
dc.citation.beginningpage | 347 | - |
dc.citation.endingpage | 361 | - |
dc.citation.publicationname | FUNDAMENTA INFORMATICAE | - |
dc.contributor.localauthor | Choe, Kwang-Moo | - |
dc.contributor.nonIdAuthor | Shilov, NV | - |
dc.contributor.nonIdAuthor | Garanina, NO | - |
dc.type.journalArticle | Article; Proceedings Paper | - |
dc.subject.keywordPlus | INFINITE-TREES | - |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.