{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T14:12:50Z","timestamp":1746195170223,"version":"3.37.3"},"reference-count":0,"publisher":"IOS Press","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"abstract":"<jats:p>Model checking, a formal and automatic verification method, has been widely used to check specifications expressed not only as qualitative properties (e.g safety and liveliness), but also as quantitative properties (e.g. degree of reliability and reachability). In this paper, we present a method for probabilistic model checking of multi-agent systems specified by a probabilistic-epistemic logic PCTLK. We define transformations from probabilistic interpreted systems into Discrete-time Markov chains (DTMC) and from PCTLK formulae to PCTL formulae so that we are able to convert the problem of model checking PCTLK to the one of PCTL. The algorithm is implemented in the probabilistic model checker PRISM. Some properties, including agents' probabilistic knowledge, are verified and simulations are shown.<\/jats:p>","DOI":"10.3233\/978-1-61499-125-0-91","type":"book-chapter","created":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T10:26:53Z","timestamp":1740133613000},"source":"Crossref","is-referenced-by-count":1,"title":["Quantitative Model Checking of Knowledge"],"prefix":"10.3233","author":[{"family":"Wan Wei","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"family":"Bentahar Jamal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"family":"Ben Hamza Abdessamad","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"7437","container-title":["Frontiers in Artificial Intelligence and Applications","New Trends in Software Methodologies, Tools and Techniques"],"original-title":[],"deposited":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T11:11:25Z","timestamp":1740136285000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.medra.org\/servlet\/aliasResolver?alias=iospressISSNISBN&issn=0922-6389&volume=246&spage=91"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"references-count":0,"URL":"https:\/\/doi.org\/10.3233\/978-1-61499-125-0-91","relation":{},"ISSN":["0922-6389"],"issn-type":[{"value":"0922-6389","type":"print"}],"subject":[],"published":{"date-parts":[[2012]]}}}