Model Checking for Probabilistic Multiagent Systems

Fu, C; Turrini, A; Huang, X; Song, L; Feng, Y; Zhang, LJ

Model Checking for Probabilistic Multiagent Systems

Fu, C Turrini, A Huang, X Song, L Feng, Y

Zhang, LJ

Permalink

Publisher:: SPRINGER SINGAPORE PTE LTD
Publication Type:: Journal Article
Citation:: Journal of Computer Science and Technology, 2023, 38, (5), pp. 1162-1186
Issue Date:: 2023-09-01

Open Access

Copyright Clearance Process

Recently Added
In Progress
Open Access

This item is open access.

The embargo period expires on 1 Sep 2024

Adobe PDF

Download Accepted versionAdobe PDF (1.53 MB)

View on publisher's site

View statistics

Full metadata record

Field	Value	Language
dc.contributor.author	Fu, C
dc.contributor.author	Turrini, A
dc.contributor.author	Huang, X
dc.contributor.author	Song, L
dc.contributor.author	Feng, Y https://orcid.org/0000-0002-3097-3896
dc.contributor.author	Zhang, LJ
dc.date.accessioned	2024-02-06T01:44:48Z
dc.date.available	2024-02-06T01:44:48Z
dc.date.issued	2023-09-01
dc.identifier.citation	Journal of Computer Science and Technology, 2023, 38, (5), pp. 1162-1186
dc.identifier.issn	1000-9000
dc.identifier.issn	1860-4749
dc.identifier.uri	http://hdl.handle.net/10453/175348
dc.description.abstract	In multiagent systems, agents usually do not have complete information of the whole system, which makes the analysis of such systems hard. The incompleteness of information is normally modelled by means of accessibility relations, and the schedulers consistent with such relations are called uniform. In this paper, we consider probabilistic multiagent systems with accessibility relations and focus on the model checking problem with respect to the probabilistic epistemic temporal logic, which can specify both temporal and epistemic properties. However, the problem is undecidable in general. We show that it becomes decidable when restricted to memoryless uniform schedulers. Then, we present two algorithms for this case: one reduces the model checking problem into a mixed integer non-linear programming (MINLP) problem, which can then be solved by Satisfiability Modulo Theories (SMT) solvers, and the other is an approximate algorithm based on the upper confidence bounds applied to trees (UCT) algorithm, which can return a result whenever queried. These algorithms have been implemented in an existing model checker and then validated on experiments. The experimental results show the efficiency and extendability of these algorithms, and the algorithm based on UCT outperforms the one based on MINLP in most cases.
dc.language	English
dc.publisher	SPRINGER SINGAPORE PTE LTD
dc.relation.ispartof	Journal of Computer Science and Technology
dc.relation.isbasedon	10.1007/s11390-022-1218-6
dc.rights	info:eu-repo/semantics/embargoedAccess
dc.rights	This version of the article has been accepted for publication, after peer review (when applicable) and is subject to Springer Nature’s AM terms of use, but is not the Version of Record and does not reflect post-acceptance improvements, or any corrections. The Version of Record is available online at: https://doi.org/10.1007/s11390-022-1218-6
dc.subject	08 Information and Computing Sciences
dc.subject.classification	Software Engineering
dc.subject.classification	46 Information and computing sciences
dc.title	Model Checking for Probabilistic Multiagent Systems
dc.type	Journal Article
utslib.citation.volume	38
utslib.for	08 Information and Computing Sciences
pubs.organisational-group	University of Technology Sydney
pubs.organisational-group	University of Technology Sydney/Faculty of Engineering and Information Technology
pubs.organisational-group	University of Technology Sydney/Strength - QSI - Centre for Quantum Software and Information
utslib.copyright.status	open_access	*
utslib.copyright.embargo	2024-09-01T00:00:00+1000Z
dc.date.updated	2024-02-06T01:44:47Z
pubs.issue	5
pubs.publication-status	Published
pubs.volume	38
utslib.citation.issue	5

Abstract:

In multiagent systems, agents usually do not have complete information of the whole system, which makes the analysis of such systems hard. The incompleteness of information is normally modelled by means of accessibility relations, and the schedulers consistent with such relations are called uniform. In this paper, we consider probabilistic multiagent systems with accessibility relations and focus on the model checking problem with respect to the probabilistic epistemic temporal logic, which can specify both temporal and epistemic properties. However, the problem is undecidable in general. We show that it becomes decidable when restricted to memoryless uniform schedulers. Then, we present two algorithms for this case: one reduces the model checking problem into a mixed integer non-linear programming (MINLP) problem, which can then be solved by Satisfiability Modulo Theories (SMT) solvers, and the other is an approximate algorithm based on the upper confidence bounds applied to trees (UCT) algorithm, which can return a result whenever queried. These algorithms have been implemented in an existing model checker and then validated on experiments. The experimental results show the efficiency and extendability of these algorithms, and the algorithm based on UCT outperforms the one based on MINLP in most cases.

Please use this identifier to cite or link to this item:

http://hdl.handle.net/10453/175348