TY - GEN
T1 - Model checking epistemic and probabilistic properties of multi-agent systems
AU - Wan, Wei
AU - Bentahar, Jamal
AU - Ben Hamza, Abdessamad
PY - 2011
Y1 - 2011
N2 - Model checking, a formal automatic verification method, has been widely used in multi-agent systems to verify specifications that contain qualitative properties (e.g safety and liveliness) and quantitative properties. Decision making processes based on inherent knowledge are necessary for agents to act appropriately, particularly in uncertain settings. In order to check epistemic (i.e knowledge) and measurable properties in multi-agent systems, we propose a new logic PCTLK, which uses probabilistic, epistemic, and temporal modal operators. We exploit Discrete-Time Markov Chains (DTMC), in which we are able to represent measurable properties with probability, to model uncertainty in multi-agent systems. We extend the formalism of interpreted systems by adding probabilistic features to suit DTMC models and to present the model checking algorithm for our logic. At the end of this paper, we simulate our algorithm using an example of online shopping.
AB - Model checking, a formal automatic verification method, has been widely used in multi-agent systems to verify specifications that contain qualitative properties (e.g safety and liveliness) and quantitative properties. Decision making processes based on inherent knowledge are necessary for agents to act appropriately, particularly in uncertain settings. In order to check epistemic (i.e knowledge) and measurable properties in multi-agent systems, we propose a new logic PCTLK, which uses probabilistic, epistemic, and temporal modal operators. We exploit Discrete-Time Markov Chains (DTMC), in which we are able to represent measurable properties with probability, to model uncertainty in multi-agent systems. We extend the formalism of interpreted systems by adding probabilistic features to suit DTMC models and to present the model checking algorithm for our logic. At the end of this paper, we simulate our algorithm using an example of online shopping.
KW - Discrete-Time Markov Chains (DTMC)
KW - Epistemic logic
KW - Interpreted systems
KW - Probabilistic logic
KW - Probabilistic model checking
UR - http://www.scopus.com/inward/record.url?scp=79960541710&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-21827-9_8
DO - 10.1007/978-3-642-21827-9_8
M3 - Conference contribution
AN - SCOPUS:79960541710
SN - 9783642218262
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 68
EP - 78
BT - Modern Approaches in Applied Intelligence - 24th International Conference on Industrial Engineering and Other Applications of Applied Intelligent Systems, IEA/AIE 2011, Proceedings
T2 - 24th International Conference on Industrial Engineering and Other Applications of Applied Intelligent Systems, IEA/AIE 2011
Y2 - 28 June 2011 through 1 July 2011
ER -